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

theorem Th1: :: FIB_NUM:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n being Nat holds m hcf n = m hcf (n + m)
proof end;

theorem Th2: :: FIB_NUM:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, m, n being Nat st k hcf m = 1 holds
k hcf (m * n) = k hcf n
proof end;

theorem Th3: :: FIB_NUM:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being real number st s > 0 holds
ex n being Nat st
( n > 0 & 0 < 1 / n & 1 / n <= s )
proof end;

scheme :: FIB_NUM:sch 1
FibInd{ P1[ Nat] } :
for k being Nat holds P1[k]
provided
A1: P1[0] and
A2: P1[1] and
A3: for k being Nat st P1[k] & P1[k + 1] holds
P1[k + 2]
proof end;

scheme :: FIB_NUM:sch 2
BinInd{ P1[ Nat, Nat] } :
for m, n being Nat holds P1[m,n]
provided
A1: for m, n being Nat st P1[m,n] holds
P1[n,m] and
A2: for k being Nat st ( for m, n being Nat st m < k & n < k holds
P1[m,n] ) holds
for m being Nat st m <= k holds
P1[k,m]
proof end;

(0 + 1) + 1 = 2
;

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

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

Lm3: for k being Nat holds Fib (k + 1) >= k
proof end;

Lm4: for m being Nat holds Fib (m + 1) >= Fib m
proof end;

Lm5: for m, n being Nat st m >= n holds
Fib m >= Fib n
proof end;

Lm6: for m being Nat holds Fib (m + 1) <> 0
proof end;

theorem Th4: :: FIB_NUM:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n being Nat holds Fib (m + (n + 1)) = ((Fib n) * (Fib m)) + ((Fib (n + 1)) * (Fib (m + 1)))
proof end;

Lm7: for n being Nat holds (Fib n) hcf (Fib (n + 1)) = 1
proof end;

theorem :: FIB_NUM:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n being Nat holds (Fib m) hcf (Fib n) = Fib (m hcf n)
proof end;

theorem Th6: :: FIB_NUM:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, a, b, c being real number st a <> 0 & delta a,b,c >= 0 holds
( ((a * (x ^2 )) + (b * x)) + c = 0 iff ( x = ((- b) - (sqrt (delta a,b,c))) / (2 * a) or x = ((- b) + (sqrt (delta a,b,c))) / (2 * a) ) )
proof end;

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

:: deftheorem defines tau FIB_NUM:def 1 :
tau = (1 + (sqrt 5)) / 2;

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

:: deftheorem defines tau_bar FIB_NUM:def 2 :
tau_bar = (1 - (sqrt 5)) / 2;

Lm8: ( tau ^2 = tau + 1 & tau_bar ^2 = tau_bar + 1 )
proof end;

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

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

Lm11: sqrt 5 < 3
proof end;

1 < tau
proof end;

then Lm12: 0 < tau
by XREAL_1:2;

Lm13: tau_bar < 0
proof end;

Lm14: abs tau_bar < 1
proof end;

theorem Th7: :: FIB_NUM:7  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 Fib n = ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)
proof end;

Lm15: for n being Nat
for x being real number st abs x <= 1 holds
abs (x |^ n) <= 1
proof end;

Lm16: for n being Nat holds abs ((tau_bar to_power n) / (sqrt 5)) < 1
proof end;

theorem :: FIB_NUM:8  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 abs ((Fib n) - ((tau to_power n) / (sqrt 5))) < 1
proof end;

theorem Th9: :: FIB_NUM:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being Real_Sequence st ( for n being Nat holds F . n = G . n ) holds
F = G
proof end;

theorem Th10: :: FIB_NUM:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g, h being Real_Sequence st g is_not_0 holds
(f /" g) (#) (g /" h) = f /" h
proof end;

theorem Th11: :: FIB_NUM:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being Real_Sequence
for n being Nat holds
( (f /" g) . n = (f . n) / (g . n) & (f /" g) . n = (f . n) * ((g . n) " ) )
proof end;

theorem :: FIB_NUM:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Real_Sequence st ( for n being Nat holds F . n = (Fib (n + 1)) / (Fib n) ) holds
( F is convergent & lim F = tau )
proof end;