let r be Real; :: thesis: ( (scf r) . 1 > 0 implies for n being Nat holds ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) > ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) )
set s1 = c_n r;
set s2 = c_d r;
set s = scf r;
defpred S2[ Nat] means ((c_n r) . ((2 * $1) + 1)) / ((c_d r) . ((2 * $1) + 1)) > ((c_n r) . (2 * $1)) / ((c_d r) . (2 * $1));
A1: ((c_n r) . (2 * 0)) / ((c_d r) . (2 * 0)) = ((scf r) . 0) / ((c_d r) . 0) by Def5
.= ((scf r) . 0) / 1 by Def6
.= (scf r) . 0 ;
assume A2: (scf r) . 1 > 0 ; :: thesis: for n being Nat holds ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) > ((c_n r) . (2 * n)) / ((c_d r) . (2 * n))
A3: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) > ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) ; :: thesis: S2[n + 1]
reconsider n = n as Element of NAT by ORDINAL1:def 12;
(((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 A4: ((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)) by XREAL_1:47;
( (c_d r) . ((2 * (n + 1)) + 1) > 0 & (c_d r) . (2 * (n + 1)) > 0 ) by A2, Th52;
hence S2[n + 1] by A4, XREAL_1:106; :: thesis: verum
end;
((c_n r) . ((2 * 0) + 1)) / ((c_d r) . ((2 * 0) + 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 A2, XCMPLX_1:113 ;
then A5: S2[ 0 ] by A2, A1, XREAL_1:29;
for n being Nat holds S2[n] from NAT_1:sch 2(A5, A3);
 hence for n being Nat holds ((c_n r) . ((2 * n) + 1)) / ((c_d r) . ((2 * n) + 1)) > ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) ; :: thesis: verum