:: IRRAT_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

notation
let x be real number ;
antonym irrational x for rational x;
end;

notation
let x, y be real number ;
synonym x .^. y for x to_power y;
end;

theorem Th1: :: IRRAT_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Nat st p is prime holds
sqrt p is irrational
proof end;

theorem :: IRRAT_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex x, y being real number st
( x is irrational & y is irrational & not x .^. y is irrational )
proof end;

scheme :: IRRAT_1:sch 1
LambdaRealSeq{ F1( set ) -> real number } :
( ex seq being Real_Sequence st
for n being Nat holds seq . n = F1(n) & ( for seq1, seq2 being Real_Sequence st ( for n being Nat holds seq1 . n = F1(n) ) & ( for n being Nat holds seq2 . n = F1(n) ) holds
seq1 = seq2 ) )
proof end;

definition
let k be Nat;
func aseq k -> Real_Sequence means :Def1: :: IRRAT_1:def 1
for n being Nat holds it . n = (n - k) / n;
correctness
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = (n - k) / n
;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = (n - k) / n ) & ( for n being Nat holds b2 . n = (n - k) / n ) holds
b1 = b2
;
proof 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 Nat holds b2 . n = (n - k) / n );

definition
let k be Nat;
func bseq k -> Real_Sequence means :Def2: :: IRRAT_1:def 2
for n being Nat holds it . n = (n choose k) * (n .^. (- k));
correctness
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = (n choose k) * (n .^. (- k))
;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = (n choose k) * (n .^. (- k)) ) & ( for n being Nat holds b2 . n = (n choose k) * (n .^. (- k)) ) holds
b1 = b2
;
proof end;
end;

:: 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 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 Nat holds it . k = (n choose k) * (n .^. (- k));
correctness
existence
ex b1 being Real_Sequence st
for k being Nat holds b1 . k = (n choose k) * (n .^. (- k))
;
uniqueness
for b1, b2 being Real_Sequence st ( for k being Nat holds b1 . k = (n choose k) * (n .^. (- k)) ) & ( for k being Nat holds b2 . k = (n choose k) * (n .^. (- k)) ) holds
b1 = b2
;
proof 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 Nat holds b2 . k = (n choose k) * (n .^. (- k)) );

theorem Th3: :: IRRAT_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k being Nat holds (cseq n) . k = (bseq k) . n
proof end;

