The abstract of the Mizar article:

Irrationality of $e$

by

Freek Wiedijk

Received July 2, 1999

MML identifier: IRRAT_1

[ Mizar article, MML identifier index ]

environ

 vocabulary INT_1, ARYTM, SEQ_1, FINSEQ_1, RAT_1, POWER, FILTER_0, SQUARE_1,
      ARYTM_3, FUNCT_1, ARYTM_1, NEWTON, QC_LANG1, RELAT_1, SEQ_2, ORDINAL2,
      ABSVALUE, SEQM_3, SUPINF_2, RLVECT_1, SERIES_1, RFINSEQ, FINSEQ_4,
      FINSEQ_2, GROUP_1, SIN_COS, IRRAT_1;
 notation XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, INT_1,
      NAT_1, NEWTON, FUNCT_1, SEQ_1, SEQ_2, POWER, ABSVALUE, SEQM_3, FINSEQ_1,
      RVSUM_1, SERIES_1, FINSEQ_2, RFINSEQ, FINSEQ_4, SIN_COS, RAT_1, SQUARE_1,
      LIMFUNC1, NAT_LAT, INT_2, PEPIN;
 constructors NAT_1, REAL_1, SEQ_2, PARTFUN1, PREPOWER, RVSUM_1, SERIES_1,
      RFINSEQ, FINSEQ_4, SIN_COS, COMSEQ_3, LIMFUNC1, NAT_LAT, PEPIN, COMPLEX1,
      MEMBERED, ARYTM_0;
 clusters RELSET_1, XREAL_0, SEQ_1, INT_1, NEWTON, NAT_1, MEMBERED, ORDINAL2,
      NUMBERS;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Square roots of primes are irrational

 reserve k, m, n, p, K, N for Nat;
 reserve i for Integer;
 reserve x, y, eps for real number;
 reserve seq, seq1, seq2 for Real_Sequence;
 reserve sq for FinSequence of REAL;

definition let x;
 redefine attr x is rational;
 antonym x is irrational;
end;

definition let x, y;
 redefine func x to_power y;
 synonym x.^.y;
end;

theorem :: IRRAT_1:1
 p is prime implies sqrt p is irrational;

theorem :: IRRAT_1:2
   ex x, y st x is irrational & y is irrational & x.^.y is rational;

begin :: A proof that e = e

scheme LambdaRealSeq{F(set)->real number}:
 (ex seq st for n holds seq.n=F(n)) &
 (for seq1, seq2 st
  (for n holds seq1.n=F(n)) & (for n holds seq2.n=F(n)) holds seq1=seq2);

definition let k;
 func aseq(k) -> Real_Sequence means
:: IRRAT_1:def 1
   for n holds it.n=(n-k)/n;
end;

definition
 let k;
 func bseq(k) -> Real_Sequence means
:: IRRAT_1:def 2
   for n holds it.n=(n choose k)*(n.^.(-k));
end;

definition
 let n;
 func cseq(n) -> Real_Sequence means
:: IRRAT_1:def 3
   for k holds it.k=(n choose k)*(n.^.(-k));
end;

theorem :: IRRAT_1:3
 cseq(n).k=bseq(k).n;

definition
 func dseq -> Real_Sequence means
:: IRRAT_1:def 4
   for n holds it.n=(1+(1/n)).^.n;
end;

definition
 func eseq -> Real_Sequence means
:: IRRAT_1:def 5
   for k holds it.k=1/(k!);
end;

:: lim(\n:(n choose k)*(n.^.(-k))) = 1/(k!)

theorem :: IRRAT_1:4
 n>0 implies (n.^.(-(k+1)))=(n.^.(-k))/n;

theorem :: IRRAT_1:5
 for x, y, z, v, w being real number holds
  x/(y*z*(v/w))=(w/z)*(x/(y*v));

theorem :: IRRAT_1:6
 (n choose (k+1))=((n-k)/(k+1))*(n choose k);

theorem :: IRRAT_1:7
 n>0 implies bseq(k+1).n=(1/(k+1))*(bseq(k).n)*(aseq(k).n);

theorem :: IRRAT_1:8
 n>0 implies aseq(k).n=1-(k/n);

theorem :: IRRAT_1:9
 aseq(k) is convergent & lim(aseq(k))=1;

theorem :: IRRAT_1:10
 for seq st for n holds seq.n=x holds seq is convergent & lim(seq)=x;

theorem :: IRRAT_1:11
 for n holds bseq(0).n=1;

theorem :: IRRAT_1:12
 (1/(k+1))*(1/(k!))=1/((k+1)!);

theorem :: IRRAT_1:13
 bseq(k) is convergent & lim(bseq(k))=1/(k!) & lim(bseq(k))=eseq.k;

:: 0 <= (n choose k)*(n.^.(-k))) <= 1/(k!)

