let x, y, z be Element of REAL ; * x,(+ y,z) = + (* x,y),(* x,z)
per cases
( x = 0 or ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & x <> 0 & y in REAL+ & z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) or ( x in REAL+ & x <> 0 & z in REAL+ & y in [:{0 },REAL+ :] \ {[0 ,0 ]} ) or ( x in REAL+ & x <> 0 & y in [:{0 },REAL+ :] \ {[0 ,0 ]} & z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) or ( x in [:{0 },REAL+ :] \ {[0 ,0 ]} & y in REAL+ & z in REAL+ ) or ( x in [:{0 },REAL+ :] \ {[0 ,0 ]} & y in REAL+ & z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) or ( x in [:{0 },REAL+ :] \ {[0 ,0 ]} & z in REAL+ & y in [:{0 },REAL+ :] \ {[0 ,0 ]} ) or ( x in [:{0 },REAL+ :] \ {[0 ,0 ]} & y in [:{0 },REAL+ :] \ {[0 ,0 ]} & z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) or ( ( not x in REAL+ or not y in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not y in REAL+ or not z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) & ( not x in REAL+ or not y in [:{0 },REAL+ :] \ {[0 ,0 ]} or not z in REAL+ ) & ( not x in REAL+ or not y in [:{0 },REAL+ :] \ {[0 ,0 ]} or not z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) & ( not x in [:{0 },REAL+ :] \ {[0 ,0 ]} or not y in REAL+ or not z in REAL+ ) & ( not x in [:{0 },REAL+ :] \ {[0 ,0 ]} or not y in REAL+ or not z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) & ( not x in [:{0 },REAL+ :] \ {[0 ,0 ]} or not y in [:{0 },REAL+ :] \ {[0 ,0 ]} or not z in REAL+ ) & ( not x in [:{0 },REAL+ :] \ {[0 ,0 ]} or not y in [:{0 },REAL+ :] \ {[0 ,0 ]} or not z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) ) )
;
suppose A1:
x = 0
;
* x,(+ y,z) = + (* x,y),(* x,z)hence * x,
(+ y,z) =
0
by Th14
.=
+ o,
o
by Th13
.=
+ (* x,y),
o
by A1, Th14
.=
+ (* x,y),
(* x,z)
by A1, Th14
;
verum end; suppose that A2:
x in REAL+
and A3:
(
y in REAL+ &
z in REAL+ )
;
* x,(+ y,z) = + (* x,y),(* x,z)A4:
( ex
x9,
y9 being
Element of
REAL+ st
(
x = x9 &
y = y9 &
* x,
y = x9 *' y9 ) & ex
x99,
z9 being
Element of
REAL+ st
(
x = x99 &
z = z9 &
* x,
z = x99 *' z9 ) )
by A2, A3, Def3;
then A5:
ex
xy9,
xz9 being
Element of
REAL+ st
(
* x,
y = xy9 &
* x,
z = xz9 &
+ (* x,y),
(* x,z) = xy9 + xz9 )
by Def2;
A6:
ex
y99,
z99 being
Element of
REAL+ st
(
y = y99 &
z = z99 &
+ y,
z = y99 + z99 )
by A3, Def2;
then
ex
x999,
yz9 being
Element of
REAL+ st
(
x = x999 &
+ y,
z = yz9 &
* x,
(+ y,z) = x999 *' yz9 )
by A2, Def3;
hence
* x,
(+ y,z) = + (* x,y),
(* x,z)
by A4, A5, A6, ARYTM_2:14;
verum end; suppose that A7:
(
x in REAL+ &
x <> 0 )
and A8:
y in REAL+
and A9:
z in [:{0 },REAL+ :] \ {[0 ,0 ]}
;
* x,(+ y,z) = + (* x,y),(* x,z)consider y99,
z99 being
Element of
REAL+ such that A10:
y = y99
and A11:
z = [0 ,z99]
and A12:
+ y,
z = y99 - z99
by A8, A9, Def2;
consider x9,
y9 being
Element of
REAL+ such that A13:
(
x = x9 &
y = y9 )
and A14:
* x,
y = x9 *' y9
by A7, A8, Def3;
consider x99,
z9 being
Element of
REAL+ such that A15:
x = x99
and A16:
z = [0 ,z9]
and A17:
* x,
z = [0 ,(x99 *' z9)]
by A7, A9, Def3;
* x,
z in [:{0 },REAL+ :]
by A17, Lm1, ZFMISC_1:106;
then A18:
ex
xy9,
xz9 being
Element of
REAL+ st
(
* x,
y = xy9 &
* x,
z = [0 ,xz9] &
+ (* x,y),
(* x,z) = xy9 - xz9 )
by A14, Def2;
A19:
z9 = z99
by A16, A11, ZFMISC_1:33;
now per cases
( z99 <=' y99 or not z99 <=' y99 )
;
suppose A20:
z99 <=' y99
;
* x,(+ y,z) = + (* x,y),(* x,z)then A21:
+ y,
z = y99 -' z99
by A12, ARYTM_1:def 2;
then
ex
x999,
yz9 being
Element of
REAL+ st
(
x = x999 &
+ y,
z = yz9 &
* x,
(+ y,z) = x999 *' yz9 )
by A7, Def3;
hence * x,
(+ y,z) =
(x9 *' y9) - (x99 *' z9)
by A13, A15, A10, A19, A20, A21, ARYTM_1:26
.=
+ (* x,y),
(* x,z)
by A14, A17, A18, ZFMISC_1:33
;
verum end; suppose A22:
not
z99 <=' y99
;
* x,(+ y,z) = + (* x,y),(* x,z)then A23:
+ y,
z = [0 ,(z99 -' y99)]
by A12, ARYTM_1:def 2;
then
+ y,
z in [:{0 },REAL+ :]
by Lm1, ZFMISC_1:106;
then consider x999,
yz9 being
Element of
REAL+ such that A24:
x = x999
and A25:
(
+ y,
z = [0 ,yz9] &
* x,
(+ y,z) = [0 ,(x999 *' yz9)] )
by A7, Def3;
thus * x,
(+ y,z) =
[0 ,(x999 *' (z99 -' y99))]
by A23, A25, ZFMISC_1:33
.=
(x9 *' y9) - (x99 *' z9)
by A7, A13, A15, A10, A19, A22, A24, ARYTM_1:27
.=
+ (* x,y),
(* x,z)
by A14, A17, A18, ZFMISC_1:33
;
verum end; hence
* x,
(+ y,z) = + (* x,y),
(* x,z)
;
verum end; suppose that A26:
(
x in REAL+ &
x <> 0 )
and A27:
z in REAL+
and A28:
y in [:{0 },REAL+ :] \ {[0 ,0 ]}
;
* x,(+ y,z) = + (* x,y),(* x,z)consider z99,
y99 being
Element of
REAL+ such that A29:
z = z99
and A30:
y = [0 ,y99]
and A31:
+ z,
y = z99 - y99
by A27, A28, Def2;
consider x9,
z9 being
Element of
REAL+ such that A32:
(
x = x9 &
z = z9 )
and A33:
* x,
z = x9 *' z9
by A26, A27, Def3;
consider x99,
y9 being
Element of
REAL+ such that A34:
x = x99
and A35:
y = [0 ,y9]
and A36:
* x,
y = [0 ,(x99 *' y9)]
by A26, A28, Def3;
* x,
y in [:{0 },REAL+ :]
by A36, Lm1, ZFMISC_1:106;
then A37:
ex
xz9,
xy9 being
Element of
REAL+ st
(
* x,
z = xz9 &
* x,
y = [0 ,xy9] &
+ (* x,z),
(* x,y) = xz9 - xy9 )
by A33, Def2;
A38:
y9 = y99
by A35, A30, ZFMISC_1:33;
now per cases
( y99 <=' z99 or not y99 <=' z99 )
;
suppose A39:
y99 <=' z99
;
* x,(+ z,y) = + (* x,z),(* x,y)then A40:
+ z,
y = z99 -' y99
by A31, ARYTM_1:def 2;
then
ex
x999,
zy9 being
Element of
REAL+ st
(
x = x999 &
+ z,
y = zy9 &
* x,
(+ z,y) = x999 *' zy9 )
by A26, Def3;
hence * x,
(+ z,y) =
(x9 *' z9) - (x99 *' y9)
by A32, A34, A29, A38, A39, A40, ARYTM_1:26
.=
+ (* x,z),
(* x,y)
by A33, A36, A37, ZFMISC_1:33
;
verum end; suppose A41:
not
y99 <=' z99
;
* x,(+ z,y) = + (* x,z),(* x,y)then A42:
+ z,
y = [0 ,(y99 -' z99)]
by A31, ARYTM_1:def 2;
then
+ z,
y in [:{0 },REAL+ :]
by Lm1, ZFMISC_1:106;
then consider x999,
zy9 being
Element of
REAL+ such that A43:
x = x999
and A44:
(
+ z,
y = [0 ,zy9] &
* x,
(+ z,y) = [0 ,(x999 *' zy9)] )
by A26, Def3;
thus * x,
(+ z,y) =
[0 ,(x999 *' (y99 -' z99))]
by A42, A44, ZFMISC_1:33
.=
(x9 *' z9) - (x99 *' y9)
by A26, A32, A34, A29, A38, A41, A43, ARYTM_1:27
.=
+ (* x,z),
(* x,y)
by A33, A36, A37, ZFMISC_1:33
;
verum end; hence
* x,
(+ y,z) = + (* x,y),
(* x,z)
;
verum end; suppose that A45:
(
x in REAL+ &
x <> 0 )
and A46:
y in [:{0 },REAL+ :] \ {[0 ,0 ]}
and A47:
z in [:{0 },REAL+ :] \ {[0 ,0 ]}
;
* x,(+ y,z) = + (* x,y),(* x,z)
( ( not
y in REAL+ or not
z in [:{0 },REAL+ :] ) & ( not
y in [:{0 },REAL+ :] or not
z in REAL+ ) )
by A46, A47, Th5, XBOOLE_0:3;
then consider y99,
z99 being
Element of
REAL+ such that A48:
y = [0 ,y99]
and A49:
z = [0 ,z99]
and A50:
+ y,
z = [0 ,(y99 + z99)]
by A46, Def2;
+ y,
z in [:{0 },REAL+ :]
by A50, Lm1, ZFMISC_1:106;
then consider x999,
yz9 being
Element of
REAL+ such that A51:
x = x999
and A52:
(
+ y,
z = [0 ,yz9] &
* x,
(+ y,z) = [0 ,(x999 *' yz9)] )
by A45, Def3;
consider x9,
y9 being
Element of
REAL+ such that A53:
x = x9
and A54:
y = [0 ,y9]
and A55:
* x,
y = [0 ,(x9 *' y9)]
by A45, A46, Def3;
A56:
y9 = y99
by A54, A48, ZFMISC_1:33;
consider x99,
z9 being
Element of
REAL+ such that A57:
x = x99
and A58:
z = [0 ,z9]
and A59:
* x,
z = [0 ,(x99 *' z9)]
by A45, A47, Def3;
* x,
z in [:{0 },REAL+ :]
by A59, Lm1, ZFMISC_1:106;
then A60:
( not
* x,
y in [:{0 },REAL+ :] or not
* x,
z in REAL+ )
by Th5, XBOOLE_0:3;
* x,
y in [:{0 },REAL+ :]
by A55, Lm1, ZFMISC_1:106;
then
( not
* x,
y in REAL+ or not
* x,
z in [:{0 },REAL+ :] )
by Th5, XBOOLE_0:3;
then consider xy9,
xz9 being
Element of
REAL+ such that A61:
* x,
y = [0 ,xy9]
and A62:
(
* x,
z = [0 ,xz9] &
+ (* x,y),
(* x,z) = [0 ,(xy9 + xz9)] )
by A55, A60, Def2, Lm1, ZFMISC_1:106;
A63:
xy9 = x9 *' y9
by A55, A61, ZFMISC_1:33;
A64:
z9 = z99
by A58, A49, ZFMISC_1:33;
thus * x,
(+ y,z) =
[0 ,(x999 *' (y99 + z99))]
by A50, A52, ZFMISC_1:33
.=
[0 ,((x9 *' y9) + (x9 *' z9))]
by A53, A51, A56, A64, ARYTM_2:14
.=
+ (* x,y),
(* x,z)
by A53, A57, A59, A62, A63, ZFMISC_1:33
;
verum suppose that A65:
x in [:{0 },REAL+ :] \ {[0 ,0 ]}
and A66:
y in REAL+
and A67:
z in REAL+
;
* x,(+ y,z) = + (* x,y),(* x,z)consider y99,
z99 being
Element of
REAL+ such that A68:
y = y99
and A69:
z = z99
and A70:
+ y,
z = y99 + z99
by A66, A67, Def2;
now per cases
( ( y <> 0 & z <> 0 ) or x = 0 or z = 0 or y = 0 )
;
suppose that A71:
y <> 0
and A72:
z <> 0
;
* x,(+ y,z) = + (* x,y),(* x,z)consider x99,
z9 being
Element of
REAL+ such that A73:
x = [0 ,x99]
and A74:
z = z9
and A75:
* x,
z = [0 ,(z9 *' x99)]
by A65, A67, A72, Def3;
y99 + z99 <> 0
by A69, A72, ARYTM_2:6;
then consider x999,
yz9 being
Element of
REAL+ such that A76:
x = [0 ,x999]
and A77:
(
+ y,
z = yz9 &
* x,
(+ y,z) = [0 ,(yz9 *' x999)] )
by A65, A70, Def3;
consider x9,
y9 being
Element of
REAL+ such that A78:
x = [0 ,x9]
and A79:
y = y9
and A80:
* x,
y = [0 ,(y9 *' x9)]
by A65, A66, A71, Def3;
A81:
x99 = x999
by A73, A76, ZFMISC_1:33;
* x,
z in [:{0 },REAL+ :]
by A75, Lm1, ZFMISC_1:106;
then A82:
( not
* x,
y in [:{0 },REAL+ :] or not
* x,
z in REAL+ )
by Th5, XBOOLE_0:3;
* x,
y in [:{0 },REAL+ :]
by A80, Lm1, ZFMISC_1:106;
then
( not
* x,
y in REAL+ or not
* x,
z in [:{0 },REAL+ :] )
by Th5, XBOOLE_0:3;
then consider xy9,
xz9 being
Element of
REAL+ such that A83:
* x,
y = [0 ,xy9]
and A84:
(
* x,
z = [0 ,xz9] &
+ (* x,y),
(* x,z) = [0 ,(xy9 + xz9)] )
by A80, A82, Def2, Lm1, ZFMISC_1:106;
A85:
xy9 = x9 *' y9
by A80, A83, ZFMISC_1:33;
x9 = x99
by A78, A73, ZFMISC_1:33;
hence * x,
(+ y,z) =
[0 ,((x9 *' y9) + (x99 *' z9))]
by A68, A69, A70, A79, A74, A77, A81, ARYTM_2:14
.=
+ (* x,y),
(* x,z)
by A75, A84, A85, ZFMISC_1:33
;
verum end; suppose A86:
x = 0
;
* x,(+ y,z) = + (* x,y),(* x,z)hence * x,
(+ y,z) =
0
by Th14
.=
+ o,
o
by Th13
.=
+ (* x,y),
o
by A86, Th14
.=
+ (* x,y),
(* x,z)
by A86, Th14
;
verum end; hence
* x,
(+ y,z) = + (* x,y),
(* x,z)
;
verum end; suppose that A89:
x in [:{0 },REAL+ :] \ {[0 ,0 ]}
and A90:
y in REAL+
and A91:
z in [:{0 },REAL+ :] \ {[0 ,0 ]}
;
* x,(+ y,z) = + (* x,y),(* x,z)consider x99,
z9 being
Element of
REAL+ such that A92:
x = [0 ,x99]
and A93:
z = [0 ,z9]
and A94:
* x,
z = z9 *' x99
by A89, A91, Def3;
now per cases
( y <> 0 or y = 0 )
;
suppose
y <> 0
;
* x,(+ y,z) = + (* x,y),(* x,z)then consider x9,
y9 being
Element of
REAL+ such that A95:
x = [0 ,x9]
and A96:
y = y9
and A97:
* x,
y = [0 ,(y9 *' x9)]
by A89, A90, Def3;
* x,
y in [:{0 },REAL+ :]
by A97, Lm1, ZFMISC_1:106;
then consider xy9,
xz9 being
Element of
REAL+ such that A98:
* x,
y = [0 ,xy9]
and A99:
(
* x,
z = xz9 &
+ (* x,y),
(* x,z) = xz9 - xy9 )
by A94, Def2;
consider y99,
z99 being
Element of
REAL+ such that A100:
y = y99
and A101:
z = [0 ,z99]
and A102:
+ y,
z = y99 - z99
by A91, A96, Def2;
A103:
z9 = z99
by A93, A101, ZFMISC_1:33;
now per cases
( z99 <=' y99 or not z99 <=' y99 )
;
suppose A104:
z99 <=' y99
;
* x,(+ y,z) = + (* x,y),(* x,z)then A105:
+ y,
z = y99 -' z99
by A102, ARYTM_1:def 2;
now per cases
( + y,z <> 0 or + y,z = 0 )
;
suppose A106:
+ y,
z <> 0
;
* x,(+ y,z) = + (* x,y),(* x,z)then consider x999,
yz9 being
Element of
REAL+ such that A107:
x = [0 ,x999]
and A108:
(
+ y,
z = yz9 &
* x,
(+ y,z) = [0 ,(yz9 *' x999)] )
by A89, A105, Def3;
not
x in {[0 ,0 ]}
by NUMBERS:def 1, XBOOLE_0:def 5;
then A109:
x999 <> 0
by A107, TARSKI:def 1;
A110:
z9 = z99
by A93, A101, ZFMISC_1:33;
A111:
x9 = x99
by A92, A95, ZFMISC_1:33;
x99 = x999
by A92, A107, ZFMISC_1:33;
hence * x,
(+ y,z) =
(x9 *' z9) - (x9 *' y9)
by A96, A100, A104, A105, A106, A108, A111, A110, A109, ARYTM_1:28
.=
+ (* x,y),
(* x,z)
by A94, A97, A98, A99, A111, ZFMISC_1:33
;
verum end; suppose A112:
+ y,
z = 0
;
* x,(+ y,z) = + (* x,y),(* x,z)then A113:
y99 = z99
by A104, A105, ARYTM_1:10;
A114:
(
xy9 = x9 *' y9 &
x9 = x99 )
by A92, A95, A97, A98, ZFMISC_1:33;
thus * x,
(+ y,z) =
0
by A112, Th14
.=
+ (* x,y),
(* x,z)
by A94, A96, A100, A99, A103, A113, A114, ARYTM_1:18
;
verum end; hence
* x,
(+ y,z) = + (* x,y),
(* x,z)
;
verum end; suppose A115:
not
z99 <=' y99
;
* x,(+ y,z) = + (* x,y),(* x,z)then A116:
+ y,
z = [0 ,(z99 -' y99)]
by A102, ARYTM_1:def 2;
then
+ y,
z in [:{0 },REAL+ :]
by Lm1, ZFMISC_1:106;
then consider x999,
yz9 being
Element of
REAL+ such that A117:
x = [0 ,x999]
and A118:
(
+ y,
z = [0 ,yz9] &
* x,
(+ y,z) = yz9 *' x999 )
by A89, Def3;
A119:
x99 = x999
by A92, A117, ZFMISC_1:33;
A120:
x9 = x99
by A92, A95, ZFMISC_1:33;
thus * x,
(+ y,z) =
x999 *' (z99 -' y99)
by A116, A118, ZFMISC_1:33
.=
(x99 *' z9) - (x9 *' y9)
by A96, A100, A103, A115, A120, A119, ARYTM_1:26
.=
+ (* x,y),
(* x,z)
by A94, A97, A98, A99, ZFMISC_1:33
;
verum end; hence
* x,
(+ y,z) = + (* x,y),
(* x,z)
;
verum end; hence
* x,
(+ y,z) = + (* x,y),
(* x,z)
;
verum end; suppose that A122:
x in [:{0 },REAL+ :] \ {[0 ,0 ]}
and A123:
z in REAL+
and A124:
y in [:{0 },REAL+ :] \ {[0 ,0 ]}
;
* x,(+ y,z) = + (* x,y),(* x,z)consider x99,
y9 being
Element of
REAL+ such that A125:
x = [0 ,x99]
and A126:
y = [0 ,y9]
and A127:
* x,
y = y9 *' x99
by A122, A124, Def3;
now per cases
( z <> 0 or z = 0 )
;
suppose
z <> 0
;
* x,(+ y,z) = + (* x,y),(* x,z)then consider x9,
z9 being
Element of
REAL+ such that A128:
x = [0 ,x9]
and A129:
z = z9
and A130:
* x,
z = [0 ,(z9 *' x9)]
by A122, A123, Def3;
* x,
z in [:{0 },REAL+ :]
by A130, Lm1, ZFMISC_1:106;
then consider xz9,
xy9 being
Element of
REAL+ such that A131:
* x,
z = [0 ,xz9]
and A132:
(
* x,
y = xy9 &
+ (* x,z),
(* x,y) = xy9 - xz9 )
by A127, Def2;
consider z99,
y99 being
Element of
REAL+ such that A133:
z = z99
and A134:
y = [0 ,y99]
and A135:
+ z,
y = z99 - y99
by A124, A129, Def2;
A136:
y9 = y99
by A126, A134, ZFMISC_1:33;
now per cases
( y99 <=' z99 or not y99 <=' z99 )
;
suppose A137:
y99 <=' z99
;
* x,(+ y,z) = + (* x,y),(* x,z)then A138:
+ z,
y = z99 -' y99
by A135, ARYTM_1:def 2;
now per cases
( + z,y <> 0 or + z,y = 0 )
;
suppose A139:
+ z,
y <> 0
;
* x,(+ z,y) = + (* x,z),(* x,y)then consider x999,
zy9 being
Element of
REAL+ such that A140:
x = [0 ,x999]
and A141:
(
+ z,
y = zy9 &
* x,
(+ z,y) = [0 ,(zy9 *' x999)] )
by A122, A138, Def3;
not
x in {[0 ,0 ]}
by NUMBERS:def 1, XBOOLE_0:def 5;
then A142:
x999 <> 0
by A140, TARSKI:def 1;
A143:
y9 = y99
by A126, A134, ZFMISC_1:33;
A144:
x9 = x99
by A125, A128, ZFMISC_1:33;
x99 = x999
by A125, A140, ZFMISC_1:33;
hence * x,
(+ z,y) =
(x9 *' y9) - (x9 *' z9)
by A129, A133, A137, A138, A139, A141, A144, A143, A142, ARYTM_1:28
.=
+ (* x,z),
(* x,y)
by A127, A130, A131, A132, A144, ZFMISC_1:33
;
verum end; suppose A145:
+ z,
y = 0
;
* x,(+ z,y) = + (* x,z),(* x,y)then A146:
z99 = y99
by A137, A138, ARYTM_1:10;
A147:
(
xz9 = x9 *' z9 &
x9 = x99 )
by A125, A128, A130, A131, ZFMISC_1:33;
thus * x,
(+ z,y) =
0
by A145, Th14
.=
+ (* x,z),
(* x,y)
by A127, A129, A133, A132, A136, A146, A147, ARYTM_1:18
;
verum end; hence
* x,
(+ y,z) = + (* x,y),
(* x,z)
;
verum end; suppose A148:
not
y99 <=' z99
;
* x,(+ y,z) = + (* x,y),(* x,z)then A149:
+ z,
y = [0 ,(y99 -' z99)]
by A135, ARYTM_1:def 2;
then
+ z,
y in [:{0 },REAL+ :]
by Lm1, ZFMISC_1:106;
then consider x999,
zy9 being
Element of
REAL+ such that A150:
x = [0 ,x999]
and A151:
(
+ z,
y = [0 ,zy9] &
* x,
(+ z,y) = zy9 *' x999 )
by A122, Def3;
A152:
x99 = x999
by A125, A150, ZFMISC_1:33;
A153:
x9 = x99
by A125, A128, ZFMISC_1:33;
thus * x,
(+ y,z) =
x999 *' (y99 -' z99)
by A149, A151, ZFMISC_1:33
.=
(x99 *' y9) - (x9 *' z9)
by A129, A133, A136, A148, A153, A152, ARYTM_1:26
.=
+ (* x,y),
(* x,z)
by A127, A130, A131, A132, ZFMISC_1:33
;
verum end; hence
* x,
(+ y,z) = + (* x,y),
(* x,z)
;
verum end; hence
* x,
(+ y,z) = + (* x,y),
(* x,z)
;
verum end; suppose that A155:
x in [:{0 },REAL+ :] \ {[0 ,0 ]}
and A156:
y in [:{0 },REAL+ :] \ {[0 ,0 ]}
and A157:
z in [:{0 },REAL+ :] \ {[0 ,0 ]}
;
* x,(+ y,z) = + (* x,y),(* x,z)
( ( not
y in REAL+ or not
z in [:{0 },REAL+ :] ) & ( not
y in [:{0 },REAL+ :] or not
z in REAL+ ) )
by A156, A157, Th5, XBOOLE_0:3;
then consider y99,
z99 being
Element of
REAL+ such that A158:
y = [0 ,y99]
and A159:
z = [0 ,z99]
and A160:
+ y,
z = [0 ,(y99 + z99)]
by A156, Def2;
consider x99,
z9 being
Element of
REAL+ such that A161:
x = [0 ,x99]
and A162:
z = [0 ,z9]
and A163:
* x,
z = z9 *' x99
by A155, A157, Def3;
A164:
z9 = z99
by A162, A159, ZFMISC_1:33;
consider x9,
y9 being
Element of
REAL+ such that A165:
x = [0 ,x9]
and A166:
y = [0 ,y9]
and A167:
* x,
y = y9 *' x9
by A155, A156, Def3;
A168:
y9 = y99
by A166, A158, ZFMISC_1:33;
+ y,
z in [:{0 },REAL+ :]
by A160, Lm1, ZFMISC_1:106;
then consider x999,
yz9 being
Element of
REAL+ such that A169:
x = [0 ,x999]
and A170:
(
+ y,
z = [0 ,yz9] &
* x,
(+ y,z) = yz9 *' x999 )
by A155, Def3;
A171:
x9 = x999
by A165, A169, ZFMISC_1:33;
A172:
( ex
xy9,
xz9 being
Element of
REAL+ st
(
* x,
y = xy9 &
* x,
z = xz9 &
+ (* x,y),
(* x,z) = xy9 + xz9 ) &
x9 = x99 )
by A165, A167, A161, A163, Def2, ZFMISC_1:33;
thus * x,
(+ y,z) =
x999 *' (y99 + z99)
by A160, A170, ZFMISC_1:33
.=
+ (* x,y),
(* x,z)
by A167, A163, A172, A171, A168, A164, ARYTM_2:14
;
verum suppose A173:
( ( not
x in REAL+ or not
y in REAL+ or not
z in REAL+ ) & ( not
x in REAL+ or not
y in REAL+ or not
z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) & ( not
x in REAL+ or not
y in [:{0 },REAL+ :] \ {[0 ,0 ]} or not
z in REAL+ ) & ( not
x in REAL+ or not
y in [:{0 },REAL+ :] \ {[0 ,0 ]} or not
z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) & ( not
x in [:{0 },REAL+ :] \ {[0 ,0 ]} or not
y in REAL+ or not
z in REAL+ ) & ( not
x in [:{0 },REAL+ :] \ {[0 ,0 ]} or not
y in REAL+ or not
z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) & ( not
x in [:{0 },REAL+ :] \ {[0 ,0 ]} or not
y in [:{0 },REAL+ :] \ {[0 ,0 ]} or not
z in REAL+ ) & ( not
x in [:{0 },REAL+ :] \ {[0 ,0 ]} or not
y in [:{0 },REAL+ :] \ {[0 ,0 ]} or not
z in [:{0 },REAL+ :] \ {[0 ,0 ]} ) )
;
* x,(+ y,z) = + (* x,y),(* x,z)A174:
not
[0 ,0 ] in REAL+
by ARYTM_2:3;
REAL =
(REAL+ \ {[0 ,0 ]}) \/ ([:{0 },REAL+ :] \ {[0 ,0 ]})
by NUMBERS:def 1, XBOOLE_1:42
.=
REAL+ \/ ([:{0 },REAL+ :] \ {[0 ,0 ]})
by A174, ZFMISC_1:65
;
hence
* x,
(+ y,z) = + (* x,y),
(* x,z)
by A173, XBOOLE_0:def 3;
verum end;