environ
vocabulary IRRAT_1, SEQ1, NEWTON, FUNC, QC_LANG, SEQ2, REAL_1, METRIC_6,
POWER, POWER1, ANAL, F_DIFF, FINSEQ, SIGMA, LEB, TUPLES, SERIES, SEQM,
RFINSEQ, FUNC_REL, PI, ONOP_1, SIN_COS, RAT_1, SQUARE, INT_1, NAT_1,
NT_LAT;
notation ARYTM, INT_1, NAT_1, NEWTON, FUNCT_1, REAL_1, SEQ_1, SEQ_2,
PREPOWER, POWER, ANAL_1, SEQM_3, FINSEQ_1, RVSUM_1, SERIES_1, FINSEQ_2,
RFINSEQ, FINSEQ_4, SIN_COS, COMPLEX1, COMSEQ_3, RAT_1, SQUARE_1, LIMFUNC1,
NAT_LAT, INT_2, PEPIN;
constructors ARYTM, NAT_1, NEWTON, FUNCT_1, REAL_1, SEQ_1, SEQ_2, FUNCT_2,
PARTFUN1, RELSET_1, RELAT_1, PREPOWER, POWER, ANAL_1, SEQM_3, FINSEQ_1,
RVSUM_1, SERIES_1, FINSEQ_2, RFINSEQ, FINSEQ_4, SIN_COS, COMPLEX1,
COMSEQ_3, RAT_1, SQUARE_1, LIMFUNC1, INT_1, NAT_LAT, INT_2, PEPIN;
theorems SEQ_1, REAL_2, PREPOWER, POWER, NEWTON, REAL_1, AXIOMS, NAT_1,
SEQ_2, SEQ_4, ANAL_1, 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;
definitions SEQ_2;
clusters RELSET_1, ARYTM, SEQ_1, INT_1;
schemes SEQ_1, NAT_1;
requirements ARYTM;
begin :: square roots of primes are irrational
reserve k, m, n, p, K, N for Nat;
reserve i, j for Integer;
reserve x, y, eps for Real;
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 T1:
p is prime implies ûp is irrational
proof
assume H1: p is prime;
then H2: p>1 by INT_2:def 5;
then H3: p>0 by AXIOMS:22;
assume ûp is rational;
then consider i, n such that H4: n<>0 & ûp=i/n &
for i1 being Integer, n1 being Nat st n1<>0 & ûp=i1/n1 holds nón1
by RAT_1:25;
H5: i=ûpùn by REAL_2:73,H4;
ûpò0 & nò0 by SQUARE_1:87,NAT_1:18,H3;
then iò0 by REAL_2:121,H5;
then reconsider m = i as Nat by INT_1:16;
H6: mý = (ûpùn)ý by H5
.= (ûp)ýùný by SQUARE_1:68
.= pùný by SQUARE_1:88,H3;
then p³mý by NAT_1:def 3;
then p³mùm by SQUARE_1:58;
then p³m by NAT_LAT:95,H1;
then consider m1 being Nat such that H7: m=pùm1 by NAT_1:def 3;
ný = mý/p by REAL_2:72,H3,H6
.= (pùm1)ý/p by H7
.= pýùm1ý/p by SQUARE_1:68
.= pùpùm1ý/p by SQUARE_1:58
.= pù(pùm1ý)/p by AXIOMS:16
.= pùm1ý by REAL_2:62,H3;
then p³ný by NAT_1:def 3;
then p³nùn by SQUARE_1:58;
then p³n by NAT_LAT:95,H1;
then consider n1 being Nat such that H8: n=pùn1 by NAT_1:def 3;
n1<>0 by H4,H8;
then H9: n1>0 by NAT_1:19;
then m1/n1 = (pùm1)/(pùn1) by REAL_2:55,H3
.= m/n by H7,H8
.= ûp by H4;
then H10: nón1 by H4,H9;
pùn1>1ùn1 by REAL_2:199,H2,H9;
then n>n1 by H8;
hence contradiction by H10;
end;
theorem T2:
ex x, y st x is irrational & y is irrational & x.^.y is rational
proof
set w = û2;
H1: w is irrational by INT_2:44,T1;
w>0 by AXIOMS:22,SQUARE_1:84;
then (w.^.w).^.w = w.^.(wùw) by POWER:38
.= w.^.(wý) by SQUARE_1:58
.= w.^.2 by SQUARE_1:88
.= wý by POWER:53
.= 2 by SQUARE_1:88;
then H2: (w.^.w).^.w is rational by RAT_1:8;
per cases;
suppose H3: w.^.w is rational;
take w, w;
thus thesis by H1,H3;
suppose H4: w.^.w is irrational;
take w.^.w, w;
thus thesis by H1,H2,H4;
end;
begin :: a proof that e = e
scheme LambdaRealSeq{F(Nat)->Real}:
(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
thus ex seq st for n holds seq.n=F(n) from ExRealSeq;
let seq1, seq2;
assume H1: for n holds seq1.n=F(n);
assume H2: for n holds seq2.n=F(n);
now let n;
thus seq1.n = F(n) by H1
.= seq2.n by H2;
end;
hence seq1 = seq2 by SEQ_1:9;
end;
definition
let k;
func aseq(k) -> Real_Sequence means
:Daseq: for n holds it.n=(n-k)/n;
correctness from LambdaRealSeq;
end;
definition
let k;
func bseq(k) -> Real_Sequence means
:Dbseq: for n holds it.n=(n choose k)ù(n.^.(-k));
correctness from LambdaRealSeq;
end;
definition
let n;
func cseq(n) -> Real_Sequence means
:Dcseq: for k holds it.k=(n choose k)ù(n.^.(-k));
correctness from LambdaRealSeq;
end;
theorem T3:
cseq(n).k=bseq(k).n
proof
thus cseq(n).k = (n choose k)ù(n.^.(-k)) by Dcseq
.= bseq(k).n by Dbseq;
end;
definition
func dseq -> Real_Sequence means
:Ddseq: for n holds it.n=(1+(1/n)).^.n;
correctness from LambdaRealSeq;
end;
definition
func eseq -> Real_Sequence means
:Deseq: for k holds it.k=1/(k!);
correctness from LambdaRealSeq;
end;
:: lim(\n:(n choose k)ù(n.^.(-k))) = 1/(k!)
theorem T4:
n>0 implies (n.^.(-(k+1)))=(n.^.(-k))/n
proof
assume H: n>0;
thus (n.^.(-(k+1))) = (n.^.((-k)-1)) by REAL_2:6
.= (n.^.(-k))/(n.^.1) by POWER:34,H
.= (n.^.(-k))/n by POWER:30;
end;
theorem T5:
for x, y, z, v, w being Real st y<>0 & z<>0 & v<>0 & w<>0 holds
x/(yùzù(v/w))=(w/z)ù(x/(yùv))
proof
let x, y, z, v, w be Real;
assume H1: y<>0 & z<>0 & v<>0 & w<>0;
H2: yùv<>0 by REAL_1:23,H1;
H3: w/z<>0 by REAL_2:50,H1;
thus x/(yùzù(v/w)) = x/(yùzù(vùw")) by REAL_1:16
.= x/(zù(yù(vùw"))) by AXIOMS:16
.= x/(zù(yùvùw")) by AXIOMS:16
.= x/(zù((yùv)/w)) by REAL_1:16
.= x/((yùv)/(w/z)) by REAL_2:61,H1
.= (w/z)ù(x/(yùv)) by REAL_2:61,H2,H3;
end;
theorem T6:
(n choose (k+1))=((n-k)/(k+1))ù(n choose k)
proof
per cases;
suppose H1: k+1ón;
reconsider l = n-(k+1) as Nat by NEWTON:2,H1;
H2: l+1 = n-(k+1-1) by REAL_1:28
.= n-k by REAL_2:17;
reconsider l1 = n-k as Nat by H2;
H3: l1 = l+1 by H2;
k ó k+1 by NAT_1:29; then H4: k ó n by AXIOMS:22,H1;
H5: k+1<>0 & l+1<>0 & l1<>0 & k!<>0 & l1!<>0 by NAT_1:21,NEWTON:23,H3;
thus (n choose (k+1)) = n!/((k+1)!ù(l!)) by NEWTON:def 3,H1
.= n!/((k!ù(k+1))ù(l!)) by NEWTON:21
.= n!/((k!ù(k+1))ù((l!)ù(l+1)/(l+1))) by REAL_2:72,H5
.= n!/((k!ù(k+1))ù((l+1)!/(l+1))) by NEWTON:21
.= n!/((k!ù(k+1))ù(l1!/(l+1))) by H3
.= n!/((k!ù(k+1))ù(l1!/l1)) by H3
.= (l1/(k+1))ù(n!/((k!)ù(l1!))) by T5,H5
.= ((n-k)/(k+1))ù(n choose k) by NEWTON:def 3,H4;
suppose H6: k+1>n & kón;
then kòn & kón by NAT_1:38;
then k=n by AXIOMS:21;
then H7: n-k=0 by REAL_1:36;
thus (n choose (k+1)) = 0 by NEWTON:def 3,H6
.= 0ù(n choose k)
.= (0ù(k+1)")ù(n choose k)
.= (0/(k+1))ù(n choose k) by REAL_1:16
.= ((n-k)/(k+1))ù(n choose k) by H7;
suppose H8: k+1>n & k>n;
thus (n choose (k+1)) = 0 by NEWTON:def 3,H8
.= ((n-k)/(k+1))ù0
.= ((n-k)/(k+1))ù(n choose k) by NEWTON:def 3,H8;
end;
theorem T7:
n>0 implies bseq(k+1).n=(1/(k+1))ù(bseq(k).n)ù(aseq(k).n)
proof
assume H: n>0;
thus bseq(k+1).n = (n choose (k+1))ù(n.^.(-(k+1))) by Dbseq
.= ((n-k)/(k+1))ù(n choose k)ù(n.^.(-(k+1))) by T6
.= ((n-k)/(k+1))ù(n choose k)ù((n.^.(-k))/n) by T4,H
.= (n-k)ù(k+1)"ù(n choose k)ù((n.^.(-k))/n) by REAL_1:16
.= (n-k)ù(k+1)"ù(n choose k)ù((n.^.(-k))ùn") by REAL_1:16
.= (n-k)ù(k+1)"ù(n choose k)ù(n.^.(-k))ùn" by AXIOMS:16
.= (k+1)"ù(n choose k)ù(n-k)ù(n.^.(-k))ùn" by AXIOMS:16
.= (k+1)"ù(n choose k)ù(n.^.(-k))ù(n-k)ùn" by AXIOMS:16
.= (k+1)"ù((n choose k)ù(n.^.(-k)))ù(n-k)ùn" by AXIOMS:16
.= (k+1)"ù((n choose k)ù(n.^.(-k)))ù((n-k)ùn") by AXIOMS:16
.= (1/(k+1))ù((n choose k)ù(n.^.(-k)))ù((n-k)ùn") by REAL_1:33
.= (1/(k+1))ù((n choose k)ù(n.^.(-k)))ù((n-k)/n) by REAL_1:16
.= (1/(k+1))ù(bseq(k).n)ù((n-k)/n) by Dbseq
.= (1/(k+1))ù(bseq(k).n)ù(aseq(k).n) by Daseq;
end;
theorem T8:
n>0 implies aseq(k).n=1-(k/n)
proof
assume H: n>0;
thus aseq(k).n = (n-k)/n by Daseq
.= (n/n)-(k/n) by REAL_1:40,H
.= 1-(k/n) by REAL_1:37,H;
end;
theorem T9:
aseq(k) is convergent & lim(aseq(k))=1
proof
H1: for eps st 00;
consider N such that H3: N>k/eps by SEQ_4:10;
kò0ùeps by NAT_1:18;
then k/epsò0 by REAL_2:177,H2;
then H4: N>0 by AXIOMS:22,H3;
take N;
let n;
assume H5: nòN;
then H6: n>0 by AXIOMS:22,H4;
kò0ùn by NAT_1:18;
then H7: k/nò0 by REAL_2:177,H6;
H8: ³.aseq(k).n-1.³ = ³.(1-(k/n))-1.³ by T8,H6
.= ³.(1+-(k/n))-1.³ by REAL_1:14
.= ³.-(k/n).³ by REAL_2:17
.= ³.k/n.³ by ANAL_1:17
.= k/n by ANAL_1:1,H7;
n>(k/eps) by AXIOMS:22,H3,H5;
then (k/eps)ùeps0 holds bseq(0).n=1
proof
let n;
assume H: n>0;
thus bseq(0).n = (n choose 0)ù(n.^.(-0)) by Dbseq
.= 1ù(n.^.(-0)) by NEWTON:29
.= 1ù(n.^.0) by REAL_1:26
.= 1 by POWER:29,H;
end;
theorem T12:
(1/(k+1))ù(1/(k!))=1/((k+1)!)
proof
k+1<>0 & k!<>0 by NAT_1:21,NEWTON:23;
hence (1/(k+1))ù(1/(k!)) = 1/((k+1)ù(k!)) by REAL_2:51
.= 1/((k+1)!) by NEWTON:21;
end;
theorem T13:
bseq(k) is convergent & lim(bseq(k))=1/(k!) & lim(bseq(k))=eseq.k
proof
H1: bseq(0) is convergent & lim(bseq(0))=1/(0!)
proof
consider bseq0 being Real_Sequence such that
H2: for n holds bseq0.n=1 from ExRealSeq;
H3: bseq0 is convergent & lim(bseq0)=1 by T10,H2;
for n st nò1 holds bseq(0).n=bseq0.n
proof
let n;
assume nò1;
then nò0+1;
then n>0 by NAT_1:38;
hence bseq(0).n = 1 by T11
.= bseq0.n by H2;
end;
then H4: ex N st for n st nòN holds bseq(0).n=bseq0.n;
hence bseq(0) is convergent by SEQ_4:31,H3;
thus lim(bseq(0)) = lim(bseq0) by SEQ_4:32,H3,H4
.= 1 by H3
.= 1/1 by REAL_2:43
.= 1/(0!) by NEWTON:18;
end;
H5: now let k;
assume H6: bseq(k) is convergent & lim(bseq(k))=1/(k!);
thus bseq(k+1) is convergent & lim(bseq(k+1))=1/((k+1)!)
proof
consider seq such that
H7: for n holds seq.n = (1/(k+1))ù(bseq(k).n) from ExRealSeq;
H8: seq = (1/(k+1))þ(bseq(k)) by SEQ_1:13,H7;
H9: seq is convergent & lim(seq)=1/((k+1)!)
proof
thus seq is convergent by SEQ_2:21,H6,H8;
thus lim(seq) = (1/(k+1))ù(1/(k!)) by SEQ_2:22,H6,H8
.= 1/((k+1)!) by T12;
end;
consider seq1 such that
H10: for n holds seq1.n=seq.nù(aseq(k).n) from ExRealSeq;
H11: seq1=seqþ(aseq(k)) by SEQ_1:12,H10;
H12: seq1 is convergent & lim(seq1)=1/((k+1)!)
proof
H13: aseq(k) is convergent & lim(aseq(k))=1 by T9;
then seqþ(aseq(k)) is convergent by SEQ_2:28,H9;
hence seq1 is convergent by H11;
thus lim(seq1) = lim(seqþ(aseq(k))) by H11
.= lim(seq)ùlim(aseq(k)) by SEQ_2:29,H9,H13
.= (1/((k+1)!))ùlim(aseq(k)) by H9
.= (1/((k+1)!))ù1 by H13
.= 1/((k+1)!);
end;
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 T7
.= (seq.n)ù(aseq(k).n) by H7
.= seq1.n by H10;
end;
then H14: ex N st for n st nòN holds bseq(k+1).n=seq1.n;
hence bseq(k+1) is convergent by SEQ_4:31,H12;
thus lim(bseq(k+1)) = lim(seq1) by SEQ_4:32,H12,H14
.= 1/((k+1)!) by H12;
end;
end;
for k holds bseq(k) is convergent & lim(bseq(k))=1/(k!) from Ind(H1,H5);
hence bseq(k) is convergent & lim(bseq(k))=1/(k!);
hence lim(bseq(k))=eseq.k by Deseq;
end;
:: 0 ó (n choose k)ù(n.^.(-k))) ó 1/(k!)
theorem T14:
k0 by AXIOMS:22,H1;
H4: aseq(k).n=(n-k)/n by Daseq;
H5: aseq(k).n=1-(k/n) by T8,H3;
n-k>0 by REAL_2:108,H1;
then (n-k)/n>0 by REAL_2:127,H3;
hence aseq(k).n>0 by H4;
k/nò0 by REAL_2:125,H2,H3;
then 1-(k/n)ó1-0 by REAL_2:107;
then 1-(k/n)ó1 by REAL_1:25;
hence aseq(k).nó1 by H5;
end;
theorem T15:
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 H1: n>0;
H2: bseq(k).n=(n choose k)ù(n.^.(-k)) by Dbseq;
(n choose k) is Nat by NEWTON:35;
then H3: (n choose k)ò0 by NAT_1:18;
n.^.(-k)>0 by POWER:39,H1;
then (n choose k)ù(n.^.(-k))ò0 by REAL_2:121,H3;
hence H4: 0óbseq(k).n by H2;
H5: bseq(0).nó1/(0!)
proof
H6: bseq(0).n=1 by T11,H1;
1 = 1/1 by REAL_2:43
.= 1/(0!) by NEWTON:18;
then 1ó1/(0!);
hence bseq(0).nó1/(0!) by H6;
end;
H7: now let k;
assume H8: bseq(k).nó1/(k!);
thus bseq(k+1).nó1/((k+1)!)
proof
(k+1)!>0 by NEWTON:23;
then H9: 1/((k+1)!)>0 by REAL_2:149;
per cases;
suppose H10: k0 by NAT_1:21;
then k+1>0 by NAT_1:19;
then 1/(k+1)>0 by REAL_2:149;
then 1/(k+1)ò0;
then (1/(k+1))ù(bseq(k).n)ó(1/(k+1))ù(1/(k!)) by AXIOMS:25,H8;
then H12: (1/(k+1))ù(bseq(k).n)ó1/((k+1)!) by T12;
aseq(k).nò0 by T14,H10;
then (1/(k+1))ù(bseq(k).n)ù(aseq(k).n)ó(1/((k+1)!))ù(aseq(k).n)
by AXIOMS:25,H12;
then H13: bseq(k+1).nó(1/((k+1)!))ù(aseq(k).n) by H11;
aseq(k).nó1 by T14,H10;
then 1/((k+1)!)ù(aseq(k).n)ó1/((k+1)!) by REAL_2:147,H9;
hence thesis by AXIOMS:22,H13;
suppose kòn;
then H14: k+1>n by NAT_1:38;
bseq(k+1).n = (n choose (k+1))ù(n.^.(-(k+1))) by Dbseq
.= 0ù(n.^.(-(k+1))) by NEWTON:def 3,H14
.= 0;
hence thesis by H9;
end;
end;
for k holds bseq(k).nó1/(k!) from Ind(H5,H7);
hence H15: bseq(k).nó1/(k!);
eseq.k=1/(k!) by Deseq;
hence H16: bseq(k).nóeseq.k by H15;
bseq(k).n=cseq(n).k by T3;
hence 0ócseq(n).k & cseq(n).kó1/(k!) & cseq(n).kóeseq.k by H4,H15,H16;
end;
:: n>0 implies (1+(1/n)).^.n = ä(\k:(n choose k)ù(n.^.(-k)))
theorem T16:
for seq st seq^\1 is summable holds
seq is summable & ä(seq)=(seq.0)+ä(seq^\1)
proof
let seq;
assume seq^\1 is summable;
hence seq is summable by SERIES_1:16;
hence ä(seq) = Partial_Sums(seq).0+ä(seq^\(1+0)) by SERIES_1:18
.= (seq.0)+ä(seq^\1) by SERIES_1:def 1;
end;
theorem T17:
for sq st len(sq)=n & 1ók & k0 holds
ä(sq)=(sq.1)+ä(sq/^1)
proof
let sq;
assume H1: len(sq)>0;
then 1ó1 & 0+1ólen(sq) by NAT_1:38;
then H2: 1îdom(sq) by FINSEQ_3:27;
sq is non empty by FINSEQ_1:25,H1;
hence ä(sq) = ä(<*ã(sq,1)*>^(sq/^1)) by FINSEQ_5:32
.= ä(<*sq.1*>^(sq/^1)) by FINSEQ_4:22,H2
.= (sq.1)+ä(sq/^1) by RVSUM_1:106;
end;
theorem T19:
for n holds
for seq, sq st
len(sq)=n &
(for k st k0 by NAT_1:38;
then H14: len(sq)>0 by H11;
n+1ò0+1 by AXIOMS:24,H12;
then n+1ò1;
then len(sq)ò1 by H11;
then H15: len(sq/^1) = len(sq)-1 by RFINSEQ:def 2
.= (n+1)-1 by H11
.= n by REAL_2:17;
H16: now let k;
assume k0 & y<>0 & kón implies
((x,y) In_Power n).(k+1)=(n choose k)ù(x.^.(n-k))ù(y.^.k)
proof
assume H1: x<>0 & y<>0 & kón;
kò0 by NAT_1:18;
then H2: k+1ò0+1 by AXIOMS:24;
then reconsider i1 = (k+1)-1 as Nat by NEWTON:2;
H3: i1=k by REAL_2:17;
then i1ón by H1;
then reconsider l = n-i1 as Nat by NEWTON:2;
H4: l=n-k by H3;
H5: len((x,y) In_Power n)=n+1 by NEWTON:def 4;
1ók+1 & k+1ón+1 by AXIOMS:24,H1,H2;
then 1ók+1 & k+1ólen((x,y) In_Power n) by H5;
then k+1îdom((x,y) In_Power n) by 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 POWER:48,H1
.= (n choose i1)ù(x.^.l)ù(y.^.i1) by POWER:48,H1
.= (n choose k)ù(x.^.l)ù(y.^.i1) by H3
.= (n choose k)ù(x.^.(n-k))ù(y.^.i1) by H4
.= (n choose k)ù(x.^.(n-k))ù(y.^.k) by H3;
end;
theorem T21:
n>0 & kón implies cseq(n).k=((1,1/n) In_Power n).(k+1)
proof
assume H1: n>0 & kón;
then H2: 1/n>0 by REAL_2:149;
H3: 1<>0;
thus ((1,1/n) In_Power n).(k+1)
= (n choose k)ù(1.^.(n-k))ù((1/n).^.k) by T20,H1,H2,H3
.= (n choose k)ù1ù((1/n).^.k) by POWER:31
.= (n choose k)ù((1/n).^.k)
.= (n choose k)ù(n.^.(-k)) by POWER:37,H1
.= cseq(n).k by Dcseq;
end;
theorem T22:
n>0 implies
cseq(n) is summable & ä(cseq(n))=(1+(1/n)).^.n & ä(cseq(n))=dseq.n
proof
assume H1: n>0;
then 1/n>0 by REAL_2:149;
then H2: 1+(1/n)>1+0 by REAL_1:59;
H3: 1+(1/n)>0 by AXIOMS:22,H2;
H4: len((1,1/n) In_Power n)=n+1 by NEWTON:def 4;
H5: now let k;
assume kn by NAT_1:38;
thus cseq(n).k = (n choose k)ù(n.^.(-k)) by Dcseq
.= 0ù(n.^.(-k)) by NEWTON:def 3,H7
.= 0;
end;
thus cseq(n) is summable by T19,H4,H5,H6;
thus H8: (1+(1/n)).^.n = (1+(1/n))|^n by POWER:48,H3
.= ä((1,1/n) In_Power n) by NEWTON:41
.= ä(cseq(n)) by T19,H4,H5,H6;
thus dseq.n = (1+(1/n)).^.n by Ddseq
.= ä(cseq(n)) by H8;
end;
:: number_e = lim(\n:(1+(1/n)).^.n)
theorem T23:
dseq is convergent & lim(dseq)=number_e
proof
H1: now let n;
thus (dseq^\1).n = dseq.(n+1) by SEQM_3:def 9
.= (1+1/(n+1)).^.(n+1) by Ddseq;
end;
then H2: dseq^\1 is convergent by POWER:67;
hence dseq is convergent by SEQ_4:35;
number_e=lim(dseq^\1) by POWER:def 4,H1;
hence number_e=lim(dseq) by SEQ_4:36,H2;
end;
:: exp(1) = ä(\k:1/(k!))
theorem T24:
eseq is summable & ä(eseq)=exp(1)
proof
now let k;
thus eseq.k = 1/(k!) by Deseq
.= (1 #N k)/(k!) by PREPOWER:8
.= (1 ExpSeq).k by SIN_COS:def 9;
end;
then H: eseq=(1 ExpSeq) by SEQ_1:9;
1 ExpSeq is summable by SIN_COS:49;
hence eseq is summable by H;
thus exp(1) = exp.1 by SIN_COS:def 27
.= ä(1 ExpSeq) by SIN_COS:def 26
.= ä(eseq) by H;
end;
:: lim(\n:(1+(1/n)).^.n) = ä(\k:1/(k!))
theorem T25:
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
H1: now let dseq0 be Real_Sequence;
assume H2: for n holds dseq0.n=Partial_Sums(cseq(n)).0;
now let n;
thus dseq0.n = Partial_Sums(cseq(n)).0 by H2
.= cseq(n).0 by SERIES_1:def 1
.= bseq(0).n by T3;
end;
then H3: dseq0 = bseq(0) by SEQ_1:9;
hence dseq0 is convergent by T13;
thus lim(dseq0) = lim(bseq(0)) by H3
.= eseq.0 by T13
.= Partial_Sums(eseq).0 by SERIES_1:def 1;
end;
H4: now let K;
assume
H5: 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;
consider dseqK being Real_Sequence such that
H6: for n holds dseqK.n=Partial_Sums(cseq(n)).K from ExRealSeq;
H7: dseqK is convergent & lim(dseqK)=Partial_Sums(eseq).K by H5,H6;
let dseqK1 being Real_Sequence;
assume H8: for n holds dseqK1.n=Partial_Sums(cseq(n)).(K+1);
now let n;
thus dseqK1.n = Partial_Sums(cseq(n)).(K+1) by H8
.= Partial_Sums(cseq(n)).K+cseq(n).(K+1) by SERIES_1:def 1
.= dseqK.n+cseq(n).(K+1) by H6
.= dseqK.n+bseq(K+1).n by T3
.= (dseqK+bseq(K+1)).n by SEQ_1:11;
end;
then H9: dseqK1=dseqK+bseq(K+1) by SEQ_1:9;
H10: bseq(K+1) is convergent by T13;
hence dseqK1 is convergent by SEQ_2:19,H7,H9;
thus lim(dseqK1) = lim(dseqK+bseq(K+1)) by H9
.= lim(dseqK)+lim(bseq(K+1)) by SEQ_2:20,H7,H10
.= Partial_Sums(eseq).K+lim(bseq(K+1)) by H7
.= Partial_Sums(eseq).K+eseq.(K+1) by T13
.= Partial_Sums(eseq).(K+1) by SERIES_1:def 1;
end;
thus thesis from Ind(H1,H4);
end;
theorem T26:
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 seq is convergent & lim(seq)=x;
then H1: for eps st eps>0 ex N st for n st nòN holds ³.seq.n-x.³0;
then consider N such that H2: for n st nòN holds ³.seq.n-x.³-eps by SEQ_2:9;
then H3: (seq.n-x)+x>-eps+x by REAL_1:59;
(seq.n-x)+x=seq.n by REAL_2:12;
then H4: seq.n>-eps+x by H3;
-eps+x=x-eps by REAL_1:def 3;
hence seq.n>x-eps by H4;
end;
theorem T27:
(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 H1:
(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);
H2: for eps st eps>0 holds ex N st for n st nòN holds ³.seq.n-x.³0;
then consider N1 being Nat such that
H4: for n st nòN1 holds seq.n>x-eps by H1;
consider N2 being Nat such that
H5: for n st nòN2 holds seq.nóx by H1;
take N = max(N1,N2);
let n;
assume nòN;
then nòN1 & nòN2 by SQUARE_1:50;
then H6: seq.n>x-eps & seq.nóx by H4,H5;
then H7: seq.n-x>(x-eps)-x by REAL_1:59;
(x-eps)-x = (x+-eps)-x by REAL_1:def 3
.= -eps by REAL_2:17;
then H8: seq.n-x>-eps by H7;
x+eps>x+0 by REAL_1:59,H3;
then seq.n0 holds ex K st Partial_Sums(seq).K>ä(seq)-eps
proof
assume H1: seq is summable;
let eps;
assume H2: eps>0;
Partial_Sums(seq) is convergent by SERIES_1:def 2,H1;
then consider K such that
H3: for k st kòK holds
Partial_Sums(seq).k>lim(Partial_Sums(seq))-eps by T26,H2;
take K;
ä(seq)=lim(Partial_Sums(seq)) by SERIES_1:def 3;
then H4: for k st kòK holds Partial_Sums(seq).k>ä(seq)-eps by H3;
thus Partial_Sums(seq).K>ä(seq)-eps by H4;
end;
theorem T29:
nò1 implies dseq.nóä(eseq)
proof
assume nò1;
then nò0+1;
then H: n>0 by NAT_1:38;
for k holds 0ócseq(n).k & cseq(n).kóeseq.k by T15,H;
then ä(cseq(n))óä(eseq) by SERIES_1:24,T24;
hence dseq.nóä(eseq) by T22,H;
end;
theorem T30:
seq is summable & (for k holds seq.kò0) implies
ä(seq)òPartial_Sums(seq).K
proof
assume H1: seq is summable & (for k holds seq.kò0);
then H2: 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 H1;
end;
then ä(seq^\(K+1))ò0 by SERIES_1:21,H2;
then Partial_Sums(seq).K+ä(seq^\(K+1))òPartial_Sums(seq).K+0 by AXIOMS:24;
hence ä(seq)òPartial_Sums(seq).K by SERIES_1:18,H1;
end;
theorem T31:
dseq is convergent & lim(dseq)=ä(eseq)
proof
for eps st eps>0 holds ex N st for n st nòN holds dseq.n>ä(eseq)-eps
proof
let eps;
assume eps>0;
then H1: eps/2>0 by REAL_2:127;
consider K such that
H2: Partial_Sums(eseq).K>ä(eseq)-eps/2 by T28,T24,H1;
consider dseqK being Real_Sequence such that
H3: for n holds dseqK.n=Partial_Sums(cseq(n)).K from ExRealSeq;
H4: dseqK is convergent & lim(dseqK)=Partial_Sums(eseq).K by T25,H3;
consider N such that
H5: for n st nòN holds dseqK.n>Partial_Sums(eseq).K-eps/2 by T26,H1,H4;
take N1 = N+1;
let n;
assume H6: nòN1;
N+1òN+0 by AXIOMS:24;
then H7: nòN by AXIOMS:22,H6;
Nò0 by NAT_1:18;
then N1>0 by NAT_1:38;
then H8: n>0 by AXIOMS:22,H6;
H9: for k holds cseq(n).kò0 by T15,H8;
cseq(n) is summable by T22,H8;
then ä(cseq(n))òPartial_Sums(cseq(n)).K by T30,H9;
then dseq.nòPartial_Sums(cseq(n)).K by T22,H8;
then H10: dseq.nòdseqK.n by H3;
dseqK.n>Partial_Sums(eseq).K-eps/2 by H5,H7;
then H11: dseq.n>Partial_Sums(eseq).K-eps/2 by AXIOMS:22,H10;
H12: ä(eseq)-eps/2-eps/2 = ä(eseq)-(eps/2+eps/2) by REAL_1:27
.= ä(eseq)-eps by REAL_2:90;
Partial_Sums(eseq).K-eps/2>ä(eseq)-eps/2-eps/2 by REAL_1:59,H2;
then Partial_Sums(eseq).K-eps/2>ä(eseq)-eps by H12;
hence dseq.n>ä(eseq)-eps by AXIOMS:22,H11;
end;
hence dseq is convergent & lim(dseq)=ä(eseq) by T27,T29;
end;
:: number_e = exp(1)
definition
redefine func number_e equals
:Dnumber_e: ä(eseq);
compatibility
proof
number_e = lim(dseq) by T23
.= ä(eseq) by T31;
hence thesis;
end;
end;
definition
redefine func number_e equals
exp(1);
compatibility
proof
number_e = ä(eseq) by Dnumber_e
.= exp(1) by T24;
hence thesis;
end;
end;
begin :: number_e is irrational
theorem T32:
x is rational implies ex n st nò2 & n!ùx is integer
proof
assume H1: x is rational;
consider i, n such that H2: n<>0 & x=i/n by RAT_1:24,H1;
per cases;
suppose n<1+1;
then H3: nó1 by NAT_1:38;
n>0 by NAT_1:19,H2;
then nò0+1 by NAT_1:38;
then H4: n=1 by AXIOMS:21,H3;
x = i/n by H2
.= i/1 by H4
.= i by REAL_2:44;
then reconsider x1 = x as Integer;
take n = 2;
n!ùx1 is integer;
hence nò2 & n!ùx is integer;
suppose H5: nò2;
take n;
thus nò2 by H5;
then nò1 by AXIOMS:22;
then reconsider m = n-1 as Nat by INT_1:18;
H6: n=m+1 by REAL_2:12;
then n!ùx = (m+1)!ùx
.= (m+1)ù(m!)ùx by NEWTON:21
.= (nù(m!))ùx by H6
.= nù(xù(m!)) by AXIOMS:16
.= (nùx)ù(m!) by AXIOMS:16
.= (nù(i/n))ù(m!) by H2
.= iù(m!) by REAL_1:43,H2;
hence n!ùx is integer;
end;
theorem T33:
n!ùeseq.k = (n!)/(k!)
proof
H: k!<>0 by NEWTON:23;
thus n!ùeseq.k = n!ù(1/(k!)) by Deseq
.= (n!)/(k!) by REAL_2:56,H;
end;
theorem T34:
(n!)/(k!)>0
proof
n!>0 & k!>0 by NEWTON:23;
hence (n!)/(k!)>0 by REAL_2:127;
end;
theorem T35:
seq is summable & (for n holds seq.n>0) implies ä(seq)>0
proof
assume H1: seq is summable & (for n holds seq.n>0);
H2: ä(seq)=(Partial_Sums(seq).0)+ä(seq^\(0+1)) by SERIES_1:18,H1
.= seq.0+ä(seq^\1) by SERIES_1:def 1;
H3: seq.0>0 by H1;
H4: seq^\1 is summable by SERIES_1:15,H1;
now let n;
(seq^\1).n = seq.(1+n) by SEQM_3:def 9;
hence (seq^\1).nò0 by H1;
end;
then ä(seq^\1)ò0 by SERIES_1:21,H4;
then ä(seq)>0+0 by REAL_1:67,H2,H3;
hence ä(seq)>0;
end;
theorem T36:
n!ùä(eseq^\(n+1))>0
proof
H1: n!>0 by NEWTON:23;
H2: eseq^\(n+1) is summable by SERIES_1:15,T24;
now let k;
H3: (eseq^\(n+1)).k = eseq.(n+1+k) by SEQM_3:def 9
.= 1/((n+1+k)!) by Deseq;
(n+1+k)!>0 by NEWTON:23;
hence (eseq^\(n+1)).k>0 by REAL_2:149,H3;
end;
then ä(eseq^\(n+1))>0 by T35,H2;
hence thesis by REAL_2:122,H1;
end;
theorem T37:
kón implies (n!)/(k!) is integer
proof
assume kón;
then reconsider m = n-k as Nat by INT_1:18;
H1: n=m+k by REAL_2:12;
for m holds ((m+k)!)/(k!) is integer
proof
k!<>0 by NEWTON:23;
then ((0+k)!)/(k!) = 1 by REAL_1:37;
then H2: ((0+k)!)/(k!) is integer;
H3: now let m;
assume ((m+k)!)/(k!) is integer;
then reconsider i = ((m+k)!)/(k!) as Integer;
H4: (m+k+1)ùi is Integer;
((m+1)+k)! = (m+k+1)! by AXIOMS:13
.= (m+k+1)ù((m+k)!) by NEWTON:21;
then (((m+1)+k)!)/(k!) = (m+k+1)ù((m+k)!)/(k!)
.= (m+k+1)ù((m+k)!)ù(k!)" by REAL_1:16
.= (m+k+1)ù(((m+k)!)ù(k!)") by AXIOMS:16
.= (m+k+1)ù(((m+k)!)/(k!)) by REAL_1:16;
hence (((m+1)+k)!)/(k!) is integer by H4;
end;
thus thesis from Ind(H2,H3);
end;
then ((m+k)!)/(k!) is integer;
hence (n!)/(k!) is integer by H1;
end;
theorem T38:
n!ùPartial_Sums(eseq).n is integer
proof
for k st kón holds n!ùPartial_Sums(eseq).k is integer
proof
H1: now assume H2: 0ón;
n!ùPartial_Sums(eseq).0 = n!ùeseq.0 by SERIES_1:def 1
.= (n!)/(0!) by T33;
hence n!ùPartial_Sums(eseq).0 is integer by T37,H2;
end;
H3: now let k;
assume H4: kón implies n!ùPartial_Sums(eseq).k is integer;
assume H5: k+1ón;
k+0ók+1 by AXIOMS:24;
then kón by AXIOMS:22,H5;
then reconsider i = n!ùPartial_Sums(eseq).k as Integer by H4;
n!ùeseq.(k+1) = (n!)/((k+1)!) by T33;
then reconsider j = n!ùeseq.(k+1) as Integer by T37,H5;
H6: 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 AXIOMS:18;
i+j is Integer;
hence n!ùPartial_Sums(eseq).(k+1) is integer by H6;
end;
thus thesis from Ind(H1,H3);
end;
hence thesis;
end;
theorem T39:
x=1/(n+1) implies (n!)/((n+k+1)!)óx.^.(k+1)
proof
assume H1: x=1/(n+1);
for k holds (n!)/((n+k+1)!)óx.^.(k+1)
proof
H2: now
H3: n+1<>0 & n!<>0 by NAT_1:21,NEWTON:23;
H4: (n!)/((n+1)!) = (n!)/((n+1)ù(n!)) by NEWTON:21
.= (n!)ù((n+1)ù(n!))" by REAL_1:16
.= (n!)ù((n+1)"ù(n!)") by REAL_1:24,H3
.= (n!)ù(n!)"ù(n+1)" by AXIOMS:16
.= 1ù(n+1)" by REAL_1:def 2,H3
.= 1/(n+1) by REAL_1:33
.= x by H1;
H5: x = x.^.(0+1) by POWER:30;
thus (n!)/((n+0+1)!)óx.^.(0+1) by H4,H5;
end;
H6: now let k;
assume H7: (n!)/((n+k+1)!)óx.^.(k+1);
nò0 & n+(k+1)ò0 by NAT_1:18;
then H8: n+1>0 & n+(k+1)+1>0 & (n+k+1)!<>0 & (n+k)!<>0
by NAT_1:38,NEWTON:23;
then 1/(n+1)>0 by REAL_2:149;
then H9: x>0 by H1;
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 REAL_2:152,H8;
then (n+(k+1)+1)"ó1/(n+1) by REAL_1:33;
then H10: (n+(k+1)+1)"óx by H1;
H11: (n!)/((n+k+1)!)>0 by T34;
(n+(k+1)+1)">0 by REAL_1:72,H8;
then H12: (n!)/((n+k+1)!)ù(n+(k+1)+1)"óx.^.(k+1)ùx
by REAL_2:197,H7,H10,H11;
x.^.(k+1)ùx = x.^.(k+1)ùx.^.1 by POWER:30
.= x.^.((k+1)+1) by POWER:32,H9;
then H13: (n!)/((n+k+1)!)ù(n+(k+1)+1)"óx.^.((k+1)+1) by H12;
(n!)/((n+(k+1)+1)!) = (n!)ù((n+(k+1)+1)!)" by REAL_1:16
.= (n!)ù((n+(k+1)+1)ù((n+(k+1))!))" by NEWTON:21
.= (n!)ù((n+(k+1)+1)ù((n+k+1)!))" by AXIOMS:13
.= (n!)ù((n+(k+1)+1)"ù((n+k+1)!)") by REAL_1:24,H8
.= (n!)ù((n+k+1)!)"ù(n+(k+1)+1)" by AXIOMS:16
.= (n!)/((n+k+1)!)ù(n+(k+1)+1)" by REAL_1:16;
hence (n!)/((n+(k+1)+1)!)óx.^.((k+1)+1) by H13;
end;
thus thesis from Ind(H2,H6);
end;
hence thesis;
end;
theorem T40:
n>0 & x=1/(n+1) implies n!ùä(eseq^\(n+1))óx/(1-x)
proof
assume H1: n>0 & x=1/(n+1);
n+1>0+1 by REAL_1:59,H1;
then 0<1/(n+1) & 1/(n+1)<1 by REAL_2:163;
then H2: 00 by NEWTON:23;
H10: (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 AXIOMS:13
.= n!ù(1/((n+k+1)!)) by Deseq
.= n!/((n+k+1)!) by REAL_2:56,H9;
hence (n!þ(eseq^\(n+1))).kò0 by T34;
seq.k=x.^.(k+1) by H3;
hence (n!þ(eseq^\(n+1))).kóseq.k by T39,H1,H10;
end;
then ä(n!þ(eseq^\(n+1)))óä(seq) by SERIES_1:24,H6;
then ä(n!þ(eseq^\(n+1)))óx/(1-x) by H7;
hence n!ùä(eseq^\(n+1))óx/(1-x) by SERIES_1:13,H8;
end;
theorem T41:
nò2 & x=1/(n+1) implies x/(1-x)<1
proof
assume H1: nò2 & x=1/(n+1);
nò0 by NAT_1:18;
then H2: n+1>0 by NAT_1:38;
then H3: x>0 by REAL_2:149,H1;
20 by AXIOMS:22,H1;
then n!ùä(eseq^\(n+1))óx/(1-x) by T40;
then n!ùä(eseq^\(n+1))<0+1 by AXIOMS:22,H4;
then H5: n!ùä(eseq^\(n+1))ó0 by INT_1:20,H3;
n!ùä(eseq^\(n+1))>0 by T36;
hence contradiction by H5;
end;