let r be Real; :: thesis: ( (scf r) . 0 > 0 & ( for n being Nat holds (scf r) . n <> 0 ) implies for n being Nat holds (c_n r) . n >= tau |^ n )
assume that
A1: (scf r) . 0 > 0 and
A2: for n being Nat holds (scf r) . n <> 0 ; :: thesis: for n being Nat holds (c_n r) . n >= tau |^ n
set s = scf r;
A3: (scf r) . 0 >= 0 + 1 by A1, INT_1:7;
set s1 = c_n r;
defpred S2[ Nat] means (c_n r) . $1 >= tau |^ $1;
A4: 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
A5: (c_n r) . n >= tau |^ n and
A6: (c_n r) . (n + 1) >= tau |^ (n + 1) ; :: thesis: S2[n + 2]
A7: (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 A8: tau |^ (n + 1) > 0 by FIB_NUM:def 1, PREPOWER:6;
A9: 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) ;
A10: (c_n r) . ((n + 1) + 1) = (((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n) by Def5;
n + 2 >= 0 + 1 by XREAL_1:7;
then (scf r) . (n + 2) >= 1 by A2, Th40;
then ((scf r) . (n + 2)) * ((c_n r) . (n + 1)) >= 1 * (tau |^ (n + 1)) by A6, A8, XREAL_1:66;
hence S2[n + 2] by A5, A10, A7, A9, XREAL_1:7; :: thesis: verum
end;
(c_n r) . 0 = (scf r) . 0 by Def5;
then A11: S2[ 0 ] by A3, NEWTON:4;
(scf r) . 1 >= 1 by A2, Th40;
then ((scf r) . 1) * ((scf r) . 0) >= 1 by A3, XREAL_1:159;
then A12: (((scf r) . 1) * ((scf r) . 0)) + 1 >= 1 + 1 by XREAL_1:6;
let n be Nat; :: thesis: (c_n r) . n >= tau |^ n
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 A13: (1 + (sqrt 5)) / 2 < 4 / 2 by XREAL_1:74;
( (c_n r) . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 & ((1 + (sqrt 5)) / 2) |^ 1 = (1 + (sqrt 5)) / 2 ) by Def5;
then A14: S2[1] by A12, A13, FIB_NUM:def 1, XXREAL_0:2;
for n being Nat holds S2[n] from FIB_NUM:sch 1(A11, A14, A4);
 hence (c_n r) . n >= tau |^ n ; :: thesis: verum