let x be object ; for k being Nat st x = - k & k <> x holds
x in [:{0},NAT:] \ {[0,0]}
let k be Nat; ( x = - k & k <> x implies x in [:{0},NAT:] \ {[0,0]} )
assume that
A1:
x = - k
and
A2:
k <> x
; x in [:{0},NAT:] \ {[0,0]}
reconsider r = x as Element of REAL by A1, XREAL_0:def 1;
r + k = 0
by A1;
then consider x1, x2, y1, y2 being Element of REAL such that
A3:
r = [*x1,x2*]
and
A4:
k = [*y1,y2*]
and
A5:
0 = [*(+ (x1,y1)),(+ (x2,y2))*]
by XCMPLX_0:def 4;
A6:
k in NAT
by ORDINAL1:def 12;
then
k in REAL
by NUMBERS:19;
then A7:
y2 = 0
by A4, ARYTM_0:24;
then A8:
y1 = k
by A4, ARYTM_0:def 5;
+ (x2,y2) = In (0,REAL)
by A5, ARYTM_0:24;
then A9:
+ (x1,y1) = 0
by A5, ARYTM_0:def 5;
A10:
now not x1 in REAL+ assume
x1 in REAL+
;
contradictionthen consider x9,
y9 being
Element of
REAL+ such that A11:
x1 = x9
and A12:
y1 = y9
and A13:
0 = x9 + y9
by A6, A8, A9, ARYTM_0:def 1, ARYTM_2:2;
A14:
y9 = 0
by A13, ARYTM_2:5;
x9 = 0
by A13, ARYTM_2:5;
hence
contradiction
by A2, A3, A4, A7, A11, A12, A14, ARYTM_0:24;
verum end;
x2 = 0
by A3, ARYTM_0:24;
then A15:
x1 = r
by A3, ARYTM_0:def 5;
r in REAL+ \/ [:{0},REAL+:]
by NUMBERS:def 1, XBOOLE_0:def 5;
then
x in [:{0},REAL+:]
by A15, A10, XBOOLE_0:def 3;
then consider x9, y9 being Element of REAL+ such that
A16:
x1 = [0,x9]
and
A17:
y1 = y9
and
A18:
0 = y9 - x9
by A6, A15, A8, A9, ARYTM_0:def 1, ARYTM_2:2;
A19:
0 in {0}
by TARSKI:def 1;
A20:
not r in {[0,0]}
by NUMBERS:def 1, XBOOLE_0:def 5;
x9 = y9
by A18, ARYTM_0:6;
then
x in [:{0},NAT:]
by A15, A8, A16, A17, A19, ZFMISC_1:87, A6;
hence
x in [:{0},NAT:] \ {[0,0]}
by A20, XBOOLE_0:def 5; verum