Copyright (c) 1999 Association of Mizar Users
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;
definitions SEQ_2;
theorems SEQ_1, REAL_2, POWER, NEWTON, REAL_1, AXIOMS, NAT_1, SEQ_2, SEQ_4,
ABSVALUE, SEQM_3, RVSUM_1, FINSEQ_2, SERIES_1, RFINSEQ, FINSEQ_3,
FINSEQ_4, FINSEQ_5, FINSEQ_1, SIN_COS, SQUARE_1, INT_1, RAT_1, INT_2,
NAT_LAT, FUNCT_2, XCMPLX_0, XCMPLX_1;
schemes SEQ_1, NAT_1;
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 Th1:
p is prime implies sqrt p is irrational
proof
assume A1: p is prime;
then A2: p>1 by INT_2:def 5;
then A3: p>0 by AXIOMS:22;
assume sqrt p is rational;
then consider i, n such that A4: n<>0 & sqrt p=i/n &
for i1 being Integer, n1 being Nat st n1<>0 & sqrt p=i1/n1 holds n<=n1
by RAT_1:25;
A5: i=sqrt p*n by A4,XCMPLX_1:88;
sqrt p>=0 & n>=0 by A3,NAT_1:18,SQUARE_1:def 4;
then i>=0 by A5,REAL_2:121;
then reconsider m = i as Nat by INT_1:16;
A6: m^2 = (sqrt p)^2*n^2 by A5,SQUARE_1:68
.= p*n^2 by A3,SQUARE_1:def 4;
then p divides m^2 by NAT_1:def 3;
then p divides m*m by SQUARE_1:def 3;
then p divides m by A1,NAT_LAT:95;
then consider m1 being Nat such that A7: m=p*m1 by NAT_1:def 3;
n^2 = m^2/p by A3,A6,XCMPLX_1:90
.= p^2*m1^2/p by A7,SQUARE_1:68
.= p*p*m1^2/p by SQUARE_1:def 3
.= p*(p*m1^2)/p by XCMPLX_1:4
.= p*m1^2 by A3,XCMPLX_1:90;
then p divides n^2 by NAT_1:def 3;
then p divides n*n by SQUARE_1:def 3;
then p divides n by A1,NAT_LAT:95;
then consider n1 being Nat such that A8: n=p*n1 by NAT_1:def 3;
A9: n1<>0 by A4,A8;
then A10: n1>0 by NAT_1:19;
A11: m1/n1 = sqrt p by A3,A4,A7,A8,XCMPLX_1:92;
p*n1>1*n1 by A2,A10,REAL_2:199;
hence contradiction by A4,A8,A9,A11;
end;
theorem
ex x, y st x is irrational & y is irrational & x.^.y is rational
proof
set w = sqrt 2;
w>0 by AXIOMS:22,SQUARE_1:84;
then A1: (w.^.w).^.w = w.^.(w*w) by POWER:38
.= w.^.(w^2) by SQUARE_1:def 3
.= w.^.2 by SQUARE_1:def 4
.= w^2 by POWER:53
.= 2 by SQUARE_1:def 4;
per cases;
suppose A2: w.^.w is rational;
take w, w;
thus thesis by A2,Th1,INT_2:44;
suppose A3: w.^.w is irrational;
take w.^.w, w;
thus thesis by A1,A3,Th1,INT_2:44;
end;
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)
proof
deffunc F1(set)=F($1);
thus ex seq st for n holds seq.n=F1(n) from ExRealSeq;
let seq1, seq2;
assume A1: for n holds seq1.n=F(n);
assume A2: for n holds seq2.n=F(n);
now let n;
thus seq1.n = F(n) by A1
.= seq2.n by A2;
end;
hence seq1 = seq2 by FUNCT_2:113;
end;
definition let k;
func aseq(k) -> Real_Sequence means
:Def1: for n holds it.n=(n-k)/n;
correctness
proof
deffunc F(Nat)=($1-k)/$1;
thus (ex seq being Real_Sequence st
for n being Nat holds seq.n=F(n)) &
(for seq1, seq2 being Real_Sequence st
(for n being Nat holds seq1.n=F(n)) &
(for n being Nat holds seq2.n=F(n)) holds seq1=seq2)
from LambdaRealSeq;
end;
end;
definition
let k;
func bseq(k) -> Real_Sequence means
:Def2: for n holds it.n=(n choose k)*(n.^.(-k));
correctness
proof
deffunc F(Nat)=($1 choose k)*($1.^.(-k));
thus (ex seq being Real_Sequence st
for n being Nat holds seq.n=F(n)) &
(for seq1, seq2 being Real_Sequence st
(for n being Nat holds seq1.n=F(n)) &
(for n being Nat holds seq2.n=F(n)) holds seq1=seq2)
from LambdaRealSeq;
end;
end;
definition
let n;
func cseq(n) -> Real_Sequence means
:Def3: for k holds it.k=(n choose k)*(n.^.(-k));
correctness
proof
deffunc F(Nat)=(n choose $1)*(n.^.(-$1));
thus (ex seq being Real_Sequence st
for n being Nat holds seq.n=F(n)) &
(for seq1, seq2 being Real_Sequence st
(for n being Nat holds seq1.n=F(n)) &
(for n being Nat holds seq2.n=F(n)) holds seq1=seq2)
from LambdaRealSeq;
end;
end;
theorem Th3:
cseq(n).k=bseq(k).n
proof
thus cseq(n).k = (n choose k)*(n.^.(-k)) by Def3
.= bseq(k).n by Def2;
end;
definition
func dseq -> Real_Sequence means
:Def4: for n holds it.n=(1+(1/n)).^.n;
correctness
proof
deffunc F(Nat)=(1+(1/$1)).^.$1;
thus (ex seq being Real_Sequence st
for n being Nat holds seq.n=F(n)) &
(for seq1, seq2 being Real_Sequence st
(for n being Nat holds seq1.n=F(n)) &
(for n being Nat holds seq2.n=F(n)) holds seq1=seq2)
from LambdaRealSeq;
end;
end;
definition
func eseq -> Real_Sequence means
:Def5: for k holds it.k=1/(k!);
correctness
proof
deffunc F(Nat)=1/($1!);
thus (ex seq being Real_Sequence st
for n being Nat holds seq.n=F(n)) &
(for seq1, seq2 being Real_Sequence st
(for n being Nat holds seq1.n=F(n)) &
(for n being Nat holds seq2.n=F(n)) holds seq1=seq2)
from LambdaRealSeq;
end;
end;
:: lim(\n:(n choose k)*(n.^.(-k))) = 1/(k!)
theorem Th4:
n>0 implies (n.^.(-(k+1)))=(n.^.(-k))/n
proof
assume A1: n>0;
thus (n.^.(-(k+1))) = (n.^.((-k)-1)) by XCMPLX_1:161
.= (n.^.(-k))/(n.^.1) by A1,POWER:34
.= (n.^.(-k))/n by POWER:30;
end;
theorem Th5:
for x, y, z, v, w being real number holds
x/(y*z*(v/w))=(w/z)*(x/(y*v))
proof
let x, y, z, v, w be real number;
thus x/(y*z*(v/w)) = x/(y*z*(v*w")) by XCMPLX_0:def 9
.= x/(z*(y*(v*w"))) by XCMPLX_1:4
.= x/(z*(y*v*w")) by XCMPLX_1:4
.= x/(z*((y*v)/w)) by XCMPLX_0:def 9
.= x/((y*v)/(w/z)) by XCMPLX_1:82
.= (w/z)*(x/(y*v)) by XCMPLX_1:82;
end;
theorem Th6:
(n choose (k+1))=((n-k)/(k+1))*(n choose k)
proof
per cases;
suppose A1: k+1<=n;
then reconsider l = n-(k+1) as Nat by INT_1:18;
A2: l+1 = n-(k+1-1) by XCMPLX_1:37
.= n-k by XCMPLX_1:26;
then reconsider l1 = n-k as Nat;
k <= k+1 by NAT_1:29; then A3: k <= n by A1,AXIOMS:22;
thus (n choose (k+1)) = n!/((k+1)!*(l!)) by A1,NEWTON:def 3
.= n!/((k!*(k+1))*(l!)) by NEWTON:21
.= n!/((k!*(k+1))*((l!)*(l+1)/(l+1))) by XCMPLX_1:90
.= n!/((k!*(k+1))*((l+1)!/(l+1))) by NEWTON:21
.= (l1/(k+1))*(n!/((k!)*(l1!))) by A2,Th5
.= ((n-k)/(k+1))*(n choose k) by A3,NEWTON:def 3;
suppose A4: k+1>n & k<=n;
then k>=n & k<=n by NAT_1:38;
then k=n by AXIOMS:21;
then n-k=0 by XCMPLX_1:14;
hence (n choose (k+1)) = ((n-k)/(k+1))*(n choose k) by A4,NEWTON:def 3;
suppose A5: k+1>n & k>n;
hence (n choose (k+1)) = ((n-k)/(k+1))*0 by NEWTON:def 3
.= ((n-k)/(k+1))*(n choose k) by A5,NEWTON:def 3;
end;
theorem Th7:
n>0 implies bseq(k+1).n=(1/(k+1))*(bseq(k).n)*(aseq(k).n)
proof
assume A1: n>0;
thus bseq(k+1).n = (n choose (k+1))*(n.^.(-(k+1))) by Def2
.= ((n-k)/(k+1))*(n choose k)*(n.^.(-(k+1))) by Th6
.= ((n-k)/(k+1))*(n choose k)*((n.^.(-k))/n) by A1,Th4
.= (n-k)*(k+1)"*(n choose k)*((n.^.(-k))/n) by XCMPLX_0:def 9
.= (n-k)*(k+1)"*(n choose k)*((n.^.(-k))*n") by XCMPLX_0:def 9
.= (n-k)*(k+1)"*(n choose k)*(n.^.(-k))*n" by XCMPLX_1:4
.= (k+1)"*(n choose k)*(n-k)*(n.^.(-k))*n" by XCMPLX_1:4
.= (k+1)"*(n choose k)*(n.^.(-k))*(n-k)*n" by XCMPLX_1:4
.= (k+1)"*((n choose k)*(n.^.(-k)))*(n-k)*n" by XCMPLX_1:4
.= (k+1)"*((n choose k)*(n.^.(-k)))*((n-k)*n") by XCMPLX_1:4
.= (1/(k+1))*((n choose k)*(n.^.(-k)))*((n-k)*n") by XCMPLX_1:217
.= (1/(k+1))*((n choose k)*(n.^.(-k)))*((n-k)/n) by XCMPLX_0:def 9
.= (1/(k+1))*(bseq(k).n)*((n-k)/n) by Def2
.= (1/(k+1))*(bseq(k).n)*(aseq(k).n) by Def1;
end;
theorem Th8:
n>0 implies aseq(k).n=1-(k/n)
proof
assume A1: n>0;
thus aseq(k).n = (n-k)/n by Def1
.= (n/n)-(k/n) by XCMPLX_1:121
.= 1-(k/n) by A1,XCMPLX_1:60;
end;
theorem Th9:
aseq(k) is convergent & lim(aseq(k))=1
proof
A1: for eps be real number st 0<eps
ex N st for n st N<=n holds abs(aseq(k).n-1)<eps
proof
let eps be real number;
assume A2: eps>0;
consider N such that A3: N>k/eps by SEQ_4:10;
A4: k>=0*eps by NAT_1:18;
take N;
let n;
assume A5: n>=N;
then A6: n>0 by A2,A3,A4,REAL_2:177;
k>=0*n by NAT_1:18;
then A7: k/n>=0 by A6,REAL_2:177;
A8: abs(aseq(k).n-1) = abs((1-(k/n))-1) by A6,Th8
.= abs((1+-(k/n))-1) by XCMPLX_0:def 8
.= abs(-(k/n)) by XCMPLX_1:26
.= abs(k/n) by ABSVALUE:17
.= k/n by A7,ABSVALUE:def 1;
n>(k/eps) by A3,A5,AXIOMS:22;
then (k/eps)*eps<n*eps by A2,REAL_1:70;
then k<n*eps by A2,XCMPLX_1:88;
hence thesis by A6,A8,REAL_2:178;
end;
thus aseq(k) is convergent
proof
take 1;
thus thesis by A1;
end;
hence lim(aseq(k))=1 by A1,SEQ_2:def 7;
end;
theorem Th10:
for seq st for n holds seq.n=x holds seq is convergent & lim(seq)=x
proof
let seq;
assume A1: for n holds seq.n=x;
then A2: seq is constant by SEQM_3:def 6;
hence seq is convergent by SEQ_4:39;
thus lim(seq) = seq.0 by A2,SEQ_4:41
.= x by A1;
end;
theorem Th11:
for n holds bseq(0).n=1
proof
let n;
thus bseq(0).n = (n choose 0)*(n.^.(-0)) by Def2
.= 1*(n.^.(-0)) by NEWTON:29
.= 1 by POWER:29;
end;
theorem Th12:
(1/(k+1))*(1/(k!))=1/((k+1)!)
proof
thus (1/(k+1))*(1/(k!)) = 1/((k+1)*(k!)) by XCMPLX_1:103
.= 1/((k+1)!) by NEWTON:21;
end;
theorem Th13:
bseq(k) is convergent & lim(bseq(k))=1/(k!) & lim(bseq(k))=eseq.k
proof
defpred P[Nat] means bseq($1) is convergent & lim(bseq($1))=1/($1!);
A1: P[0]
proof
deffunc F(set)=1;
consider bseq0 being Real_Sequence such that
A2: for n holds bseq0.n=F(n) from ExRealSeq;
A3: bseq0 is convergent & lim(bseq0)=1 by A2,Th10;
A4: for n st n>=1 holds bseq(0).n=bseq0.n
proof
let n;
assume n>=1;
thus bseq(0).n = 1 by Th11
.= bseq0.n by A2;
end;
hence bseq(0) is convergent by A3,SEQ_4:31;
thus lim(bseq(0)) = 1/(0!) by A3,A4,NEWTON:18,SEQ_4:32;
end;
A5: now let k;
assume A6: P[k];
thus P[k+1]
proof
deffunc F(Nat)=(1/(k+1))*(bseq(k).$1);
consider seq such that
A7: for n holds seq.n = F(n) from ExRealSeq;
A8: seq = (1/(k+1))(#)(bseq(k)) by A7,SEQ_1:13;
A9: seq is convergent & lim(seq)=1/((k+1)!)
proof
thus seq is convergent by A6,A8,SEQ_2:21;
thus lim(seq) = (1/(k+1))*(1/(k!)) by A6,A8,SEQ_2:22
.= 1/((k+1)!) by Th12;
end;
deffunc G(Nat)=seq.$1*(aseq(k).$1);
consider seq1 such that
A10: for n holds seq1.n=G(n) from ExRealSeq;
A11: seq1=seq(#)(aseq(k)) by A10,SEQ_1:12;
A12: seq1 is convergent & lim(seq1)=1/((k+1)!)
proof
A13: aseq(k) is convergent & lim(aseq(k))=1 by Th9;
hence seq1 is convergent by A9,A11,SEQ_2:28;
thus lim(seq1) = lim(seq)*lim(aseq(k)) by A9,A11,A13,SEQ_2:29
.= 1/((k+1)!) by A9,A13;
end;
A14: for n st n>=1 holds bseq(k+1).n=seq1.n
proof
let n;
assume n>=1;
then n>=0+1;
then n>0 by NAT_1:38;
hence bseq(k+1).n = (1/(k+1))*(bseq(k).n)*(aseq(k).n) by Th7
.= (seq.n)*(aseq(k).n) by A7
.= seq1.n by A10;
end;
hence bseq(k+1) is convergent by A12,SEQ_4:31;
thus lim(bseq(k+1)) = 1/((k+1)!) by A12,A14,SEQ_4:32;
end;
end;
for k holds P[k] from Ind(A1,A5);
hence bseq(k) is convergent & lim(bseq(k))=1/(k!);
hence lim(bseq(k))=eseq.k by Def5;
end;
:: 0 <= (n choose k)*(n.^.(-k))) <= 1/(k!)
theorem Th14:
k<n implies 0<aseq(k).n & aseq(k).n<=1
proof
assume A1: k<n;
A2: 0<=k by NAT_1:18;
A3: aseq(k).n=(n-k)/n by Def1;
n-k>0 by A1,SQUARE_1:11;
hence aseq(k).n>0 by A1,A2,A3,REAL_2:127;
n >= 0 by A1, A2, AXIOMS:22; then
k/n>=0 by A2,REAL_2:125;
then 1-(k/n)<=1-0 by REAL_2:106;
hence aseq(k).n<=1 by A1,A2,Th8;
end;
theorem Th15:
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
proof
assume A1: n>0;
A2: bseq(k).n=(n choose k)*(n.^.(-k)) by Def2;
(n choose k) is Nat by NEWTON:35;
then A3: (n choose k)>=0 by NAT_1:18;
n.^.(-k)>0 by A1,POWER:39;
hence A4: 0<=bseq(k).n by A2,A3,REAL_2:121;
defpred P[Nat] means bseq($1).n<=1/($1!);
A5: P[0] by Th11,NEWTON:18;
A6: now let k;
assume A7: P[k];
thus P[k+1]
proof
A8: (k+1)!>0 by NEWTON:23;
then A9: 1/((k+1)!)>0 by REAL_2:127;
per cases;
suppose A10: k<n;
A11: bseq(k+1).n=(1/(k+1))*(bseq(k).n)*(aseq(k).n) by A1,Th7;
k+1>0 by NAT_1:19;
then 1/(k+1)>0 by REAL_2:127;
then (1/(k+1))*(bseq(k).n)<=(1/(k+1))*(1/(k!)) by A7,AXIOMS:25;
then A12: (1/(k+1))*(bseq(k).n)<=1/((k+1)!) by Th12;
aseq(k).n>=0 by A10,Th14;
then A13: (1/(k+1))*(bseq(k).n)*(aseq(k).n)<=(1/((k+1)!))*(aseq(k).n)
by A12,AXIOMS:25;
aseq(k).n<=1 by A10,Th14;
then 1/((k+1)!)*(aseq(k).n)<=1/((k+1)!) by A9,REAL_2:147;
hence thesis by A11,A13,AXIOMS:22;
suppose k>=n;
then A14: k+1>n by NAT_1:38;
bseq(k+1).n = (n choose (k+1))*(n.^.(-(k+1))) by Def2
.= 0*(n.^.(-(k+1))) by A14,NEWTON:def 3
.= 0;
hence thesis by A8,REAL_2:127;
end;
end;
for k holds P[k] from Ind(A5,A6);
hence A15: bseq(k).n<=1/(k!);
hence bseq(k).n<=eseq.k by Def5;
hence 0<=cseq(n).k & cseq(n).k<=1/(k!) & cseq(n).k<=eseq.k by A4,A15,Th3;
end;
:: n>0 implies (1+(1/n)).^.n = Sum (\k:(n choose k)*(n.^.(-k)))
theorem Th16:
for seq st seq^\1 is summable holds
seq is summable & Sum(seq)=(seq.0)+Sum(seq^\1)
proof
let seq;
assume seq^\1 is summable;
hence seq is summable by SERIES_1:16;
hence Sum(seq) = Partial_Sums(seq).0+Sum(seq^\(1+0)) by SERIES_1:18
.= (seq.0)+Sum(seq^\1) by SERIES_1:def 1;
end;
theorem Th17:
for D being non empty set, sq being FinSequence of D
st 1<=k & k<len sq holds (sq/^1).k=sq.(k+1)
proof let D be non empty set, sq be FinSequence of D;
assume A1: 1<=k & k<len sq;
then A2: len(sq)>=1 by AXIOMS:22;
then A3: len(sq/^1)=len sq-1 by RFINSEQ:def 2;
A4: k+1<=len sq by A1,NAT_1:38;
len sq=(len sq-1)+1 by XCMPLX_1:27;
then k<=len sq-1 by A4,REAL_1:53;
then k in dom(sq/^1) by A1,A3,FINSEQ_3:27;
hence (sq/^1).k=sq.(k+1) by A2,RFINSEQ:def 2;
end;
theorem Th18:
for sq st len(sq)>0 holds
Sum(sq)=(sq.1)+Sum(sq/^1)
proof
let sq;
assume A1: len sq>0;
then 1<=1 & 0+1<=len sq by NAT_1:38;
then A2: 1 in dom sq by FINSEQ_3:27;
sq is non empty by A1,FINSEQ_1:25;
hence Sum(sq) = Sum(<*sq/.1*>^(sq/^1)) by FINSEQ_5:32
.= Sum(<*sq.1*>^(sq/^1)) by A2,FINSEQ_4:def 4
.= (sq.1)+Sum(sq/^1) by RVSUM_1:106;
end;
theorem Th19:
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)
proof
defpred P[Nat] means
for seq, sq st
len(sq)=$1 &
(for k st k<$1 holds seq.k=sq.(k+1)) &
(for k st k>=$1 holds seq.k=0) holds
seq is summable & Sum(seq)=Sum(sq);
now
let seq, sq;
assume A1: len(sq)=0 &
(for k st k<0 holds seq.k=sq.(k+1)) &
(for k st k>=0 holds seq.k=0);
then sq is Element of 0-tuples_on REAL by FINSEQ_2:110;
then A2: Sum(sq)=0 by RVSUM_1:109;
defpred P[Nat] means Partial_Sums(seq).$1=0;
A3: now let k;
k>=0 by NAT_1:18;
hence seq.k = 0 by A1;
end;
then seq.0=0;
then A4: P[0] by SERIES_1:def 1;
A5: now let k;
assume A6: P[k];
Partial_Sums(seq).(k+1)
= (Partial_Sums(seq).k)+(seq.(k+1)) by SERIES_1:def 1;
hence P[k+1] by A3,A6;
end;
for k holds P[k] from Ind(A4,A5);
then A7:
Partial_Sums(seq) is convergent & lim(Partial_Sums(seq))=0 by Th10;
hence seq is summable by SERIES_1:def 2;
thus Sum(seq) = Sum(sq) by A2,A7,SERIES_1:def 3;
end; then A8: P[0];
now let n;
assume A9:
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);
let seq, sq;
assume A10: len(sq)=n+1 &
(for k st k<n+1 holds seq.k=sq.(k+1)) &
(for k st k>=n+1 holds seq.k=0);
A11: n>=0 by NAT_1:18;
A12: n+1>0 by NAT_1:18;
n+1>=0+1 by A11,AXIOMS:24;
then A13: len(sq/^1) = len(sq)-1 by A10,RFINSEQ:def 2
.= n by A10,XCMPLX_1:26;
A14: now let k;
assume k<n;
then A15: k+1<n+1 by REAL_1:53;
k>=0 by NAT_1:18;
then A16: k+1>=0+1 by AXIOMS:24;
thus (seq^\1).k = seq.(k+1) by SEQM_3:def 9
.= sq.((k+1)+1) by A10,A15
.= (sq/^1).(k+1) by A10,A15,A16,Th17;
end;
now let k;
assume k>=n;
then A17: k+1>=n+1 by AXIOMS:24;
thus (seq^\1).k = seq.(k+1) by SEQM_3:def 9
.= 0 by A10,A17;
end;
then A18: seq^\1 is summable & Sum(seq^\1)=Sum(sq/^1) by A9,A13,A14;
hence seq is summable by Th16;
thus Sum(seq) = (seq.0)+Sum(seq^\1) by A18,Th16
.= (sq.(0+1))+Sum(seq^\1) by A10,A12
.= Sum(sq) by A10,A12,A18,Th18;
end; then A19: P[k] implies P[k+1];
thus P[n] from Ind(A8,A19);
end;
theorem Th20:
x<>0 & y<>0 & k<=n implies
((x,y) In_Power n).(k+1)=(n choose k)*(x.^.(n-k))*(y.^.k)
proof
assume A1: x<>0 & y<>0 & k<=n;
k>=0 by NAT_1:18;
then A2: k+1>=0+1 by AXIOMS:24;
then reconsider i1 = (k+1)-1 as Nat by INT_1:18;
A3: i1=k by XCMPLX_1:26;
then reconsider l = n-i1 as Nat by A1,INT_1:18;
A4: len((x,y) In_Power n)=n+1 by NEWTON:def 4;
1<=k+1 & k+1<=n+1 by A1,A2,AXIOMS:24;
then k+1 in dom((x,y) In_Power n) by A4,FINSEQ_3:27;
hence ((x,y) In_Power n).(k+1)
= (n choose i1)*(x|^l)*(y|^i1) by NEWTON:def 4
.= (n choose i1)*(x.^.l)*(y|^i1) by A1,POWER:48
.= (n choose k)*(x.^.(n-k))*(y.^.k) by A1,A3,POWER:48;
end;
theorem Th21:
n>0 & k<=n implies cseq(n).k=((1,1/n) In_Power n).(k+1)
proof
assume A1: n>0 & k<=n;
then 1/n>0 by REAL_2:127;
hence ((1,1/n) In_Power n).(k+1)
= (n choose k)*(1 .^. (n-k))*((1/n).^.k) by A1,Th20
.= (n choose k)*1*((1/n).^.k) by POWER:31
.= (n choose k)*(n.^.(-k)) by A1,POWER:37
.= cseq(n).k by Def3;
end;
theorem Th22:
n>0 implies
cseq(n) is summable & Sum(cseq(n))=(1+(1/n)).^.n & Sum(cseq(n))=dseq.n
proof
assume A1: n>0;
then 1/n>0 by REAL_2:127;
then 1+(1/n)>1+0 by REAL_1:53;
then A2: 1+(1/n)>0 by AXIOMS:22;
A3: len((1,1/n) In_Power n)=n+1 by NEWTON:def 4;
A4: now let k;
assume k<n+1;
then k<=n by NAT_1:38;
hence cseq(n).k=((1,1/n) In_Power n).(k+1) by A1,Th21;
end;
A5: now let k;
assume k>=n+1;
then A6: k>n by NAT_1:38;
thus cseq(n).k = (n choose k)*(n.^.(-k)) by Def3
.= 0*(n.^.(-k)) by A6,NEWTON:def 3
.= 0;
end;
hence cseq(n) is summable by A3,A4,Th19;
thus (1+(1/n)).^.n = (1+(1/n))|^n by A2,POWER:48
.= Sum((1,1/n) In_Power n) by NEWTON:41
.= Sum(cseq(n)) by A3,A4,A5,Th19;
hence dseq.n = Sum(cseq(n)) by Def4;
end;
:: number_e = lim(\n:(1+(1/n)).^.n)
theorem Th23:
dseq is convergent & lim(dseq)=number_e
proof
A1: now let n;
thus (dseq^\1).n = dseq.(n+1) by SEQM_3:def 9
.= (1+1/(n+1)).^.(n+1) by Def4;
end;
then A2: dseq^\1 is convergent by POWER:67;
hence dseq is convergent by SEQ_4:35;
number_e=lim(dseq^\1) by A1,POWER:def 4;
hence number_e=lim(dseq) by A2,SEQ_4:36;
end;
:: exp(1) = Sum (\k:1/(k!))
theorem Th24:
eseq is summable & Sum(eseq)=exp(1)
proof
now let k;
thus eseq.k = 1/(k!) by Def5
.= (1 |^ k)/(k!) by NEWTON:15
.= (1 ExpSeq).k by SIN_COS:def 9;
end;
then A1: eseq=(1 ExpSeq) by FUNCT_2:113;
hence eseq is summable by SIN_COS:49;
thus exp(1) = exp.1 by SIN_COS:def 27
.= Sum(eseq) by A1,SIN_COS:def 26;
end;
:: lim(\n:(1+(1/n)).^.n) = Sum (\k:1/(k!))
theorem Th25:
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
proof
defpred P[Nat] means
for dseqK being Real_Sequence st
for n holds dseqK.n=Partial_Sums(cseq(n)).$1 holds
dseqK is convergent & lim(dseqK)=Partial_Sums(eseq).$1;
now let dseq0 be Real_Sequence;
assume A1: for n holds dseq0.n=Partial_Sums(cseq(n)).0;
now let n;
thus dseq0.n = Partial_Sums(cseq(n)).0 by A1
.= cseq(n).0 by SERIES_1:def 1
.= bseq(0).n by Th3;
end;
then A2: dseq0 = bseq(0) by FUNCT_2:113;
hence dseq0 is convergent by Th13;
thus lim(dseq0) = eseq.0 by A2,Th13
.= Partial_Sums(eseq).0 by SERIES_1:def 1;
end; then A3: P[0];
now let K;
assume
A4: 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;
deffunc F(Nat)=Partial_Sums(cseq($1)).K;
consider dseqK being Real_Sequence such that
A5: for n holds dseqK.n=F(n) from ExRealSeq;
A6: dseqK is convergent & lim(dseqK)=Partial_Sums(eseq).K by A4,A5;
let dseqK1 be Real_Sequence;
assume A7: for n holds dseqK1.n=Partial_Sums(cseq(n)).(K+1);
now let n;
thus dseqK1.n = Partial_Sums(cseq(n)).(K+1) by A7
.= Partial_Sums(cseq(n)).K+cseq(n).(K+1) by SERIES_1:def 1
.= dseqK.n+cseq(n).(K+1) by A5
.= dseqK.n+bseq(K+1).n by Th3
.= (dseqK+bseq(K+1)).n by SEQ_1:11;
end;
then A8: dseqK1=dseqK+bseq(K+1) by FUNCT_2:113;
A9: bseq(K+1) is convergent by Th13;
hence dseqK1 is convergent by A6,A8,SEQ_2:19;
thus lim(dseqK1) = lim(dseqK)+lim(bseq(K+1)) by A6,A8,A9,SEQ_2:20
.= Partial_Sums(eseq).K+eseq.(K+1) by A6,Th13
.= Partial_Sums(eseq).(K+1) by SERIES_1:def 1;
end; then A10: P[n] implies P[n+1];
thus P[n] from Ind(A3,A10);
end;
theorem Th26:
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
proof
assume A1: seq is convergent & lim(seq)=x;
let eps;
assume eps>0;
then consider N such that A2: for n st n>=N holds abs(seq.n-x)<eps by A1,SEQ_2
:def 7;
take N;
let n;
assume n>=N;
then abs(seq.n-x)<eps by A2;
then seq.n-x>-eps by SEQ_2:9;
then (seq.n-x)+x>-eps+x by REAL_1:53;
then seq.n>-eps+x by XCMPLX_1:27;
hence seq.n>x-eps by XCMPLX_0:def 8;
end;
theorem Th27:
(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
proof
assume A1:
(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);
A2: for eps be real number st eps>0
ex N st for n st n>=N holds abs(seq.n-x)<eps
proof
let eps be real number;
assume A3: eps>0;
then consider N1 being Nat such that
A4: for n st n>=N1 holds seq.n>x-eps by A1;
consider N2 being Nat such that
A5: for n st n>=N2 holds seq.n<=x by A1;
take N = max(N1,N2);
let n;
assume n>=N;
then n>=N1 & n>=N2 by SQUARE_1:50;
then A6: seq.n>x-eps & seq.n<=x by A4,A5;
then A7: seq.n-x>(x-eps)-x by REAL_1:54;
A8: (x-eps)-x = (x+-eps)-x by XCMPLX_0:def 8
.= -eps by XCMPLX_1:26;
x+eps>x+0 by A3,REAL_1:53;
then seq.n<x+eps by A6,AXIOMS:22;
then seq.n-x<eps by REAL_1:84;
hence abs (seq.n-x)<eps by A7,A8,SEQ_2:9;
end;
hence seq is convergent by SEQ_2:def 6;
hence lim(seq)=x by A2,SEQ_2:def 7;
end;
theorem Th28:
seq is summable implies
for eps st eps>0 holds ex K st Partial_Sums(seq).K>Sum(seq)-eps
proof
assume A1: seq is summable;
let eps;
assume A2: eps>0;
Partial_Sums(seq) is convergent by A1,SERIES_1:def 2;
then consider K such that
A3: for k st k>=K holds
Partial_Sums(seq).k>lim(Partial_Sums(seq))-eps by A2,Th26;
take K;
Sum(seq)=lim(Partial_Sums(seq)) by SERIES_1:def 3;
hence Partial_Sums(seq).K>Sum(seq)-eps by A3;
end;
theorem Th29:
n>=1 implies dseq.n<=Sum(eseq)
proof
assume n>=1;
then n>=0+1;
then A1: n>0 by NAT_1:38;
then for k holds 0<=cseq(n).k & cseq(n).k<=eseq.k by Th15;
then Sum(cseq(n))<=Sum(eseq) by Th24,SERIES_1:24;
hence dseq.n<=Sum(eseq) by A1,Th22;
end;
theorem Th30:
seq is summable & (for k holds seq.k>=0) implies
Sum(seq)>=Partial_Sums(seq).K
proof
assume A1: seq is summable & (for k holds seq.k>=0);
then A2: seq^\(K+1) is summable by SERIES_1:15;
now let k;
(seq^\(K+1)).k = seq.(K+1+k) by SEQM_3:def 9;
hence (seq^\(K+1)).k>=0 by A1;
end;
then Sum(seq^\(K+1))>=0 by A2,SERIES_1:21;
then Partial_Sums(seq).K+Sum(seq^\(K+1))>=Partial_Sums(seq).K+0 by AXIOMS:24;
hence Sum(seq)>=Partial_Sums(seq).K by A1,SERIES_1:18;
end;
theorem Th31:
dseq is convergent & lim(dseq)=Sum(eseq)
proof
for eps st eps>0 holds ex N st for n st n>=N holds dseq.n>Sum(eseq)-eps
proof
let eps;
assume eps>0;
then A1: eps/2>0 by REAL_2:127;
then consider K such that
A2: Partial_Sums(eseq).K>Sum(eseq)-eps/2 by Th24,Th28;
deffunc F(Nat)=Partial_Sums(cseq($1)).K;
consider dseqK being Real_Sequence such that
A3: for n holds dseqK.n=F(n) from ExRealSeq;
dseqK is convergent & lim(dseqK)=Partial_Sums(eseq).K by A3,Th25;
then consider N such that
A4: for n st n>=N holds dseqK.n>Partial_Sums(eseq).K-eps/2 by A1,Th26;
take N1 = N+1;
let n;
assume A5: n>=N1;
N+1>=N+0 by AXIOMS:24;
then A6: n>=N by A5,AXIOMS:22;
A7: n>0 by A5,NAT_1:18;
then A8: for k holds cseq(n).k>=0 by Th15;
cseq(n) is summable by A7,Th22;
then Sum(cseq(n))>=Partial_Sums(cseq(n)).K by A8,Th30;
then dseq.n>=Partial_Sums(cseq(n)).K by A7,Th22;
then A9: dseq.n>=dseqK.n by A3;
dseqK.n>Partial_Sums(eseq).K-eps/2 by A4,A6;
then A10: dseq.n>Partial_Sums(eseq).K-eps/2 by A9,AXIOMS:22;
A11: Sum(eseq)-eps/2-eps/2 = Sum(eseq)-(eps/2+eps/2) by XCMPLX_1:36
.= Sum(eseq)-eps by XCMPLX_1:66;
Partial_Sums(eseq).K-eps/2>Sum(eseq)-eps/2-eps/2 by A2,REAL_1:54;
hence dseq.n>Sum(eseq)-eps by A10,A11,AXIOMS:22;
end;
hence dseq is convergent & lim(dseq)=Sum(eseq) by Th27,Th29;
end;
:: number_e = exp(1)
definition
redefine func number_e equals
:Def6: Sum(eseq);
compatibility by Th23,Th31;
end;
definition
redefine func number_e equals
exp(1);
compatibility by Def6,Th24;
end;
begin :: number_e is irrational
theorem Th32:
x is rational implies ex n st n>=2 & n!*x is integer
proof
assume x is rational;
then consider i, n such that A1: n<>0 & x=i/n by RAT_1:24;
per cases;
suppose n<1+1;
then A2: n<=1 by NAT_1:38;
n>0 by A1,NAT_1:19;
then n>=0+1 by NAT_1:38;
then n=1 by A2,AXIOMS:21;
then reconsider x1 = x as Integer by A1;
take n = 2;
n!*x1 is integer;
hence n>=2 & n!*x is integer;
suppose A3: n>=2;
take n;
thus n>=2 by A3;
n>=1 by A3,AXIOMS:22;
then reconsider m = n-1 as Nat by INT_1:18;
A4: n=m+1 by XCMPLX_1:27;
then n!*x = (m+1)*(m!)*x by NEWTON:21
.= (n*x)*(m!) by A4,XCMPLX_1:4
.= i*(m!) by A1,XCMPLX_1:88;
hence n!*x is integer;
end;
theorem Th33:
n!*eseq.k = (n!)/(k!)
proof
thus n!*eseq.k = n!*(1/(k!)) by Def5
.= (n!)/(k!) by XCMPLX_1:100;
end;
theorem Th34:
(n!)/(k!)>0
proof
n!>0 & k!>0 by NEWTON:23;
hence (n!)/(k!)>0 by REAL_2:127;
end;
theorem Th35:
seq is summable & (for n holds seq.n>0) implies Sum(seq)>0
proof
assume A1: seq is summable & (for n holds seq.n>0);
then A2: Sum(seq)=(Partial_Sums(seq).0)+Sum(seq^\(0+1)) by SERIES_1:18
.= seq.0+Sum(seq^\1) by SERIES_1:def 1;
A3: seq.0>0 by A1;
A4: seq^\1 is summable by A1,SERIES_1:15;
now let n;
(seq^\1).n = seq.(1+n) by SEQM_3:def 9;
hence (seq^\1).n>=0 by A1;
end;
then Sum(seq^\1)>=0 by A4,SERIES_1:21;
then Sum(seq)>0+0 by A2,A3,REAL_1:67;
hence Sum(seq)>0;
end;
theorem Th36:
n!*Sum(eseq^\(n+1))>0
proof
A1: n!>0 by NEWTON:23;
A2: eseq^\(n+1) is summable by Th24,SERIES_1:15;
now let k;
A3: (eseq^\(n+1)).k = eseq.(n+1+k) by SEQM_3:def 9
.= 1/((n+1+k)!) by Def5;
(n+1+k)!>0 by NEWTON:23;
hence (eseq^\(n+1)).k>0 by A3,REAL_2:127;
end;
then Sum(eseq^\(n+1))>0 by A2,Th35;
hence thesis by A1,REAL_2:122;
end;
theorem Th37:
k<=n implies (n!)/(k!) is integer
proof
assume k<=n;
then reconsider m = n-k as Nat by INT_1:18;
defpred P[Nat] means (($1+k)!)/(k!) is integer;
A1: n=m+k by XCMPLX_1:27;
for m holds ((m+k)!)/(k!) is integer
proof
k!<>0 by NEWTON:23;
then A2: P[0] by XCMPLX_1:60;
now let m;
assume ((m+k)!)/(k!) is integer;
then reconsider i = ((m+k)!)/(k!) as Integer;
A3: (m+k+1)*i is Integer;
((m+1)+k)! = (m+k+1)! by XCMPLX_1:1
.= (m+k+1)*((m+k)!) by NEWTON:21;
then (((m+1)+k)!)/(k!) = (m+k+1)*((m+k)!)*(k!)" by XCMPLX_0:def 9
.= (m+k+1)*(((m+k)!)*(k!)") by XCMPLX_1:4
.= (m+k+1)*(((m+k)!)/(k!)) by XCMPLX_0:def 9;
hence (((m+1)+k)!)/(k!) is integer by A3;
end; then A4: for n being Nat holds P[n] implies P[n+1];
for n being Nat holds P[n] from Ind(A2,A4); hence thesis;
end;
hence (n!)/(k!) is integer by A1;
end;
theorem Th38:
n!*Partial_Sums(eseq).n is integer
proof
defpred P[Nat] means $1<=n implies n!*Partial_Sums(eseq).$1 is integer;
for k st k<=n holds n!*Partial_Sums(eseq).k is integer
proof
now assume A1: 0<=n;
n!*Partial_Sums(eseq).0 = n!*eseq.0 by SERIES_1:def 1
.= (n!)/(0!) by Th33;
hence n!*Partial_Sums(eseq).0 is integer by A1,Th37;
end; then A2: P[0];
now let k;
assume A3: k<=n implies n!*Partial_Sums(eseq).k is integer;
assume A4: k+1<=n;
k+0<=k+1 by AXIOMS:24;
then reconsider i = n!*Partial_Sums(eseq).k as Integer by A3,A4,AXIOMS:22;
n!*eseq.(k+1) = (n!)/((k+1)!) by Th33;
then reconsider j = n!*eseq.(k+1) as Integer by A4,Th37;
A5: n!*Partial_Sums(eseq).(k+1)
= n!*(Partial_Sums(eseq).k+eseq.(k+1)) by SERIES_1:def 1
.= n!*Partial_Sums(eseq).k+n!*eseq.(k+1) by XCMPLX_1:8;
i+j is Integer;
hence n!*Partial_Sums(eseq).(k+1) is integer by A5;
end; then A6: P[k] implies P[k+1];
for k holds P[k] from Ind(A2,A6); hence thesis;
end;
hence thesis;
end;
theorem Th39:
x=1/(n+1) implies (n!)/((n+k+1)!)<=x.^.(k+1)
proof
assume A1: x=1/(n+1);
defpred P[Nat] means (n!)/((n+$1+1)!)<=x.^.($1+1);
for k holds (n!)/((n+k+1)!)<=x.^.(k+1)
proof
A2: now
A3: n+1<>0 & n!<>0 by NEWTON:23;
(n!)/((n+1)!) = (n!)/((n+1)*(n!)) by NEWTON:21
.= (n!)*((n+1)*(n!))" by XCMPLX_0:def 9
.= (n!)*((n+1)"*(n!)") by XCMPLX_1:205
.= (n!)*(n!)"*(n+1)" by XCMPLX_1:4
.= 1*(n+1)" by A3,XCMPLX_0:def 7
.= x by A1,XCMPLX_1:217;
hence P[0] by POWER:30;
end;
A4: now let k;
assume A5: P[k];
A6: n+1>0 & n+(k+1)+1>0 & (n+k+1)!<>0 & (n+k)!<>0
by NAT_1:18,NEWTON:23;
then A7: 1/(n+1)>0 by REAL_2:127;
k+1>=0 by NAT_1:18;
then n+(k+1)>=n+0 by AXIOMS:24;
then n+(k+1)+1>=n+1 by AXIOMS:24;
then 1/(n+(k+1)+1)<=1/(n+1) by A6,REAL_2:152;
then A8: (n+(k+1)+1)"<=1/(n+1) by XCMPLX_1:217;
A9: (n!)/((n+k+1)!)>0 by Th34;
A10: (n+(k+1)+1)">0 by A6,REAL_1:72;
A11: x.^.(k+1)*x = x.^.(k+1)*x.^.1 by POWER:30
.= x.^.((k+1)+1) by A1,A7,POWER:32;
(n!)/((n+(k+1)+1)!) = (n!)*((n+(k+1)+1)!)" by XCMPLX_0:def 9
.= (n!)*((n+(k+1)+1)*((n+(k+1))!))" by NEWTON:21
.= (n!)*((n+(k+1)+1)*((n+k+1)!))" by XCMPLX_1:1
.= (n!)*((n+(k+1)+1)"*((n+k+1)!)") by XCMPLX_1:205
.= (n!)*((n+k+1)!)"*(n+(k+1)+1)" by XCMPLX_1:4
.= (n!)/((n+k+1)!)*(n+(k+1)+1)" by XCMPLX_0:def 9;
hence P[k+1] by A1,A5,A8,A9,A10,A11,REAL_2:197;
end;
thus for n holds P[n] from Ind(A2,A4);
end;
hence thesis;
end;
theorem Th40:
n>0 & x=1/(n+1) implies n!*Sum(eseq^\(n+1))<=x/(1-x)
proof
assume A1: n>0 & x=1/(n+1);
then A2:n+1>0+1 by REAL_1:53;
then A3: n+1>0 by AXIOMS:22;
then A4:0<1/(n+1) by REAL_2:127;
A5: 0<x & x<1 by A1,A2,A3,REAL_2:127,SQUARE_1:2;
deffunc F(Nat)=x.^.($1+1);
consider seq being Real_Sequence such that
A6: for k holds seq.k=F(k) from ExRealSeq;
A7: seq.0 = x.^.(0+1) by A6
.= x by POWER:30;
A8: abs x=x by A1,A4,ABSVALUE:def 1;
A9: abs x<1 by A5,ABSVALUE:def 1;
A10: now let k;
thus seq.(k+1) = x.^.(k+1+1) by A6
.= x.^.1*x.^.(k+1) by A1,A4,POWER:32
.= x*x.^.(k+1) by POWER:30
.= x*seq.k by A6;
end;
then A11: seq is summable & Sum(seq)=seq.0/(1-x) by A5,A8,SERIES_1:29;
A12: Sum(seq)=x/(1-x) by A7,A9,A10,SERIES_1:29;
A13: eseq^\(n+1) is summable by Th24,SERIES_1:15;
now let k;
A14: (n!(#)(eseq^\(n+1))).k = n!*((eseq^\(n+1)).k) by SEQ_1:13
.= n!*eseq.(n+1+k) by SEQM_3:def 9
.= n!*eseq.(n+k+1) by XCMPLX_1:1
.= n!*(1/((n+k+1)!)) by Def5
.= n!/((n+k+1)!) by XCMPLX_1:100;
hence (n!(#)(eseq^\(n+1))).k>=0 by Th34;
seq.k=x.^.(k+1) by A6;
hence (n!(#)(eseq^\(n+1))).k<=seq.k by A1,A14,Th39;
end;
then Sum(n!(#)(eseq^\(n+1)))<=Sum(seq) by A11,SERIES_1:24;
hence n!*Sum(eseq^\(n+1))<=x/(1-x) by A12,A13,SERIES_1:13;
end;
theorem Th41:
for n be real number holds
n>=2 & x=1/(n+1) implies x/(1-x)<1
proof
let n be real number;
A1: n+1 > n by REAL_2:174;
assume A2: n>=2 & x=1/(n+1);
then n>=0 by AXIOMS:22;
then A3: x>0 by A1,A2,REAL_2:127;
2<n+1 by A1,A2,AXIOMS:22;
then 2/(n+1)<1 by REAL_2:142;
then 2*x<1 by A2,XCMPLX_1:100;
then x+x<1 by XCMPLX_1:11;
then x<1-x by REAL_1:86;
hence x/(1-x)<1 by A3,REAL_2:142;
end;
theorem
number_e is irrational
proof
assume number_e is rational;
then consider n such that A1: n>=2 & n!*number_e is integer by Th32;
A2: n!*number_e = n!*((Partial_Sums(eseq).n)+Sum(eseq^\(n+1)))
by Def6,Th24,SERIES_1:18
.= n!*(Partial_Sums(eseq).n)+n!*Sum(eseq^\(n+1)) by XCMPLX_1:8;
reconsider ne = n!*number_e as Integer by A1;
reconsider ne1 = n!*Partial_Sums(eseq).n as Integer by Th38;
A3: n!*Sum(eseq^\(n+1))=ne-ne1 by A2,XCMPLX_1:26;
set x = 1/(n+1);
A4: x/(1-x)<1 by A1,Th41;
n>0 by A1,AXIOMS:22;
then n!*Sum(eseq^\(n+1))<=x/(1-x) by Th40;
then n!*Sum(eseq^\(n+1))<0+1 by A4,AXIOMS:22;
then n!*Sum(eseq^\(n+1))<=0 by A3,INT_1:20;
hence contradiction by Th36;
end;