theorem :: IRRAT_1:14
 k<n implies 0<aseq(k).n & aseq(k).n<=1;

theorem :: IRRAT_1:15
 n>0 implies
  0<=bseq(k).n & bseq(k).n<=1/(k!) & bseq(k).n<=eseq.k &
  0<=cseq(n).k & cseq(n).k<=1/(k!) & cseq(n).k<=eseq.k;

:: n>0 implies (1+(1/n)).^.n = Sum (\k:(n choose k)*(n.^.(-k)))

theorem :: IRRAT_1:16
 for seq st seq^\1 is summable holds
  seq is summable & Sum(seq)=(seq.0)+Sum(seq^\1);

theorem :: IRRAT_1:17
 for D being non empty set, sq being FinSequence of D
  st 1<=k & k<len sq holds (sq/^1).k=sq.(k+1);

theorem :: IRRAT_1:18
 for sq st len(sq)>0 holds
  Sum(sq)=(sq.1)+Sum(sq/^1);

theorem :: IRRAT_1:19
 for n holds
  for seq, sq st
   len(sq)=n &
   (for k st k<n holds seq.k=sq.(k+1)) &
   (for k st k>=n holds seq.k=0) holds
    seq is summable & Sum(seq)=Sum(sq);

theorem :: IRRAT_1:20
 x<>0 & y<>0 & k<=n implies
  ((x,y) In_Power n).(k+1)=(n choose k)*(x.^.(n-k))*(y.^.k);

theorem :: IRRAT_1:21
 n>0 & k<=n implies cseq(n).k=((1,1/n) In_Power n).(k+1);

theorem :: IRRAT_1:22
 n>0 implies
  cseq(n) is summable & Sum(cseq(n))=(1+(1/n)).^.n & Sum(cseq(n))=dseq.n;

:: number_e = lim(\n:(1+(1/n)).^.n)

theorem :: IRRAT_1:23
 dseq is convergent & lim(dseq)=number_e;

:: exp(1) = Sum (\k:1/(k!))

theorem :: IRRAT_1:24
 eseq is summable & Sum(eseq)=exp(1);

:: lim(\n:(1+(1/n)).^.n) = Sum (\k:1/(k!))

theorem :: IRRAT_1:25
 for K holds
  for dseqK being Real_Sequence st
   for n holds dseqK.n=Partial_Sums(cseq(n)).K holds
    dseqK is convergent & lim(dseqK)=Partial_Sums(eseq).K;

theorem :: IRRAT_1:26
 seq is convergent & lim(seq)=x implies
  for eps st eps>0 holds ex N st for n st n>=N holds seq.n>x-eps;

theorem :: IRRAT_1:27
 (for eps st eps>0 holds ex N st for n st n>=N holds seq.n>x-eps) &
 (ex N st for n st n>=N holds seq.n<=x) implies
  seq is convergent & lim(seq)=x;

theorem :: IRRAT_1:28
 seq is summable implies
  for eps st eps>0 holds ex K st Partial_Sums(seq).K>Sum(seq)-eps;

theorem :: IRRAT_1:29
 n>=1 implies dseq.n<=Sum(eseq);

theorem :: IRRAT_1:30
 seq is summable & (for k holds seq.k>=0) implies
  Sum(seq)>=Partial_Sums(seq).K;

theorem :: IRRAT_1:31
 dseq is convergent & lim(dseq)=Sum(eseq);

:: number_e = exp(1)

definition
 redefine func number_e equals
:: IRRAT_1:def 6
   Sum(eseq);
end;

definition
 redefine func number_e equals
:: IRRAT_1:def 7
    exp(1);
end;

begin :: number_e is irrational

theorem :: IRRAT_1:32
 x is rational implies ex n st n>=2 & n!*x is integer;

theorem :: IRRAT_1:33
 n!*eseq.k = (n!)/(k!);

theorem :: IRRAT_1:34
 (n!)/(k!)>0;

theorem :: IRRAT_1:35
 seq is summable & (for n holds seq.n>0) implies Sum(seq)>0;

theorem :: IRRAT_1:36
 n!*Sum(eseq^\(n+1))>0;

theorem :: IRRAT_1:37
 k<=n implies (n!)/(k!) is integer;

theorem :: IRRAT_1:38
 n!*Partial_Sums(eseq).n is integer;

theorem :: IRRAT_1:39
 x=1/(n+1) implies (n!)/((n+k+1)!)<=x.^.(k+1);

theorem :: IRRAT_1:40
 n>0 & x=1/(n+1) implies n!*Sum(eseq^\(n+1))<=x/(1-x);

theorem :: IRRAT_1:41
for n be real number holds
 n>=2 & x=1/(n+1) implies x/(1-x)<1;

theorem :: IRRAT_1:42
   number_e is irrational;