:: 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;