let r, s, t be Real; :: thesis: ( r <= s & 0 <= t implies r * t <= s * t )

reconsider x1 = r, y1 = s, z1 = t as Element of REAL by Def1;

assume that

A1: r <= s and

A2: 0 <= t ; :: thesis: r * t <= s * t

0 is Element of REAL+ by ARYTM_2:20;

then not 0 in [:{0},REAL+:] by ARYTM_0:5, XBOOLE_0:3;

then A3: t in REAL+ by A2, XXREAL_0:def 5;

for x9 being Element of REAL

for r being Real st x9 = r holds

* (x9,z1) = r * t

assume A12: not r * t <= s * t ; :: thesis: contradiction

then A13: t <> 0 ;

reconsider x1 = r, y1 = s, z1 = t as Element of REAL by Def1;

assume that

A1: r <= s and

A2: 0 <= t ; :: thesis: r * t <= s * t

0 is Element of REAL+ by ARYTM_2:20;

then not 0 in [:{0},REAL+:] by ARYTM_0:5, XBOOLE_0:3;

then A3: t in REAL+ by A2, XXREAL_0:def 5;

for x9 being Element of REAL

for r being Real st x9 = r holds

* (x9,z1) = r * t

proof

then A11:
( * (y1,z1) = s * t & * (x1,z1) = r * t )
;
let x9 be Element of REAL ; :: thesis: for r being Real st x9 = r holds

* (x9,z1) = r * t

let r be Real; :: thesis: ( x9 = r implies * (x9,z1) = r * t )

assume A4: x9 = r ; :: thesis: * (x9,z1) = r * t

consider x1, x2, y1, y2 being Element of REAL such that

A5: r = [*x1,x2*] and

A6: t = [*y1,y2*] and

A7: r * t = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by XCMPLX_0:def 5;

x2 = 0 by A5, Lm1;

then A8: * (x2,y1) = 0 by ARYTM_0:12;

A9: y2 = 0 by A6, Lm1;

then * (x1,y2) = 0 by ARYTM_0:12;

then A10: + ((* (x1,y2)),(* (x2,y1))) = 0 by A8, ARYTM_0:11;

( r = x1 & t = y1 ) by A5, A6, Lm1;

hence * (x9,z1) = + ((* (x1,y1)),(* ((opp x2),y2))) by A4, A9, ARYTM_0:11, ARYTM_0:12

.= + ((* (x1,y1)),(opp (* (x2,y2)))) by ARYTM_0:15

.= r * t by A7, A10, ARYTM_0:def 5 ;

:: thesis: verum

end;* (x9,z1) = r * t

let r be Real; :: thesis: ( x9 = r implies * (x9,z1) = r * t )

assume A4: x9 = r ; :: thesis: * (x9,z1) = r * t

consider x1, x2, y1, y2 being Element of REAL such that

A5: r = [*x1,x2*] and

A6: t = [*y1,y2*] and

A7: r * t = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by XCMPLX_0:def 5;

x2 = 0 by A5, Lm1;

then A8: * (x2,y1) = 0 by ARYTM_0:12;

A9: y2 = 0 by A6, Lm1;

then * (x1,y2) = 0 by ARYTM_0:12;

then A10: + ((* (x1,y2)),(* (x2,y1))) = 0 by A8, ARYTM_0:11;

( r = x1 & t = y1 ) by A5, A6, Lm1;

hence * (x9,z1) = + ((* (x1,y1)),(* ((opp x2),y2))) by A4, A9, ARYTM_0:11, ARYTM_0:12

.= + ((* (x1,y1)),(opp (* (x2,y2)))) by ARYTM_0:15

.= r * t by A7, A10, ARYTM_0:def 5 ;

:: thesis: verum

assume A12: not r * t <= s * t ; :: thesis: contradiction

then A13: t <> 0 ;

per cases
( ( r in REAL+ & s in REAL+ ) or ( r in [:{0},REAL+:] & s in REAL+ ) or ( r in [:{0},REAL+:] & s in [:{0},REAL+:] ) )
by A1, XXREAL_0:def 5;

end;

suppose that A14:
r in REAL+
and

A15: s in REAL+ ; :: thesis: contradiction

A15: s in REAL+ ; :: thesis: contradiction

consider s9, t99 being Element of REAL+ such that

A16: s = s9 and

