let a, b, c be Real; :: thesis: ( a > 1 & c > b implies a #R c > a #R b )

assume that

A1: a > 1 and

A2: c > b ; :: thesis: a #R c > a #R b

consider p being Rational such that

A3: b < p and

A4: p < c by A2, RAT_1:7;

consider q being Rational such that

A5: b < q and

A6: q < p by A3, RAT_1:7;

consider s2 being Rational_Sequence such that

A7: s2 is convergent and

A8: b = lim s2 and

A9: for n being Nat holds s2 . n <= b by Th67;

A10: a #Q q < a #Q p by A1, A6, Th64;

a #Q s2 is convergent by A1, A7, Th69;

then a #R b <= a #Q q by A1, A7, A8, A11, Def6;

then A12: a #R b < a #Q p by A10, XXREAL_0:2;

consider s1 being Rational_Sequence such that

A13: s1 is convergent and

A14: c = lim s1 and

A15: for n being Nat holds s1 . n >= c by Th68;

a #Q s1 is convergent by A1, A13, Th69;

then a #R c >= a #Q p by A1, A13, A14, A16, Def6;

hence a #R c > a #R b by A12, XXREAL_0:2; :: thesis: verum

assume that

A1: a > 1 and

A2: c > b ; :: thesis: a #R c > a #R b

consider p being Rational such that

A3: b < p and

A4: p < c by A2, RAT_1:7;

consider q being Rational such that

A5: b < q and

A6: q < p by A3, RAT_1:7;

consider s2 being Rational_Sequence such that

A7: s2 is convergent and

A8: b = lim s2 and

A9: for n being Nat holds s2 . n <= b by Th67;

A10: a #Q q < a #Q p by A1, A6, Th64;

now :: thesis: for n being Nat holds (a #Q s2) . n <= a #Q q

then A11:
lim (a #Q s2) <= a #Q q
by A1, A7, Th2, Th69;let n be Nat; :: thesis: (a #Q s2) . n <= a #Q q

s2 . n <= b by A9;

then s2 . n <= q by A5, XXREAL_0:2;

then a #Q (s2 . n) <= a #Q q by A1, Th63;

hence (a #Q s2) . n <= a #Q q by Def5; :: thesis: verum

end;s2 . n <= b by A9;

then s2 . n <= q by A5, XXREAL_0:2;

then a #Q (s2 . n) <= a #Q q by A1, Th63;

hence (a #Q s2) . n <= a #Q q by Def5; :: thesis: verum

a #Q s2 is convergent by A1, A7, Th69;

then a #R b <= a #Q q by A1, A7, A8, A11, Def6;

then A12: a #R b < a #Q p by A10, XXREAL_0:2;

consider s1 being Rational_Sequence such that

A13: s1 is convergent and

A14: c = lim s1 and

A15: for n being Nat holds s1 . n >= c by Th68;

now :: thesis: for n being Nat holds (a #Q s1) . n >= a #Q p

then A16:
lim (a #Q s1) >= a #Q p
by A1, A13, Th1, Th69;let n be Nat; :: thesis: (a #Q s1) . n >= a #Q p

s1 . n >= c by A15;

then s1 . n >= p by A4, XXREAL_0:2;

then a #Q (s1 . n) >= a #Q p by A1, Th63;

hence (a #Q s1) . n >= a #Q p by Def5; :: thesis: verum

end;s1 . n >= c by A15;

then s1 . n >= p by A4, XXREAL_0:2;

then a #Q (s1 . n) >= a #Q p by A1, Th63;

hence (a #Q s1) . n >= a #Q p by Def5; :: thesis: verum

a #Q s1 is convergent by A1, A13, Th69;

then a #R c >= a #Q p by A1, A13, A14, A16, Def6;

hence a #R c > a #R b by A12, XXREAL_0:2; :: thesis: verum