let n be Nat; :: thesis: ( 3 <= n implies tau to_power (n - 2) < Fib n )

defpred S_{1}[ Nat] means tau to_power ($1 - 2) < Fib $1;

A1: for k being Nat st k >= 3 & ( for i being Nat st i >= 3 & i < k holds

S_{1}[i] ) holds

S_{1}[k]

S_{1}[k]
from NAT_1:sch 9(A1);

hence ( 3 <= n implies tau to_power (n - 2) < Fib n ) ; :: thesis: verum

defpred S

A1: for k being Nat st k >= 3 & ( for i being Nat st i >= 3 & i < k holds

S

S

proof

for k being Nat st k >= 3 holds
let k be Nat; :: thesis: ( k >= 3 & ( for i being Nat st i >= 3 & i < k holds

S_{1}[i] ) implies S_{1}[k] )

assume A2: k >= 3 ; :: thesis: ( ex i being Nat st

( i >= 3 & i < k & not S_{1}[i] ) or S_{1}[k] )

assume A3: for i being Nat st i >= 3 & i < k holds

S_{1}[i]
; :: thesis: S_{1}[k]

LL: ( ( 3 <= k & k <= 3 + 1 ) or 4 < k ) by A2;

_{1}[k]
; :: thesis: verum

end;S

assume A2: k >= 3 ; :: thesis: ( ex i being Nat st

( i >= 3 & i < k & not S

assume A3: for i being Nat st i >= 3 & i < k holds

S

LL: ( ( 3 <= k & k <= 3 + 1 ) or 4 < k ) by A2;

now :: thesis: ( ( k = 3 & S_{1}[3] ) or ( k = 4 & S_{1}[4] ) or ( 4 < k & S_{1}[k] ) )end;

hence
Sper cases
( k = 3 or k = 4 or 4 < k )
by LL, NAT_1:9;

end;

case
k = 4
; :: thesis: S_{1}[4]

tau to_power (4 - 2) =
tau to_power (0 + 2)

.= (tau to_power 0) + (tau to_power (0 + 1)) by FIB_NUM3:9

.= 1 + tau by POWER:24 ;

then tau to_power (4 - 2) < 1 + 2 by THTU2, XREAL_1:6;

hence S_{1}[4]
by FIB_NUM2:23; :: thesis: verum

end;.= (tau to_power 0) + (tau to_power (0 + 1)) by FIB_NUM3:9

.= 1 + tau by POWER:24 ;

then tau to_power (4 - 2) < 1 + 2 by THTU2, XREAL_1:6;

hence S

case LC4A:
4 < k
; :: thesis: S_{1}[k]

then
k - 4 in NAT
by INT_1:5;

then reconsider z = k - 4 as Nat ;

4 - 3 < k - 0 by XREAL_1:14, LC4A;

then k - 1 in NAT by INT_1:5;

then reconsider x = k - 1 as Nat ;

4 - 2 < k - 0 by XREAL_1:14, LC4A;

then k - 2 in NAT by INT_1:5;

then reconsider y = k - 2 as Nat ;

4 + 1 <= k by INT_1:7, LC4A;

then ( 5 - 2 <= k - 2 & 5 - 2 <= k - 1 ) by XREAL_1:13;

then ( 3 <= x & 3 <= y & x < k & y < k ) by XREAL_1:44;

then ( tau to_power (x - 2) < Fib x & tau to_power (y - 2) < Fib y ) by A3;

then (tau to_power z) + (tau to_power (z + 1)) < (Fib x) + (Fib y) by XREAL_1:8;

then tau to_power (z + 2) < (Fib x) + (Fib y) by FIB_NUM3:9;

then tau to_power (k - 2) < Fib ((y + 1) + 1) by PRE_FF:1;

hence S_{1}[k]
; :: thesis: verum

end;then reconsider z = k - 4 as Nat ;

4 - 3 < k - 0 by XREAL_1:14, LC4A;

then k - 1 in NAT by INT_1:5;

then reconsider x = k - 1 as Nat ;

4 - 2 < k - 0 by XREAL_1:14, LC4A;

then k - 2 in NAT by INT_1:5;

then reconsider y = k - 2 as Nat ;

4 + 1 <= k by INT_1:7, LC4A;

then ( 5 - 2 <= k - 2 & 5 - 2 <= k - 1 ) by XREAL_1:13;

then ( 3 <= x & 3 <= y & x < k & y < k ) by XREAL_1:44;

then ( tau to_power (x - 2) < Fib x & tau to_power (y - 2) < Fib y ) by A3;

then (tau to_power z) + (tau to_power (z + 1)) < (Fib x) + (Fib y) by XREAL_1:8;

then tau to_power (z + 2) < (Fib x) + (Fib y) by FIB_NUM3:9;

then tau to_power (k - 2) < Fib ((y + 1) + 1) by PRE_FF:1;

hence S

S

hence ( 3 <= n implies tau to_power (n - 2) < Fib n ) ; :: thesis: verum