let r be Real; :: thesis: ( ( for n being Nat holds (scf r) . n > 0 ) implies for n being Nat st n >= 1 holds
((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1)) )
set s = scf r;
set s1 = c_n r;
set s2 = c_d r;
defpred S2[ Nat] means ((c_n r) . ((2 * $1) + 1)) / ((c_d r) . ((2 * $1) + 1)) < ((c_n r) . ((2 * $1) - 1)) / ((c_d r) . ((2 * $1) - 1));
assume A1: for n being Nat holds (scf r) . n > 0 ; :: thesis: for n being Nat st n >= 1 holds
((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1))
then A2: (scf r) . 3 > 0 ;
(cocf r) . 3 = ((c_n r) . 3) * (((c_d r) ") . 3) by SEQ_1:8
.= ((c_n r) . 3) * (((c_d r) . 3) ") by VALUED_1:10
.= ((c_n r) . 3) * (1 / ((c_d r) . 3))
.= ((c_n r) . 3) / ((c_d r) . 3) ;
then A3: ((c_n r) . ((2 * 1) + 1)) / ((c_d r) . ((2 * 1) + 1)) = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / (((scf r) . 2) + (1 / ((scf r) . 3)))))) by A1, Th74
.= ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / (((((scf r) . 2) * ((scf r) . 3)) + 1) / ((scf r) . 3))))) by A2, XCMPLX_1:113
.= ((scf r) . 0) + (1 / (((scf r) . 1) + (((scf r) . 3) / ((((scf r) . 2) * ((scf r) . 3)) + 1)))) by XCMPLX_1:57 ;
let n be Nat; :: thesis: ( n >= 1 implies ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1)) )
A4: (scf r) . 1 > 0 by A1;
A5: (scf r) . 1 > 0 by A1;
A6: 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
((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1)) ; :: thesis: S2[n + 1]
(((c_n r) . ((2 * (n + 1)) + 1)) * ((c_d r) . ((2 * (n + 1)) - 1))) - (((c_n r) . ((2 * (n + 1)) - 1)) * ((c_d r) . ((2 * (n + 1)) + 1))) = (((((scf r) . (((2 * n) + 1) + 2)) * ((c_n r) . (((2 * n) + 1) + 1))) + ((c_n r) . ((2 * n) + 1))) * ((c_d r) . ((2 * n) + 1))) - (((c_n r) . ((2 * n) + 1)) * ((c_d r) . ((2 * n) + 3))) by Def5
.= (((((scf r) . (((2 * n) + 1) + 2)) * ((c_n r) . (((2 * n) + 1) + 1))) + ((c_n r) . ((2 * n) + 1))) * ((c_d r) . ((2 * n) + 1))) - (((c_n r) . ((2 * n) + 1)) * ((((scf r) . (((2 * n) + 1) + 2)) * ((c_d r) . (((2 * n) + 1) + 1))) + ((c_d r) . ((2 * n) + 1)))) by Def6
.= ((scf r) . (((2 * n) + 1) + 2)) * ((((c_n r) . (((2 * n) + 1) + 1)) * ((c_d r) . ((2 * n) + 1))) - (((c_n r) . ((2 * n) + 1)) * ((c_d r) . (((2 * n) + 1) + 1))))
.= ((scf r) . (((2 * n) + 1) + 2)) * ((- 1) |^ ((2 * n) + 1)) by Th64
.= ((scf r) . (((2 * n) + 1) + 2)) * (- (1 |^ ((2 * n) + 1))) by WSIERP_1:2
.= ((scf r) . (((2 * n) + 1) + 2)) * (- 1) ;
then (((c_n r) . ((2 * (n + 1)) + 1)) * ((c_d r) . ((2 * (n + 1)) - 1))) - (((c_n r) . ((2 * (n + 1)) - 1)) * ((c_d r) . ((2 * (n + 1)) + 1))) < 0 by A1, XREAL_1:132;
then A7: ((c_n r) . ((2 * (n + 1)) + 1)) * ((c_d r) . ((2 * (n + 1)) - 1)) < ((c_n r) . ((2 * (n + 1)) - 1)) * ((c_d r) . ((2 * (n + 1)) + 1)) by XREAL_1:48;
( (c_d r) . ((2 * n) + 1) > 0 & (c_d r) . ((2 * n) + 3) > 0 ) by A5, Th52;
hence S2[n + 1] by A7, XREAL_1:106; :: thesis: verum
end;
(scf r) . 2 > 0 by A1;
then ((scf r) . 3) / ((((scf r) . 2) * ((scf r) . 3)) + 1) > 0 by A2, XREAL_1:139;
then A8: 1 / (((scf r) . 1) + (((scf r) . 3) / ((((scf r) . 2) * ((scf r) . 3)) + 1))) < 1 / ((scf r) . 1) by A4, XREAL_1:29, XREAL_1:76;
((c_n r) . ((2 * 1) - 1)) / ((c_d r) . ((2 * 1) - 1)) = ((((scf r) . 1) * ((scf r) . 0)) + 1) / ((c_d r) . 1) by Def5
.= ((((scf r) . 1) * ((scf r) . 0)) + 1) / ((scf r) . 1) by Def6
.= ((scf r) . 0) + (1 / ((scf r) . 1)) by A4, XCMPLX_1:113 ;
then A9: S2[1] by A8, A3, XREAL_1:8;
for n being Nat st n >= 1 holds
S2[n] from NAT_1:sch 8(A9, A6);
 hence ( n >= 1 implies ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1)) ) ; :: thesis: verum