let n be Nat; for r being Real st r is irrational holds
( (((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n) > 0 & (((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) - ((c_d r) . n) > 0 )
let r be Real; ( r is irrational implies ( (((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n) > 0 & (((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) - ((c_d r) . n) > 0 ) )
assume A1:
r is irrational
; ( (((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n) > 0 & (((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) - ((c_d r) . n) > 0 )
then A2:
(c_d r) . (n + 1) >= 1
by Th8;
(rfs r) . ((n + 1) + 1) > 1
by A1, Th4;
then A4:
((rfs r) . (n + 2)) * ((c_d r) . (n + 1)) > 1 * ((c_d r) . (n + 1))
by A2, XREAL_1:68;
then A5:
((c_d r) . (n + 1)) * ((rfs r) . (n + 2)) > 1
by A2, XXREAL_0:2;
A6:
((c_d r) . n) + 1 >= 1 + 1
by A1, Th8, XREAL_1:6;
(c_d r) . (n + 1) >= (c_d r) . n
by A1, Th7;
then
((c_d r) . (n + 1)) * ((rfs r) . (n + 2)) > (c_d r) . n
by A4, XXREAL_0:2;
then
(((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) - ((c_d r) . n) > ((c_d r) . n) - ((c_d r) . n)
by XREAL_1:14;
hence
( (((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n) > 0 & (((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) - ((c_d r) . n) > 0 )
by A5, A6, XREAL_1:6; verum