let r be real number ; :: thesis: ( ( for n being Nat holds (scf r) . n <> 0 ) implies for n being Nat holds 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2 )) <= 1 / (((c_d r) . n) ^2 ) )
assume A1: for n being Nat holds (scf r) . n <> 0 ; :: thesis: for n being Nat holds 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2 )) <= 1 / (((c_d r) . n) ^2 )
set s2 = c_d r;
set s = scf r;
let n be Nat; :: thesis: 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2 )) <= 1 / (((c_d r) . n) ^2 )
A2: n + 1 >= 1 + 0 by XREAL_1:9;
A3: (scf r) . (n + 1) <> 0 by A1;
(scf r) . 1 <> 0 by A1;
then (scf r) . 1 > 0 by Th38;
then A4: (c_d r) . n > 0 by Th52;
then ((c_d r) . n) ^2 > 0 by SQUARE_1:74;
then ((scf r) . (n + 1)) * (((c_d r) . n) ^2 ) >= 1 * (((c_d r) . n) ^2 ) by A2, A3, Th40, XREAL_1:66;
hence 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2 )) <= 1 / (((c_d r) . n) ^2 ) by A4, SQUARE_1:74, XREAL_1:120; :: thesis: verum