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) - 1)) / ((c_d r) . ((2 * n) - 1)) )
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) - 1)) / ((c_d r) . ((2 * n) - 1))
then A2:
(scf r) . 1 > 0
;
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));
(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 * 1)) / ((c_d r) . (2 * 1))
;
then A3:
((c_n r) . (2 * 1)) / ((c_d r) . (2 * 1)) = ((scf r) . 0 ) + (1 / (((scf r) . 1) + (1 / ((scf r) . 2))))
by A1, Th73;
(cocf r) . 1 =
((c_n r) . 1) * (((c_d r) " ) . 1)
by SEQ_1:12
.=
((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 A4:
((c_n r) . ((2 * 1) - 1)) / ((c_d r) . ((2 * 1) - 1)) = ((scf r) . 0 ) + (1 / ((scf r) . 1))
by A2, Th72;
A5:
( (scf r) . 1 > 0 & (scf r) . 2 > 0 )
by A1;
1 / (((scf r) . 1) + (1 / ((scf r) . 2))) < 1 / ((scf r) . 1)
by A5, XREAL_1:31, XREAL_1:78;
then A6:
S2[1]
by A3, A4, XREAL_1:10;
A7:
for n being Nat st n >= 1 & S2[n] holds
S2[n + 1]
A9:
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) - 1)) / ((c_d r) . ((2 * n) - 1)) )
thus
( 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)) )
by A9; :: thesis: verum