let r be real number ; :: 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;
set s1 = c_n r;
defpred S2[ Nat] means (c_n r) . $1 >= tau |^ $1;
A3: (c_n r) . 0 = (scf r) . 0 by Def6;
A4: (scf r) . 0 >= 1
proof
(scf r) . 0 >= 0 + 1 by A1, INT_1:20;
hence (scf r) . 0 >= 1 ; :: thesis: verum
end;
then A5: S2[ 0 ] by A3, NEWTON:9;
A6: (c_n r) . 1 = (((scf r) . 1) * ((scf r) . 0 )) + 1 by Def6;
(scf r) . 1 >= 1 by A2, Th40;
then ((scf r) . 1) * ((scf r) . 0 ) >= 1 by A4, XREAL_1:161;
then A7: (((scf r) . 1) * ((scf r) . 0 )) + 1 >= 1 + 1 by XREAL_1:8;
A8: ((1 + (sqrt 5)) / 2) |^ 1 = (1 + (sqrt 5)) / 2 by NEWTON:10;
sqrt 5 < sqrt (3 ^2 ) by SQUARE_1:95;
then sqrt 5 < 3 by SQUARE_1:89;
then 1 + (sqrt 5) < 1 + 3 by XREAL_1:10;
then (1 + (sqrt 5)) / 2 < 4 / 2 by XREAL_1:76;
then A9: S2[1] by A6, A7, A8, FIB_NUM:def 1, XXREAL_0:2;
A10: 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
A11: (c_n r) . n >= tau |^ n and
A12: (c_n r) . (n + 1) >= tau |^ (n + 1) ; :: thesis: S2[n + 2]
sqrt 5 >= 0 by SQUARE_1:def 4;
then 1 + (sqrt 5) > 0 + 0 ;
then (1 + (sqrt 5)) / 2 > 0 by XREAL_1:141;
then A13: tau |^ (n + 1) > 0 by FIB_NUM:def 1, PREPOWER:13;
A14: (c_n r) . ((n + 1) + 1) = (((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n) by Def6;
n + 2 >= 0 + 1 by XREAL_1:9;
then (scf r) . (n + 2) >= 1 by A2, Th40;
then A15: ((scf r) . (n + 2)) * ((c_n r) . (n + 1)) >= 1 * (tau |^ (n + 1)) by A12, A13, XREAL_1:68;
A16: (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:11
.= (((1 + (sqrt 5)) / 2) |^ n) * ((6 + (2 * (sqrt 5))) / 4) ;
tau |^ (n + 2) = (((1 + (sqrt 5)) / 2) |^ n) * (((1 + (sqrt 5)) / 2) |^ 2) by FIB_NUM:def 1, NEWTON:13
.= (((1 + (sqrt 5)) / 2) |^ n) * (((1 + (sqrt 5)) / 2) ^2 ) by WSIERP_1:2
.= (((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 4
.= (((1 + (sqrt 5)) / 2) |^ n) * ((6 + (2 * (sqrt 5))) / 4) ;
hence S2[n + 2] by A11, A14, A15, A16, XREAL_1:9; :: thesis: verum
end;
A17: for n being Nat holds S2[n] from FIB_NUM:sch 1(A5, A9, A10);
 let n be Nat; :: thesis: (c_n r) . n >= tau |^ n
thus (c_n r) . n >= tau |^ n by A17; :: thesis: verum