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) - 2)) / ((c_d r) . ((2 * n) - 2)) )
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) - 2)) / ((c_d r) . ((2 * $1) - 2));
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) - 2)) / ((c_d r) . ((2 * n) - 2))
then A2: (scf r) . 1 > 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
((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) > ((c_n r) . ((2 * n) - 2)) / ((c_d r) . ((2 * n) - 2)) ; :: thesis: S2[n + 1]
(((c_n r) . (2 * (n + 1))) * ((c_d r) . ((2 * (n + 1)) - 2))) - (((c_n r) . ((2 * (n + 1)) - 2)) * ((c_d r) . (2 * (n + 1)))) = (((((scf r) . ((2 * n) + 2)) * ((c_n r) . ((2 * n) + 1))) + ((c_n r) . (2 * n))) * ((c_d r) . (2 * n))) - (((c_n r) . (2 * n)) * ((c_d r) . ((2 * n) + 2))) by Def5
.= (((((scf r) . ((2 * n) + 2)) * ((c_n r) . ((2 * n) + 1))) + ((c_n r) . (2 * n))) * ((c_d r) . (2 * n))) - (((c_n r) . (2 * n)) * ((((scf r) . ((2 * n) + 2)) * ((c_d r) . ((2 * n) + 1))) + ((c_d r) . (2 * n)))) by Def6
.= ((scf r) . ((2 * n) + 2)) * ((((c_n r) . ((2 * n) + 1)) * ((c_d r) . (2 * n))) - (((c_n r) . (2 * n)) * ((c_d r) . ((2 * n) + 1))))
.= ((scf r) . ((2 * n) + 2)) * ((- 1) |^ (2 * n)) by Th64
.= ((scf r) . ((2 * n) + 2)) * (1 |^ (2 * n)) by WSIERP_1:2
.= ((scf r) . ((2 * n) + 2)) * 1
.= (scf r) . ((2 * n) + 2) ;
then A5: ((c_n r) . (2 * (n + 1))) * ((c_d r) . ((2 * (n + 1)) - 2)) > ((c_n r) . ((2 * (n + 1)) - 2)) * ((c_d r) . (2 * (n + 1))) by A1, XREAL_1:47;
( (c_d r) . (2 * n) > 0 & (c_d r) . ((2 * n) + 2) > 0 ) by A3, Th52;
hence S2[n + 1] by A5, XREAL_1:106; :: thesis: verum
end;
let n be Nat; :: thesis: ( n >= 1 implies ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) > ((c_n r) . ((2 * n) - 2)) / ((c_d r) . ((2 * n) - 2)) )
A6: ((c_n r) . ((2 * 1) - 2)) / ((c_d r) . ((2 * 1) - 2)) = ((scf r) . 0) / ((c_d r) . 0) by Def5
.= ((scf r) . 0) / 1 by Def6
.= (scf r) . 0 ;
A7: (scf r) . 2 > 0 by A1;
(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) / ((c_d r) . 2) ;
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
.= ((scf r) . 0) + (1 / (((((scf r) . 1) * ((scf r) . 2)) + 1) / ((scf r) . 2))) by A7, XCMPLX_1:113
.= ((scf r) . 0) + (((scf r) . 2) / ((((scf r) . 1) * ((scf r) . 2)) + 1)) by XCMPLX_1:57 ;
then A8: S2[1] by A2, A7, A6, XREAL_1:29, XREAL_1:139;
for n being Nat st n >= 1 holds
S2[n] from NAT_1:sch 8(A8, A4);
 hence ( n >= 1 implies ((c_n r) . (2 * n)) / ((c_d r) . (2 * n)) > ((c_n r) . ((2 * n) - 2)) / ((c_d r) . ((2 * n) - 2)) ) ; :: thesis: verum