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