Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users

### Irrationality of \$e\$

by
Freek Wiedijk

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;
```