let r be real number ; :: thesis: ( ( for n being Nat holds (scf r) . n <> 0 ) implies for n being Nat holds (c_d r) . (n + 1) >= tau |^ n )
set s2 = c_d r;
set s = scf r;
defpred S2[ Nat] means (c_d r) . ($1 + 1) >= tau |^ $1;
sqrt 5 < sqrt (3 ^2) by SQUARE_1:27;
then sqrt 5 < 3 by SQUARE_1:22;
then 1 + (sqrt 5) < 1 + 3 by XREAL_1:8;
then A1: ( ((1 + (sqrt 5)) / 2) |^ 1 = (1 + (sqrt 5)) / 2 & (1 + (sqrt 5)) / 2 < 4 / 2 ) by NEWTON:5, XREAL_1:74;
assume A2: for n being Nat holds (scf r) . n <> 0 ; :: thesis: for n being Nat holds (c_d r) . (n + 1) >= tau |^ n
then A3: (scf r) . 1 >= 1 by Th40;
then (c_d r) . (0 + 1) >= 1 by Def7;
then A4: S2[ 0 ] by NEWTON:4;
let n be Nat; :: thesis: (c_d r) . (n + 1) >= tau |^ n
A5: for n being Nat st S2[n] & S2[n + 1] holds
S2[n + 2]
proof
let n be Nat; :: thesis: ( S2[n] & S2[n + 1] implies S2[n + 2] )
assume that
A6: (c_d r) . (n + 1) >= tau |^ n and
A7: (c_d r) . ((n + 1) + 1) >= tau |^ (n + 1) ; :: thesis: S2[n + 2]
A8: (tau |^ (n + 1)) + (tau |^ n) = ((((1 + (sqrt 5)) / 2) |^ n) * ((1 + (sqrt 5)) / 2)) + (((1 + (sqrt 5)) / 2) |^ n) by FIB_NUM:def 1, NEWTON:6
.= (((1 + (sqrt 5)) / 2) |^ n) * ((6 + (2 * (sqrt 5))) / 4) ;
sqrt 5 >= 0 by SQUARE_1:def 2;
then (1 + (sqrt 5)) / 2 > 0 by XREAL_1:139;
then A9: tau |^ (n + 1) > 0 by FIB_NUM:def 1, PREPOWER:6;
A10: tau |^ (n + 2) = (((1 + (sqrt 5)) / 2) |^ n) * (((1 + (sqrt 5)) / 2) |^ 2) by FIB_NUM:def 1, NEWTON:8
.= (((1 + (sqrt 5)) / 2) |^ n) * (((1 + (sqrt 5)) / 2) ^2) by WSIERP_1:1
.= (((1 + (sqrt 5)) / 2) |^ n) * ((((1 ^2) + ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2)) / 4)
.= (((1 + (sqrt 5)) / 2) |^ n) * (((1 + (2 * (sqrt 5))) + 5) / 4) by SQUARE_1:def 2
.= (((1 + (sqrt 5)) / 2) |^ n) * ((6 + (2 * (sqrt 5))) / 4) ;
A11: (c_d r) . ((n + 2) + 1) = (((scf r) . ((n + 1) + 2)) * ((c_d r) . ((n + 1) + 1))) + ((c_d r) . (n + 1)) by Def7
.= (((scf r) . (n + 3)) * ((c_d r) . ((n + 1) + 1))) + ((c_d r) . (n + 1)) ;
n + 3 >= 0 + 1 by XREAL_1:7;
then (scf r) . (n + 3) >= 1 by A2, Th40;
then ((scf r) . (n + 3)) * ((c_d r) . ((n + 1) + 1)) >= 1 * (tau |^ (n + 1)) by A7, A9, XREAL_1:66;
hence S2[n + 2] by A6, A11, A8, A10, XREAL_1:7; :: thesis: verum
end;
(scf r) . 2 >= 1 by A2, Th40;
then ((scf r) . 2) * ((scf r) . 1) >= 1 by A3, XREAL_1:159;
then A12: (((scf r) . 2) * ((scf r) . 1)) + 1 >= 1 + 1 by XREAL_1:6;
(c_d r) . (1 + 1) = (((scf r) . (0 + 2)) * ((c_d r) . (0 + 1))) + ((c_d r) . 0) by Def7
.= (((scf r) . 2) * ((c_d r) . 1)) + 1 by Def7
.= (((scf r) . 2) * ((scf r) . 1)) + 1 by Def7 ;
then A13: S2[1] by A12, A1, FIB_NUM:def 1, XXREAL_0:2;
for n being Nat holds S2[n] from FIB_NUM:sch 1(A4, A13, A5);
 hence (c_d r) . (n + 1) >= tau |^ n ; :: thesis: verum