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