let r be real number ; :: thesis: ( ( for n being Nat holds (scf r) . n > 0 ) implies for n being Nat holds ((c_d r) . (n + 1)) / ((c_d r) . n) >= 1 / ((scf r) . (n + 2)) )
assume A1: for n being Nat holds (scf r) . n > 0 ; :: thesis: for n being Nat holds ((c_d r) . (n + 1)) / ((c_d r) . n) >= 1 / ((scf r) . (n + 2))
set s = scf r;
set s1 = c_d r;
A2: for n being Nat holds
( (c_d r) . 0 = 1 & (c_d r) . 1 = (scf r) . 1 & (c_d r) . (n + 2) = (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n) ) by Def7;
defpred S₂[ Nat] means ((c_d r) . ($1 + 1)) / ((c_d r) . $1) >= 1 / ((scf r) . ($1 + 2));
(scf r) . 1 <> 0 by A1;
then A3: ((c_d r) . (0 + 1)) / ((c_d r) . 0 ) >= 1 by A2, Th40;
(scf r) . 2 <> 0 by A1;
then (scf r) . (0 + 2) >= 1 by Th40;
then 1 / ((scf r) . (0 + 2)) <= 1 / 1 by XREAL_1:120;
then A4: S₂[ 0 ] by A3, XXREAL_0:2;
A5: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume ((c_d r) . (n + 1)) / ((c_d r) . n) >= 1 / ((scf r) . (n + 2)) ; :: thesis: S₂[n + 1]
set r = (c_d r) . (n + 1);
A6: (scf r) . 1 > 0 by A1;
then A7: (c_d r) . (n + 1) > 0 by Th52;
A8: ((c_d r) . (n + 2)) / ((c_d r) . (n + 1)) = ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) / ((c_d r) . (n + 1)) by Def7
.= ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) / ((c_d r) . (n + 1))) + (((c_d r) . n) / ((c_d r) . (n + 1)))
.= (((scf r) . (n + 2)) * (((c_d r) . (n + 1)) / ((c_d r) . (n + 1)))) + (((c_d r) . n) / ((c_d r) . (n + 1)))
.= ((scf r) . (n + 2)) + (((c_d r) . n) / ((c_d r) . (n + 1))) by A7, XCMPLX_1:89 ;
(c_d r) . n > 0 by A6, Th52;
then A9: ((c_d r) . n) / ((c_d r) . (n + 1)) > 0 by A7, XREAL_1:141;
A10: n + 2 >= 0 + 1 by XREAL_1:9;
(scf r) . (n + 2) <> 0 by A1;
then (scf r) . (n + 2) >= 1 by A10, Th40;
then A11: ((c_d r) . (n + 2)) / ((c_d r) . (n + 1)) >= 1 + 0 by A8, A9, XREAL_1:9;
A12: n + 3 >= 0 + 1 by XREAL_1:9;
(scf r) . (n + 3) <> 0 by A1;
then (scf r) . (n + 3) >= 1 by A12, Th40;
then 1 / ((scf r) . (n + 3)) <= 1 / 1 by XREAL_1:120;
hence S₂[n + 1] by A11, XXREAL_0:2; :: thesis: verum

end;

for n being Nat holds S₂[n] from NAT_1:sch 2(A4, A5);
hence for n being Nat holds ((c_d r) . (n + 1)) / ((c_d r) . n) >= 1 / ((scf r) . (n + 2)) ; :: thesis: verum