:: IRRAT_1 semantic presentation

notation

let c₁ be real number ;
antonym irrational c₁ for rational c₁;

end;

notation

let c₁, c₂ be real number ;
synonym c₁ .^. c₂ for c₁ to_power c₂;

end;

theorem Th1: :: IRRAT_1:1

for b₁ being Nat st b₁ is prime holds
sqrt b₁ is irrational

proof end;

theorem Th2: :: IRRAT_1:2

ex b₁, b₂ being real number st
( b₁ is irrational & b₂ is irrational & not b₁ .^. b₂ is irrational )

proof end;

scheme :: IRRAT_1:sch 1
s1{ F₁( set ) -> real number } :

( ex b₁ being Real_Sequence st
for b₂ being Nat holds b₁ . b₂ = F₁(b₂) & ( for b₁, b₂ being Real_Sequence st ( for b₃ being Nat holds b₁ . b₃ = F₁(b₃) ) & ( for b₃ being Nat holds b₂ . b₃ = F₁(b₃) ) holds
b₁ = b₂ ) )

proof end;

definition

let c₁ be Nat;
func aseq c₁ -> Real_Sequence means :Def1: :: IRRAT_1:def 1
for b₁ being Nat holds a₂ . b₁ = (b₁ - a₁) / b₁;
correctness

proof end;

end;

:: deftheorem Def1 defines aseq IRRAT_1:def 1 :

definition

let c₁ be Nat;
func bseq c₁ -> Real_Sequence means :Def2: :: IRRAT_1:def 2
for b₁ being Nat holds a₂ . b₁ = (b₁ choose a₁) * (b₁ .^. (- a₁));
correctness

proof end;

end;

:: deftheorem Def2 defines bseq IRRAT_1:def 2 :

definition

let c₁ be Nat;
func cseq c₁ -> Real_Sequence means :Def3: :: IRRAT_1:def 3
for b₁ being Nat holds a₂ . b₁ = (a₁ choose b₁) * (a₁ .^. (- b₁));
correctness

proof end;

end;

:: deftheorem Def3 defines cseq IRRAT_1:def 3 :

theorem Th3: :: IRRAT_1:3

for b₁, b₂ being Nat holds (cseq b₁) . b₂ = (bseq b₂) . b₁

proof end;

definition

func dseq -> Real_Sequence means :Def4: :: IRRAT_1:def 4
for b₁ being Nat holds a₁ . b₁ = (1 + (1 / b₁)) .^. b₁;
correctness

proof end;

end;

:: deftheorem Def4 defines dseq IRRAT_1:def 4 :

definition

func eseq -> Real_Sequence means :Def5: :: IRRAT_1:def 5
for b₁ being Nat holds a₁ . b₁ = 1 / (b₁ ! );
correctness

proof end;

end;

:: deftheorem Def5 defines eseq IRRAT_1:def 5 :

theorem Th4: :: IRRAT_1:4

for b₁, b₂ being Nat st b₁ > 0 holds
b₁ .^. (- (b₂ + 1)) = (b₁ .^. (- b₂)) / b₁

proof end;

Lemma9: for b₁, b₂, b₃, b₄, b₅ being real number holds b₁ / ((b₂ * b₃) * (b₄ / b₅)) = (b₅ / b₃) * (b₁ / (b₂ * b₄))
by XCMPLX_1:235;

theorem Th5: :: IRRAT_1:5

canceled;

theorem Th6: :: IRRAT_1:6

for b₁, b₂ being Nat holds b₁ choose (b₂ + 1) = ((b₁ - b₂) / (b₂ + 1)) * (b₁ choose b₂)

proof end;

theorem Th7: :: IRRAT_1:7

for b₁, b₂ being Nat st b₁ > 0 holds
(bseq (b₂ + 1)) . b₁ = ((1 / (b₂ + 1)) * ((bseq b₂) . b₁)) * ((aseq b₂) . b₁)

proof end;

theorem Th8: :: IRRAT_1:8

for b₁, b₂ being Nat st b₁ > 0 holds
(aseq b₂) . b₁ = 1 - (b₂ / b₁)

proof end;

theorem Th9: :: IRRAT_1:9

for b₁ being Nat holds
( aseq b₁ is convergent & lim (aseq b₁) = 1 )

proof end;

