:: IRRAT_1 semantic presentation begin notation let x be real number ; antonym irrational x for rational ; end; notation let x, y be real number ; synonym x ^ y for x to_power y; end; theorem Th1: :: IRRAT_1:1 for p being Element of NAT st p is prime holds sqrt p is irrational proof let p be Element of NAT ; ::_thesis: ( p is prime implies sqrt p is irrational ) assume A1: p is prime ; ::_thesis: sqrt p is irrational then A2: p > 1 by INT_2:def_4; assume sqrt p is rational ; ::_thesis: contradiction then consider i being Integer, n being Element of NAT such that A3: n <> 0 and A4: sqrt p = i / n and A5: for i1 being Integer for n1 being Element of NAT st n1 <> 0 & sqrt p = i1 / n1 holds n <= n1 by RAT_1:9; A6: i = (sqrt p) * n by A3, A4, XCMPLX_1:87; sqrt p >= 0 by SQUARE_1:def_2; then reconsider m = i as Element of NAT by A6, INT_1:3; A7: m ^2 = ((sqrt p) ^2) * (n ^2) by A6 .= p * (n ^2) by SQUARE_1:def_2 ; then p divides m ^2 by NAT_D:def_3; then p divides m by A1, NEWTON:80; then consider m1 being Nat such that A8: m = p * m1 by NAT_D:def_3; n ^2 = (p * (p * (m1 ^2))) / p by A2, A7, A8, XCMPLX_1:89 .= p * (m1 ^2) by A2, XCMPLX_1:89 ; then p divides n ^2 by NAT_D:def_3; then p divides n by A1, NEWTON:80; then consider n1 being Nat such that A9: n = p * n1 by NAT_D:def_3; A10: m1 / n1 = sqrt p by A2, A4, A8, A9, XCMPLX_1:91; A11: n1 <> 0 by A3, A9; then p * n1 > 1 * n1 by A2, XREAL_1:98; hence contradiction by A5, A9, A11, A10; ::_thesis: verum end; theorem :: IRRAT_1:2 ex x, y being real number st ( x is irrational & y is irrational & x ^ y is rational ) proof set w = sqrt 2; A1: ((sqrt 2) ^ (sqrt 2)) ^ (sqrt 2) = (sqrt 2) ^ ((sqrt 2) ^2) by POWER:33, SQUARE_1:19 .= (sqrt 2) ^ 2 by SQUARE_1:def_2 .= (sqrt 2) ^2 by POWER:46 .= 2 by SQUARE_1:def_2 ; percases ( (sqrt 2) ^ (sqrt 2) is rational or (sqrt 2) ^ (sqrt 2) is irrational ) ; supposeA2: (sqrt 2) ^ (sqrt 2) is rational ; ::_thesis: ex x, y being real number st ( x is irrational & y is irrational & x ^ y is rational ) take sqrt 2 ; ::_thesis: ex y being real number st ( sqrt 2 is irrational & y is irrational & (sqrt 2) ^ y is rational ) take sqrt 2 ; ::_thesis: ( sqrt 2 is irrational & sqrt 2 is irrational & (sqrt 2) ^ (sqrt 2) is rational ) thus ( sqrt 2 is irrational & sqrt 2 is irrational & (sqrt 2) ^ (sqrt 2) is rational ) by A2, Th1, INT_2:28; ::_thesis: verum end; supposeA3: (sqrt 2) ^ (sqrt 2) is irrational ; ::_thesis: ex x, y being real number st ( x is irrational & y is irrational & x ^ y is rational ) take (sqrt 2) ^ (sqrt 2) ; ::_thesis: ex y being real number st ( (sqrt 2) ^ (sqrt 2) is irrational & y is irrational & ((sqrt 2) ^ (sqrt 2)) ^ y is rational ) take sqrt 2 ; ::_thesis: ( (sqrt 2) ^ (sqrt 2) is irrational & sqrt 2 is irrational & ((sqrt 2) ^ (sqrt 2)) ^ (sqrt 2) is rational ) thus ( (sqrt 2) ^ (sqrt 2) is irrational & sqrt 2 is irrational & ((sqrt 2) ^ (sqrt 2)) ^ (sqrt 2) is rational ) by A1, A3, Th1, INT_2:28; ::_thesis: verum end; end; end; begin scheme :: IRRAT_1:sch 1 LambdaRealSeq{ F1( set ) -> real number } : ( ex seq being Real_Sequence st for n being Element of NAT holds seq . n = F1(n) & ( for seq1, seq2 being Real_Sequence st ( for n being Element of NAT holds seq1 . n = F1(n) ) & ( for n being Element of NAT holds seq2 . n = F1(n) ) holds seq1 = seq2 ) ) proof thus ex seq being Real_Sequence st for n being Element of NAT holds seq . n = F1(n) from SEQ_1:sch_1(); ::_thesis: for seq1, seq2 being Real_Sequence st ( for n being Element of NAT holds seq1 . n = F1(n) ) & ( for n being Element of NAT holds seq2 . n = F1(n) ) holds seq1 = seq2 let seq1, seq2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq1 . n = F1(n) ) & ( for n being Element of NAT holds seq2 . n = F1(n) ) implies seq1 = seq2 ) assume A1: for n being Element of NAT holds seq1 . n = F1(n) ; ::_thesis: ( ex n being Element of NAT st not seq2 . n = F1(n) or seq1 = seq2 ) assume A2: for n being Element of NAT holds seq2 . n = F1(n) ; ::_thesis: seq1 = seq2 now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_=_seq2_._n let n be Element of NAT ; ::_thesis: seq1 . n = seq2 . n thus seq1 . n = F1(n) by A1 .= seq2 . n by A2 ; ::_thesis: verum end; hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; definition let k be Nat; func aseq k -> Real_Sequence means :Def1: :: IRRAT_1:def 1 for n being Element of NAT holds it . n = (n - k) / n; correctness existence ex b1 being Real_Sequence st for n being Element of NAT holds b1 . n = (n - k) / n; uniqueness for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = (n - k) / n ) & ( for n being Element of NAT holds b2 . n = (n - k) / n ) holds b1 = b2; proof deffunc H1( Element of NAT ) -> Element of COMPLEX = (\$1 - k) / \$1; thus ( ex seq being Real_Sequence st for n being Element of NAT holds seq . n = H1(n) & ( for seq1, seq2 being Real_Sequence st ( for n being Element of NAT holds seq1 . n = H1(n) ) & ( for n being Element of NAT holds seq2 . n = H1(n) ) holds seq1 = seq2 ) ) from IRRAT_1:sch_1(); ::_thesis: verum end; func bseq k -> Real_Sequence means :Def2: :: IRRAT_1:def 2 for n being Element of NAT holds it . n = (n choose k) * (n ^ (- k)); correctness existence ex b1 being Real_Sequence st for n being Element of NAT holds b1 . n = (n choose k) * (n ^ (- k)); uniqueness for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = (n choose k) * (n ^ (- k)) ) & ( for n being Element of NAT holds b2 . n = (n choose k) * (n ^ (- k)) ) holds b1 = b2; proof deffunc H1( Element of NAT ) -> set = (\$1 choose k) * (\$1 ^ (- k)); thus ( ex seq being Real_Sequence st for n being Element of NAT holds seq . n = H1(n) & ( for seq1, seq2 being Real_Sequence st ( for n being Element of NAT holds seq1 . n = H1(n) ) & ( for n being Element of NAT holds seq2 . n = H1(n) ) holds seq1 = seq2 ) ) from IRRAT_1:sch_1(); ::_thesis: verum end; end; :: deftheorem Def1 defines aseq IRRAT_1:def_1_:_ for k being Nat for b2 being Real_Sequence holds ( b2 = aseq k iff for n being Element of NAT holds b2 . n = (n - k) / n ); :: deftheorem Def2 defines bseq IRRAT_1:def_2_:_ for k being Nat for b2 being Real_Sequence holds ( b2 = bseq k iff for n being Element of NAT holds b2 . n = (n choose k) * (n ^ (- k)) ); definition let n be Nat; func cseq n -> Real_Sequence means :Def3: :: IRRAT_1:def 3 for k being Element of NAT holds it . k = (n choose k) * (n ^ (- k)); correctness existence ex b1 being Real_Sequence st for k being Element of NAT holds b1 . k = (n choose k) * (n ^ (- k)); uniqueness for b1, b2 being Real_Sequence st ( for k being Element of NAT holds b1 . k = (n choose k) * (n ^ (- k)) ) & ( for k being Element of NAT holds b2 . k = (n choose k) * (n ^ (- k)) ) holds b1 = b2; proof deffunc H1( Element of NAT ) -> set = (n choose \$1) * (n ^ (- \$1)); thus ( ex seq being Real_Sequence st for n being Element of NAT holds seq . n = H1(n) & ( for seq1, seq2 being Real_Sequence st ( for n being Element of NAT holds seq1 . n = H1(n) ) & ( for n being Element of NAT holds seq2 . n = H1(n) ) holds seq1 = seq2 ) ) from IRRAT_1:sch_1(); ::_thesis: verum end; end; :: deftheorem Def3 defines cseq IRRAT_1:def_3_:_ for n being Nat for b2 being Real_Sequence holds ( b2 = cseq n iff for k being Element of NAT holds b2 . k = (n choose k) * (n ^ (- k)) ); theorem Th3: :: IRRAT_1:3 for n, k being Element of NAT holds (cseq n) . k = (bseq k) . n proof let n, k be Element of NAT ; ::_thesis: (cseq n) . k = (bseq k) . n thus (cseq n) . k = (n choose k) * (n ^ (- k)) by Def3 .= (bseq k) . n by Def2 ; ::_thesis: verum end; definition func dseq -> Real_Sequence means :Def4: :: IRRAT_1:def 4 for n being Element of NAT holds it . n = (1 + (1 / n)) ^ n; correctness existence ex b1 being Real_Sequence st for n being Element of NAT holds b1 . n = (1 + (1 / n)) ^ n; uniqueness for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = (1 + (1 / n)) ^ n ) & ( for n being Element of NAT holds b2 . n = (1 + (1 / n)) ^ n ) holds b1 = b2; proof deffunc H1( Element of NAT ) -> set = (1 + (1 / \$1)) ^ \$1; thus ( ex seq being Real_Sequence st for n being Element of NAT holds seq . n = H1(n) & ( for seq1, seq2 being Real_Sequence st ( for n being Element of NAT holds seq1 . n = H1(n) ) & ( for n being Element of NAT holds seq2 . n = H1(n) ) holds seq1 = seq2 ) ) from IRRAT_1:sch_1(); ::_thesis: verum end; end; :: deftheorem Def4 defines dseq IRRAT_1:def_4_:_ for b1 being Real_Sequence holds ( b1 = dseq iff for n being Element of NAT holds b1 . n = (1 + (1 / n)) ^ n ); definition func eseq -> Real_Sequence means :Def5: :: IRRAT_1:def 5 for k being Element of NAT holds it . k = 1 / (k !); correctness existence ex b1 being Real_Sequence st for k being Element of NAT holds b1 . k = 1 / (k !); uniqueness for b1, b2 being Real_Sequence st ( for k being Element of NAT holds b1 . k = 1 / (k !) ) & ( for k being Element of NAT holds b2 . k = 1 / (k !) ) holds b1 = b2; proof deffunc H1( Element of NAT ) -> Element of COMPLEX = 1 / (\$1 !); thus ( ex seq being Real_Sequence st for n being Element of NAT holds seq . n = H1(n) & ( for seq1, seq2 being Real_Sequence st ( for n being Element of NAT holds seq1 . n = H1(n) ) & ( for n being Element of NAT holds seq2 . n = H1(n) ) holds seq1 = seq2 ) ) from IRRAT_1:sch_1(); ::_thesis: verum end; end; :: deftheorem Def5 defines eseq IRRAT_1:def_5_:_ for b1 being Real_Sequence holds ( b1 = eseq iff for k being Element of NAT holds b1 . k = 1 / (k !) ); theorem Th4: :: IRRAT_1:4 for n, k being Element of NAT st n > 0 holds n ^ (- (k + 1)) = (n ^ (- k)) / n proof let n, k be Element of NAT ; ::_thesis: ( n > 0 implies n ^ (- (k + 1)) = (n ^ (- k)) / n ) assume A1: n > 0 ; ::_thesis: n ^ (- (k + 1)) = (n ^ (- k)) / n thus n ^ (- (k + 1)) = n ^ ((- k) - 1) .= (n ^ (- k)) / (n ^ 1) by A1, POWER:29 .= (n ^ (- k)) / n by POWER:25 ; ::_thesis: verum end; theorem Th5: :: IRRAT_1:5 for n, k being Element of NAT holds n choose (k + 1) = ((n - k) / (k + 1)) * (n choose k) proof let n, k be Element of NAT ; ::_thesis: n choose (k + 1) = ((n - k) / (k + 1)) * (n choose k) percases ( k + 1 <= n or ( k + 1 > n & k <= n ) or ( k + 1 > n & k > n ) ) ; supposeA1: k + 1 <= n ; ::_thesis: n choose (k + 1) = ((n - k) / (k + 1)) * (n choose k) then reconsider l = n - (k + 1) as Element of NAT by INT_1:5; l + 1 = n - k ; then reconsider l1 = n - k as Element of NAT ; k <= k + 1 by NAT_1:11; then A2: k <= n by A1, XXREAL_0:2; thus n choose (k + 1) = (n !) / (((k + 1) !) * (l !)) by A1, NEWTON:def_3 .= (n !) / (((k !) * (k + 1)) * (l !)) by NEWTON:15 .= (n !) / (((k !) * (k + 1)) * (((l !) * (l + 1)) / (l + 1))) by XCMPLX_1:89 .= (n !) / (((k !) * (k + 1)) * (((l + 1) !) / (l + 1))) by NEWTON:15 .= (l1 / (k + 1)) * ((n !) / ((k !) * (l1 !))) by XCMPLX_1:233 .= ((n - k) / (k + 1)) * (n choose k) by A2, NEWTON:def_3 ; ::_thesis: verum end; supposeA3: ( k + 1 > n & k <= n ) ; ::_thesis: n choose (k + 1) = ((n - k) / (k + 1)) * (n choose k) then k >= n by NAT_1:13; then k = n by A3, XXREAL_0:1; hence n choose (k + 1) = ((n - k) / (k + 1)) * (n choose k) by A3, NEWTON:def_3; ::_thesis: verum end; supposeA4: ( k + 1 > n & k > n ) ; ::_thesis: n choose (k + 1) = ((n - k) / (k + 1)) * (n choose k) hence n choose (k + 1) = ((n - k) / (k + 1)) * 0 by NEWTON:def_3 .= ((n - k) / (k + 1)) * (n choose k) by A4, NEWTON:def_3 ; ::_thesis: verum end; end; end; theorem Th6: :: IRRAT_1:6 for n, k being Element of NAT st n > 0 holds (bseq (k + 1)) . n = ((1 / (k + 1)) * ((bseq k) . n)) * ((aseq k) . n) proof let n, k be Element of NAT ; ::_thesis: ( n > 0 implies (bseq (k + 1)) . n = ((1 / (k + 1)) * ((bseq k) . n)) * ((aseq k) . n) ) assume A1: n > 0 ; ::_thesis: (bseq (k + 1)) . n = ((1 / (k + 1)) * ((bseq k) . n)) * ((aseq k) . n) 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 Th5 .= (((n - k) / (k + 1)) * (n choose k)) * ((n ^ (- k)) / n) by A1, Th4 .= (((n - k) * ((k + 1) ")) * (n choose k)) * ((n ^ (- k)) / n) .= (((n - k) * ((k + 1) ")) * (n choose k)) * ((n ^ (- k)) * (n ")) .= (((k + 1) ") * ((n choose k) * (n ^ (- k)))) * ((n - k) * (n ")) .= ((1 / (k + 1)) * ((n choose k) * (n ^ (- k)))) * ((n - k) * (n ")) .= ((1 / (k + 1)) * ((n choose k) * (n ^ (- k)))) * ((n - k) / n) .= ((1 / (k + 1)) * ((bseq k) . n)) * ((n - k) / n) by Def2 .= ((1 / (k + 1)) * ((bseq k) . n)) * ((aseq k) . n) by Def1 ; ::_thesis: verum end; theorem Th7: :: IRRAT_1:7 for n, k being Element of NAT st n > 0 holds (aseq k) . n = 1 - (k / n) proof let n, k be Element of NAT ; ::_thesis: ( n > 0 implies (aseq k) . n = 1 - (k / n) ) assume A1: n > 0 ; ::_thesis: (aseq k) . n = 1 - (k / n) thus (aseq k) . n = (n - k) / n by Def1 .= (n / n) - (k / n) .= 1 - (k / n) by A1, XCMPLX_1:60 ; ::_thesis: verum end; theorem Th8: :: IRRAT_1:8 for k being Element of NAT holds ( aseq k is convergent & lim (aseq k) = 1 ) proof let k be Element of NAT ; ::_thesis: ( aseq k is convergent & lim (aseq k) = 1 ) A1: for eps being real number st 0 < eps holds ex N being Element of NAT st for n being Element of NAT st N <= n holds abs (((aseq k) . n) - 1) < eps proof let eps be real number ; ::_thesis: ( 0 < eps implies ex N being Element of NAT st for n being Element of NAT st N <= n holds abs (((aseq k) . n) - 1) < eps ) assume A2: eps > 0 ; ::_thesis: ex N being Element of NAT st for n being Element of NAT st N <= n holds abs (((aseq k) . n) - 1) < eps consider N being Element of NAT such that A3: N > k / eps by SEQ_4:3; take N ; ::_thesis: for n being Element of NAT st N <= n holds abs (((aseq k) . n) - 1) < eps let n be Element of NAT ; ::_thesis: ( N <= n implies abs (((aseq k) . n) - 1) < eps ) assume A4: n >= N ; ::_thesis: abs (((aseq k) . n) - 1) < eps then n > k / eps by A3, XXREAL_0:2; then (k / eps) * eps < n * eps by A2, XREAL_1:68; then A5: k < n * eps by A2, XCMPLX_1:87; A6: n > 0 by A2, A3, A4; then abs (((aseq k) . n) - 1) = abs ((1 - (k / n)) - 1) by Th7 .= abs (- (k / n)) .= abs (k / n) by COMPLEX1:52 .= k / n by ABSVALUE:def_1 ; hence abs (((aseq k) . n) - 1) < eps by A6, A5, XREAL_1:83; ::_thesis: verum end; thus aseq k is convergent ::_thesis: lim (aseq k) = 1 proof take 1 ; :: according to SEQ_2:def_6 ::_thesis: for b1 being set holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= abs K56(((aseq k) . b3),1) ) ) thus for b1 being set holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= abs K56(((aseq k) . b3),1) ) ) by A1; ::_thesis: verum end; hence lim (aseq k) = 1 by A1, SEQ_2:def_7; ::_thesis: verum end; theorem Th9: :: IRRAT_1:9 for x being real number for seq being Real_Sequence st ( for n being Nat holds seq . n = x ) holds ( seq is convergent & lim seq = x ) proof let x be real number ; ::_thesis: for seq being Real_Sequence st ( for n being Nat holds seq . n = x ) holds ( seq is convergent & lim seq = x ) let seq be Real_Sequence; ::_thesis: ( ( for n being Nat holds seq . n = x ) implies ( seq is convergent & lim seq = x ) ) assume A1: for n being Nat holds seq . n = x ; ::_thesis: ( seq is convergent & lim seq = x ) x in REAL by XREAL_0:def_1; then A2: seq is constant by A1, VALUED_0:def_18; hence seq is convergent ; ::_thesis: lim seq = x thus lim seq = seq . 0 by A2, SEQ_4:26 .= x by A1 ; ::_thesis: verum end; theorem Th10: :: IRRAT_1:10 for n being Element of NAT holds (bseq 0) . n = 1 proof let n be Element of NAT ; ::_thesis: (bseq 0) . n = 1 thus (bseq 0) . n = (n choose 0) * (n ^ (- 0)) by Def2 .= 1 * (n ^ (- 0)) by NEWTON:19 .= 1 by POWER:24 ; ::_thesis: verum end; theorem Th11: :: IRRAT_1:11 for k being Element of NAT holds (1 / (k + 1)) * (1 / (k !)) = 1 / ((k + 1) !) proof let k be Element of NAT ; ::_thesis: (1 / (k + 1)) * (1 / (k !)) = 1 / ((k + 1) !) thus (1 / (k + 1)) * (1 / (k !)) = 1 / ((k + 1) * (k !)) by XCMPLX_1:102 .= 1 / ((k + 1) !) by NEWTON:15 ; ::_thesis: verum end; theorem Th12: :: IRRAT_1:12 for k being Element of NAT holds ( bseq k is convergent & lim (bseq k) = 1 / (k !) & lim (bseq k) = eseq . k ) proof let k be Element of NAT ; ::_thesis: ( bseq k is convergent & lim (bseq k) = 1 / (k !) & lim (bseq k) = eseq . k ) defpred S1[ Nat] means ( bseq \$1 is convergent & lim (bseq \$1) = 1 / (\$1 !) ); A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof deffunc H1( Element of NAT ) -> set = (1 / (k + 1)) * ((bseq k) . \$1); consider seq being Real_Sequence such that A3: for n being Element of NAT holds seq . n = H1(n) from SEQ_1:sch_1(); deffunc H2( Element of NAT ) -> set = (seq . \$1) * ((aseq k) . \$1); consider seq1 being Real_Sequence such that A4: for n being Element of NAT holds seq1 . n = H2(n) from SEQ_1:sch_1(); A5: for n being Element of NAT st n >= 1 holds (bseq (k + 1)) . n = seq1 . n proof let n be Element of NAT ; ::_thesis: ( n >= 1 implies (bseq (k + 1)) . n = seq1 . n ) assume n >= 1 ; ::_thesis: (bseq (k + 1)) . n = seq1 . n hence (bseq (k + 1)) . n = ((1 / (k + 1)) * ((bseq k) . n)) * ((aseq k) . n) by Th6 .= (seq . n) * ((aseq k) . n) by A3 .= seq1 . n by A4 ; ::_thesis: verum end; A6: seq = (1 / (k + 1)) (#) (bseq k) by A3, SEQ_1:9; then A7: seq is convergent by A2, SEQ_2:7; A8: lim seq = (1 / (k + 1)) * (1 / (k !)) by A2, A6, SEQ_2:8 .= 1 / ((k + 1) !) by Th11 ; A9: aseq k is convergent by Th8; A10: seq1 = seq (#) (aseq k) by A4, SEQ_1:8; then A11: seq1 is convergent by A7, A9, SEQ_2:14; hence bseq (k + 1) is convergent by A5, SEQ_4:18; ::_thesis: lim (bseq (k + 1)) = 1 / ((k + 1) !) lim seq1 = (lim seq) * (lim (aseq k)) by A7, A10, A9, SEQ_2:15 .= 1 / ((k + 1) !) by A8, Th8 ; hence lim (bseq (k + 1)) = 1 / ((k + 1) !) by A11, A5, SEQ_4:19; ::_thesis: verum end; end; A12: S1[ 0 ] proof reconsider bseq0 = NAT --> 1 as Real_Sequence by FUNCOP_1:45; A13: for n being Nat holds bseq0 . n = 1 proof let n be Nat; ::_thesis: bseq0 . n = 1 n in NAT by ORDINAL1:def_12; hence bseq0 . n = 1 by FUNCOP_1:7; ::_thesis: verum end; then A14: bseq0 is convergent by Th9; A15: for n being Element of NAT st n >= 1 holds (bseq 0) . n = bseq0 . n proof let n be Element of NAT ; ::_thesis: ( n >= 1 implies (bseq 0) . n = bseq0 . n ) assume n >= 1 ; ::_thesis: (bseq 0) . n = bseq0 . n thus (bseq 0) . n = 1 by Th10 .= bseq0 . n by FUNCOP_1:7 ; ::_thesis: verum end; hence bseq 0 is convergent by A14, SEQ_4:18; ::_thesis: lim (bseq 0) = 1 / (0 !) lim bseq0 = 1 by A13, Th9; hence lim (bseq 0) = 1 / (0 !) by A14, A15, NEWTON:12, SEQ_4:19; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A12, A1); hence ( bseq k is convergent & lim (bseq k) = 1 / (k !) ) ; ::_thesis: lim (bseq k) = eseq . k hence lim (bseq k) = eseq . k by Def5; ::_thesis: verum end; theorem Th13: :: IRRAT_1:13 for k, n being Element of NAT st k < n holds ( 0 < (aseq k) . n & (aseq k) . n <= 1 ) proof let k, n be Element of NAT ; ::_thesis: ( k < n implies ( 0 < (aseq k) . n & (aseq k) . n <= 1 ) ) A1: (aseq k) . n = (n - k) / n by Def1; assume A2: k < n ; ::_thesis: ( 0 < (aseq k) . n & (aseq k) . n <= 1 ) then n - k > 0 by XREAL_1:50; hence (aseq k) . n > 0 by A2, A1, XREAL_1:139; ::_thesis: (aseq k) . n <= 1 1 - (k / n) <= 1 - 0 by XREAL_1:6; hence (aseq k) . n <= 1 by A2, Th7; ::_thesis: verum end; theorem Th14: :: IRRAT_1:14 for n, k being Element of NAT st n > 0 holds ( 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 let n, k be Element of NAT ; ::_thesis: ( 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 ) ) defpred S1[ Element of NAT ] means (bseq \$1) . n <= 1 / (\$1 !); assume A1: n > 0 ; ::_thesis: ( 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 ) then A2: n ^ (- k) > 0 by POWER:34; A3: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof percases ( k < n or k >= n ) ; supposeA5: k < n ; ::_thesis: S1[k + 1] (1 / (k + 1)) * ((bseq k) . n) <= (1 / (k + 1)) * (1 / (k !)) by A4, XREAL_1:64; then A6: (1 / (k + 1)) * ((bseq k) . n) <= 1 / ((k + 1) !) by Th11; (aseq k) . n >= 0 by A5, Th13; then A7: ((1 / (k + 1)) * ((bseq k) . n)) * ((aseq k) . n) <= (1 / ((k + 1) !)) * ((aseq k) . n) by A6, XREAL_1:64; (aseq k) . n <= 1 by A5, Th13; then A8: (1 / ((k + 1) !)) * ((aseq k) . n) <= 1 / ((k + 1) !) by XREAL_1:153; (bseq (k + 1)) . n = ((1 / (k + 1)) * ((bseq k) . n)) * ((aseq k) . n) by A1, Th6; hence S1[k + 1] by A7, A8, XXREAL_0:2; ::_thesis: verum end; suppose k >= n ; ::_thesis: S1[k + 1] then A9: k + 1 > n by NAT_1:13; (bseq (k + 1)) . n = (n choose (k + 1)) * (n ^ (- (k + 1))) by Def2 .= 0 * (n ^ (- (k + 1))) by A9, NEWTON:def_3 .= 0 ; hence S1[k + 1] ; ::_thesis: verum end; end; end; end; A10: (bseq k) . n = (n choose k) * (n ^ (- k)) by Def2; hence 0 <= (bseq k) . n by A2; ::_thesis: ( (bseq k) . n <= 1 / (k !) & (bseq k) . n <= eseq . k & 0 <= (cseq n) . k & (cseq n) . k <= 1 / (k !) & (cseq n) . k <= eseq . k ) A11: S1[ 0 ] by Th10, NEWTON:12; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A11, A3); hence A12: (bseq k) . n <= 1 / (k !) ; ::_thesis: ( (bseq k) . n <= eseq . k & 0 <= (cseq n) . k & (cseq n) . k <= 1 / (k !) & (cseq n) . k <= eseq . k ) hence (bseq k) . n <= eseq . k by Def5; ::_thesis: ( 0 <= (cseq n) . k & (cseq n) . k <= 1 / (k !) & (cseq n) . k <= eseq . k ) hence ( 0 <= (cseq n) . k & (cseq n) . k <= 1 / (k !) & (cseq n) . k <= eseq . k ) by A10, A2, A12, Th3; ::_thesis: verum end; theorem Th15: :: IRRAT_1:15 for seq being Real_Sequence st seq ^\ 1 is summable holds ( seq is summable & Sum seq = (seq . 0) + (Sum (seq ^\ 1)) ) proof let seq be Real_Sequence; ::_thesis: ( seq ^\ 1 is summable implies ( seq is summable & Sum seq = (seq . 0) + (Sum (seq ^\ 1)) ) ) assume A1: seq ^\ 1 is summable ; ::_thesis: ( seq is summable & Sum seq = (seq . 0) + (Sum (seq ^\ 1)) ) hence seq is summable by SERIES_1:13; ::_thesis: Sum seq = (seq . 0) + (Sum (seq ^\ 1)) thus Sum seq = ((Partial_Sums seq) . 0) + (Sum (seq ^\ (1 + 0))) by A1, SERIES_1:13, SERIES_1:15 .= (seq . 0) + (Sum (seq ^\ 1)) by SERIES_1:def_1 ; ::_thesis: verum end; theorem Th16: :: IRRAT_1:16 for k being Element of NAT for D being non empty set for sq being FinSequence of D st 1 <= k & k < len sq holds (sq /^ 1) . k = sq . (k + 1) proof let k be Element of NAT ; ::_thesis: for D being non empty set for sq being FinSequence of D st 1 <= k & k < len sq holds (sq /^ 1) . k = sq . (k + 1) let D be non empty set ; ::_thesis: for sq being FinSequence of D st 1 <= k & k < len sq holds (sq /^ 1) . k = sq . (k + 1) let sq be FinSequence of D; ::_thesis: ( 1 <= k & k < len sq implies (sq /^ 1) . k = sq . (k + 1) ) assume that A1: 1 <= k and A2: k < len sq ; ::_thesis: (sq /^ 1) . k = sq . (k + 1) A3: len sq = ((len sq) - 1) + 1 ; k + 1 <= len sq by A2, NAT_1:13; then A4: k <= (len sq) - 1 by A3, XREAL_1:6; A5: len sq >= 1 by A1, A2, XXREAL_0:2; then len (sq /^ 1) = (len sq) - 1 by RFINSEQ:def_1; then k in dom (sq /^ 1) by A1, A4, FINSEQ_3:25; hence (sq /^ 1) . k = sq . (k + 1) by A5, RFINSEQ:def_1; ::_thesis: verum end; theorem Th17: :: IRRAT_1:17 for sq being FinSequence of REAL st len sq > 0 holds Sum sq = (sq . 1) + (Sum (sq /^ 1)) proof let sq be FinSequence of REAL ; ::_thesis: ( len sq > 0 implies Sum sq = (sq . 1) + (Sum (sq /^ 1)) ) assume A1: len sq > 0 ; ::_thesis: Sum sq = (sq . 1) + (Sum (sq /^ 1)) then 0 + 1 <= len sq by NAT_1:13; then A2: 1 in dom sq by FINSEQ_3:25; thus Sum sq = Sum (<*(sq /. 1)*> ^ (sq /^ 1)) by A1, CARD_1:27, FINSEQ_5:29 .= Sum (<*(sq . 1)*> ^ (sq /^ 1)) by A2, PARTFUN1:def_6 .= (sq . 1) + (Sum (sq /^ 1)) by RVSUM_1:76 ; ::_thesis: verum end; theorem Th18: :: IRRAT_1:18 for n being Element of NAT for seq being Real_Sequence for sq being FinSequence of REAL st len sq = n & ( for k being Element of NAT st k < n holds seq . k = sq . (k + 1) ) & ( for k being Element of NAT st k >= n holds seq . k = 0 ) holds ( seq is summable & Sum seq = Sum sq ) proof defpred S1[ Element of NAT ] means for seq being Real_Sequence for sq being FinSequence of REAL st len sq = \$1 & ( for k being Element of NAT st k < \$1 holds seq . k = sq . (k + 1) ) & ( for k being Element of NAT st k >= \$1 holds seq . k = 0 ) holds ( seq is summable & Sum seq = Sum sq ); now__::_thesis:_for_n_being_Element_of_NAT_st_(_for_seq_being_Real_Sequence for_sq_being_FinSequence_of_REAL_st_len_sq_=_n_&_(_for_k_being_Element_of_NAT_st_k_<_n_holds_ seq_._k_=_sq_._(k_+_1)_)_&_(_for_k_being_Element_of_NAT_st_k_>=_n_holds_ seq_._k_=_0_)_holds_ (_seq_is_summable_&_Sum_seq_=_Sum_sq_)_)_holds_ for_seq_being_Real_Sequence for_sq_being_FinSequence_of_REAL_st_len_sq_=_n_+_1_&_(_for_k_being_Element_of_NAT_st_k_<_n_+_1_holds_ seq_._k_=_sq_._(k_+_1)_)_&_(_for_k_being_Element_of_NAT_st_k_>=_n_+_1_holds_ seq_._k_=_0_)_holds_ (_seq_is_summable_&_Sum_seq_=_Sum_sq_) let n be Element of NAT ; ::_thesis: ( ( for seq being Real_Sequence for sq being FinSequence of REAL st len sq = n & ( for k being Element of NAT st k < n holds seq . k = sq . (k + 1) ) & ( for k being Element of NAT st k >= n holds seq . k = 0 ) holds ( seq is summable & Sum seq = Sum sq ) ) implies for seq being Real_Sequence for sq being FinSequence of REAL st len sq = n + 1 & ( for k being Element of NAT st k < n + 1 holds seq . k = sq . (k + 1) ) & ( for k being Element of NAT st k >= n + 1 holds seq . k = 0 ) holds ( seq is summable & Sum seq = Sum sq ) ) assume A1: for seq being Real_Sequence for sq being FinSequence of REAL st len sq = n & ( for k being Element of NAT st k < n holds seq . k = sq . (k + 1) ) & ( for k being Element of NAT st k >= n holds seq . k = 0 ) holds ( seq is summable & Sum seq = Sum sq ) ; ::_thesis: for seq being Real_Sequence for sq being FinSequence of REAL st len sq = n + 1 & ( for k being Element of NAT st k < n + 1 holds seq . k = sq . (k + 1) ) & ( for k being Element of NAT st k >= n + 1 holds seq . k = 0 ) holds ( seq is summable & Sum seq = Sum sq ) let seq be Real_Sequence; ::_thesis: for sq being FinSequence of REAL st len sq = n + 1 & ( for k being Element of NAT st k < n + 1 holds seq . k = sq . (k + 1) ) & ( for k being Element of NAT st k >= n + 1 holds seq . k = 0 ) holds ( seq is summable & Sum seq = Sum sq ) let sq be FinSequence of REAL ; ::_thesis: ( len sq = n + 1 & ( for k being Element of NAT st k < n + 1 holds seq . k = sq . (k + 1) ) & ( for k being Element of NAT st k >= n + 1 holds seq . k = 0 ) implies ( seq is summable & Sum seq = Sum sq ) ) assume that A2: len sq = n + 1 and A3: for k being Element of NAT st k < n + 1 holds seq . k = sq . (k + 1) and A4: for k being Element of NAT st k >= n + 1 holds seq . k = 0 ; ::_thesis: ( seq is summable & Sum seq = Sum sq ) A5: now__::_thesis:_for_k_being_Element_of_NAT_st_k_<_n_holds_ (seq_^\_1)_._k_=_(sq_/^_1)_._(k_+_1) let k be Element of NAT ; ::_thesis: ( k < n implies (seq ^\ 1) . k = (sq /^ 1) . (k + 1) ) A6: k + 1 >= 0 + 1 by XREAL_1:6; assume k < n ; ::_thesis: (seq ^\ 1) . k = (sq /^ 1) . (k + 1) then A7: k + 1 < n + 1 by XREAL_1:6; thus (seq ^\ 1) . k = seq . (k + 1) by NAT_1:def_3 .= sq . ((k + 1) + 1) by A3, A7 .= (sq /^ 1) . (k + 1) by A2, A7, A6, Th16 ; ::_thesis: verum end; A8: now__::_thesis:_for_k_being_Element_of_NAT_st_k_>=_n_holds_ (seq_^\_1)_._k_=_0 let k be Element of NAT ; ::_thesis: ( k >= n implies (seq ^\ 1) . k = 0 ) assume k >= n ; ::_thesis: (seq ^\ 1) . k = 0 then A9: k + 1 >= n + 1 by XREAL_1:6; thus (seq ^\ 1) . k = seq . (k + 1) by NAT_1:def_3 .= 0 by A4, A9 ; ::_thesis: verum end; n + 1 >= 0 + 1 by XREAL_1:6; then A10: len (sq /^ 1) = (len sq) - 1 by A2, RFINSEQ:def_1 .= n by A2 ; then A11: Sum (seq ^\ 1) = Sum (sq /^ 1) by A1, A5, A8; A12: seq ^\ 1 is summable by A1, A10, A5, A8; hence seq is summable by Th15; ::_thesis: Sum seq = Sum sq thus Sum seq = (seq . 0) + (Sum (seq ^\ 1)) by A12, Th15 .= (sq . (0 + 1)) + (Sum (seq ^\ 1)) by A3 .= Sum sq by A2, A11, Th17 ; ::_thesis: verum end; then A13: for k being Element of NAT st S1[k] holds S1[k + 1] ; now__::_thesis:_for_seq_being_Real_Sequence for_sq_being_FinSequence_of_REAL_st_len_sq_=_0_&_(_for_k_being_Element_of_NAT_st_k_<_0_holds_ seq_._k_=_sq_._(k_+_1)_)_&_(_for_k_being_Element_of_NAT_st_k_>=_0_holds_ seq_._k_=_0_)_holds_ (_seq_is_summable_&_Sum_seq_=_Sum_sq_) let seq be Real_Sequence; ::_thesis: for sq being FinSequence of REAL st len sq = 0 & ( for k being Element of NAT st k < 0 holds seq . k = sq . (k + 1) ) & ( for k being Element of NAT st k >= 0 holds seq . k = 0 ) holds ( seq is summable & Sum seq = Sum sq ) let sq be FinSequence of REAL ; ::_thesis: ( len sq = 0 & ( for k being Element of NAT st k < 0 holds seq . k = sq . (k + 1) ) & ( for k being Element of NAT st k >= 0 holds seq . k = 0 ) implies ( seq is summable & Sum seq = Sum sq ) ) assume that A14: len sq = 0 and for k being Element of NAT st k < 0 holds seq . k = sq . (k + 1) and A15: for k being Element of NAT st k >= 0 holds seq . k = 0 ; ::_thesis: ( seq is summable & Sum seq = Sum sq ) sq is Element of 0 -tuples_on REAL by A14, FINSEQ_2:92; then A16: Sum sq = 0 by RVSUM_1:79; defpred S2[ Nat] means (Partial_Sums seq) . \$1 = 0 ; A17: now__::_thesis:_for_k_being_Nat_st_S2[k]_holds_ S2[k_+_1] let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] ) k in NAT by ORDINAL1:def_12; then A18: (Partial_Sums seq) . (k + 1) = ((Partial_Sums seq) . k) + (seq . (k + 1)) by SERIES_1:def_1; assume S2[k] ; ::_thesis: S2[k + 1] hence S2[k + 1] by A15, A18; ::_thesis: verum end; seq . 0 = 0 by A15; then A19: S2[ 0 ] by SERIES_1:def_1; A20: for k being Nat holds S2[k] from NAT_1:sch_2(A19, A17); then Partial_Sums seq is convergent by Th9; hence seq is summable by SERIES_1:def_2; ::_thesis: Sum seq = Sum sq lim (Partial_Sums seq) = 0 by A20, Th9; hence Sum seq = Sum sq by A16, SERIES_1:def_3; ::_thesis: verum end; then A21: S1[ 0 ] ; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A21, A13); ::_thesis: verum end; theorem Th19: :: IRRAT_1:19 for k, n being Element of NAT for x, y being real number st k <= n holds ((x,y) In_Power n) . (k + 1) = ((n choose k) * (x ^ (n - k))) * (y ^ k) proof let k, n be Element of NAT ; ::_thesis: for x, y being real number st k <= n holds ((x,y) In_Power n) . (k + 1) = ((n choose k) * (x ^ (n - k))) * (y ^ k) let x, y be real number ; ::_thesis: ( k <= n implies ((x,y) In_Power n) . (k + 1) = ((n choose k) * (x ^ (n - k))) * (y ^ k) ) reconsider i1 = (k + 1) - 1 as Element of NAT ; A1: ( k + 1 >= 0 + 1 & len ((x,y) In_Power n) = n + 1 ) by NEWTON:def_4, XREAL_1:6; assume A2: k <= n ; ::_thesis: ((x,y) In_Power n) . (k + 1) = ((n choose k) * (x ^ (n - k))) * (y ^ k) then reconsider l = n - i1 as Element of NAT by INT_1:5; k + 1 <= n + 1 by A2, XREAL_1:6; then k + 1 in dom ((x,y) In_Power n) by A1, FINSEQ_3:25; hence ((x,y) In_Power n) . (k + 1) = ((n choose i1) * (x ^ l)) * (y |^ i1) by NEWTON:def_4 .= ((n choose k) * (x ^ (n - k))) * (y ^ k) ; ::_thesis: verum end; theorem Th20: :: IRRAT_1:20 for n, k being Element of NAT st n > 0 & k <= n holds (cseq n) . k = ((1,(1 / n)) In_Power n) . (k + 1) proof let n, k be Element of NAT ; ::_thesis: ( n > 0 & k <= n implies (cseq n) . k = ((1,(1 / n)) In_Power n) . (k + 1) ) assume that A1: n > 0 and A2: k <= n ; ::_thesis: (cseq n) . k = ((1,(1 / n)) In_Power n) . (k + 1) thus ((1,(1 / n)) In_Power n) . (k + 1) = ((n choose k) * (1 ^ (n - k))) * ((1 / n) ^ k) by A2, Th19 .= ((n choose k) * 1) * ((1 / n) ^ k) by POWER:26 .= (n choose k) * (n ^ (- k)) by A1, POWER:32 .= (cseq n) . k by Def3 ; ::_thesis: verum end; theorem Th21: :: IRRAT_1:21 for n being Element of NAT st n > 0 holds ( cseq n is summable & Sum (cseq n) = (1 + (1 / n)) ^ n & Sum (cseq n) = dseq . n ) proof let n be Element of NAT ; ::_thesis: ( n > 0 implies ( cseq n is summable & Sum (cseq n) = (1 + (1 / n)) ^ n & Sum (cseq n) = dseq . n ) ) A1: now__::_thesis:_for_k_being_Element_of_NAT_st_k_>=_n_+_1_holds_ (cseq_n)_._k_=_0 let k be Element of NAT ; ::_thesis: ( k >= n + 1 implies (cseq n) . k = 0 ) assume k >= n + 1 ; ::_thesis: (cseq n) . k = 0 then A2: k > n by NAT_1:13; thus (cseq n) . k = (n choose k) * (n ^ (- k)) by Def3 .= 0 * (n ^ (- k)) by A2, NEWTON:def_3 .= 0 ; ::_thesis: verum end; assume A3: n > 0 ; ::_thesis: ( cseq n is summable & Sum (cseq n) = (1 + (1 / n)) ^ n & Sum (cseq n) = dseq . n ) A4: now__::_thesis:_for_k_being_Element_of_NAT_st_k_<_n_+_1_holds_ (cseq_n)_._k_=_((1,(1_/_n))_In_Power_n)_._(k_+_1) let k be Element of NAT ; ::_thesis: ( k < n + 1 implies (cseq n) . k = ((1,(1 / n)) In_Power n) . (k + 1) ) assume k < n + 1 ; ::_thesis: (cseq n) . k = ((1,(1 / n)) In_Power n) . (k + 1) then k <= n by NAT_1:13; hence (cseq n) . k = ((1,(1 / n)) In_Power n) . (k + 1) by A3, Th20; ::_thesis: verum end; A5: len ((1,(1 / n)) In_Power n) = n + 1 by NEWTON:def_4; hence cseq n is summable by A4, A1, Th18; ::_thesis: ( Sum (cseq n) = (1 + (1 / n)) ^ n & Sum (cseq n) = dseq . n ) thus (1 + (1 / n)) ^ n = Sum ((1,(1 / n)) In_Power n) by NEWTON:30 .= Sum (cseq n) by A5, A4, A1, Th18 ; ::_thesis: Sum (cseq n) = dseq . n hence Sum (cseq n) = dseq . n by Def4; ::_thesis: verum end; theorem Th22: :: IRRAT_1:22 ( dseq is convergent & lim dseq = number_e ) proof A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_(dseq_^\_1)_._n_=_(1_+_(1_/_(n_+_1)))_^_(n_+_1) let n be Element of NAT ; ::_thesis: (dseq ^\ 1) . n = (1 + (1 / (n + 1))) ^ (n + 1) thus (dseq ^\ 1) . n = dseq . (n + 1) by NAT_1:def_3 .= (1 + (1 / (n + 1))) ^ (n + 1) by Def4 ; ::_thesis: verum end; then A2: dseq ^\ 1 is convergent by POWER:59; hence dseq is convergent by SEQ_4:21; ::_thesis: lim dseq = number_e number_e = lim (dseq ^\ 1) by A1, POWER:def_4; hence lim dseq = number_e by A2, SEQ_4:22; ::_thesis: verum end; theorem Th23: :: IRRAT_1:23 ( eseq is summable & Sum eseq = exp_R 1 ) proof now__::_thesis:_for_k_being_Element_of_NAT_holds_eseq_._k_=_(1_rExpSeq)_._k let k be Element of NAT ; ::_thesis: eseq . k = (1 rExpSeq) . k thus eseq . k = 1 / (k !) by Def5 .= (1 |^ k) / (k !) by NEWTON:10 .= (1 rExpSeq) . k by SIN_COS:def_5 ; ::_thesis: verum end; then A1: eseq = 1 rExpSeq by FUNCT_2:63; hence eseq is summable by SIN_COS:45; ::_thesis: Sum eseq = exp_R 1 thus exp_R 1 = exp_R . 1 by SIN_COS:def_23 .= Sum eseq by A1, SIN_COS:def_22 ; ::_thesis: verum end; theorem Th24: :: IRRAT_1:24 for K being Element of NAT for dseqK being Real_Sequence st ( for n being Element of NAT holds dseqK . n = (Partial_Sums (cseq n)) . K ) holds ( dseqK is convergent & lim dseqK = (Partial_Sums eseq) . K ) proof defpred S1[ Element of NAT ] means for dseqK being Real_Sequence st ( for n being Element of NAT holds dseqK . n = (Partial_Sums (cseq n)) . \$1 ) holds ( dseqK is convergent & lim dseqK = (Partial_Sums eseq) . \$1 ); now__::_thesis:_for_K_being_Element_of_NAT_st_(_for_dseqK_being_Real_Sequence_st_(_for_n_being_Element_of_NAT_holds_dseqK_._n_=_(Partial_Sums_(cseq_n))_._K_)_holds_ (_dseqK_is_convergent_&_lim_dseqK_=_(Partial_Sums_eseq)_._K_)_)_holds_ for_dseqK1_being_Real_Sequence_st_(_for_n_being_Element_of_NAT_holds_dseqK1_._n_=_(Partial_Sums_(cseq_n))_._(K_+_1)_)_holds_ (_dseqK1_is_convergent_&_lim_dseqK1_=_(Partial_Sums_eseq)_._(K_+_1)_) let K be Element of NAT ; ::_thesis: ( ( for dseqK being Real_Sequence st ( for n being Element of NAT holds dseqK . n = (Partial_Sums (cseq n)) . K ) holds ( dseqK is convergent & lim dseqK = (Partial_Sums eseq) . K ) ) implies for dseqK1 being Real_Sequence st ( for n being Element of NAT holds dseqK1 . n = (Partial_Sums (cseq n)) . (K + 1) ) holds ( dseqK1 is convergent & lim dseqK1 = (Partial_Sums eseq) . (K + 1) ) ) deffunc H1( Element of NAT ) -> Element of REAL = (Partial_Sums (cseq \$1)) . K; consider dseqK being Real_Sequence such that A1: for n being Element of NAT holds dseqK . n = H1(n) from SEQ_1:sch_1(); assume A2: for dseqK being Real_Sequence st ( for n being Element of NAT holds dseqK . n = (Partial_Sums (cseq n)) . K ) holds ( dseqK is convergent & lim dseqK = (Partial_Sums eseq) . K ) ; ::_thesis: for dseqK1 being Real_Sequence st ( for n being Element of NAT holds dseqK1 . n = (Partial_Sums (cseq n)) . (K + 1) ) holds ( dseqK1 is convergent & lim dseqK1 = (Partial_Sums eseq) . (K + 1) ) then A3: dseqK is convergent by A1; let dseqK1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds dseqK1 . n = (Partial_Sums (cseq n)) . (K + 1) ) implies ( dseqK1 is convergent & lim dseqK1 = (Partial_Sums eseq) . (K + 1) ) ) assume A4: for n being Element of NAT holds dseqK1 . n = (Partial_Sums (cseq n)) . (K + 1) ; ::_thesis: ( dseqK1 is convergent & lim dseqK1 = (Partial_Sums eseq) . (K + 1) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_dseqK1_._n_=_(dseqK_+_(bseq_(K_+_1)))_._n let n be Element of NAT ; ::_thesis: dseqK1 . n = (dseqK + (bseq (K + 1))) . n thus dseqK1 . n = (Partial_Sums (cseq n)) . (K + 1) by A4 .= ((Partial_Sums (cseq n)) . K) + ((cseq n) . (K + 1)) by SERIES_1:def_1 .= (dseqK . n) + ((cseq n) . (K + 1)) by A1 .= (dseqK . n) + ((bseq (K + 1)) . n) by Th3 .= (dseqK + (bseq (K + 1))) . n by SEQ_1:7 ; ::_thesis: verum end; then A5: dseqK1 = dseqK + (bseq (K + 1)) by FUNCT_2:63; A6: lim dseqK = (Partial_Sums eseq) . K by A2, A1; A7: bseq (K + 1) is convergent by Th12; hence dseqK1 is convergent by A3, A5, SEQ_2:5; ::_thesis: lim dseqK1 = (Partial_Sums eseq) . (K + 1) thus lim dseqK1 = (lim dseqK) + (lim (bseq (K + 1))) by A3, A5, A7, SEQ_2:6 .= ((Partial_Sums eseq) . K) + (eseq . (K + 1)) by A6, Th12 .= (Partial_Sums eseq) . (K + 1) by SERIES_1:def_1 ; ::_thesis: verum end; then A8: for n being Element of NAT st S1[n] holds S1[n + 1] ; now__::_thesis:_for_dseq0_being_Real_Sequence_st_(_for_n_being_Element_of_NAT_holds_dseq0_._n_=_(Partial_Sums_(cseq_n))_._0_)_holds_ (_dseq0_is_convergent_&_lim_dseq0_=_(Partial_Sums_eseq)_._0_) let dseq0 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds dseq0 . n = (Partial_Sums (cseq n)) . 0 ) implies ( dseq0 is convergent & lim dseq0 = (Partial_Sums eseq) . 0 ) ) assume A9: for n being Element of NAT holds dseq0 . n = (Partial_Sums (cseq n)) . 0 ; ::_thesis: ( dseq0 is convergent & lim dseq0 = (Partial_Sums eseq) . 0 ) now__::_thesis:_for_n_being_Element_of_NAT_holds_dseq0_._n_=_(bseq_0)_._n let n be Element of NAT ; ::_thesis: dseq0 . n = (bseq 0) . n thus dseq0 . n = (Partial_Sums (cseq n)) . 0 by A9 .= (cseq n) . 0 by SERIES_1:def_1 .= (bseq 0) . n by Th3 ; ::_thesis: verum end; then A10: dseq0 = bseq 0 by FUNCT_2:63; hence dseq0 is convergent by Th12; ::_thesis: lim dseq0 = (Partial_Sums eseq) . 0 thus lim dseq0 = eseq . 0 by A10, Th12 .= (Partial_Sums eseq) . 0 by SERIES_1:def_1 ; ::_thesis: verum end; then A11: S1[ 0 ] ; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A11, A8); ::_thesis: verum end; theorem Th25: :: IRRAT_1:25 for x being real number for seq being Real_Sequence st seq is convergent & lim seq = x holds for eps being real number st eps > 0 holds ex N being Element of NAT st for n being Element of NAT st n >= N holds seq . n > x - eps proof let x be real number ; ::_thesis: for seq being Real_Sequence st seq is convergent & lim seq = x holds for eps being real number st eps > 0 holds ex N being Element of NAT st for n being Element of NAT st n >= N holds seq . n > x - eps let seq be Real_Sequence; ::_thesis: ( seq is convergent & lim seq = x implies for eps being real number st eps > 0 holds ex N being Element of NAT st for n being Element of NAT st n >= N holds seq . n > x - eps ) assume A1: ( seq is convergent & lim seq = x ) ; ::_thesis: for eps being real number st eps > 0 holds ex N being Element of NAT st for n being Element of NAT st n >= N holds seq . n > x - eps let eps be real number ; ::_thesis: ( eps > 0 implies ex N being Element of NAT st for n being Element of NAT st n >= N holds seq . n > x - eps ) assume eps > 0 ; ::_thesis: ex N being Element of NAT st for n being Element of NAT st n >= N holds seq . n > x - eps then consider N being Element of NAT such that A2: for n being Element of NAT st n >= N holds abs ((seq . n) - x) < eps by A1, SEQ_2:def_7; take N ; ::_thesis: for n being Element of NAT st n >= N holds seq . n > x - eps let n be Element of NAT ; ::_thesis: ( n >= N implies seq . n > x - eps ) assume n >= N ; ::_thesis: seq . n > x - eps then abs ((seq . n) - x) < eps by A2; then (seq . n) - x > - eps by SEQ_2:1; then ((seq . n) - x) + x > (- eps) + x by XREAL_1:6; hence seq . n > x - eps ; ::_thesis: verum end; theorem Th26: :: IRRAT_1:26 for x being real number for seq being Real_Sequence st ( for eps being real number st eps > 0 holds ex N being Element of NAT st for n being Element of NAT st n >= N holds seq . n > x - eps ) & ex N being Element of NAT st for n being Element of NAT st n >= N holds seq . n <= x holds ( seq is convergent & lim seq = x ) proof let x be real number ; ::_thesis: for seq being Real_Sequence st ( for eps being real number st eps > 0 holds ex N being Element of NAT st for n being Element of NAT st n >= N holds seq . n > x - eps ) & ex N being Element of NAT st for n being Element of NAT st n >= N holds seq . n <= x holds ( seq is convergent & lim seq = x ) let seq be Real_Sequence; ::_thesis: ( ( for eps being real number st eps > 0 holds ex N being Element of NAT st for n being Element of NAT st n >= N holds seq . n > x - eps ) & ex N being Element of NAT st for n being Element of NAT st n >= N holds seq . n <= x implies ( seq is convergent & lim seq = x ) ) assume that A1: for eps being real number st eps > 0 holds ex N being Element of NAT st for n being Element of NAT st n >= N holds seq . n > x - eps and A2: ex N being Element of NAT st for n being Element of NAT st n >= N holds seq . n <= x ; ::_thesis: ( seq is convergent & lim seq = x ) A3: for eps being real number st eps > 0 holds ex N being Element of NAT st for n being Element of NAT st n >= N holds abs ((seq . n) - x) < eps proof let eps be real number ; ::_thesis: ( eps > 0 implies ex N being Element of NAT st for n being Element of NAT st n >= N holds abs ((seq . n) - x) < eps ) assume A4: eps > 0 ; ::_thesis: ex N being Element of NAT st for n being Element of NAT st n >= N holds abs ((seq . n) - x) < eps then A5: x + eps > x + 0 by XREAL_1:6; consider N2 being Element of NAT such that A6: for n being Element of NAT st n >= N2 holds seq . n <= x by A2; consider N1 being Element of NAT such that A7: for n being Element of NAT st n >= N1 holds seq . n > x - eps by A1, A4; take N = max (N1,N2); ::_thesis: for n being Element of NAT st n >= N holds abs ((seq . n) - x) < eps let n be Element of NAT ; ::_thesis: ( n >= N implies abs ((seq . n) - x) < eps ) assume A8: n >= N ; ::_thesis: abs ((seq . n) - x) < eps then n >= N1 by XXREAL_0:30; then seq . n > x - eps by A7; then A9: (seq . n) - x > (x - eps) - x by XREAL_1:9; seq . n <= x by A6, A8, XXREAL_0:30; then seq . n < x + eps by A5, XXREAL_0:2; then (seq . n) - x < eps by XREAL_1:19; hence abs ((seq . n) - x) < eps by A9, SEQ_2:1; ::_thesis: verum end; hence seq is convergent by SEQ_2:def_6; ::_thesis: lim seq = x hence lim seq = x by A3, SEQ_2:def_7; ::_thesis: verum end; theorem Th27: :: IRRAT_1:27 for seq being Real_Sequence st seq is summable holds for eps being real number st eps > 0 holds ex K being Element of NAT st (Partial_Sums seq) . K > (Sum seq) - eps proof let seq be Real_Sequence; ::_thesis: ( seq is summable implies for eps being real number st eps > 0 holds ex K being Element of NAT st (Partial_Sums seq) . K > (Sum seq) - eps ) assume seq is summable ; ::_thesis: for eps being real number st eps > 0 holds ex K being Element of NAT st (Partial_Sums seq) . K > (Sum seq) - eps then A1: Partial_Sums seq is convergent by SERIES_1:def_2; let eps be real number ; ::_thesis: ( eps > 0 implies ex K being Element of NAT st (Partial_Sums seq) . K > (Sum seq) - eps ) assume eps > 0 ; ::_thesis: ex K being Element of NAT st (Partial_Sums seq) . K > (Sum seq) - eps then consider K being Element of NAT such that A2: for k being Element of NAT st k >= K holds (Partial_Sums seq) . k > (lim (Partial_Sums seq)) - eps by A1, Th25; take K ; ::_thesis: (Partial_Sums seq) . K > (Sum seq) - eps Sum seq = lim (Partial_Sums seq) by SERIES_1:def_3; hence (Partial_Sums seq) . K > (Sum seq) - eps by A2; ::_thesis: verum end; theorem Th28: :: IRRAT_1:28 for n being Element of NAT st n >= 1 holds dseq . n <= Sum eseq proof let n be Element of NAT ; ::_thesis: ( n >= 1 implies dseq . n <= Sum eseq ) assume A1: n >= 1 ; ::_thesis: dseq . n <= Sum eseq then for k being Element of NAT holds ( 0 <= (cseq n) . k & (cseq n) . k <= eseq . k ) by Th14; then Sum (cseq n) <= Sum eseq by Th23, SERIES_1:20; hence dseq . n <= Sum eseq by A1, Th21; ::_thesis: verum end; theorem Th29: :: IRRAT_1:29 for K being Element of NAT for seq being Real_Sequence st seq is summable & ( for k being Element of NAT holds seq . k >= 0 ) holds Sum seq >= (Partial_Sums seq) . K proof let K be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is summable & ( for k being Element of NAT holds seq . k >= 0 ) holds Sum seq >= (Partial_Sums seq) . K let seq be Real_Sequence; ::_thesis: ( seq is summable & ( for k being Element of NAT holds seq . k >= 0 ) implies Sum seq >= (Partial_Sums seq) . K ) assume that A1: seq is summable and A2: for k being Element of NAT holds seq . k >= 0 ; ::_thesis: Sum seq >= (Partial_Sums seq) . K A3: now__::_thesis:_for_k_being_Element_of_NAT_holds_(seq_^\_(K_+_1))_._k_>=_0 let k be Element of NAT ; ::_thesis: (seq ^\ (K + 1)) . k >= 0 (seq ^\ (K + 1)) . k = seq . ((K + 1) + k) by NAT_1:def_3; hence (seq ^\ (K + 1)) . k >= 0 by A2; ::_thesis: verum end; seq ^\ (K + 1) is summable by A1, SERIES_1:12; then Sum (seq ^\ (K + 1)) >= 0 by A3, SERIES_1:18; then ((Partial_Sums seq) . K) + (Sum (seq ^\ (K + 1))) >= ((Partial_Sums seq) . K) + 0 by XREAL_1:6; hence Sum seq >= (Partial_Sums seq) . K by A1, SERIES_1:15; ::_thesis: verum end; theorem Th30: :: IRRAT_1:30 ( dseq is convergent & lim dseq = Sum eseq ) proof for eps being real number st eps > 0 holds ex N being Element of NAT st for n being Element of NAT st n >= N holds dseq . n > (Sum eseq) - eps proof let eps be real number ; ::_thesis: ( eps > 0 implies ex N being Element of NAT st for n being Element of NAT st n >= N holds dseq . n > (Sum eseq) - eps ) assume A1: eps > 0 ; ::_thesis: ex N being Element of NAT st for n being Element of NAT st n >= N holds dseq . n > (Sum eseq) - eps then consider K being Element of NAT such that A2: (Partial_Sums eseq) . K > (Sum eseq) - (eps / 2) by Th23, Th27, XREAL_1:139; A3: ((Partial_Sums eseq) . K) - (eps / 2) > ((Sum eseq) - (eps / 2)) - (eps / 2) by A2, XREAL_1:9; deffunc H1( Element of NAT ) -> Element of REAL = (Partial_Sums (cseq \$1)) . K; consider dseqK being Real_Sequence such that A4: for n being Element of NAT holds dseqK . n = H1(n) from SEQ_1:sch_1(); ( dseqK is convergent & lim dseqK = (Partial_Sums eseq) . K ) by A4, Th24; then consider N being Element of NAT such that A5: for n being Element of NAT st n >= N holds dseqK . n > ((Partial_Sums eseq) . K) - (eps / 2) by A1, Th25, XREAL_1:139; take N1 = N + 1; ::_thesis: for n being Element of NAT st n >= N1 holds dseq . n > (Sum eseq) - eps let n be Element of NAT ; ::_thesis: ( n >= N1 implies dseq . n > (Sum eseq) - eps ) assume A6: n >= N1 ; ::_thesis: dseq . n > (Sum eseq) - eps then ( ( for k being Element of NAT holds (cseq n) . k >= 0 ) & cseq n is summable ) by Th14, Th21; then Sum (cseq n) >= (Partial_Sums (cseq n)) . K by Th29; then dseq . n >= (Partial_Sums (cseq n)) . K by A6, Th21; then A7: dseq . n >= dseqK . n by A4; N + 1 >= N + 0 by XREAL_1:6; then n >= N by A6, XXREAL_0:2; then dseqK . n > ((Partial_Sums eseq) . K) - (eps / 2) by A5; then dseq . n > ((Partial_Sums eseq) . K) - (eps / 2) by A7, XXREAL_0:2; hence dseq . n > (Sum eseq) - eps by A3, XXREAL_0:2; ::_thesis: verum end; hence ( dseq is convergent & lim dseq = Sum eseq ) by Th26, Th28; ::_thesis: verum end; definition redefine func number_e equals :: IRRAT_1:def 6 Sum eseq; compatibility for b1 being set holds ( b1 = number_e iff b1 = Sum eseq ) by Th22, Th30; end; :: deftheorem defines number_e IRRAT_1:def_6_:_ number_e = Sum eseq; definition redefine func number_e equals :: IRRAT_1:def 7 exp_R 1; compatibility for b1 being set holds ( b1 = number_e iff b1 = exp_R 1 ) by Th23; end; :: deftheorem defines number_e IRRAT_1:def_7_:_ number_e = exp_R 1; begin theorem Th31: :: IRRAT_1:31 for x being real number st x is rational holds ex n being Element of NAT st ( n >= 2 & (n !) * x is integer ) proof let x be real number ; ::_thesis: ( x is rational implies ex n being Element of NAT st ( n >= 2 & (n !) * x is integer ) ) assume x is rational ; ::_thesis: ex n being Element of NAT st ( n >= 2 & (n !) * x is integer ) then consider i being Integer, n being Element of NAT such that A1: n <> 0 and A2: x = i / n by RAT_1:8; percases ( n < 1 + 1 or n >= 2 ) ; supposeA3: n < 1 + 1 ; ::_thesis: ex n being Element of NAT st ( n >= 2 & (n !) * x is integer ) A4: n >= 0 + 1 by A1, NAT_1:13; n <= 1 by A3, NAT_1:13; then n = 1 by A4, XXREAL_0:1; then reconsider x1 = x as Integer by A2; take n = 2; ::_thesis: ( n >= 2 & (n !) * x is integer ) (n !) * x1 is integer ; hence ( n >= 2 & (n !) * x is integer ) ; ::_thesis: verum end; supposeA5: n >= 2 ; ::_thesis: ex n being Element of NAT st ( n >= 2 & (n !) * x is integer ) take n ; ::_thesis: ( n >= 2 & (n !) * x is integer ) thus n >= 2 by A5; ::_thesis: (n !) * x is integer reconsider m = n - 1 as Element of NAT by A5, INT_1:5, XXREAL_0:2; (n !) * x = ((m + 1) * (m !)) * x by NEWTON:15 .= (n * x) * (m !) .= i * (m !) by A1, A2, XCMPLX_1:87 ; hence (n !) * x is integer ; ::_thesis: verum end; end; end; theorem Th32: :: IRRAT_1:32 for n, k being Element of NAT holds (n !) * (eseq . k) = (n !) / (k !) proof let n, k be Element of NAT ; ::_thesis: (n !) * (eseq . k) = (n !) / (k !) thus (n !) * (eseq . k) = (n !) * (1 / (k !)) by Def5 .= (n !) / (k !) ; ::_thesis: verum end; theorem :: IRRAT_1:33 for n, k being Element of NAT holds (n !) / (k !) > 0 by XREAL_1:139; theorem Th34: :: IRRAT_1:34 for seq being Real_Sequence st seq is summable & ( for n being Element of NAT holds seq . n > 0 ) holds Sum seq > 0 proof let seq be Real_Sequence; ::_thesis: ( seq is summable & ( for n being Element of NAT holds seq . n > 0 ) implies Sum seq > 0 ) assume that A1: seq is summable and A2: for n being Element of NAT holds seq . n > 0 ; ::_thesis: Sum seq > 0 A3: Sum seq = ((Partial_Sums seq) . 0) + (Sum (seq ^\ (0 + 1))) by A1, SERIES_1:15 .= (seq . 0) + (Sum (seq ^\ 1)) by SERIES_1:def_1 ; A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq_^\_1)_._n_>=_0 let n be Element of NAT ; ::_thesis: (seq ^\ 1) . n >= 0 (seq ^\ 1) . n = seq . (1 + n) by NAT_1:def_3; hence (seq ^\ 1) . n >= 0 by A2; ::_thesis: verum end; seq ^\ 1 is summable by A1, SERIES_1:12; then Sum (seq ^\ 1) >= 0 by A4, SERIES_1:18; then Sum seq > 0 + 0 by A2, A3, XREAL_1:8; hence Sum seq > 0 ; ::_thesis: verum end; theorem Th35: :: IRRAT_1:35 for n being Element of NAT holds (n !) * (Sum (eseq ^\ (n + 1))) > 0 proof let n be Element of NAT ; ::_thesis: (n !) * (Sum (eseq ^\ (n + 1))) > 0 A1: now__::_thesis:_for_k_being_Element_of_NAT_holds_(eseq_^\_(n_+_1))_._k_>_0 let k be Element of NAT ; ::_thesis: (eseq ^\ (n + 1)) . k > 0 (eseq ^\ (n + 1)) . k = eseq . ((n + 1) + k) by NAT_1:def_3 .= 1 / (((n + 1) + k) !) by Def5 ; hence (eseq ^\ (n + 1)) . k > 0 ; ::_thesis: verum end; eseq ^\ (n + 1) is summable by Th23, SERIES_1:12; then ( n ! > 0 & Sum (eseq ^\ (n + 1)) > 0 ) by A1, Th34; hence (n !) * (Sum (eseq ^\ (n + 1))) > 0 by XREAL_1:129; ::_thesis: verum end; theorem Th36: :: IRRAT_1:36 for k, n being Element of NAT st k <= n holds (n !) / (k !) is integer proof let k, n be Element of NAT ; ::_thesis: ( k <= n implies (n !) / (k !) is integer ) defpred S1[ Element of NAT ] means ((\$1 + k) !) / (k !) is integer ; assume k <= n ; ::_thesis: (n !) / (k !) is integer then reconsider m = n - k as Element of NAT by INT_1:5; A1: n = m + k ; now__::_thesis:_for_m_being_Element_of_NAT_st_((m_+_k)_!)_/_(k_!)_is_integer_holds_ (((m_+_1)_+_k)_!)_/_(k_!)_is_integer let m be Element of NAT ; ::_thesis: ( ((m + k) !) / (k !) is integer implies (((m + 1) + k) !) / (k !) is integer ) A2: (((m + 1) + k) !) / (k !) = (((m + k) + 1) * ((m + k) !)) * ((k !) ") by NEWTON:15 .= ((m + k) + 1) * (((m + k) !) * ((k !) ")) .= ((m + k) + 1) * (((m + k) !) / (k !)) ; assume ((m + k) !) / (k !) is integer ; ::_thesis: (((m + 1) + k) !) / (k !) is integer then reconsider i = ((m + k) !) / (k !) as Integer ; ((m + k) + 1) * i is Integer ; hence (((m + 1) + k) !) / (k !) is integer by A2; ::_thesis: verum end; then A3: for n being Element of NAT st S1[n] holds S1[n + 1] ; A4: S1[ 0 ] by XCMPLX_1:60; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A3); hence (n !) / (k !) is integer by A1; ::_thesis: verum end; theorem Th37: :: IRRAT_1:37 for n being Element of NAT holds (n !) * ((Partial_Sums eseq) . n) is integer proof let n be Element of NAT ; ::_thesis: (n !) * ((Partial_Sums eseq) . n) is integer defpred S1[ Element of NAT ] means ( \$1 <= n implies (n !) * ((Partial_Sums eseq) . \$1) is integer ); now__::_thesis:_for_k_being_Element_of_NAT_st_(_k_<=_n_implies_(n_!)_*_((Partial_Sums_eseq)_._k)_is_integer_)_&_k_+_1_<=_n_holds_ (n_!)_*_((Partial_Sums_eseq)_._(k_+_1))_is_integer let k be Element of NAT ; ::_thesis: ( ( k <= n implies (n !) * ((Partial_Sums eseq) . k) is integer ) & k + 1 <= n implies (n !) * ((Partial_Sums eseq) . (k + 1)) is integer ) assume A1: ( k <= n implies (n !) * ((Partial_Sums eseq) . k) is integer ) ; ::_thesis: ( k + 1 <= n implies (n !) * ((Partial_Sums eseq) . (k + 1)) is integer ) assume A2: k + 1 <= n ; ::_thesis: (n !) * ((Partial_Sums eseq) . (k + 1)) is integer k + 0 <= k + 1 by XREAL_1:6; then reconsider i = (n !) * ((Partial_Sums eseq) . k) as Integer by A1, A2, XXREAL_0:2; (n !) * (eseq . (k + 1)) = (n !) / ((k + 1) !) by Th32; then reconsider j = (n !) * (eseq . (k + 1)) as Integer by A2, Th36; A3: i + j is Integer ; (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))) ; hence (n !) * ((Partial_Sums eseq) . (k + 1)) is integer by A3; ::_thesis: verum end; then A4: for k being Element of NAT st S1[k] holds S1[k + 1] ; now__::_thesis:_(_0_<=_n_implies_(n_!)_*_((Partial_Sums_eseq)_._0)_is_integer_) assume 0 <= n ; ::_thesis: (n !) * ((Partial_Sums eseq) . 0) is integer (n !) * ((Partial_Sums eseq) . 0) = (n !) * (eseq . 0) by SERIES_1:def_1 .= (n !) / (0 !) by Th32 ; hence (n !) * ((Partial_Sums eseq) . 0) is integer by Th36; ::_thesis: verum end; then A5: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A4); hence (n !) * ((Partial_Sums eseq) . n) is integer ; ::_thesis: verum end; theorem Th38: :: IRRAT_1:38 for n, k being Element of NAT for x being real number st x = 1 / (n + 1) holds (n !) / (((n + k) + 1) !) <= x ^ (k + 1) proof let n, k be Element of NAT ; ::_thesis: for x being real number st x = 1 / (n + 1) holds (n !) / (((n + k) + 1) !) <= x ^ (k + 1) let x be real number ; ::_thesis: ( x = 1 / (n + 1) implies (n !) / (((n + k) + 1) !) <= x ^ (k + 1) ) defpred S1[ Element of NAT ] means (n !) / (((n + \$1) + 1) !) <= x ^ (\$1 + 1); assume A1: x = 1 / (n + 1) ; ::_thesis: (n !) / (((n + k) + 1) !) <= x ^ (k + 1) A2: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] A4: (n !) / (((n + (k + 1)) + 1) !) = (n !) * ((((n + (k + 1)) + 1) !) ") .= (n !) * ((((n + (k + 1)) + 1) * (((n + k) + 1) !)) ") by NEWTON:15 .= (n !) * ((((n + (k + 1)) + 1) ") * ((((n + k) + 1) !) ")) by XCMPLX_1:204 .= ((n !) * ((((n + k) + 1) !) ")) * (((n + (k + 1)) + 1) ") .= ((n !) / (((n + k) + 1) !)) * (((n + (k + 1)) + 1) ") ; n + (k + 1) >= n + 0 by XREAL_1:6; then (n + (k + 1)) + 1 >= n + 1 by XREAL_1:6; then A5: ((n + (k + 1)) + 1) " <= 1 / (n + 1) by XREAL_1:85; (x ^ (k + 1)) * x = (x ^ (k + 1)) * (x ^ 1) by POWER:25 .= x ^ ((k + 1) + 1) by A1, POWER:27 ; hence S1[k + 1] by A1, A3, A5, A4, XREAL_1:66; ::_thesis: verum end; (n !) / ((n + 1) !) = (n !) / ((n + 1) * (n !)) by NEWTON:15 .= (n !) * (((n + 1) * (n !)) ") .= (n !) * (((n + 1) ") * ((n !) ")) by XCMPLX_1:204 .= ((n !) * ((n !) ")) * ((n + 1) ") .= 1 * ((n + 1) ") by XCMPLX_0:def_7 .= x by A1 ; then A6: S1[ 0 ] by POWER:25; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A2); hence (n !) / (((n + k) + 1) !) <= x ^ (k + 1) ; ::_thesis: verum end; theorem Th39: :: IRRAT_1:39 for n being Element of NAT for x being real number st n > 0 & x = 1 / (n + 1) holds (n !) * (Sum (eseq ^\ (n + 1))) <= x / (1 - x) proof let n be Element of NAT ; ::_thesis: for x being real number st n > 0 & x = 1 / (n + 1) holds (n !) * (Sum (eseq ^\ (n + 1))) <= x / (1 - x) let x be real number ; ::_thesis: ( n > 0 & x = 1 / (n + 1) implies (n !) * (Sum (eseq ^\ (n + 1))) <= x / (1 - x) ) assume that A1: n > 0 and A2: x = 1 / (n + 1) ; ::_thesis: (n !) * (Sum (eseq ^\ (n + 1))) <= x / (1 - x) deffunc H1( Element of NAT ) -> set = x ^ (\$1 + 1); consider seq being Real_Sequence such that A3: for k being Element of NAT holds seq . k = H1(k) from SEQ_1:sch_1(); A4: now__::_thesis:_for_k_being_Element_of_NAT_holds_ (_((n_!)_(#)_(eseq_^\_(n_+_1)))_._k_>=_0_&_((n_!)_(#)_(eseq_^\_(n_+_1)))_._k_<=_seq_._k_) let k be Element of NAT ; ::_thesis: ( ((n !) (#) (eseq ^\ (n + 1))) . k >= 0 & ((n !) (#) (eseq ^\ (n + 1))) . k <= seq . k ) A5: ((n !) (#) (eseq ^\ (n + 1))) . k = (n !) * ((eseq ^\ (n + 1)) . k) by SEQ_1:9 .= (n !) * (eseq . ((n + 1) + k)) by NAT_1:def_3 .= (n !) * (1 / (((n + k) + 1) !)) by Def5 .= (n !) / (((n + k) + 1) !) ; hence ((n !) (#) (eseq ^\ (n + 1))) . k >= 0 ; ::_thesis: ((n !) (#) (eseq ^\ (n + 1))) . k <= seq . k seq . k = x ^ (k + 1) by A3; hence ((n !) (#) (eseq ^\ (n + 1))) . k <= seq . k by A2, A5, Th38; ::_thesis: verum end; A6: seq . 0 = x ^ (0 + 1) by A3 .= x by POWER:25 ; A7: eseq ^\ (n + 1) is summable by Th23, SERIES_1:12; n + 1 > 0 + 1 by A1, XREAL_1:6; then A8: x < 1 by A2, XREAL_1:212; A9: now__::_thesis:_for_k_being_Element_of_NAT_holds_seq_._(k_+_1)_=_x_*_(seq_._k) let k be Element of NAT ; ::_thesis: seq . (k + 1) = x * (seq . k) thus seq . (k + 1) = x ^ ((k + 1) + 1) by A3 .= (x ^ 1) * (x ^ (k + 1)) by A2, POWER:27 .= x * (x ^ (k + 1)) by POWER:25 .= x * (seq . k) by A3 ; ::_thesis: verum end; abs x = x by A2, ABSVALUE:def_1; then seq is summable by A8, A9, SERIES_1:25; then A10: Sum ((n !) (#) (eseq ^\ (n + 1))) <= Sum seq by A4, SERIES_1:20; abs x < 1 by A2, A8, ABSVALUE:def_1; then Sum seq = x / (1 - x) by A6, A9, SERIES_1:25; hence (n !) * (Sum (eseq ^\ (n + 1))) <= x / (1 - x) by A7, A10, SERIES_1:10; ::_thesis: verum end; theorem Th40: :: IRRAT_1:40 for x, n being real number st n >= 2 & x = 1 / (n + 1) holds x / (1 - x) < 1 proof let x, n be real number ; ::_thesis: ( n >= 2 & x = 1 / (n + 1) implies x / (1 - x) < 1 ) assume that A1: n >= 2 and A2: x = 1 / (n + 1) ; ::_thesis: x / (1 - x) < 1 n + 1 > n by XREAL_1:29; then 2 < n + 1 by A1, XXREAL_0:2; then 2 / (n + 1) < 1 by XREAL_1:189; then x + x < 1 by A2; then x < 1 - x by XREAL_1:20; hence x / (1 - x) < 1 by A1, A2, XREAL_1:189; ::_thesis: verum end; theorem :: IRRAT_1:41 number_e is irrational proof assume number_e is rational ; ::_thesis: contradiction then consider n being Element of NAT such that A1: n >= 2 and A2: (n !) * number_e is integer by Th31; reconsider ne = (n !) * number_e as Integer by A2; set x = 1 / (n + 1); reconsider ne1 = (n !) * ((Partial_Sums eseq) . n) as Integer by Th37; (n !) * number_e = (n !) * (((Partial_Sums eseq) . n) + (Sum (eseq ^\ (n + 1)))) by Th23, SERIES_1:15 .= ((n !) * ((Partial_Sums eseq) . n)) + ((n !) * (Sum (eseq ^\ (n + 1)))) ; then A3: (n !) * (Sum (eseq ^\ (n + 1))) = ne - ne1 ; ( (1 / (n + 1)) / (1 - (1 / (n + 1))) < 1 & (n !) * (Sum (eseq ^\ (n + 1))) <= (1 / (n + 1)) / (1 - (1 / (n + 1))) ) by A1, Th39, Th40; then (n !) * (Sum (eseq ^\ (n + 1))) < 0 + 1 by XXREAL_0:2; hence contradiction by A3, Th35, INT_1:7; ::_thesis: verum end;