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 :: IRRAT_1:1 p is prime implies š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(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); 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 st y<>0 & z<>0 & v<>0 & w<>0 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 st n>0 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 k0 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 = ”(\k:(n choose k)˜(n.^.(-k))) theorem :: IRRAT_1:16 for seq st seq^\1 is summable holds seq is summable & ”(seq)=(seq.0)+”(seq^\1); theorem :: IRRAT_1:17 for sq st len(sq)=n & 1Ûk & k0 holds ”(sq)=(sq.1)+”(sq/^1); theorem :: IRRAT_1:19 for n holds for seq, sq st len(sq)=n & (for k st k0 & 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 & ”(cseq(n))=(1+(1/n)).^.n & ”(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) = ”(\k:1/(k!)) theorem :: IRRAT_1:24 eseq is summable & ”(eseq)=exp(1); :: lim(\n:(1+(1/n)).^.n) = ”(\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>”(seq)-eps; theorem :: IRRAT_1:29 nÚ1 implies dseq.nÛ”(eseq); theorem :: IRRAT_1:30 seq is summable & (for k holds seq.kÚ0) implies ”(seq)ÚPartial_Sums(seq).K; theorem :: IRRAT_1:31 dseq is convergent & lim(dseq)=”(eseq); :: number_e = exp(1) definition redefine func number_e equals :: IRRAT_1:def 6 ”(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 ”(seq)>0; theorem :: IRRAT_1:36 n!˜”(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!˜”(eseq^\(n+1))Ûx/(1-x); theorem :: IRRAT_1:41 nÚ2 & x=1/(n+1) implies x/(1-x)<1; theorem :: IRRAT_1:42 number_e is irrational;