:: Irrationality of e :: by Freek Wiedijk :: :: Received July 2, 1999 :: Copyright (c) 1999-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, INT_1, SEQ_1, FINSEQ_1, RAT_1, ORDINAL4, POWER, INT_2, SQUARE_1, XXREAL_0, CARD_1, ARYTM_3, RELAT_1, NAT_1, FUNCT_1, ARYTM_1, REALSET1, SEQ_2, ORDINAL2, COMPLEX1, VALUED_1, SERIES_1, CARD_3, XBOOLE_0, RFINSEQ, PARTFUN1, FINSEQ_2, NEWTON, SIN_COS, IRRAT_1, REAL_1, ASYMPT_1; notations XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, INT_1, COMPLEX1, SQUARE_1, NAT_1, FUNCT_1, PARTFUN1, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, POWER, FINSEQ_1, RVSUM_1, SERIES_1, FINSEQ_2, RFINSEQ, SIN_COS, RAT_1, INT_2, PEPIN, NEWTON; constructors ARYTM_0, REAL_1, NAT_1, NAT_D, SEQ_2, PARTFUN1, RVSUM_1, LIMFUNC1, COMSEQ_3, RFINSEQ, BINARITH, SIN_COS, PEPIN, SERIES_1, POWER, RELSET_1, COMSEQ_2, SEQ_1, NUMBERS, FUNCOP_1; registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, NEWTON, XBOOLE_0, VALUED_0, VALUED_1, FUNCT_2, POWER, FINSEQ_1, SQUARE_1, RVSUM_1, SEQ_1, SEQ_2; 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; reserve seq, seq1, seq2 for Real_Sequence; reserve sq for FinSequence of REAL; notation let x be Real; antonym x is irrational for x is rational; end; notation let x, y be Real; synonym x ^ y for x to_power y; end; ::$N The Irrationality of the Square Root of 2 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 :: IRRAT_1:sch 1 LambdaRealSeq{F(set)->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 be Nat; func aseq(k) -> Real_Sequence means :: IRRAT_1:def 1 for n holds it.n=(n-k)/n; func bseq(k) -> Real_Sequence means :: IRRAT_1:def 2 for n holds it.n=(n choose k)*(n ^ (-k)); end; definition let n be Nat; 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 (n choose (k+1))=((n-k)/(k+1))*(n choose k); theorem :: IRRAT_1:6 n>0 implies bseq(k+1).n=(1/(k+1))*(bseq(k).n)*(aseq(k).n); theorem :: IRRAT_1:7 n>0 implies aseq(k).n=1-(k/n); theorem :: IRRAT_1:8 aseq(k) is convergent & lim(aseq(k))=1; theorem :: IRRAT_1:9 for seq st for n being Nat holds seq.n=x holds seq is convergent & lim(seq)=x ; theorem :: IRRAT_1:10 for n holds bseq(0).n=1; theorem :: IRRAT_1:11 (1/(k+1))*(1/(k!))=1/((k+1)!); theorem :: IRRAT_1:12 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:13 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 = Sum (k:(n choose k)*(n ^ (-k))) theorem :: IRRAT_1:15 for seq st seq^\1 is summable holds seq is summable & Sum(seq)=( seq.0)+Sum(seq^\1); theorem :: IRRAT_1:16 for D being non empty set, sq being FinSequence of D st 1<=k & k 0 holds Sum(sq)=(sq.1)+Sum(sq/^1); theorem :: IRRAT_1:18 for n holds for seq, sq st len(sq)=n & (for k st k=n holds seq.k=0) holds seq is summable & Sum(seq)=Sum (sq); theorem :: IRRAT_1:19 k<=n implies ((x,y) In_Power n).(k+1)=(n choose k)*(x ^ (n-k))*( y ^ k); theorem :: IRRAT_1:20 n>0 & k<=n implies cseq(n).k=((1,1/n) In_Power n).(k+1); theorem :: IRRAT_1:21 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:22 dseq is convergent & lim(dseq)=number_e; :: exp(1) = Sum (k:1/(k!)) theorem :: IRRAT_1:23 eseq is summable & Sum(eseq)=exp_R(1); :: lim(n:(1+(1/n)) ^ n) = Sum (k:1/(k!)) theorem :: IRRAT_1:24 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:25 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:26 (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:27 seq is summable implies for eps st eps>0 holds ex K st Partial_Sums(seq).K>Sum(seq)-eps; theorem :: IRRAT_1:28 n>=1 implies dseq.n<=Sum(eseq); theorem :: IRRAT_1:29 seq is summable & (for k holds seq.k>=0) implies Sum(seq)>= Partial_Sums(seq).K; theorem :: IRRAT_1:30 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_R(1); end; begin :: number_e is irrational theorem :: IRRAT_1:31 x is rational implies ex n st n>=2 & n!*x is integer; theorem :: IRRAT_1:32 n!*eseq.k = (n!)/(k!); theorem :: IRRAT_1:33 (n!)/(k!)>0; theorem :: IRRAT_1:34 seq is summable & (for n holds seq.n>0) implies Sum(seq)>0; theorem :: IRRAT_1:35 n!*Sum(eseq^\(n+1))>0; theorem :: IRRAT_1:36 k<=n implies (n!)/(k!) is integer; theorem :: IRRAT_1:37 n!*Partial_Sums(eseq).n is integer; theorem :: IRRAT_1:38 x=1/(n+1) implies (n!)/((n+k+1)!)<=x ^ (k+1); theorem :: IRRAT_1:39 n>0 & x=1/(n+1) implies n!*Sum(eseq^\(n+1))<=x/(1-x); theorem :: IRRAT_1:40 for n be Real st n>=2 & x=1/(n+1) holds x/(1-x)<1; ::$N Irrationality of e theorem :: IRRAT_1:41 number_e is irrational;