let a be Real; :: thesis: for Z9 being Element of REAL+ st Z9 = 0 holds
for x9 being Element of REAL+ st x9 = a holds
Z9 - x9 = - a
let Z9 be Element of REAL+ ; :: thesis: ( Z9 = 0 implies for x9 being Element of REAL+ st x9 = a holds
Z9 - x9 = - a )
assume A0: Z9 = 0 ; :: thesis: for x9 being Element of REAL+ st x9 = a holds
Z9 - x9 = - a
let xx be Element of REAL+ ; :: thesis: ( xx = a implies Z9 - xx = - a )
assume A1: xx = a ; :: thesis: Z9 - xx = - a
per cases ( xx = 0 or xx <> 0 ) ;
suppose xx = 0 ; :: thesis: Z9 - xx = - a
hence Z9 - xx = - a by A0, A1, ARYTM_1:18; :: thesis: verum
end;
suppose A2: xx <> 0 ; :: thesis: Z9 - xx = - a
set b = Z9 - xx;
A3: Z9 <=' xx by A0, ARYTM_1:6;
then not xx <=' Z9 by A0, A2, ARYTM_1:4;
then A4: Z9 - xx = [{},(xx -' Z9)] by ARYTM_1:def 2;
now :: thesis: not Z9 - xx = [0,0]
assume Z9 - xx = [0,0] ; :: thesis: contradiction
then xx -' Z9 = 0 by A4, XTUPLE_0:1;
hence contradiction by A0, A2, A3, ARYTM_1:10; :: thesis: verum
end;
then A5: not Z9 - xx in {[0,0]} by TARSKI:def 1;
A6: xx -' Z9 = (xx -' Z9) + Z9 by A0, ARYTM_2:def 8
.= xx by A3, ARYTM_1:def 1 ;
0 in {0} by TARSKI:def 1;
then A7: Z9 - xx in [:{0},REAL+:] by A4, ZFMISC_1:87;
then Z9 - xx in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 3;
then reconsider b = Z9 - xx as Element of REAL by A5, NUMBERS:def 1, XBOOLE_0:def 5;
consider x1, x2, y1, y2 being Element of REAL such that
A8: a = [*x1,x2*] and
A9: b = [*y1,y2*] and
A10: a + b = [*(+ (x1,y1)),(+ (x2,y2))*] by XCMPLX_0:def 4;
a + b in REAL by XREAL_0:def 1;
then + (x2,y2) = 0 by A10, ARYTM_0:24;
then A11: a + b = + (x1,y1) by A10, ARYTM_0:def 5;
a in REAL by XREAL_0:def 1;
then x2 = 0 by A8, ARYTM_0:24;
then A12: a = x1 by A8, ARYTM_0:def 5;
y2 = 0 by A9, ARYTM_0:24;
then A13: b = y1 by A9, ARYTM_0:def 5;
then consider x9, y9 being Element of REAL+ such that
A14: x1 = x9 and
A15: y1 = [0,y9] and
A16: + (x1,y1) = x9 - y9 by A1, A7, A12, ARYTM_0:def 1;
y9 = xx -' Z9 by A4, A13, A15, XTUPLE_0:1;
then a + b = 0 by A1, A12, A11, A14, A16, A6, ARYTM_1:18;
hence Z9 - xx = - a ; :: thesis: verum
end;
end;