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)) / ((c_d r) . (2 * n)) < ((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)) / ((c_d r) . (2 * $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)) / ((c_d r) . (2 * n)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1))
then ( (scf r) . 1 > 0 & (scf r) . 2 > 0 ) ;
then A2: 1 / (((scf r) . 1) + (1 / ((scf r) . 2))) < 1 / ((scf r) . 1) by XREAL_1:29, XREAL_1:76;
let n be Nat; :: thesis: ( n >= 1 implies ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1)) )
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
((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1)) ; :: thesis: S2[n + 1]
(((c_n r) . (2 * (n + 1))) * ((c_d r) . ((2 * (n + 1)) - 1))) - (((c_n r) . ((2 * (n + 1)) - 1)) * ((c_d r) . (2 * (n + 1)))) = (((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)))
.= (- 1) |^ ((2 * n) + 1) by Th64
.= - (1 |^ ((2 * n) + 1)) by WSIERP_1:2
.= - 1 ;
then A5: ((c_n r) . (2 * (n + 1))) * ((c_d r) . ((2 * (n + 1)) - 1)) < ((c_n r) . ((2 * (n + 1)) - 1)) * ((c_d r) . (2 * (n + 1))) by XREAL_1:48;
( (c_d r) . ((2 * n) + 1) > 0 & (c_d r) . ((2 * n) + 2) > 0 ) by A3, Th52;
hence S2[n + 1] by A5, XREAL_1:106; :: thesis: verum
end;
(cocf r) . 1 = ((c_n r) . 1) * (((c_d r) ") . 1) by SEQ_1:8
.= ((c_n r) . 1) * (((c_d r) . 1) ") by VALUED_1:10
.= ((c_n r) . 1) * (1 / ((c_d r) . 1))
.= ((c_n r) . ((2 * 1) - 1)) / ((c_d r) . ((2 * 1) - 1)) ;
then A6: ((c_n r) . ((2 * 1) - 1)) / ((c_d r) . ((2 * 1) - 1)) = ((scf r) . 0) + (1 / ((scf r) . 1)) by A3, Th72;
(cocf r) . 2 = ((c_n r) . 2) * (((c_d r) ") . 2) by SEQ_1:8
.= ((c_n r) . 2) * (((c_d r) . 2) ") by VALUED_1:10
.= ((c_n r) . 2) * (1 / ((c_d r) . 2))
.= ((c_n r) . (2 * 1)) / ((c_d r) . (2 * 1)) ;
then ((c_n r) . (2 * 1)) / ((c_d r) . (2 * 1)) = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / ((scf r) . 2)))) by A1, Th73;
then A7: S2[1] by A6, A2, XREAL_1:8;
for n being Nat st n >= 1 holds
S2[n] from NAT_1:sch 8(A7, A4);
 hence ( n >= 1 implies ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) < ((c_n r) . ((2 * n) - 1)) / ((c_d r) . ((2 * n) - 1)) ) ; :: thesis: verum