let x, y, z be Element of REAL ; :: thesis: ( + x,y = 0 & + x,z = 0 implies y = z )
assume that
A1:
+ x,y = 0
and
A2:
+ x,z = 0
; :: thesis: y = z
per cases
( ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & y in REAL+ & z in [:{0 },REAL+ :] ) or ( x in REAL+ & z in REAL+ & y in [:{0 },REAL+ :] ) or ( x in REAL+ & y in [:{0 },REAL+ :] & z in [:{0 },REAL+ :] ) or ( z in REAL+ & y in REAL+ & x in [:{0 },REAL+ :] ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0 },REAL+ :] ) & ( not y in REAL+ or not x in [:{0 },REAL+ :] ) ) or ( ( not x in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not z in [:{0 },REAL+ :] ) & ( not z in REAL+ or not x in [:{0 },REAL+ :] ) ) )
;
suppose that A5:
x in REAL+
and A6:
y in REAL+
and A7:
z in [:{0 },REAL+ :]
;
:: thesis: y = zA8:
ex
x',
y' being
Element of
REAL+ st
(
x = x' &
y = y' &
0 = x' + y' )
by A1, A5, A6, ARYTM_0:def 2;
consider x'',
y'' being
Element of
REAL+ such that A9:
x = x''
and A10:
(
z = [0 ,y''] &
0 = x'' - y'' )
by A2, A5, A7, ARYTM_0:def 2;
A11:
x'' = 0
by A8, A9, ARYTM_2:6;
A12:
[{} ,{} ] in {[{} ,{} ]}
by TARSKI:def 1;
A13:
not
[{} ,{} ] in REAL
by A12, NUMBERS:def 1, XBOOLE_0:def 5;
A14:
z in REAL
;
thus
y = z
by A10, A11, A13, A14, ARYTM_1:19;
:: thesis: verum end; suppose that A15:
x in REAL+
and A16:
z in REAL+
and A17:
y in [:{0 },REAL+ :]
;
:: thesis: y = zA18:
ex
x',
z' being
Element of
REAL+ st
(
x = x' &
z = z' &
0 = x' + z' )
by A2, A15, A16, ARYTM_0:def 2;
consider x'',
y' being
Element of
REAL+ such that A19:
x = x''
and A20:
(
y = [0 ,y'] &
0 = x'' - y' )
by A1, A15, A17, ARYTM_0:def 2;
A21:
x'' = 0
by A18, A19, ARYTM_2:6;
A22:
[0 ,0 ] in {[0 ,0 ]}
by TARSKI:def 1;
A23:
not
[0 ,0 ] in REAL
by A22, NUMBERS:def 1, XBOOLE_0:def 5;
A24:
y in REAL
;
thus
y = z
by A20, A21, A23, A24, ARYTM_1:19;
:: thesis: verum end; suppose that A25:
x in REAL+
and A26:
y in [:{0 },REAL+ :]
and A27:
z in [:{0 },REAL+ :]
;
:: thesis: y = zconsider x',
y' being
Element of
REAL+ such that A28:
x = x'
and A29:
y = [0 ,y']
and A30:
0 = x' - y'
by A1, A25, A26, ARYTM_0:def 2;
consider x'',
z' being
Element of
REAL+ such that A31:
x = x''
and A32:
z = [0 ,z']
and A33:
0 = x'' - z'
by A2, A25, A27, ARYTM_0:def 2;
A34:
y' =
x'
by A30, ARYTM_0:6
.=
z'
by A28, A31, A33, ARYTM_0:6
;
thus
y = z
by A29, A32, A34;
:: thesis: verum end; suppose that A35:
z in REAL+
and A36:
y in REAL+
and A37:
x in [:{0 },REAL+ :]
;
:: thesis: y = zconsider x',
y' being
Element of
REAL+ such that A38:
x = [0 ,x']
and A39:
y = y'
and A40:
0 = y' - x'
by A1, A36, A37, ARYTM_0:def 2;
consider x'',
z' being
Element of
REAL+ such that A41:
x = [0 ,x'']
and A42:
z = z'
and A43:
0 = z' - x''
by A2, A35, A37, ARYTM_0:def 2;
A44:
x' = x''
by A38, A41, ZFMISC_1:33;
A45:
z' =
x'
by A43, A44, ARYTM_0:6
.=
y'
by A40, ARYTM_0:6
;
thus
y = z
by A39, A42, A45;
:: thesis: verum end;