let r be Real; ( ( for n being Nat holds (scf r) . n > 0 ) implies for n being Nat holds (c_d r) . (n + 2) <= (2 * ((scf r) . (n + 2))) * ((c_d r) . (n + 1)) )
assume A1:
for n being Nat holds (scf r) . n > 0
; for n being Nat holds (c_d r) . (n + 2) <= (2 * ((scf r) . (n + 2))) * ((c_d r) . (n + 1))
let n be Nat; (c_d r) . (n + 2) <= (2 * ((scf r) . (n + 2))) * ((c_d r) . (n + 1))
set s = scf r;
set s1 = c_d r;
A2:
(scf r) . (n + 2) > 0
by A1;
(scf r) . 1 > 0
by A1;
then A3:
(c_d r) . n > 0
by Th52;
A4:
((c_d r) . (n + 1)) / ((c_d r) . n) >= 1 / ((scf r) . (n + 2))
by A1, Th58;
(((c_d r) . (n + 1)) / ((c_d r) . n)) * ((c_d r) . n) =
(((c_d r) . n) / ((c_d r) . n)) * ((c_d r) . (n + 1))
.=
(c_d r) . (n + 1)
by A3, XCMPLX_1:88
;
then A5:
(c_d r) . (n + 1) >= ((c_d r) . n) / ((scf r) . (n + 2))
by A4, A3, XREAL_1:64;
(((c_d r) . n) / ((scf r) . (n + 2))) * ((scf r) . (n + 2)) =
(((scf r) . (n + 2)) / ((scf r) . (n + 2))) * ((c_d r) . n)
.=
(c_d r) . n
by A2, XCMPLX_1:88
;
then
((c_d r) . (n + 1)) * ((scf r) . (n + 2)) >= (c_d r) . n
by A5, A2, XREAL_1:64;
then
(((c_d r) . (n + 1)) * ((scf r) . (n + 2))) + (((c_d r) . (n + 1)) * ((scf r) . (n + 2))) >= ((c_d r) . n) + (((c_d r) . (n + 1)) * ((scf r) . (n + 2)))
by XREAL_1:6;
hence
(c_d r) . (n + 2) <= (2 * ((scf r) . (n + 2))) * ((c_d r) . (n + 1))
by Def6; verum