let b be Nat; 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; ( (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
; 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 S2[ Nat] means (c_n r) . $1 <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ ($1 + 1);
A4:
for n being Nat st S2[n] & S2[n + 1] holds
S2[n + 2]
let n be Nat; (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:
S2[1]
by A15, A16, XXREAL_0:2;
(c_n r) . 0 = (scf r) . 0
by Def5;
then A18:
S2[ 0 ]
by A3, A12, XXREAL_0:2;
for n being Nat holds S2[n]
from FIB_NUM:sch 1(A18, A17, A4);
hence
(c_n r) . n <= ((b + (sqrt ((b ^2) + 4))) / 2) |^ (n + 1)
; verum