let a, b, c be Real; ( a <= b & 0 <= c implies a * c <= b * c )
assume that
A1:
a <= b
and
A2:
0 <= c
; a * c <= b * c
0 is Element of REAL+
by ARYTM_2:20;
then
not 0 in [:{0},REAL+:]
by ARYTM_0:5, XBOOLE_0:3;
then A3:
c in REAL+
by A2, XXREAL_0:def 5;
reconsider x1 = a, y1 = b, z1 = c as Element of REAL by XREAL_0:def 1;
A4:
* (y1,z1) = b * c
by Lm11;
A5:
* (x1,z1) = a * c
by Lm11;
assume A6:
not a * c <= b * c
; contradiction
then A7:
c <> 0
;
per cases
( ( a in REAL+ & b in REAL+ ) or ( a in [:{0},REAL+:] & b in REAL+ ) or ( a in [:{0},REAL+:] & b in [:{0},REAL+:] ) )
by A1, XXREAL_0:def 5;
suppose that A8:
a in REAL+
and A9:
b in REAL+
;
contradictionconsider b9,
c99 being
Element of
REAL+ such that A10:
b = b9
and A11:
c = c99
and A12:
* (
y1,
z1)
= b9 *' c99
by A3, A9, ARYTM_0:def 2;
consider a9,
c9 being
Element of
REAL+ such that A13:
a = a9
and A14:
c = c9
and A15:
* (
x1,
z1)
= a9 *' c9
by A3, A8, ARYTM_0:def 2;
ex
a99,
b99 being
Element of
REAL+ st
(
a = a99 &
b = b99 &
a99 <=' b99 )
by A1, A8, A9, XXREAL_0:def 5;
then
a9 *' c9 <=' b9 *' c9
by A13, A10, ARYTM_1:8;
hence
contradiction
by A4, A5, A6, A14, A15, A11, A12, Lm1;
verum end; suppose that A16:
a in [:{0},REAL+:]
and A17:
b in REAL+
;
contradiction
ex
a9,
c9 being
Element of
REAL+ st
(
a = [0,a9] &
c = c9 &
* (
x1,
z1)
= [0,(c9 *' a9)] )
by A3, A7, A16, ARYTM_0:def 2;
then
* (
x1,
z1)
in [:{0},REAL+:]
by Lm4, ZFMISC_1:87;
then A18:
not
* (
x1,
z1)
in REAL+
by ARYTM_0:5, XBOOLE_0:3;
ex
b9,
c99 being
Element of
REAL+ st
(
b = b9 &
c = c99 &
* (
y1,
z1)
= b9 *' c99 )
by A3, A17, ARYTM_0:def 2;
then
not
* (
y1,
z1)
in [:{0},REAL+:]
by ARYTM_0:5, XBOOLE_0:3;
hence
contradiction
by A4, A5, A6, A18, XXREAL_0:def 5;
verum suppose that A19:
a in [:{0},REAL+:]
and A20:
b in [:{0},REAL+:]
;
contradictionconsider b9,
c99 being
Element of
REAL+ such that A21:
b = [0,b9]
and A22:
c = c99
and A23:
* (
y1,
z1)
= [0,(c99 *' b9)]
by A3, A7, A20, ARYTM_0:def 2;
A24:
* (
y1,
z1)
in [:{0},REAL+:]
by A23, Lm4, ZFMISC_1:87;
consider a99,
b99 being
Element of
REAL+ such that A25:
a = [0,a99]
and A26:
b = [0,b99]
and A27:
b99 <=' a99
by A1, A19, A20, XXREAL_0:def 5;
A28:
b9 = b99
by A26, A21, XTUPLE_0:1;
consider a9,
c9 being
Element of
REAL+ such that A29:
a = [0,a9]
and A30:
c = c9
and A31:
* (
x1,
z1)
= [0,(c9 *' a9)]
by A3, A7, A19, ARYTM_0:def 2;
A32:
* (
x1,
z1)
in [:{0},REAL+:]
by A31, Lm4, ZFMISC_1:87;
a9 = a99
by A25, A29, XTUPLE_0:1;
then
b9 *' c9 <=' a9 *' c9
by A27, A28, ARYTM_1:8;
hence
contradiction
by A4, A5, A6, A30, A31, A22, A23, A32, A24, Lm1;
verum end;