let a be Nat; :: thesis: for r being real number st a > 0 & ( for n being Nat holds (scf r) . n >= a ) holds
for n being Nat holds (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2 ) + 4))) / 2) |^ n
let r be real number ; :: thesis: ( a > 0 & ( for n being Nat holds (scf r) . n >= a ) implies for n being Nat holds (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2 ) + 4))) / 2) |^ n )
assume that
A1: a > 0 and
A2: for n being Nat holds (scf r) . n >= a ; :: thesis: for n being Nat holds (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2 ) + 4))) / 2) |^ n
set s2 = c_d r;
set s = scf r;
defpred S2[ Nat] means (c_d r) . ($1 + 1) >= ((a + (sqrt ((a ^2 ) + 4))) / 2) |^ $1;
A3: (scf r) . 1 > 0 by A1, A2;
then (scf r) . 1 >= 1 by Th40;
then (c_d r) . (0 + 1) >= 1 by Def7;
then A4: S2[ 0 ] by NEWTON:9;
A5: (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 ;
(scf r) . 2 > 0 by A1, A2;
then ((scf r) . 2) * ((scf r) . 1) >= 1 * ((scf r) . 1) by A3, Th40, XREAL_1:66;
then A6: (((scf r) . 2) * ((scf r) . 1)) + 1 >= ((scf r) . 1) + 1 by XREAL_1:8;
(scf r) . 1 >= a by A2;
then ((scf r) . 1) + 1 >= a + 1 by XREAL_1:8;
then A7: (((scf r) . 2) * ((scf r) . 1)) + 1 >= a + 1 by A6, XXREAL_0:2;
A8: ((a + (sqrt ((a ^2 ) + 4))) / 2) |^ 1 = (a + (sqrt ((a ^2 ) + 4))) / 2 by NEWTON:10;
4 * a > 0 by A1, XREAL_1:131;
then A9: (a ^2 ) + 4 < ((a ^2 ) + 4) + (4 * a) by XREAL_1:41;
sqrt ((a ^2 ) + 4) < sqrt ((a + 2) ^2 ) by A9, SQUARE_1:95;
then sqrt ((a ^2 ) + 4) < a + 2 by SQUARE_1:89;
then a + (sqrt ((a ^2 ) + 4)) < a + (a + 2) by XREAL_1:10;
then (a + (sqrt ((a ^2 ) + 4))) / 2 < ((2 * a) + (2 * 1)) / 2 by XREAL_1:76;
then A10: S2[1] by A5, A7, A8, XXREAL_0:2;
A11: 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
A12: (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2 ) + 4))) / 2) |^ n and
A13: (c_d r) . ((n + 1) + 1) >= ((a + (sqrt ((a ^2 ) + 4))) / 2) |^ (n + 1) ; :: thesis: S2[n + 2]
sqrt ((a ^2 ) + 4) > 0 by SQUARE_1:93;
then a + (sqrt ((a ^2 ) + 4)) > 0 ;
then (a + (sqrt ((a ^2 ) + 4))) / 2 > 0 by XREAL_1:141;
then A15: ((a + (sqrt ((a ^2 ) + 4))) / 2) |^ (n + 1) > 0 by PREPOWER:13;
A16: (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)) ;
(scf r) . (n + 3) >= a by A2;
then A17: ((scf r) . (n + 3)) * ((c_d r) . ((n + 1) + 1)) >= a * (((a + (sqrt ((a ^2 ) + 4))) / 2) |^ (n + 1)) by A13, A15, XREAL_1:68;
A18: (a * (((a + (sqrt ((a ^2 ) + 4))) / 2) |^ (n + 1))) + (((a + (sqrt ((a ^2 ) + 4))) / 2) |^ n) = (a * ((((a + (sqrt ((a ^2 ) + 4))) / 2) |^ n) * ((a + (sqrt ((a ^2 ) + 4))) / 2))) + (((a + (sqrt ((a ^2 ) + 4))) / 2) |^ n) by NEWTON:11
.= (((a + (sqrt ((a ^2 ) + 4))) / 2) |^ n) * ((((a ^2 ) + (a * (sqrt ((a ^2 ) + 4)))) + 2) / 2) ;
((a + (sqrt ((a ^2 ) + 4))) / 2) |^ (n + 2) = (((a + (sqrt ((a ^2 ) + 4))) / 2) |^ n) * (((a + (sqrt ((a ^2 ) + 4))) / 2) |^ 2) by NEWTON:13
.= (((a + (sqrt ((a ^2 ) + 4))) / 2) |^ n) * (((a + (sqrt ((a ^2 ) + 4))) / 2) ^2 ) by WSIERP_1:2
.= (((a + (sqrt ((a ^2 ) + 4))) / 2) |^ n) * ((((a ^2 ) + ((2 * a) * (sqrt ((a ^2 ) + 4)))) + ((sqrt ((a ^2 ) + 4)) ^2 )) / (2 * 2))
.= (((a + (sqrt ((a ^2 ) + 4))) / 2) |^ n) * ((((a ^2 ) + ((2 * a) * (sqrt ((a ^2 ) + 4)))) + ((a ^2 ) + 4)) / (2 * 2)) by SQUARE_1:def 4
.= (((a + (sqrt ((a ^2 ) + 4))) / 2) |^ n) * ((((a ^2 ) + (a * (sqrt ((a ^2 ) + 4)))) + 2) / 2) ;
hence S2[n + 2] by A12, A16, A17, A18, XREAL_1:9; :: thesis: verum
end;
A19: for n being Nat holds S2[n] from FIB_NUM:sch 1(A4, A10, A11);
 let n be Nat; :: thesis: (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2 ) + 4))) / 2) |^ n
thus (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2 ) + 4))) / 2) |^ n by A19; :: thesis: verum