reconsider z9 = 0 as Element of REAL+ by ARYTM_2:21;
A1: x in REAL+ \/ [:{0 },REAL+ :] by NUMBERS:def 1, XBOOLE_0:def 5;
per cases ( x = 0 or ( x in REAL+ & x <> 0 ) or x in [:{0 },REAL+ :] ) by A1, XBOOLE_0:def 3;
suppose A2: x = 0 ; :: thesis: ex b1 being Element of REAL st + x,b1 = 0
then reconsider x9 = x as Element of REAL+ by ARYTM_2:21;
take x ; :: thesis: + x,x = 0
x9 + x9 = 0 by A2, ARYTM_2:def 8;
hence + x,x = 0 by Def2; :: thesis: verum
end;
suppose that A3: x in REAL+ and
A4: x <> 0 ; :: thesis: ex b1 being Element of REAL st + x,b1 = 0
A5: [0 ,x] <> [0 ,0 ] by A4, ZFMISC_1:33;
0 in {0 } by TARSKI:def 1;
then A6: [0 ,x] in [:{0 },REAL+ :] by A3, ZFMISC_1:106;
then [0 ,x] in REAL+ \/ [:{0 },REAL+ :] by XBOOLE_0:def 3;
then reconsider y = [0 ,x] as Element of REAL by A5, NUMBERS:def 1, ZFMISC_1:64;
reconsider x9 = x as Element of REAL+ by A3;
A7: x9 <=' x9 ;
take y ; :: thesis: + x,y = 0
z9 + x9 = x9 by ARYTM_2:def 8;
then z9 = x9 -' x9 by A7, ARYTM_1:def 1;
then 0 = x9 - x9 by A7, ARYTM_1:def 2;
hence + x,y = 0 by A6, Def2; :: thesis: verum
end;
suppose A8: x in [:{0 },REAL+ :] ; :: thesis: ex b1 being Element of REAL st + x,b1 = 0
then consider a, b being set such that
A9: a in {0 } and
A10: b in REAL+ and
A11: x = [a,b] by ZFMISC_1:103;
reconsider y = b as Element of REAL by A10, Th1;
take y ; :: thesis: + x,y = 0
now
per cases ( ( x in REAL+ & y in REAL+ ) or ( x in REAL+ & y in [:{0 },REAL+ :] ) or ( 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+ :] ) ) ) ;
case ( x in REAL+ & y in REAL+ ) ; :: thesis: ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 0 = x9 + y9 )
hence ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 0 = x9 + y9 ) by A8, Th5, XBOOLE_0:3; :: thesis: verum
end;
case ( x in REAL+ & y in [:{0 },REAL+ :] ) ; :: thesis: ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0 ,y9] & 0 = x9 - y9 )
hence ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0 ,y9] & 0 = x9 - y9 ) by A10, Th5, XBOOLE_0:3; :: thesis: verum
end;
case ( y in REAL+ & x in [:{0 },REAL+ :] ) ; :: thesis: ex x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = y9 & 0 = y9 - x9 )
reconsider x9 = b, y9 = y as Element of REAL+ by A10;
take x9 = x9; :: thesis: ex y9 being Element of REAL+ st
( x = [0 ,x9] & y = y9 & 0 = y9 - x9 )
take y9 = y9; :: thesis: ( x = [0 ,x9] & y = y9 & 0 = y9 - x9 )
thus x = [0 ,x9] by A9, A11, TARSKI:def 1; :: thesis: ( y = y9 & 0 = y9 - x9 )
thus y = y9 ; :: thesis: 0 = y9 - x9
thus 0 = y9 - x9 by ARYTM_1:18; :: thesis: verum
end;
case ( ( 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+ :] ) ) ; :: thesis: ex x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = [0 ,y9] & 0 = [0 ,(y9 + x9)] )
hence ex x9, y9 being Element of REAL+ st
( x = [0 ,x9] & y = [0 ,y9] & 0 = [0 ,(y9 + x9)] ) by A8, A10; :: thesis: verum
end;
end;
end;
hence + x,y = 0 by Def2; :: thesis: verum
end;
end;