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