let b be Nat; :: thesis: for r being Real st (scf r) . 0 > 0 & ( for n being Nat holds (scf r) . n <= b ) holds
for n being Nat holds (c_n r) . n <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)
let r be Real; :: thesis: ( (scf r) . 0 > 0 & ( for n being Nat holds (scf r) . n <= b ) implies for n being Nat holds (c_n r) . n <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1) )
assume that
A1: (scf r) . 0 > 0 and
A2: for n being Nat holds (scf r) . n <= b ; :: thesis: for n being Nat holds (c_n r) . n <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)
set s1 = c_n r;
set s = scf r;
A3: (scf r) . 0 <= b by A2;
defpred S₂[ Nat] means (c_n r) . $1 <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ ($1 + 1);
A4: for n being Nat st S₂[n] & S₂[n + 1] holds
S₂[n + 2]

proof

let n be Nat; :: thesis: ( S₂[n] & S₂[n + 1] implies S₂[n + 2] )
assume that
A5: (c_n r) . n <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1) and
A6: (c_n r) . (n + 1) <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ ((n + 1) + 1) ; :: thesis: S₂[n + 2]
n + 2 >= 0 + 1 by XREAL_1:7;
then A7: (scf r) . (n + 2) >= 0 by Th38;
( (scf r) . (n + 2) <= b & (c_n r) . (n + 1) > 0 ) by A1, A2, Th45;
then A8: ((scf r) . (n + 2)) * ((c_n r) . (n + 1)) <= b * (((b + (sqrt ((b ^2) + 4))) / 2) |^ ((n + 1) + 1)) by A6, A7, XREAL_1:66;
A9: (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:6
.= (((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) * ((((b ^2) + (b * (sqrt ((b ^2) + 4)))) + 2) / 2) ;
A10: ((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:8
.= (((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) * (((b + (sqrt ((b ^2) + 4))) / 2) ^2) by WSIERP_1:1
.= (((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 2
.= (((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)) * ((((b ^2) + (b * (sqrt ((b ^2) + 4)))) + 2) / 2) ;
(c_n r) . ((n + 1) + 1) = (((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n) by Def5;
hence S₂[n + 2] by A5, A8, A9, A10, XREAL_1:7; :: thesis: verum

end;

let n be Nat; :: thesis: (c_n r) . n <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)
(b ^2) + 4 > b ^2 by XREAL_1:39;
then sqrt ((b ^2) + 4) > sqrt (b ^2) by SQUARE_1:27;
then A11: sqrt ((b ^2) + 4) > b by SQUARE_1:22;
then b + (sqrt ((b ^2) + 4)) > b + b by XREAL_1:8;
then (b + (sqrt ((b ^2) + 4))) / 2 > (2 * b) / 2 by XREAL_1:74;
then A12: ((b + (sqrt ((b ^2) + 4))) / 2) |^ (0 + 1) > b ;
A13: (scf r) . 1 >= 0 by Th38;
A14: (c_n r) . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 by Def5;
(scf r) . 1 <= b by A2;
then ((scf r) . 1) * ((scf r) . 0) <= b ^2 by A1, A3, A13, XREAL_1:66;
then A15: (c_n r) . 1 <= (b ^2) + 1 by A14, XREAL_1:6;
b * (sqrt ((b ^2) + 4)) >= b * b by A11, XREAL_1:64;
then (b ^2) + (b * (sqrt ((b ^2) + 4))) >= (b ^2) + (b * b) by XREAL_1:6;
then ((b ^2) + (b * (sqrt ((b ^2) + 4)))) + 2 >= ((b ^2) + (b ^2)) + 2 by XREAL_1:6;
then A16: (((b ^2) + (b * (sqrt ((b ^2) + 4)))) + 2) / 2 >= (2 * ((b ^2) + 1)) / 2 by XREAL_1:72;
((b + (sqrt ((b ^2) + 4))) / 2) |^ (1 + 1) = ((b + (sqrt ((b ^2) + 4))) / 2) ^2 by WSIERP_1:1
.= (((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 2
.= (((b ^2) + (b * (sqrt ((b ^2) + 4)))) + 2) / 2 ;
then A17: S₂[1] by A15, A16, XXREAL_0:2;
(c_n r) . 0 = (scf r) . 0 by Def5;
then A18: S₂[ 0 ] by A3, A12, XXREAL_0:2;
for n being Nat holds S₂[n] from FIB_NUM:sch 1(A18, A17, A4);
hence (c_n r) . n <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1) ; :: thesis: verum