theorem Th10: :: IRRAT_1:10

for b₁ being real number
for b₂ being Real_Sequence st ( for b₃ being Nat holds b₂ . b₃ = b₁ ) holds
( b₂ is convergent & lim b₂ = b₁ )

proof end;

theorem Th11: :: IRRAT_1:11

for b₁ being Nat holds (bseq 0) . b₁ = 1

proof end;

theorem Th12: :: IRRAT_1:12

for b₁ being Nat holds (1 / (b₁ + 1)) * (1 / (b₁ ! )) = 1 / ((b₁ + 1) ! )

proof end;

theorem Th13: :: IRRAT_1:13

for b₁ being Nat holds
( bseq b₁ is convergent & lim (bseq b₁) = 1 / (b₁ ! ) & lim (bseq b₁) = eseq . b₁ )

proof end;

theorem Th14: :: IRRAT_1:14

for b₁, b₂ being Nat st b₁ < b₂ holds
( 0 < (aseq b₁) . b₂ & (aseq b₁) . b₂ <= 1 )

proof end;

theorem Th15: :: IRRAT_1:15

for b₁, b₂ being Nat st b₁ > 0 holds
( 0 <= (bseq b₂) . b₁ & (bseq b₂) . b₁ <= 1 / (b₂ ! ) & (bseq b₂) . b₁ <= eseq . b₂ & 0 <= (cseq b₁) . b₂ & (cseq b₁) . b₂ <= 1 / (b₂ ! ) & (cseq b₁) . b₂ <= eseq . b₂ )

proof end;

theorem Th16: :: IRRAT_1:16

for b₁ being Real_Sequence st b₁ ^\ 1 is summable holds
( b₁ is summable & Sum b₁ = (b₁ . 0) + (Sum (b₁ ^\ 1)) )

proof end;

theorem Th17: :: IRRAT_1:17

for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence of b₂ st 1 <= b₁ & b₁ < len b₃ holds
(b₃ /^ 1) . b₁ = b₃ . (b₁ + 1)

proof end;

theorem Th18: :: IRRAT_1:18

for b₁ being FinSequence of REAL st len b₁ > 0 holds
Sum b₁ = (b₁ . 1) + (Sum (b₁ /^ 1))

proof end;

theorem Th19: :: IRRAT_1:19

for b₁ being Nat
for b₂ being Real_Sequence
for b₃ being FinSequence of REAL st len b₃ = b₁ & ( for b₄ being Nat st b₄ < b₁ holds
b₂ . b₄ = b₃ . (b₄ + 1) ) & ( for b₄ being Nat st b₄ >= b₁ holds
b₂ . b₄ = 0 ) holds
( b₂ is summable & Sum b₂ = Sum b₃ )

proof end;

theorem Th20: :: IRRAT_1:20

for b₁, b₂ being Nat
for b₃, b₄ being real number st b₃ <> 0 & b₄ <> 0 & b₁ <= b₂ holds
(b₃,b₄ In_Power b₂) . (b₁ + 1) = ((b₂ choose b₁) * (b₃ .^. (b₂ - b₁))) * (b₄ .^. b₁)

proof end;

theorem Th21: :: IRRAT_1:21

for b₁, b₂ being Nat st b₁ > 0 & b₂ <= b₁ holds
(cseq b₁) . b₂ = (1,(1 / b₁) In_Power b₁) . (b₂ + 1)

proof end;

theorem Th22: :: IRRAT_1:22

for b₁ being Nat st b₁ > 0 holds
( cseq b₁ is summable & Sum (cseq b₁) = (1 + (1 / b₁)) .^. b₁ & Sum (cseq b₁) = dseq . b₁ )

proof end;

theorem Th23: :: IRRAT_1:23

( dseq is convergent & lim dseq = number_e )

proof end;

theorem Th24: :: IRRAT_1:24

( eseq is summable & Sum eseq = exp 1 )

proof end;

theorem Th25: :: IRRAT_1:25

for b₁ being Nat
for b₂ being Real_Sequence st ( for b₃ being Nat holds b₂ . b₃ = (Partial_Sums (cseq b₃)) . b₁ ) holds
( b₂ is convergent & lim b₂ = (Partial_Sums eseq ) . b₁ )

proof end;

theorem Th26: :: IRRAT_1:26

