hereby :: thesis: ( ( x in REAL+ & y in [:{0 },REAL+ :] implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & b1 = x' - y' ) ) & ( y in REAL+ & x in [:{0 },REAL+ :] implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & b1 = y' - x' ) ) & ( ( 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+ :] ) implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & b1 = [0 ,(x' + y')] ) ) )
end;
A1:
y in REAL+ \/ [:{0 },REAL+ :]
by NUMBERS:def 1, XBOOLE_0:def 5;
hereby :: thesis: ( ( y in REAL+ & x in [:{0 },REAL+ :] implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & b1 = y' - x' ) ) & ( ( 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+ :] ) implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & b1 = [0 ,(x' + y')] ) ) )
assume
x in REAL+
;
:: thesis: ( y in [:{0 },REAL+ :] implies ex IT being Element of REAL ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & IT = x' - y' ) )then reconsider x' =
x as
Element of
REAL+ ;
assume
y in [:{0 },REAL+ :]
;
:: thesis: ex IT being Element of REAL ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & IT = x' - y' )then consider z,
y' being
set such that A2:
z in {0 }
and A3:
y' in REAL+
and A4:
y = [z,y']
by ZFMISC_1:103;
reconsider y' =
y' as
Element of
REAL+ by A3;
reconsider IT =
x' - y' as
Element of
REAL by Th4;
take IT =
IT;
:: thesis: ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & IT = x' - y' )take x' =
x';
:: thesis: ex y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & IT = x' - y' )take y' =
y';
:: thesis: ( x = x' & y = [0 ,y'] & IT = x' - y' )thus
(
x = x' &
y = [0 ,y'] &
IT = x' - y' )
by A2, A4, TARSKI:def 1;
:: thesis: verum
end;
hereby :: thesis: ( ( 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+ :] ) implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & b1 = [0 ,(x' + y')] ) )
assume
y in REAL+
;
:: thesis: ( x in [:{0 },REAL+ :] implies ex IT being Element of REAL ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & IT = y' - x' ) )then reconsider y' =
y as
Element of
REAL+ ;
assume
x in [:{0 },REAL+ :]
;
:: thesis: ex IT being Element of REAL ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & IT = y' - x' )then consider z,
x' being
set such that A5:
z in {0 }
and A6:
x' in REAL+
and A7:
x = [z,x']
by ZFMISC_1:103;
reconsider x' =
x' as
Element of
REAL+ by A6;
reconsider IT =
y' - x' as
Element of
REAL by Th4;
take IT =
IT;
:: thesis: ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & IT = y' - x' )take x' =
x';
:: thesis: ex y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & IT = y' - x' )take y' =
y';
:: thesis: ( x = [0 ,x'] & y = y' & IT = y' - x' )thus
(
x = [0 ,x'] &
y = y' &
IT = y' - x' )
by A5, A7, TARSKI:def 1;
:: thesis: verum
end;
assume that
A8:
( not x in REAL+ or not y in REAL+ )
and
A9:
( not x in REAL+ or not y in [:{0 },REAL+ :] )
and
A10:
( not y in REAL+ or not x in [:{0 },REAL+ :] )
; :: thesis: ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & b1 = [0 ,(x' + y')] )
A11:
x in REAL+ \/ [:{0 },REAL+ :]
by NUMBERS:def 1, XBOOLE_0:def 5;
then
( x in REAL+ or x in [:{0 },REAL+ :] )
by XBOOLE_0:def 3;
then consider z1, x' being set such that
A12:
z1 in {0 }
and
A13:
x' in REAL+
and
A14:
x = [z1,x']
by A1, A8, A9, XBOOLE_0:def 3, ZFMISC_1:103;
( y in REAL+ or y in [:{0 },REAL+ :] )
by A1, XBOOLE_0:def 3;
then consider z2, y' being set such that
A15:
z2 in {0 }
and
A16:
y' in REAL+
and
A17:
y = [z2,y']
by A11, A8, A10, XBOOLE_0:def 3, ZFMISC_1:103;
reconsider x' = x' as Element of REAL+ by A13;
reconsider y' = y' as Element of REAL+ by A16;
x = [0 ,x']
by A12, A14, TARSKI:def 1;
then
x' + y' <> 0
by Th3, ARYTM_2:6;
then reconsider IT = [0 ,(y' + x')] as Element of REAL by Th2;
take
IT
; :: thesis: ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & IT = [0 ,(x' + y')] )
take
x'
; :: thesis: ex y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & IT = [0 ,(x' + y')] )
take
y'
; :: thesis: ( x = [0 ,x'] & y = [0 ,y'] & IT = [0 ,(x' + y')] )
thus
( x = [0 ,x'] & y = [0 ,y'] & IT = [0 ,(x' + y')] )
by A12, A14, A15, A17, TARSKI:def 1; :: thesis: verum