:: FIB_NUM semantic presentation

theorem Th1: :: FIB_NUM:1

for b₁, b₂ being Nat holds b₁ hcf b₂ = b₁ hcf (b₂ + b₁)

proof end;

theorem Th2: :: FIB_NUM:2

for b₁, b₂, b₃ being Nat st b₁ hcf b₂ = 1 holds
b₁ hcf (b₂ * b₃) = b₁ hcf b₃

proof end;

theorem Th3: :: FIB_NUM:3

for b₁ being real number st b₁ > 0 holds
ex b₂ being Nat st
( b₂ > 0 & 0 < 1 / b₂ & 1 / b₂ <= b₁ )

proof end;

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

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

provided

E4: P₁[0] and
E5: P₁[1] and
E6: for b₁ being Nat st P₁[b₁] & P₁[b₁ + 1] holds
P₁[b₁ + 2]

proof end;

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

for b₁, b₂ being Nat holds P₁[b₁,b₂]

provided

E4: for b₁, b₂ being Nat st P₁[b₁,b₂] holds
P₁[b₂,b₁] and
E5: for b₁ being Nat st ( for b₂, b₃ being Nat st b₂ < b₁ & b₃ < b₁ holds
P₁[b₂,b₃] ) holds
for b₂ being Nat st b₂ <= b₁ holds
P₁[b₁,b₂]

proof end;

(0 + 1) + 1 = 2
;

then Lemma4: Fib 2 = 1
by PRE_FF:1;

Lemma5: (1 + 1) + 1 = 3
;

Lemma6: for b₁ being Nat holds Fib (b₁ + 1) >= b₁

proof end;

Lemma7: for b₁ being Nat holds Fib (b₁ + 1) >= Fib b₁

proof end;

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

proof end;

Lemma9: for b₁ being Nat holds Fib (b₁ + 1) <> 0

proof end;

theorem Th4: :: FIB_NUM:4

for b₁, b₂ being Nat holds Fib (b₁ + (b₂ + 1)) = ((Fib b₂) * (Fib b₁)) + ((Fib (b₂ + 1)) * (Fib (b₁ + 1)))

proof end;

Lemma11: for b₁ being Nat holds (Fib b₁) hcf (Fib (b₁ + 1)) = 1

proof end;

theorem Th5: :: FIB_NUM:5

for b₁, b₂ being Nat holds (Fib b₁) hcf (Fib b₂) = Fib (b₁ hcf b₂)

proof end;

theorem Th6: :: FIB_NUM:6

for b₁, b₂, b₃, b₄ being real number st b₂ <> 0 & delta b₂,b₃,b₄ >= 0 holds
( ((b₂ * (b₁ ^2 )) + (b₃ * b₁)) + b₄ = 0 iff ( b₁ = ((- b₃) - (sqrt (delta b₂,b₃,b₄))) / (2 * b₂) or b₁ = ((- b₃) + (sqrt (delta b₂,b₃,b₄))) / (2 * b₂) ) )

proof end;

definition

func tau -> real number equals :: FIB_NUM:def 1
(1 + (sqrt 5)) / 2;
correctness ;

end;

:: deftheorem Def1 defines tau FIB_NUM:def 1 :

definition

func tau_bar -> real number equals :: FIB_NUM:def 2
(1 - (sqrt 5)) / 2;
correctness ;

end;

:: deftheorem Def2 defines tau_bar FIB_NUM:def 2 :

Lemma13: ( tau ^2 = tau + 1 & tau_bar ^2 = tau_bar + 1 )

proof end;

Lemma14: 2 < sqrt 5
by SQUARE_1:85, SQUARE_1:95;

Lemma15: sqrt 5 <> 0
by SQUARE_1:85, SQUARE_1:95;

Lemma16: sqrt 5 < 3

proof end;

1 < tau

proof end;

then Lemma17: 0 < tau
by XREAL_1:2;

Lemma18: tau_bar < 0

proof end;

Lemma19: abs tau_bar < 1

proof end;

theorem Th7: :: FIB_NUM:7

for b₁ being Nat holds Fib b₁ = ((tau to_power b₁) - (tau_bar to_power b₁)) / (sqrt 5)

proof end;

Lemma21: for b₁ being Nat
for b₂ being real number st abs b₂ <= 1 holds
abs (b₂ |^ b₁) <= 1

proof end;

Lemma22: for b₁ being Nat holds abs ((tau_bar to_power b₁) / (sqrt 5)) < 1

proof end;

theorem Th8: :: FIB_NUM:8

for b₁ being Nat holds abs ((Fib b₁) - ((tau to_power b₁) / (sqrt 5))) < 1

proof end;

theorem Th9: :: FIB_NUM:9

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

proof end;

theorem Th10: :: FIB_NUM:10

for b₁, b₂, b₃ being Real_Sequence st b₂ is_not_0 holds
(b₁ /" b₂) (#) (b₂ /" b₃) = b₁ /" b₃

proof end;

theorem Th11: :: FIB_NUM:11

for b₁, b₂ being Real_Sequence
for b₃ being Nat holds
( (b₁ /" b₂) . b₃ = (b₁ . b₃) / (b₂ . b₃) & (b₁ /" b₂) . b₃ = (b₁ . b₃) * ((b₂ . b₃) " ) )

proof end;

theorem Th12: :: FIB_NUM:12

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = (Fib (b₂ + 1)) / (Fib b₂) ) holds
( b₁ is convergent & lim b₁ = tau )

proof end;