:: by Freek Wiedijk

::

:: Received July 2, 1999

:: Copyright (c) 1999-2021 Association of Mizar Users

:: The Irrationality of the Square Root of 2

scheme :: IRRAT_1:sch 1

LambdaRealSeq{ F_{1}( set ) -> Real } :

LambdaRealSeq{ F

( ex seq being Real_Sequence st

for n being Nat holds seq . n = F_{1}(n) & ( for seq1, seq2 being Real_Sequence st ( for n being Nat holds seq1 . n = F_{1}(n) ) & ( for n being Nat holds seq2 . n = F_{1}(n) ) holds

seq1 = seq2 ) )

for n being Nat holds seq . n = F

seq1 = seq2 ) )

proof end;

definition

let k be Nat;

existence

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = (n - k) / n;

uniqueness

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = (n - k) / n ) & ( for n being Nat holds b_{2} . n = (n - k) / n ) holds

b_{1} = b_{2};

existence

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = (n choose k) * (n ^ (- k));

uniqueness

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = (n choose k) * (n ^ (- k)) ) & ( for n being Nat holds b_{2} . n = (n choose k) * (n ^ (- k)) ) holds

b_{1} = b_{2};

end;
func aseq k -> Real_Sequence means :Def1: :: IRRAT_1:def 1

for n being Nat holds it . n = (n - k) / n;

correctness for n being Nat holds it . n = (n - k) / n;

existence

ex b

for n being Nat holds b

uniqueness

for b

b

proof end;

func bseq k -> Real_Sequence means :Def2: :: IRRAT_1:def 2

for n being Nat holds it . n = (n choose k) * (n ^ (- k));

correctness for n being Nat holds it . n = (n choose k) * (n ^ (- k));

existence

ex b

for n being Nat holds b

uniqueness

for b

b

proof end;

:: deftheorem Def1 defines aseq IRRAT_1:def 1 :

for k being Nat

for b_{2} being Real_Sequence holds

( b_{2} = aseq k iff for n being Nat holds b_{2} . n = (n - k) / n );

for k being Nat

for b

( b

:: deftheorem Def2 defines bseq IRRAT_1:def 2 :

for k being Nat

for b_{2} being Real_Sequence holds

( b_{2} = bseq k iff for n being Nat holds b_{2} . n = (n choose k) * (n ^ (- k)) );

for k being Nat

for b

( b

definition

let n be Nat;

existence

ex b_{1} being Real_Sequence st

for k being Nat holds b_{1} . k = (n choose k) * (n ^ (- k));

uniqueness

for b_{1}, b_{2} being Real_Sequence st ( for k being Nat holds b_{1} . k = (n choose k) * (n ^ (- k)) ) & ( for k being Nat holds b_{2} . k = (n choose k) * (n ^ (- k)) ) holds

b_{1} = b_{2};

end;
func cseq n -> Real_Sequence means :Def3: :: IRRAT_1:def 3

for k being Nat holds it . k = (n choose k) * (n ^ (- k));

correctness for k being Nat holds it . k = (n choose k) * (n ^ (- k));

existence

ex b

for k being Nat holds b

uniqueness

for b

b

proof end;

:: deftheorem Def3 defines cseq IRRAT_1:def 3 :

for n being Nat

for b_{2} being Real_Sequence holds

( b_{2} = cseq n iff for k being Nat holds b_{2} . k = (n choose k) * (n ^ (- k)) );

for n being Nat

for b

( b

definition

existence

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = (1 + (1 / n)) ^ n;

uniqueness

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = (1 + (1 / n)) ^ n ) & ( for n being Nat holds b_{2} . n = (1 + (1 / n)) ^ n ) holds

b_{1} = b_{2};

end;

func dseq -> Real_Sequence means :Def4: :: IRRAT_1:def 4

for n being Nat holds it . n = (1 + (1 / n)) ^ n;

correctness for n being Nat holds it . n = (1 + (1 / n)) ^ n;

existence

ex b

for n being Nat holds b

uniqueness

for b

b

proof end;

:: deftheorem Def4 defines dseq IRRAT_1:def 4 :

for b_{1} being Real_Sequence holds

( b_{1} = dseq iff for n being Nat holds b_{1} . n = (1 + (1 / n)) ^ n );

for b

( b

definition

correctness

existence

ex b_{1} being Real_Sequence st

for k being Nat holds b_{1} . k = 1 / (k !);

uniqueness

for b_{1}, b_{2} being Real_Sequence st ( for k being Nat holds b_{1} . k = 1 / (k !) ) & ( for k being Nat holds b_{2} . k = 1 / (k !) ) holds

b_{1} = b_{2};

end;
existence

ex b

for k being Nat holds b

uniqueness

for b

b

proof end;

:: deftheorem Def5 defines eseq IRRAT_1:def 5 :

for b_{1} being Real_Sequence holds

( b_{1} = eseq iff for k being Nat holds b_{1} . k = 1 / (k !) );

for b

( b

:: lim(n:(n choose k)*(n ^ (-k))) = 1/(k!)

theorem Th6: :: IRRAT_1:6

for k, n being Nat st n > 0 holds

(bseq (k + 1)) . n = ((1 / (k + 1)) * ((bseq k) . n)) * ((aseq k) . n)

(bseq (k + 1)) . n = ((1 / (k + 1)) * ((bseq k) . n)) * ((aseq k) . n)

proof end;

theorem Th9: :: IRRAT_1:9

for x being Real

for seq being Real_Sequence st ( for n being Nat holds seq . n = x ) holds

( seq is convergent & lim seq = x )

for seq being Real_Sequence st ( for n being Nat holds seq . n = x ) holds

( seq is convergent & lim seq = x )

proof end;

:: 0 <= (n choose k)*(n ^ (-k))) <= 1/(k!)

theorem Th14: :: IRRAT_1:14

for k, n 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 )

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

:: n>0 implies (1+(1/n)) ^ n = Sum (k:(n choose k)*(n ^ (-k)))

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)) )