A17: ( t = t99 & * (y1,z1) = s9 *' t99 ) by A3, A15, ARYTM_0:def 2;

consider x9, t9 being Element of REAL+ such that

A18: r = x9 and

A19: ( t = t9 & * (x1,z1) = x9 *' t9 ) by A3, A14, ARYTM_0:def 2;

ex x99, s99 being Element of REAL+ st

( r = x99 & s = s99 & x99 <=' s99 ) by A1, A14, A15, XXREAL_0:def 5;

then x9 *' t9 <=' s9 *' t9 by A18, A16, ARYTM_1:8;

hence contradiction by A11, A12, A19, A17, Lm2; :: thesis: verum

end;A16: s = s9 and

A17: ( t = t99 & * (y1,z1) = s9 *' t99 ) by A3, A15, ARYTM_0:def 2;

consider x9, t9 being Element of REAL+ such that

A18: r = x9 and

A19: ( t = t9 & * (x1,z1) = x9 *' t9 ) by A3, A14, ARYTM_0:def 2;

ex x99, s99 being Element of REAL+ st

( r = x99 & s = s99 & x99 <=' s99 ) by A1, A14, A15, XXREAL_0:def 5;

then x9 *' t9 <=' s9 *' t9 by A18, A16, ARYTM_1:8;

hence contradiction by A11, A12, A19, A17, Lm2; :: thesis: verum

suppose that A20:
r in [:{0},REAL+:]
and

A21: s in REAL+ ; :: thesis: contradiction

A21: s in REAL+ ; :: thesis: contradiction

ex x9, t9 being Element of REAL+ st

( r = [0,x9] & t = t9 & * (x1,z1) = [0,(t9 *' x9)] ) by A3, A13, A20, ARYTM_0:def 2;

then * (x1,z1) in [:{0},REAL+:] by Lm3, ZFMISC_1:87;

then A22: not * (x1,z1) in REAL+ by ARYTM_0:5, XBOOLE_0:3;

ex s9, t99 being Element of REAL+ st

( s = s9 & t = t99 & * (y1,z1) = s9 *' t99 ) by A3, A21, ARYTM_0:def 2;

then not * (y1,z1) in [:{0},REAL+:] by ARYTM_0:5, XBOOLE_0:3;

hence contradiction by A11, A12, A22, XXREAL_0:def 5; :: thesis: verum

end;( r = [0,x9] & t = t9 & * (x1,z1) = [0,(t9 *' x9)] ) by A3, A13, A20, ARYTM_0:def 2;

then * (x1,z1) in [:{0},REAL+:] by Lm3, ZFMISC_1:87;

then A22: not * (x1,z1) in REAL+ by ARYTM_0:5, XBOOLE_0:3;

ex s9, t99 being Element of REAL+ st

( s = s9 & t = t99 & * (y1,z1) = s9 *' t99 ) by A3, A21, ARYTM_0:def 2;

then not * (y1,z1) in [:{0},REAL+:] by ARYTM_0:5, XBOOLE_0:3;

hence contradiction by A11, A12, A22, XXREAL_0:def 5; :: thesis: verum

suppose that A23:
r in [:{0},REAL+:]
and

A24: s in [:{0},REAL+:] ; :: thesis: contradiction

A24: s in [:{0},REAL+:] ; :: thesis: contradiction

consider s9, t99 being Element of REAL+ such that

A25: s = [0,s9] and

A26: t = t99 and

A27: * (y1,z1) = [0,(t99 *' s9)] by A3, A13, A24, ARYTM_0:def 2;

A28: * (y1,z1) in [:{0},REAL+:] by A27, Lm3, ZFMISC_1:87;

consider x99, s99 being Element of REAL+ such that

A29: r = [0,x99] and

A30: s = [0,s99] and

A31: s99 <=' x99 by A1, A23, A24, XXREAL_0:def 5;

A32: s9 = s99 by A30, A25, XTUPLE_0:1;

consider x9, t9 being Element of REAL+ such that

A33: r = [0,x9] and

A34: t = t9 and

A35: * (x1,z1) = [0,(t9 *' x9)] by A3, A13, A23, ARYTM_0:def 2;

A36: * (x1,z1) in [:{0},REAL+:] by A35, Lm3, ZFMISC_1:87;

x9 = x99 by A29, A33, XTUPLE_0:1;

then s9 *' t9 <=' x9 *' t9 by A31, A32, ARYTM_1:8;

hence contradiction by A11, A12, A34, A35, A26, A27, A36, A28, Lm2; :: thesis: verum

end;A25: s = [0,s9] and

A26: t = t99 and

A27: * (y1,z1) = [0,(t99 *' s9)] by A3, A13, A24, ARYTM_0:def 2;

A28: * (y1,z1) in [:{0},REAL+:] by A27, Lm3, ZFMISC_1:87;

consider x99, s99 being Element of REAL+ such that

A29: r = [0,x99] and

A30: s = [0,s99] and

A31: s99 <=' x99 by A1, A23, A24, XXREAL_0:def 5;

A32: s9 = s99 by A30, A25, XTUPLE_0:1;

consider x9, t9 being Element of REAL+ such that

A33: r = [0,x9] and

A34: t = t9 and

A35: * (x1,z1) = [0,(t9 *' x9)] by A3, A13, A23, ARYTM_0:def 2;

A36: * (x1,z1) in [:{0},REAL+:] by A35, Lm3, ZFMISC_1:87;

x9 = x99 by A29, A33, XTUPLE_0:1;

then s9 *' t9 <=' x9 *' t9 by A31, A32, ARYTM_1:8;

hence contradiction by A11, A12, A34, A35, A26, A27, A36, A28, Lm2; :: thesis: verum