let r, s, t be Real; ( 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
; 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
let x9 be
Element of
REAL ;
for r being Real st x9 = r holds
* (x9,z1) = r * tlet r be
Real;
( x9 = r implies * (x9,z1) = r * t )
assume A4:
x9 = r
;
* (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
;
verum
end;
then A11:
( * (y1,z1) = s * t & * (x1,z1) = r * t )
;
assume A12:
not r * t <= s * t
; 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;
suppose that A14:
r in REAL+
and A15:
s in REAL+
;
contradictionconsider 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;
verum end; suppose that A20:
r in [:{0},REAL+:]
and A21:
s in REAL+
;
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;
verum suppose that A23:
r in [:{0},REAL+:]
and A24:
s in [:{0},REAL+:]
;
contradictionconsider 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;
verum end;