( seq is summable & Sum seq = (seq . 0) + (Sum (seq ^\ 1)) )

proof end;

theorem Th16: :: IRRAT_1:16

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)

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

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 )

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 Th19: :: IRRAT_1:19

for k, n being Nat

for x, y being Real st k <= n holds

((x,y) In_Power n) . (k + 1) = ((n choose k) * (x ^ (n - k))) * (y ^ k)

for x, y being Real st 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

for n being Nat st n > 0 holds

( cseq n is summable & Sum (cseq n) = (1 + (1 / n)) ^ n & Sum (cseq n) = dseq . n )

( cseq n is summable & Sum (cseq n) = (1 + (1 / n)) ^ n & Sum (cseq n) = dseq . n )

proof end;

:: number_e = lim(n:(1+(1/n)) ^ n)

:: exp(1) = Sum (k:1/(k!))

:: lim(n:(1+(1/n)) ^ n) = Sum (k:1/(k!))

theorem Th24: :: IRRAT_1:24

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 )

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 Th25: :: IRRAT_1:25

for x being Real

for seq being Real_Sequence st seq is convergent & lim seq = x holds

for eps being Real st eps > 0 holds

ex N being Nat st

for n being Nat st n >= N holds

seq . n > x - eps

for seq being Real_Sequence st seq is convergent & lim seq = x holds

for eps being Real st eps > 0 holds

ex N being Nat st

for n being Nat st n >= N holds

seq . n > x - eps

proof end;

theorem Th26: :: IRRAT_1:26

for x being Real

for seq being Real_Sequence st ( for eps being Real 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 )

for seq being Real_Sequence st ( for eps being Real 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 Th27: :: IRRAT_1:27

for seq being Real_Sequence st seq is summable holds

for eps being Real st eps > 0 holds

ex K being Nat st (Partial_Sums seq) . K > (Sum seq) - eps

for eps being Real st eps > 0 holds

ex K being Nat st (Partial_Sums seq) . K > (Sum seq) - eps

proof end;

theorem Th29: :: IRRAT_1:29

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

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;

:: number_e = exp(1)

definition
end;

definition
end;

theorem Th34: :: IRRAT_1:34

for seq being Real_Sequence st seq is summable & ( for n being Nat holds seq . n > 0 ) holds

Sum seq > 0

Sum seq > 0

proof end;

theorem Th38: :: IRRAT_1:38

for k, n being Nat

for x being Real st x = 1 / (n + 1) holds

(n !) / (((n + k) + 1) !) <= x ^ (k + 1)

for x being Real st x = 1 / (n + 1) holds

(n !) / (((n + k) + 1) !) <= x ^ (k + 1)

proof end;

theorem Th39: :: IRRAT_1:39

for n being Nat

for x being Real st n > 0 & x = 1 / (n + 1) holds

(n !) * (Sum (eseq ^\ (n + 1))) <= x / (1 - x)

for x being Real st n > 0 & x = 1 / (n + 1) holds

(n !) * (Sum (eseq ^\ (n + 1))) <= x / (1 - x)

proof end;