for b₁ being real number
for b₂ being Real_Sequence st b₂ is convergent & lim b₂ = b₁ holds
for b₃ being real number st b₃ > 0 holds
ex b₄ being Nat st
for b₅ being Nat st b₅ >= b₄ holds
b₂ . b₅ > b₁ - b₃

proof end;

theorem Th27: :: IRRAT_1:27

for b₁ being real number
for b₂ being Real_Sequence st ( for b₃ being real number st b₃ > 0 holds
ex b₄ being Nat st
for b₅ being Nat st b₅ >= b₄ holds
b₂ . b₅ > b₁ - b₃ ) & ex b₃ being Nat st
for b₄ being Nat st b₄ >= b₃ holds
b₂ . b₄ <= b₁ holds
( b₂ is convergent & lim b₂ = b₁ )

proof end;

theorem Th28: :: IRRAT_1:28

for b₁ being Real_Sequence st b₁ is summable holds
for b₂ being real number st b₂ > 0 holds
ex b₃ being Nat st (Partial_Sums b₁) . b₃ > (Sum b₁) - b₂

proof end;

theorem Th29: :: IRRAT_1:29

for b₁ being Nat st b₁ >= 1 holds
dseq . b₁ <= Sum eseq

proof end;

theorem Th30: :: IRRAT_1:30

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is summable & ( for b₃ being Nat holds b₂ . b₃ >= 0 ) holds
Sum b₂ >= (Partial_Sums b₂) . b₁

proof end;

theorem Th31: :: IRRAT_1:31

( dseq is convergent & lim dseq = Sum eseq )

proof end;

definition

redefine func number_e -> set equals :Def6: :: IRRAT_1:def 6
Sum eseq ;
compatibility by Th23, Th31;

end;

:: deftheorem Def6 defines number_e IRRAT_1:def 6 :

definition

redefine func number_e -> set equals :: IRRAT_1:def 7
exp 1;
compatibility by Def6, Th24;

end;

:: deftheorem Def7 defines number_e IRRAT_1:def 7 :

theorem Th32: :: IRRAT_1:32

for b₁ being real number st not b₁ is irrational holds
ex b₂ being Nat st
( b₂ >= 2 & (b₂ ! ) * b₁ is integer )

proof end;

theorem Th33: :: IRRAT_1:33

for b₁, b₂ being Nat holds (b₁ ! ) * (eseq . b₂) = (b₁ ! ) / (b₂ ! )

proof end;

theorem Th34: :: IRRAT_1:34

for b₁, b₂ being Nat holds (b₁ ! ) / (b₂ ! ) > 0

proof end;

theorem Th35: :: IRRAT_1:35

for b₁ being Real_Sequence st b₁ is summable & ( for b₂ being Nat holds b₁ . b₂ > 0 ) holds
Sum b₁ > 0

proof end;

theorem Th36: :: IRRAT_1:36

for b₁ being Nat holds (b₁ ! ) * (Sum (eseq ^\ (b₁ + 1))) > 0

proof end;

theorem Th37: :: IRRAT_1:37

for b₁, b₂ being Nat st b₁ <= b₂ holds
(b₂ ! ) / (b₁ ! ) is integer

proof end;

theorem Th38: :: IRRAT_1:38

for b₁ being Nat holds (b₁ ! ) * ((Partial_Sums eseq ) . b₁) is integer

proof end;

theorem Th39: :: IRRAT_1:39

for b₁, b₂ being Nat
for b₃ being real number st b₃ = 1 / (b₁ + 1) holds
(b₁ ! ) / (((b₁ + b₂) + 1) ! ) <= b₃ .^. (b₂ + 1)

proof end;

theorem Th40: :: IRRAT_1:40

for b₁ being Nat
for b₂ being real number st b₁ > 0 & b₂ = 1 / (b₁ + 1) holds
(b₁ ! ) * (Sum (eseq ^\ (b₁ + 1))) <= b₂ / (1 - b₂)

proof end;

theorem Th41: :: IRRAT_1:41

for b₁, b₂ being real number st b₂ >= 2 & b₁ = 1 / (b₂ + 1) holds
b₁ / (1 - b₁) < 1

proof end;

theorem Th42: :: IRRAT_1:42

number_e is irrational

proof end;