:: FIB_NUM2 semantic presentation

theorem Th1: :: FIB_NUM2:1

for b₁ being non empty Nat holds (b₁ -' 1) + 2 = b₁ + 1

proof end;

theorem Th2: :: FIB_NUM2:2

for b₁ being odd Integer
for b₂ being non empty real number holds (- b₂) to_power b₁ = - (b₂ to_power b₁)

proof end;

theorem Th3: :: FIB_NUM2:3

for b₁ being odd Integer holds (- 1) to_power b₁ = - 1

proof end;

theorem Th4: :: FIB_NUM2:4

for b₁ being even Integer
for b₂ being non empty real number holds (- b₂) to_power b₁ = b₂ to_power b₁

proof end;

theorem Th5: :: FIB_NUM2:5

for b₁ being even Integer holds (- 1) to_power b₁ = 1

proof end;

theorem Th6: :: FIB_NUM2:6

for b₁ being non empty real number
for b₂ being Integer holds ((- 1) * b₁) to_power b₂ = ((- 1) to_power b₂) * (b₁ to_power b₂)

proof end;

theorem Th7: :: FIB_NUM2:7

for b₁, b₂ being Nat
for b₃ being non empty real number holds b₃ to_power (b₁ + b₂) = (b₃ to_power b₁) * (b₃ to_power b₂)

proof end;

theorem Th8: :: FIB_NUM2:8

for b₁ being Nat
for b₂ being non empty real number
for b₃ being odd Integer holds (b₂ to_power b₃) to_power b₁ = b₂ to_power (b₃ * b₁)

proof end;

theorem Th9: :: FIB_NUM2:9

for b₁ being Nat holds ((- 1) to_power (- b₁)) ^2 = 1

proof end;

theorem Th10: :: FIB_NUM2:10

for b₁, b₂ being Nat
for b₃ being non empty real number holds (b₃ to_power (- b₁)) * (b₃ to_power (- b₂)) = b₃ to_power ((- b₁) - b₂)

proof end;

theorem Th11: :: FIB_NUM2:11

for b₁ being Nat holds (- 1) to_power (- (2 * b₁)) = 1

proof end;

theorem Th12: :: FIB_NUM2:12

for b₁ being Nat
for b₂ being non empty real number holds (b₂ to_power b₁) * (b₂ to_power (- b₁)) = 1

proof end;

registration

let c₁ be odd Integer;
cluster - a₁ -> odd ;
coherence

proof end;

end;

registration

let c₁ be even Integer;
cluster - a₁ -> even ;
coherence

proof end;

end;

theorem Th13: :: FIB_NUM2:13

for b₁ being Nat holds (- 1) to_power (- b₁) = (- 1) to_power b₁

proof end;

theorem Th14: :: FIB_NUM2:14

for b₁, b₂, b₃, b₄, b₅ being Nat st b₂ divides b₃ & b₂ divides b₁ holds
b₂ divides (b₃ * b₄) + (b₁ * b₅)

proof end;

registration

cluster non empty finite natural-membered with_non-empty_elements set ;
existence

proof end;

end;

registration

let c₁ be Function of NAT , NAT ;
let c₂ be finite natural-membered with_non-empty_elements set ;
cluster a₁ | a₂ -> FinSubsequence-like ;
coherence

proof end;

end;

theorem Th15: :: FIB_NUM2:15

for b₁ being FinSubsequence holds rng (Seq b₁) c= rng b₁

proof end;

definition

let c₁ be Function of NAT , NAT ;
let c₂ be finite natural-membered with_non-empty_elements set ;
func Prefix c₁,c₂ -> FinSequence of NAT equals :: FIB_NUM2:def 1
Seq (a₁ | a₂);
coherence

proof end;

end;

:: deftheorem Def1 defines Prefix FIB_NUM2:def 1 :

theorem Th16: :: FIB_NUM2:16

for b₁, b₂, b₃ being Nat st b₃ <> 0 & b₃ + b₁ <= b₂ holds
b₁ < b₂

proof end;

registration

cluster omega -> bounded_below ;
coherence

proof end;

end;

registration

cluster K417(1,2,3) -> natural-membered with_non-empty_elements ;
coherence

proof end;

end;

registration

cluster K418(1,2,3,4) -> natural-membered with_non-empty_elements ;
coherence

proof end;

end;

theorem Th17: :: FIB_NUM2:17

for b₁, b₂ being Nat
for b₃, b₄ being set st 0 < b₁ & b₁ < b₂ holds
{[b₁,b₃],[b₂,b₄]} is FinSubsequence

proof end;

theorem Th18: :: FIB_NUM2:18

for b₁, b₂ being Nat
for b₃, b₄ being set
for b₅ being FinSubsequence st b₁ < b₂ & b₅ = {[b₁,b₃],[b₂,b₄]} holds
Seq b₅ = <*b₃,b₄*>

proof end;

registration

let c₁ be Nat;
cluster Seg a₁ -> with_non-empty_elements ;
coherence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
cluster -> with_non-empty_elements Element of K40(a₁);
coherence

proof end;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be set ;
cluster a₁ /\ a₂ -> with_non-empty_elements ;
coherence

proof end;

cluster a₂ /\ a₁ -> with_non-empty_elements ;
coherence ;

end;

theorem Th19: :: FIB_NUM2:19

for b₁ being Nat
for b₂ being set st b₁ >= 1 holds
{[b₁,b₂]} is FinSubsequence

proof end;

theorem Th20: :: FIB_NUM2:20

for b₁ being Nat
for b₂ being set
for b₃ being FinSubsequence st b₃ = {[1,b₂]} holds
b₁ Shift b₃ = {[(1 + b₁),b₂]}

proof end;

theorem Th21: :: FIB_NUM2:21

for b₁ being FinSubsequence
for b₂, b₃ being Nat st dom b₁ c= Seg b₂ & b₃ > b₂ holds
ex b₄ being FinSequence st
( b₁ c= b₄ & dom b₄ = Seg b₃ )

proof end;

theorem Th22: :: FIB_NUM2:22

for b₁ being FinSubsequence ex b₂ being FinSequence st b₁ c= b₂

proof end;

scheme :: FIB_NUM2:sch 1
s1{ P₁[ Nat] } :

for b₁ being non empty Nat holds P₁[b₁]

provided

E22: P₁[1] and
E23: P₁[2] and
E24: for b₁ being non empty Nat st P₁[b₁] & P₁[b₁ + 1] holds
P₁[b₁ + 2]

proof end;

scheme :: FIB_NUM2:sch 2
s2{ P₁[ Nat] } :

for b₁ being non trivial Nat holds P₁[b₁]

provided

E22: P₁[2] and
E23: P₁[3] and
E24: for b₁ being non trivial Nat st P₁[b₁] & P₁[b₁ + 1] holds
P₁[b₁ + 2]

proof end;

theorem Th23: :: FIB_NUM2:23

Fib 2 = 1

proof end;

theorem Th24: :: FIB_NUM2:24

Fib 3 = 2

proof end;

theorem Th25: :: FIB_NUM2:25

Fib 4 = 3

proof end;

theorem Th26: :: FIB_NUM2:26

for b₁ being Nat holds Fib (b₁ + 2) = (Fib b₁) + (Fib (b₁ + 1))

proof end;

theorem Th27: :: FIB_NUM2:27

for b₁ being Nat holds Fib (b₁ + 3) = (Fib (b₁ + 2)) + (Fib (b₁ + 1))

proof end;

theorem Th28: :: FIB_NUM2:28

for b₁ being Nat holds Fib (b₁ + 4) = (Fib (b₁ + 2)) + (Fib (b₁ + 3))

proof end;

theorem Th29: :: FIB_NUM2:29

for b₁ being Nat holds Fib (b₁ + 5) = (Fib (b₁ + 3)) + (Fib (b₁ + 4))

proof end;

Lemma29: for b₁ being Nat holds Fib ((2 * (b₁ + 2)) + 1) = (Fib ((2 * b₁) + 3)) + (Fib ((2 * b₁) + 4))

proof end;

theorem Th30: :: FIB_NUM2:30

for b₁ being Nat holds Fib (b₁ + 2) = (Fib (b₁ + 3)) - (Fib (b₁ + 1))

proof end;

theorem Th31: :: FIB_NUM2:31

for b₁ being Nat holds Fib (b₁ + 1) = (Fib (b₁ + 2)) - (Fib b₁)

proof end;

theorem Th32: :: FIB_NUM2:32

for b₁ being Nat holds Fib b₁ = (Fib (b₁ + 2)) - (Fib (b₁ + 1))

proof end;

theorem Th33: :: FIB_NUM2:33

for b₁ being Nat holds ((Fib b₁) * (Fib (b₁ + 2))) - ((Fib (b₁ + 1)) ^2 ) = (- 1) |^ (b₁ + 1)

proof end;

theorem Th34: :: FIB_NUM2:34

for b₁ being non empty Nat holds ((Fib (b₁ -' 1)) * (Fib (b₁ + 1))) - ((Fib b₁) ^2 ) = (- 1) |^ b₁

proof end;

theorem Th35: :: FIB_NUM2:35

tau > 0

proof end;

theorem Th36: :: FIB_NUM2:36

tau_bar = (- tau ) to_power (- 1)

proof end;

theorem Th37: :: FIB_NUM2:37

for b₁ being Nat holds (- tau ) to_power ((- 1) * b₁) = ((- tau ) to_power (- 1)) to_power b₁

proof end;

theorem Th38: :: FIB_NUM2:38

- (1 / tau ) = tau_bar

proof end;

theorem Th39: :: FIB_NUM2:39

for b₁ being Nat holds (((tau to_power b₁) ^2 ) - (2 * ((- 1) to_power b₁))) + ((tau to_power (- b₁)) ^2 ) = ((tau to_power b₁) - (tau_bar to_power b₁)) ^2

proof end;

theorem Th40: :: FIB_NUM2:40

for b₁, b₂ being non empty Nat st b₂ <= b₁ holds
((Fib b₁) ^2 ) - ((Fib (b₁ + b₂)) * (Fib (b₁ -' b₂))) = ((- 1) |^ (b₁ -' b₂)) * ((Fib b₂) ^2 )

proof end;

theorem Th41: :: FIB_NUM2:41

for b₁ being Nat holds ((Fib b₁) ^2 ) + ((Fib (b₁ + 1)) ^2 ) = Fib ((2 * b₁) + 1)

proof end;

theorem Th42: :: FIB_NUM2:42

for b₁ being Nat
for b₂ being non empty Nat holds Fib (b₁ + b₂) = ((Fib b₂) * (Fib (b₁ + 1))) + ((Fib (b₂ -' 1)) * (Fib b₁))

proof end;

theorem Th43: :: FIB_NUM2:43

for b₁ being Nat
for b₂ being non empty Nat holds Fib b₂ divides Fib (b₂ * b₁)

proof end;

theorem Th44: :: FIB_NUM2:44

for b₁ being Nat
for b₂ being non empty Nat st b₂ divides b₁ holds
Fib b₂ divides Fib b₁

proof end;

theorem Th45: :: FIB_NUM2:45

for b₁ being Nat holds Fib b₁ <= Fib (b₁ + 1)

proof end;

theorem Th46: :: FIB_NUM2:46

for b₁ being Nat st b₁ > 1 holds
Fib b₁ < Fib (b₁ + 1)

proof end;

theorem Th47: :: FIB_NUM2:47

for b₁, b₂ being Nat st b₁ >= b₂ holds
Fib b₁ >= Fib b₂

proof end;

theorem Th48: :: FIB_NUM2:48

for b₁, b₂ being Nat st b₂ > 1 & b₂ < b₁ holds
Fib b₂ < Fib b₁

proof end;

theorem Th49: :: FIB_NUM2:49

for b₁ being Nat holds
( Fib b₁ = 1 iff ( b₁ = 1 or b₁ = 2 ) )

proof end;

theorem Th50: :: FIB_NUM2:50

for b₁, b₂ being Nat st b₂ > 1 & b₁ <> 0 & b₁ <> 1 & ( ( b₁ <> 1 & b₂ <> 2 ) or ( b₁ <> 2 & b₂ <> 1 ) ) holds
( Fib b₁ = Fib b₂ iff b₁ = b₂ )

proof end;

theorem Th51: :: FIB_NUM2:51

for b₁ being Nat st b₁ > 1 & b₁ <> 4 & not b₁ is prime holds
ex b₂ being non empty Nat st
( b₂ <> 1 & b₂ <> 2 & b₂ <> b₁ & b₂ divides b₁ )

proof end;

theorem Th52: :: FIB_NUM2:52

for b₁ being Nat st b₁ > 1 & b₁ <> 4 & Fib b₁ is prime holds
b₁ is prime

proof end;

definition

func FIB -> Function of NAT , NAT means :Def2: :: FIB_NUM2:def 2
for b₁ being Nat holds a₁ . b₁ = Fib b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines FIB FIB_NUM2:def 2 :

definition

func EvenNAT -> Subset of NAT equals :: FIB_NUM2:def 3
{ (2 * b₁) where B is Nat : verum } ;
coherence

proof end;

func OddNAT -> Subset of NAT equals :: FIB_NUM2:def 4
{ ((2 * b₁) + 1) where B is Nat : verum } ;
coherence

proof end;

end;

:: deftheorem Def3 defines EvenNAT FIB_NUM2:def 3 :

:: deftheorem Def4 defines OddNAT FIB_NUM2:def 4 :

theorem Th53: :: FIB_NUM2:53

for b₁ being Nat holds
( 2 * b₁ in EvenNAT & not (2 * b₁) + 1 in EvenNAT )

proof end;

theorem Th54: :: FIB_NUM2:54

for b₁ being Nat holds
( (2 * b₁) + 1 in OddNAT & not 2 * b₁ in OddNAT )

proof end;

definition

let c₁ be Nat;
func EvenFibs c₁ -> FinSequence of NAT equals :: FIB_NUM2:def 5
Prefix FIB ,(EvenNAT /\ (Seg a₁));
coherence ;
func OddFibs c₁ -> FinSequence of NAT equals :: FIB_NUM2:def 6
Prefix FIB ,(OddNAT /\ (Seg a₁));
coherence ;

end;

:: deftheorem Def5 defines EvenFibs FIB_NUM2:def 5 :

:: deftheorem Def6 defines OddFibs FIB_NUM2:def 6 :

theorem Th55: :: FIB_NUM2:55

EvenFibs 0 = {}

proof end;

theorem Th56: :: FIB_NUM2:56

Seq (FIB | {2}) = <*1*>

proof end;

theorem Th57: :: FIB_NUM2:57

EvenFibs 2 = <*1*>

proof end;

theorem Th58: :: FIB_NUM2:58

EvenFibs 4 = <*1,3*>

proof end;

theorem Th59: :: FIB_NUM2:59

for b₁ being Nat holds (EvenNAT /\ (Seg ((2 * b₁) + 2))) \/ {((2 * b₁) + 4)} = EvenNAT /\ (Seg ((2 * b₁) + 4))

proof end;

theorem Th60: :: FIB_NUM2:60

for b₁ being Nat holds (FIB | (EvenNAT /\ (Seg ((2 * b₁) + 2)))) \/ {[((2 * b₁) + 4),(FIB . ((2 * b₁) + 4))]} = FIB | (EvenNAT /\ (Seg ((2 * b₁) + 4)))

proof end;

theorem Th61: :: FIB_NUM2:61

for b₁ being Nat holds EvenFibs ((2 * b₁) + 2) = (EvenFibs (2 * b₁)) ^ <*(Fib ((2 * b₁) + 2))*>

proof end;

theorem Th62: :: FIB_NUM2:62

OddFibs 1 = <*1*>

proof end;

theorem Th63: :: FIB_NUM2:63

OddFibs 3 = <*1,2*>

proof end;

theorem Th64: :: FIB_NUM2:64

for b₁ being Nat holds (OddNAT /\ (Seg ((2 * b₁) + 3))) \/ {((2 * b₁) + 5)} = OddNAT /\ (Seg ((2 * b₁) + 5))

proof end;

theorem Th65: :: FIB_NUM2:65

for b₁ being Nat holds (FIB | (OddNAT /\ (Seg ((2 * b₁) + 3)))) \/ {[((2 * b₁) + 5),(FIB . ((2 * b₁) + 5))]} = FIB | (OddNAT /\ (Seg ((2 * b₁) + 5)))

proof end;

theorem Th66: :: FIB_NUM2:66

for b₁ being Nat holds OddFibs ((2 * b₁) + 3) = (OddFibs ((2 * b₁) + 1)) ^ <*(Fib ((2 * b₁) + 3))*>

proof end;

theorem Th67: :: FIB_NUM2:67

for b₁ being Nat holds Sum (EvenFibs ((2 * b₁) + 2)) = (Fib ((2 * b₁) + 3)) - 1

proof end;

theorem Th68: :: FIB_NUM2:68

for b₁ being Nat holds Sum (OddFibs ((2 * b₁) + 1)) = Fib ((2 * b₁) + 2)

proof end;

theorem Th69: :: FIB_NUM2:69

for b₁ being Nat holds Fib b₁, Fib (b₁ + 1) are_relative_prime

proof end;

theorem Th70: :: FIB_NUM2:70

for b₁ being non empty Nat
for b₂ being Nat st b₂ <> 1 & b₂ divides Fib b₁ holds
not b₂ divides Fib (b₁ -' 1)

proof end;

theorem Th71: :: FIB_NUM2:71

for b₁ being Nat
for b₂ being non empty Nat st b₁ is prime & b₂ is prime & b₁ divides Fib b₂ holds
for b₃ being Nat st b₃ < b₂ & b₃ <> 0 holds
not b₁ divides Fib b₃

proof end;

theorem Th72: :: FIB_NUM2:72

for b₁ being non empty Nat holds {((Fib b₁) * (Fib (b₁ + 3))),((2 * (Fib (b₁ + 1))) * (Fib (b₁ + 2))),(((Fib (b₁ + 1)) ^2 ) + ((Fib (b₁ + 2)) ^2 ))} is Pythagorean_triple

proof end;