definition
func dseq -> Real_Sequence means :Def4: :: IRRAT_1:def 4
for n being Nat holds it . n = (1 + (1 / n)) .^. n;
correctness
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = (1 + (1 / n)) .^. n
;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = (1 + (1 / n)) .^. n ) & ( for n being Nat holds b2 . n = (1 + (1 / n)) .^. n ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def4 defines dseq IRRAT_1:def 4 :
for b1 being Real_Sequence holds
( b1 = dseq iff for n being Nat holds b1 . n = (1 + (1 / n)) .^. n );

definition
func eseq -> Real_Sequence means :Def5: :: IRRAT_1:def 5
for k being Nat holds it . k = 1 / (k ! );
correctness
existence
ex b1 being Real_Sequence st
for k being Nat holds b1 . k = 1 / (k ! )
;
uniqueness
for b1, b2 being Real_Sequence st ( for k being Nat holds b1 . k = 1 / (k ! ) ) & ( for k being Nat holds b2 . k = 1 / (k ! ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def5 defines eseq IRRAT_1:def 5 :
for b1 being Real_Sequence holds
( b1 = eseq iff for k being Nat holds b1 . k = 1 / (k ! ) );

theorem Th4: :: IRRAT_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k being Nat st n > 0 holds
n .^. (- (k + 1)) = (n .^. (- k)) / n
proof end;

Lm1: for x, y, z, v, w being real number holds x / ((y * z) * (v / w)) = (w / z) * (x / (y * v))
by XCMPLX_1:235;

theorem :: IRRAT_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th6: :: IRRAT_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k being Nat holds n choose (k + 1) = ((n - k) / (k + 1)) * (n choose k)
proof end;

theorem Th7: :: IRRAT_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k being Nat st n > 0 holds
(bseq (k + 1)) . n = ((1 / (k + 1)) * ((bseq k) . n)) * ((aseq k) . n)
proof end;

theorem Th8: :: IRRAT_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k being Nat st n > 0 holds
(aseq k) . n = 1 - (k / n)
proof end;

theorem Th9: :: IRRAT_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat holds
( aseq k is convergent & lim (aseq k) = 1 )
proof end;

theorem Th10: :: IRRAT_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th11: :: IRRAT_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds (bseq 0) . n = 1
proof end;

theorem Th12: :: IRRAT_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat holds (1 / (k + 1)) * (1 / (k ! )) = 1 / ((k + 1) ! )
proof end;

theorem Th13: :: IRRAT_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat holds
( bseq k is convergent & lim (bseq k) = 1 / (k ! ) & lim (bseq k) = eseq . k )
proof end;

theorem Th14: :: IRRAT_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being Nat st k < n holds
( 0 < (aseq k) . n & (aseq k) . n <= 1 )
proof end;

theorem Th15: :: IRRAT_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k being 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 end;

theorem Th16: :: IRRAT_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for seq being Real_Sequence st seq ^\ 1 is summable holds
( seq is summable & Sum seq = (seq . 0) + (Sum (seq ^\ 1)) )
proof end;

theorem Th17: :: IRRAT_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being 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 end;

theorem Th18: :: IRRAT_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for sq being FinSequence of REAL st len sq > 0 holds
Sum sq = (sq . 1) + (Sum (sq /^ 1))
proof end;

theorem Th19: :: IRRAT_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for seq being Real_Sequence
for sq being FinSequence of REAL st len sq = n & ( for k being Nat st k < n holds
seq . k = sq . (k + 1) ) & ( for k being Nat st k >= n holds
seq . k = 0 ) holds
( seq is summable & Sum seq = Sum sq )
proof end;

theorem Th20: :: IRRAT_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being Nat
for x, y being real number st x <> 0 & y <> 0 & k <= n holds
(x,y In_Power n) . (k + 1) = ((n choose k) * (x .^. (n - k))) * (y .^. k)
proof end;

theorem Th21: :: IRRAT_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k being Nat st n > 0 & k <= n holds
(cseq n) . k = (1,(1 / n) In_Power n) . (k + 1)
proof end;

theorem Th22: :: IRRAT_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat st n > 0 holds
( cseq n is summable & Sum (cseq n) = (1 + (1 / n)) .^. n & Sum (cseq n) = dseq . n )
proof end;

theorem Th23: :: IRRAT_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( dseq is convergent & lim dseq = number_e )
proof end;

theorem Th24: :: IRRAT_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( eseq is summable & Sum eseq = exp 1 )
proof end;

theorem Th25: :: IRRAT_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Nat
for dseqK being Real_Sequence st ( for n being Nat holds dseqK . n = (Partial_Sums (cseq n)) . K ) holds
( dseqK is convergent & lim dseqK = (Partial_Sums eseq ) . K )
proof end;

theorem Th26: :: IRRAT_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Nat st
for n being Nat st n >= N holds
seq . n > x - eps
proof end;

theorem Th27: :: IRRAT_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number
for seq being Real_Sequence st ( for eps being real number st eps > 0 holds
ex N being Nat st
for n being Nat st n >= N holds
seq . n > x - eps ) & ex N being Nat st
for n being Nat st n >= N holds
seq . n <= x holds
( seq is convergent & lim seq = x )
proof end;

theorem Th28: :: IRRAT_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for seq being Real_Sequence st seq is summable holds
for eps being real number st eps > 0 holds
ex K being Nat st (Partial_Sums seq) . K > (Sum seq) - eps
proof end;

theorem Th29: :: IRRAT_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat st n >= 1 holds
dseq . n <= Sum eseq
proof end;

theorem Th30: :: IRRAT_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Nat
for seq being Real_Sequence st seq is summable & ( for k being Nat holds seq . k >= 0 ) holds
Sum seq >= (Partial_Sums seq) . K
proof end;

theorem Th31: :: IRRAT_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( dseq is convergent & lim dseq = Sum eseq )
proof end;

definition
redefine func number_e equals :Def6: :: IRRAT_1:def 6
Sum eseq ;
compatibility
for b1 being set holds
( b1 = number_e iff b1 = Sum eseq )
by Th23, Th31;
end;

:: deftheorem Def6 defines number_e IRRAT_1:def 6 :
number_e = Sum eseq ;

definition
redefine func number_e equals :: IRRAT_1:def 7
exp 1;
compatibility
for b1 being set holds
( b1 = number_e iff b1 = exp 1 )
by Def6, Th24;
end;

:: deftheorem defines number_e IRRAT_1:def 7 :
number_e = exp 1;

theorem Th32: :: IRRAT_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st not x is irrational holds
ex n being Nat st
( n >= 2 & (n ! ) * x is integer )
proof end;

theorem Th33: :: IRRAT_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k being Nat holds (n ! ) * (eseq . k) = (n ! ) / (k ! )
proof end;

theorem :: IRRAT_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k being Nat holds (n ! ) / (k ! ) > 0
proof end;

theorem Th35: :: IRRAT_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for seq being Real_Sequence st seq is summable & ( for n being Nat holds seq . n > 0 ) holds
Sum seq > 0
proof end;

theorem Th36: :: IRRAT_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds (n ! ) * (Sum (eseq ^\ (n + 1))) > 0
proof end;

theorem Th37: :: IRRAT_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being Nat st k <= n holds
(n ! ) / (k ! ) is integer
proof end;

theorem Th38: :: IRRAT_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds (n ! ) * ((Partial_Sums eseq ) . n) is integer
proof end;

theorem Th39: :: IRRAT_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k being Nat
for x being real number st x = 1 / (n + 1) holds
(n ! ) / (((n + k) + 1) ! ) <= x .^. (k + 1)
proof end;

theorem Th40: :: IRRAT_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for x being real number st n > 0 & x = 1 / (n + 1) holds
(n ! ) * (Sum (eseq ^\ (n + 1))) <= x / (1 - x)
proof end;

theorem Th41: :: IRRAT_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, n being real number st n >= 2 & x = 1 / (n + 1) holds
x / (1 - x) < 1
proof end;

theorem :: IRRAT_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
number_e is irrational
proof end;