let r be Real; :: 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;
defpred S2[ Nat] means 1 / (((c_d r) . $1) * ((c_d r) . ($1 + 1))) < 1 / (((scf r) . ($1 + 1)) * (((c_d r) . $1) ^2));
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) . 2 > 0 ;
A3: (scf r) . 1 > 0 by A1;
A4: for n being Nat st n >= 1 & S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( n >= 1 & S2[n] implies S2[n + 1] )
assume that
n >= 1 and
1 / (((c_d r) . n) * ((c_d r) . (n + 1))) < 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2)) ; :: thesis: S2[n + 1]
A5: (c_d r) . (n + 1) > 0 by A3, Th52;
then A6: ((c_d r) . (n + 1)) ^2 > 0 by SQUARE_1:12;
(scf r) . (n + 2) > 0 by A1;
then A7: ((scf r) . (n + 2)) * (((c_d r) . (n + 1)) ^2) > 0 by A6, XREAL_1:129;
(c_d r) . n > 0 by A3, Th52;
then A8: ((c_d r) . (n + 1)) * ((c_d r) . n) > 0 by A5, XREAL_1:129;
((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 Def6
.= (((scf r) . (n + 2)) * (((c_d r) . (n + 1)) ^2)) + (((c_d r) . (n + 1)) * ((c_d r) . n)) ;
hence S2[n + 1] by A8, A7, XREAL_1:29, XREAL_1:76; :: thesis: verum
end;
A9: (scf r) . 1 > 0 by A1;
then ((scf r) . 1) ^2 > 0 by SQUARE_1:12;
then ((scf r) . 2) * (((scf r) . 1) ^2) > 0 by A2, XREAL_1:129;
then A10: 1 / ((((scf r) . 2) * (((scf r) . 1) ^2)) + ((scf r) . 1)) < 1 / (((scf r) . 2) * (((scf r) . 1) ^2)) by A9, XREAL_1:29, XREAL_1:76;
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)) )
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 Def6
.= 1 / (((c_d r) . 1) * ((((scf r) . 2) * ((scf r) . 1)) + ((c_d r) . 0))) by Def6
.= 1 / (((scf r) . 1) * ((((scf r) . 2) * ((scf r) . 1)) + ((c_d r) . 0))) by Def6
.= 1 / (((scf r) . 1) * ((((scf r) . 2) * ((scf r) . 1)) + 1)) by Def6
.= 1 / ((((scf r) . 2) * (((scf r) . 1) ^2)) + ((scf r) . 1)) ;
then A11: S2[1] by A10, Def6;
for n being Nat st n >= 1 holds
S2[n] from NAT_1:sch 8(A11, A4);
 hence ( n >= 1 implies 1 / (((c_d r) . n) * ((c_d r) . (n + 1))) < 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2)) ) ; :: thesis: verum