let r be real number ; :: 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;
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 & (scf r) . 2 > 0 )
by A1;
A5: ((c_n r) . ((2 * 1) - 2)) / ((c_d r) . ((2 * 1) - 2)) =
((scf r) . 0 ) / ((c_d r) . 0 )
by Def6
.=
((scf r) . 0 ) / 1
by Def7
.=
(scf r) . 0
;
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));
(cocf r) . 2 =
((c_n r) . 2) * (((c_d r) " ) . 2)
by SEQ_1:12
.=
((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 A3, XCMPLX_1:114
.=
((scf r) . 0 ) + (((scf r) . 2) / ((((scf r) . 1) * ((scf r) . 2)) + 1))
by XCMPLX_1:57
;
then A6:
S2[1]
by A3, A5, XREAL_1:31, XREAL_1:141;
A7:
for n being Nat st n >= 1 & S2[n] holds
S2[n + 1]
A11:
for n being Nat st n >= 1 holds
S2[n]
from NAT_1:sch 8(A6, A7);
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)) )
thus
( 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)) )
by A11; :: thesis: verum