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

proof

let n be Nat; :: thesis: ( n >= 1 & S₂[n] implies S₂[n + 1] )
assume ( n >= 1 & 1 / (((c_d r) . n) * ((c_d r) . (n + 1))) < 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2 )) ) ; :: thesis: S₂[n + 1]
A7: (scf r) . (n + 2) > 0 by A1;
A8: ( (c_d r) . (n + 1) > 0 & (c_d r) . n > 0 ) by A2, Th52;
then A9: ((c_d r) . (n + 1)) * ((c_d r) . n) > 0 by XREAL_1:131;
((c_d r) . (n + 1)) ^2 > 0 by A8, SQUARE_1:74;
then A10: ((scf r) . (n + 2)) * (((c_d r) . (n + 1)) ^2 ) > 0 by A7, XREAL_1:131;
((c_d r) . (n + 1)) * ((c_d r) . ((n + 1) + 1)) = ((c_d r) . (n + 1)) * ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) by Def7
.= (((scf r) . (n + 2)) * (((c_d r) . (n + 1)) ^2 )) + (((c_d r) . (n + 1)) * ((c_d r) . n)) ;
hence S₂[n + 1] by A9, A10, XREAL_1:31, XREAL_1:78; :: thesis: verum

end;

A11: for n being Nat st n >= 1 holds
S₂[n] from NAT_1:sch 8(A5, A6);
let n be Nat; :: thesis: ( n >= 1 implies 1 / (((c_d r) . n) * ((c_d r) . (n + 1))) < 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2 )) )
thus ( n >= 1 implies 1 / (((c_d r) . n) * ((c_d r) . (n + 1))) < 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2 )) ) by A11; :: thesis: verum