let a, b, c be real number ; :: thesis: ( a <= b & 0 <= c implies a * c <= b * c )
assume that
A1:
a <= b
and
A2:
0 <= c
; :: thesis: a * c <= b * c
reconsider x1 = a, y1 = b, z1 = c as Element of REAL by XREAL_0:def 1;
A3:
( * y1,z1 = b * c & * x1,z1 = a * c )
by Lm11;
not o in [:{0 },REAL+ :]
by ARYTM_0:5, XBOOLE_0:3;
then A4:
c in REAL+
by A2, XXREAL_0:def 5;
assume A5:
not a * c <= b * c
; :: thesis: contradiction
then A6:
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 A7:
a in REAL+
and A8:
b in REAL+
;
:: thesis: contradictionconsider a'',
b'' being
Element of
REAL+ such that A9:
a = a''
and A10:
b = b''
and A11:
a'' <=' b''
by A1, A7, A8, XXREAL_0:def 5;
consider a',
c' being
Element of
REAL+ such that A12:
a = a'
and A13:
c = c'
and A14:
* x1,
z1 = a' *' c'
by A4, A7, ARYTM_0:def 3;
consider b',
c'' being
Element of
REAL+ such that A15:
b = b'
and A16:
c = c''
and A17:
* y1,
z1 = b' *' c''
by A4, A8, ARYTM_0:def 3;
a' *' c' <=' b' *' c'
by A9, A10, A11, A12, A15, ARYTM_1:8;
hence
contradiction
by A3, A5, A13, A14, A16, A17, Lm1;
:: thesis: verum end; suppose that A18:
a in [:{0 },REAL+ :]
and A19:
b in REAL+
;
:: thesis: contradictionconsider a',
c' being
Element of
REAL+ such that
a = [0 ,a']
and
c = c'
and A20:
* x1,
z1 = [0 ,(c' *' a')]
by A4, A6, A18, ARYTM_0:def 3;
consider b',
c'' being
Element of
REAL+ such that
b = b'
and
c = c''
and A21:
* y1,
z1 = b' *' c''
by A4, A19, ARYTM_0:def 3;
* x1,
z1 in [:{0 },REAL+ :]
by A20, Lm4, ZFMISC_1:106;
then
( not
* x1,
z1 in REAL+ & not
* y1,
z1 in [:{0 },REAL+ :] )
by A21, ARYTM_0:5, XBOOLE_0:3;
hence
contradiction
by A3, A5, XXREAL_0:def 5;
:: thesis: verum end; suppose that A22:
a in [:{0 },REAL+ :]
and A23:
b in [:{0 },REAL+ :]
;
:: thesis: contradictionconsider a'',
b'' being
Element of
REAL+ such that A24:
a = [0 ,a'']
and A25:
b = [0 ,b'']
and A26:
b'' <=' a''
by A1, A22, A23, XXREAL_0:def 5;
consider a',
c' being
Element of
REAL+ such that A27:
a = [0 ,a']
and A28:
c = c'
and A29:
* x1,
z1 = [0 ,(c' *' a')]
by A4, A6, A22, ARYTM_0:def 3;
consider b',
c'' being
Element of
REAL+ such that A30:
b = [0 ,b']
and A31:
c = c''
and A32:
* y1,
z1 = [0 ,(c'' *' b')]
by A4, A6, A23, ARYTM_0:def 3;
A33:
a' = a''
by A24, A27, ZFMISC_1:33;
A34:
b' = b''
by A25, A30, ZFMISC_1:33;
A35:
(
* x1,
z1 in [:{0 },REAL+ :] &
* y1,
z1 in [:{0 },REAL+ :] )
by A29, A32, Lm4, ZFMISC_1:106;
b' *' c' <=' a' *' c'
by A26, A33, A34, ARYTM_1:8;
hence
contradiction
by A3, A5, A28, A29, A31, A32, A35, Lm1;
:: thesis: verum end;