:: ARYTM_0 semantic presentation begin Lm1: {} in {{}} by TARSKI:def_1; theorem Th1: :: ARYTM_0:1 REAL+ c= REAL proof REAL+ c= REAL+ \/ [:{{}},REAL+:] by XBOOLE_1:7; hence REAL+ c= REAL by ARYTM_2:3, NUMBERS:def_1, ZFMISC_1:34; ::_thesis: verum end; theorem Th2: :: ARYTM_0:2 for x being Element of REAL+ st x <> {} holds [{},x] in REAL proof let x be Element of REAL+ ; ::_thesis: ( x <> {} implies [{},x] in REAL ) assume A1: x <> {} ; ::_thesis: [{},x] in REAL A2: now__::_thesis:_not_[{},x]_in_{[{},{}]} assume [{},x] in {[{},{}]} ; ::_thesis: contradiction then [{},x] = [{},{}] by TARSKI:def_1; hence contradiction by A1, XTUPLE_0:1; ::_thesis: verum end; {} in {{}} by TARSKI:def_1; then [{},x] in [:{{}},REAL+:] by ZFMISC_1:87; then [{},x] in REAL+ \/ [:{{}},REAL+:] by XBOOLE_0:def_3; hence [{},x] in REAL by A2, NUMBERS:def_1, XBOOLE_0:def_5; ::_thesis: verum end; theorem Th3: :: ARYTM_0:3 for y being set st [{},y] in REAL holds y <> {} proof let y be set ; ::_thesis: ( [{},y] in REAL implies y <> {} ) assume that A1: [{},y] in REAL and A2: y = {} ; ::_thesis: contradiction [{},y] in {[{},{}]} by A2, TARSKI:def_1; hence contradiction by A1, NUMBERS:def_1, XBOOLE_0:def_5; ::_thesis: verum end; theorem Th4: :: ARYTM_0:4 for x, y being Element of REAL+ holds x - y in REAL proof let x, y be Element of REAL+ ; ::_thesis: x - y in REAL percases ( y <=' x or not y <=' x ) ; suppose y <=' x ; ::_thesis: x - y in REAL then x - y = x -' y by ARYTM_1:def_2; then x - y in REAL+ ; hence x - y in REAL by Th1; ::_thesis: verum end; supposeA1: not y <=' x ; ::_thesis: x - y in REAL then x - y = [{},(y -' x)] by ARYTM_1:def_2; hence x - y in REAL by A1, Th2, ARYTM_1:9; ::_thesis: verum end; end; end; theorem Th5: :: ARYTM_0:5 REAL+ misses [:{{}},REAL+:] proof assume REAL+ meets [:{{}},REAL+:] ; ::_thesis: contradiction then consider x being set such that A1: x in REAL+ and A2: x in [:{{}},REAL+:] by XBOOLE_0:3; consider x1, x2 being set such that A3: x1 in {{}} and x2 in REAL+ and A4: x = [x1,x2] by A2, ZFMISC_1:84; x1 = {} by A3, TARSKI:def_1; hence contradiction by A1, A4, ARYTM_2:3; ::_thesis: verum end; begin theorem Th6: :: ARYTM_0:6 for x, y being Element of REAL+ st x - y = {} holds x = y proof let x, y be Element of REAL+ ; ::_thesis: ( x - y = {} implies x = y ) assume A1: x - y = {} ; ::_thesis: x = y {} <> [{},(y -' x)] ; then ( y <=' x & x -' y = {} ) by A1, ARYTM_1:def_2; hence x = y by ARYTM_1:10; ::_thesis: verum end; Lm2: for a, b being set holds not 1 = [a,b] proof let a, b be set ; ::_thesis: not 1 = [a,b] assume 1 = [a,b] ; ::_thesis: contradiction then A1: {{}} = {{a,b},{a}} by ORDINAL3:15, TARSKI:def_5; {a} in {{a,b},{a}} by TARSKI:def_2; hence contradiction by A1, TARSKI:def_1; ::_thesis: verum end; theorem Th7: :: ARYTM_0:7 for x, y, z being Element of REAL+ st x <> {} & x *' y = x *' z holds y = z proof let x, y, z be Element of REAL+ ; ::_thesis: ( x <> {} & x *' y = x *' z implies y = z ) assume that A1: x <> {} and A2: x *' y = x *' z ; ::_thesis: y = z percases ( z <=' y or y <=' z ) ; supposeA3: z <=' y ; ::_thesis: y = z then x *' (y -' z) = (x *' y) - (x *' z) by ARYTM_1:26 .= {} by A2, ARYTM_1:18 ; then {} = y -' z by A1, ARYTM_1:2 .= y - z by A3, ARYTM_1:def_2 ; hence y = z by Th6; ::_thesis: verum end; supposeA4: y <=' z ; ::_thesis: y = z then x *' (z -' y) = (x *' z) - (x *' y) by ARYTM_1:26 .= {} by A2, ARYTM_1:18 ; then {} = z -' y by A1, ARYTM_1:2 .= z - y by A4, ARYTM_1:def_2 ; hence y = z by Th6; ::_thesis: verum end; end; end; begin definition let x, y be Element of REAL ; func + (x,y) -> Element of REAL means :Def1: :: ARYTM_0:def 1 ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & it = x9 + y9 ) if ( x in REAL+ & y in REAL+ ) ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & it = x9 - y9 ) if ( x in REAL+ & y in [:{0},REAL+:] ) ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & it = y9 - x9 ) if ( y in REAL+ & x in [:{0},REAL+:] ) otherwise ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & it = [0,(x9 + y9)] ); existence ( ( x in REAL+ & y in REAL+ implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 + y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = x9 - y9 ) ) & ( y in REAL+ & x in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = y9 - x9 ) ) & ( ( 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 x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = [0,(x9 + y9)] ) ) ) proof hereby ::_thesis: ( ( x in REAL+ & y in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = x9 - y9 ) ) & ( y in REAL+ & x in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = y9 - x9 ) ) & ( ( 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 x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = [0,(x9 + y9)] ) ) ) assume ( x in REAL+ & y in REAL+ ) ; ::_thesis: ex IT being Element of REAL ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & IT = x9 + y9 ) then reconsider x9 = x, y9 = y as Element of REAL+ ; x9 + y9 in REAL+ ; then reconsider IT = x9 + y9 as Element of REAL by Th1; take IT = IT; ::_thesis: ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & IT = x9 + y9 ) take x9 = x9; ::_thesis: ex y9 being Element of REAL+ st ( x = x9 & y = y9 & IT = x9 + y9 ) take y9 = y9; ::_thesis: ( x = x9 & y = y9 & IT = x9 + y9 ) thus ( x = x9 & y = y9 & IT = x9 + y9 ) ; ::_thesis: verum 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 x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = y9 - x9 ) ) & ( ( 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 x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = [0,(x9 + y9)] ) ) ) assume x in REAL+ ; ::_thesis: ( y in [:{0},REAL+:] implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & IT = x9 - y9 ) ) then reconsider x9 = x as Element of REAL+ ; assume y in [:{0},REAL+:] ; ::_thesis: ex IT being Element of REAL ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & IT = x9 - y9 ) then consider z, y9 being set such that A2: z in {0} and A3: y9 in REAL+ and A4: y = [z,y9] by ZFMISC_1:84; reconsider y9 = y9 as Element of REAL+ by A3; reconsider IT = x9 - y9 as Element of REAL by Th4; take IT = IT; ::_thesis: ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & IT = x9 - y9 ) take x9 = x9; ::_thesis: ex y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & IT = x9 - y9 ) take y9 = y9; ::_thesis: ( x = x9 & y = [0,y9] & IT = x9 - y9 ) thus ( x = x9 & y = [0,y9] & IT = x9 - y9 ) 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 x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = [0,(x9 + y9)] ) ) assume y in REAL+ ; ::_thesis: ( x in [:{0},REAL+:] implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT = y9 - x9 ) ) then reconsider y9 = y as Element of REAL+ ; assume x in [:{0},REAL+:] ; ::_thesis: ex IT being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT = y9 - x9 ) then consider z, x9 being set such that A5: z in {0} and A6: x9 in REAL+ and A7: x = [z,x9] by ZFMISC_1:84; reconsider x9 = x9 as Element of REAL+ by A6; reconsider IT = y9 - x9 as Element of REAL by Th4; take IT = IT; ::_thesis: ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT = y9 - x9 ) take x9 = x9; ::_thesis: ex y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT = y9 - x9 ) take y9 = y9; ::_thesis: ( x = [0,x9] & y = y9 & IT = y9 - x9 ) thus ( x = [0,x9] & y = y9 & IT = y9 - x9 ) 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 x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = [0,(x9 + y9)] ) 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, x9 being set such that A12: z1 in {0} and A13: x9 in REAL+ and A14: x = [z1,x9] by A1, A8, A9, XBOOLE_0:def_3, ZFMISC_1:84; ( y in REAL+ or y in [:{0},REAL+:] ) by A1, XBOOLE_0:def_3; then consider z2, y9 being set such that A15: z2 in {0} and A16: y9 in REAL+ and A17: y = [z2,y9] by A11, A8, A10, XBOOLE_0:def_3, ZFMISC_1:84; reconsider x9 = x9 as Element of REAL+ by A13; reconsider y9 = y9 as Element of REAL+ by A16; x = [0,x9] by A12, A14, TARSKI:def_1; then x9 + y9 <> 0 by Th3, ARYTM_2:5; then reconsider IT = [0,(y9 + x9)] as Element of REAL by Th2; take IT ; ::_thesis: ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT = [0,(x9 + y9)] ) take x9 ; ::_thesis: ex y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT = [0,(x9 + y9)] ) take y9 ; ::_thesis: ( x = [0,x9] & y = [0,y9] & IT = [0,(x9 + y9)] ) thus ( x = [0,x9] & y = [0,y9] & IT = [0,(x9 + y9)] ) by A12, A14, A15, A17, TARSKI:def_1; ::_thesis: verum end; uniqueness for b1, b2 being Element of REAL holds ( ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 + y9 ) & ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b2 = x9 + y9 ) implies b1 = b2 ) & ( x in REAL+ & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = x9 - y9 ) & ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b2 = x9 - y9 ) implies b1 = b2 ) & ( y in REAL+ & x in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = y9 - x9 ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b2 = y9 - x9 ) implies b1 = b2 ) & ( ( 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+:] ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = [0,(x9 + y9)] ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b2 = [0,(x9 + y9)] ) implies b1 = b2 ) ) proof let IT1, IT2 be Element of REAL ; ::_thesis: ( ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & IT1 = x9 + y9 ) & ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & IT2 = x9 + y9 ) implies IT1 = IT2 ) & ( x in REAL+ & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & IT1 = x9 - y9 ) & ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & IT2 = x9 - y9 ) implies IT1 = IT2 ) & ( y in REAL+ & x in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT1 = y9 - x9 ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT2 = y9 - x9 ) implies IT1 = IT2 ) & ( ( 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+:] ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT1 = [0,(x9 + y9)] ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT2 = [0,(x9 + y9)] ) implies IT1 = IT2 ) ) thus ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & IT1 = x9 + y9 ) & ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & IT2 = x9 + y9 ) implies IT1 = IT2 ) ; ::_thesis: ( ( x in REAL+ & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & IT1 = x9 - y9 ) & ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & IT2 = x9 - y9 ) implies IT1 = IT2 ) & ( y in REAL+ & x in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT1 = y9 - x9 ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT2 = y9 - x9 ) implies IT1 = IT2 ) & ( ( 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+:] ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT1 = [0,(x9 + y9)] ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT2 = [0,(x9 + y9)] ) implies IT1 = IT2 ) ) thus ( x in REAL+ & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & IT1 = x9 - y9 ) & ex x99, y99 being Element of REAL+ st ( x = x99 & y = [0,y99] & IT2 = x99 - y99 ) implies IT1 = IT2 ) by XTUPLE_0:1; ::_thesis: ( ( y in REAL+ & x in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT1 = y9 - x9 ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT2 = y9 - x9 ) implies IT1 = IT2 ) & ( ( 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+:] ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT1 = [0,(x9 + y9)] ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT2 = [0,(x9 + y9)] ) implies IT1 = IT2 ) ) thus ( y in REAL+ & x in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT1 = y9 - x9 ) & ex x99, y99 being Element of REAL+ st ( x = [0,x99] & y = y99 & IT2 = y99 - x99 ) implies IT1 = IT2 ) by XTUPLE_0:1; ::_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+:] ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT1 = [0,(x9 + y9)] ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT2 = [0,(x9 + y9)] ) implies IT1 = IT2 ) assume that ( not x in REAL+ or not y in REAL+ ) and ( not x in REAL+ or not y in [:{0},REAL+:] ) and ( not y in REAL+ or not x in [:{0},REAL+:] ) ; ::_thesis: ( for x9, y9 being Element of REAL+ holds ( not x = [0,x9] or not y = [0,y9] or not IT1 = [0,(x9 + y9)] ) or for x9, y9 being Element of REAL+ holds ( not x = [0,x9] or not y = [0,y9] or not IT2 = [0,(x9 + y9)] ) or IT1 = IT2 ) given x9, y9 being Element of REAL+ such that A18: x = [0,x9] and A19: ( y = [0,y9] & IT1 = [0,(x9 + y9)] ) ; ::_thesis: ( for x9, y9 being Element of REAL+ holds ( not x = [0,x9] or not y = [0,y9] or not IT2 = [0,(x9 + y9)] ) or IT1 = IT2 ) given x99, y99 being Element of REAL+ such that A20: x = [0,x99] and A21: ( y = [0,y99] & IT2 = [0,(x99 + y99)] ) ; ::_thesis: IT1 = IT2 x9 = x99 by A18, A20, XTUPLE_0:1; hence IT1 = IT2 by A19, A21, XTUPLE_0:1; ::_thesis: verum end; consistency for b1 being Element of REAL holds ( ( x in REAL+ & y in REAL+ & x in REAL+ & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 + y9 ) iff ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = x9 - y9 ) ) ) & ( x in REAL+ & y in REAL+ & y in REAL+ & x in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 + y9 ) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = y9 - x9 ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] & y in REAL+ & x in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = x9 - y9 ) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = y9 - x9 ) ) ) ) by Th5, XBOOLE_0:3; commutativity for b1, x, y being Element of REAL st ( x in REAL+ & y in REAL+ implies ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 + y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = x9 - y9 ) ) & ( y in REAL+ & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = y9 - x9 ) ) & ( ( 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 x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = [0,(x9 + y9)] ) ) holds ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st ( y = x9 & x = y9 & b1 = x9 + y9 ) ) & ( y in REAL+ & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st ( y = x9 & x = [0,y9] & b1 = x9 - y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st ( y = [0,x9] & x = y9 & b1 = y9 - x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) implies ex x9, y9 being Element of REAL+ st ( y = [0,x9] & x = [0,y9] & b1 = [0,(x9 + y9)] ) ) ) ; func * (x,y) -> Element of REAL means :Def2: :: ARYTM_0:def 2 ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & it = x9 *' y9 ) if ( x in REAL+ & y in REAL+ ) ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & it = [0,(x9 *' y9)] ) if ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 ) ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & it = [0,(y9 *' x9)] ) if ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 ) ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & it = y9 *' x9 ) if ( x in [:{0},REAL+:] & y in [:{0},REAL+:] ) otherwise it = 0 ; existence ( ( x in REAL+ & y in REAL+ implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 *' y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) implies ex b1 being Element of REAL st b1 = 0 ) ) proof hereby ::_thesis: ( ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) implies ex b1 being Element of REAL st b1 = 0 ) ) assume ( x in REAL+ & y in REAL+ ) ; ::_thesis: ex IT being Element of REAL ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & IT = x9 *' y9 ) then reconsider x9 = x, y9 = y as Element of REAL+ ; x9 *' y9 in REAL+ ; then reconsider IT = x9 *' y9 as Element of REAL by Th1; take IT = IT; ::_thesis: ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & IT = x9 *' y9 ) take x9 = x9; ::_thesis: ex y9 being Element of REAL+ st ( x = x9 & y = y9 & IT = x9 *' y9 ) take y9 = y9; ::_thesis: ( x = x9 & y = y9 & IT = x9 *' y9 ) thus ( x = x9 & y = y9 & IT = x9 *' y9 ) ; ::_thesis: verum end; hereby ::_thesis: ( ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) implies ex b1 being Element of REAL st b1 = 0 ) ) assume x in REAL+ ; ::_thesis: ( y in [:{0},REAL+:] & x <> 0 implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] ) ) then reconsider x9 = x as Element of REAL+ ; assume y in [:{0},REAL+:] ; ::_thesis: ( x <> 0 implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] ) ) then consider z, y9 being set such that A22: z in {0} and A23: y9 in REAL+ and A24: y = [z,y9] by ZFMISC_1:84; reconsider y9 = y9 as Element of REAL+ by A23; y = [0,y9] by A22, A24, TARSKI:def_1; then A25: y9 <> 0 by Th3; assume x <> 0 ; ::_thesis: ex IT being Element of REAL ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] ) then reconsider IT = [0,(x9 *' y9)] as Element of REAL by A25, Th2, ARYTM_1:2; take IT = IT; ::_thesis: ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] ) take x9 = x9; ::_thesis: ex y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] ) take y9 = y9; ::_thesis: ( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] ) thus ( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] ) by A22, A24, TARSKI:def_1; ::_thesis: verum end; hereby ::_thesis: ( ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) implies ex b1 being Element of REAL st b1 = 0 ) ) assume y in REAL+ ; ::_thesis: ( x in [:{0},REAL+:] & y <> 0 implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] ) ) then reconsider y9 = y as Element of REAL+ ; assume x in [:{0},REAL+:] ; ::_thesis: ( y <> 0 implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] ) ) then consider z, x9 being set such that A26: z in {0} and A27: x9 in REAL+ and A28: x = [z,x9] by ZFMISC_1:84; reconsider x9 = x9 as Element of REAL+ by A27; x = [0,x9] by A26, A28, TARSKI:def_1; then A29: x9 <> 0 by Th3; assume y <> 0 ; ::_thesis: ex IT being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] ) then reconsider IT = [0,(y9 *' x9)] as Element of REAL by A29, Th2, ARYTM_1:2; take IT = IT; ::_thesis: ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] ) take x9 = x9; ::_thesis: ex y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] ) take y9 = y9; ::_thesis: ( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] ) thus ( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] ) by A26, A28, 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+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) implies ex b1 being Element of REAL st b1 = 0 ) assume x in [:{0},REAL+:] ; ::_thesis: ( y in [:{0},REAL+:] implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT = y9 *' x9 ) ) then consider z1, x9 being set such that A30: z1 in {0} and A31: x9 in REAL+ and A32: x = [z1,x9] by ZFMISC_1:84; reconsider x9 = x9 as Element of REAL+ by A31; assume y in [:{0},REAL+:] ; ::_thesis: ex IT being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT = y9 *' x9 ) then consider z2, y9 being set such that A33: z2 in {0} and A34: y9 in REAL+ and A35: y = [z2,y9] by ZFMISC_1:84; reconsider y9 = y9 as Element of REAL+ by A34; x9 *' y9 in REAL+ ; then reconsider IT = y9 *' x9 as Element of REAL by Th1; take IT = IT; ::_thesis: ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT = y9 *' x9 ) take x9 = x9; ::_thesis: ex y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT = y9 *' x9 ) take y9 = y9; ::_thesis: ( x = [0,x9] & y = [0,y9] & IT = y9 *' x9 ) thus ( x = [0,x9] & y = [0,y9] & IT = y9 *' x9 ) by A30, A32, A33, A35, TARSKI:def_1; ::_thesis: verum end; thus ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) implies ex b1 being Element of REAL st b1 = 0 ) ; ::_thesis: verum end; uniqueness for b1, b2 being Element of REAL holds ( ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 *' y9 ) & ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b2 = x9 *' y9 ) implies b1 = b2 ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 & ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) & ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b2 = [0,(x9 *' y9)] ) implies b1 = b2 ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b2 = [0,(y9 *' x9)] ) implies b1 = b2 ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b2 = y9 *' x9 ) implies b1 = b2 ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & b1 = 0 & b2 = 0 implies b1 = b2 ) ) proof let IT1, IT2 be Element of REAL ; ::_thesis: ( ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & IT1 = x9 *' y9 ) & ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & IT2 = x9 *' y9 ) implies IT1 = IT2 ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 & ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & IT1 = [0,(x9 *' y9)] ) & ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & IT2 = [0,(x9 *' y9)] ) implies IT1 = IT2 ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT1 = [0,(y9 *' x9)] ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT2 = [0,(y9 *' x9)] ) implies IT1 = IT2 ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT1 = y9 *' x9 ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT2 = y9 *' x9 ) implies IT1 = IT2 ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) ) thus ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & IT1 = x9 *' y9 ) & ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & IT2 = x9 *' y9 ) implies IT1 = IT2 ) ; ::_thesis: ( ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 & ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & IT1 = [0,(x9 *' y9)] ) & ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & IT2 = [0,(x9 *' y9)] ) implies IT1 = IT2 ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT1 = [0,(y9 *' x9)] ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT2 = [0,(y9 *' x9)] ) implies IT1 = IT2 ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT1 = y9 *' x9 ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT2 = y9 *' x9 ) implies IT1 = IT2 ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) ) thus ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 & ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & IT1 = [0,(x9 *' y9)] ) & ex x99, y99 being Element of REAL+ st ( x = x99 & y = [0,y99] & IT2 = [0,(x99 *' y99)] ) implies IT1 = IT2 ) by XTUPLE_0:1; ::_thesis: ( ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT1 = [0,(y9 *' x9)] ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT2 = [0,(y9 *' x9)] ) implies IT1 = IT2 ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT1 = y9 *' x9 ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT2 = y9 *' x9 ) implies IT1 = IT2 ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) ) thus ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & IT1 = [0,(y9 *' x9)] ) & ex x99, y99 being Element of REAL+ st ( x = [0,x99] & y = y99 & IT2 = [0,(y99 *' x99)] ) implies IT1 = IT2 ) by XTUPLE_0:1; ::_thesis: ( ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT1 = y9 *' x9 ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT2 = y9 *' x9 ) implies IT1 = IT2 ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) ) hereby ::_thesis: ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) assume that x in [:{0},REAL+:] and y in [:{0},REAL+:] ; ::_thesis: ( ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & IT1 = y9 *' x9 ) & ex x99, y99 being Element of REAL+ st ( x = [0,x99] & y = [0,y99] & IT2 = y99 *' x99 ) implies IT1 = IT2 ) given x9, y9 being Element of REAL+ such that A36: x = [0,x9] and A37: ( y = [0,y9] & IT1 = y9 *' x9 ) ; ::_thesis: ( ex x99, y99 being Element of REAL+ st ( x = [0,x99] & y = [0,y99] & IT2 = y99 *' x99 ) implies IT1 = IT2 ) given x99, y99 being Element of REAL+ such that A38: x = [0,x99] and A39: ( y = [0,y99] & IT2 = y99 *' x99 ) ; ::_thesis: IT1 = IT2 x9 = x99 by A36, A38, XTUPLE_0:1; hence IT1 = IT2 by A37, A39, XTUPLE_0:1; ::_thesis: verum end; thus ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) ; ::_thesis: verum end; consistency for b1 being Element of REAL holds ( ( x in REAL+ & y in REAL+ & x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 *' y9 ) iff ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) ) ) & ( x in REAL+ & y in REAL+ & y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 *' y9 ) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) ) ) & ( x in REAL+ & y in REAL+ & x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 *' y9 ) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 & y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 & x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 & x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) ) ) ) by Th5, XBOOLE_0:3; commutativity for b1, x, y being Element of REAL st ( x in REAL+ & y in REAL+ implies ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 *' y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) implies b1 = 0 ) holds ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st ( y = x9 & x = y9 & b1 = x9 *' y9 ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ex x9, y9 being Element of REAL+ st ( y = x9 & x = [0,y9] & b1 = [0,(x9 *' y9)] ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ex x9, y9 being Element of REAL+ st ( y = [0,x9] & x = y9 & b1 = [0,(y9 *' x9)] ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st ( y = [0,x9] & x = [0,y9] & b1 = y9 *' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) implies b1 = 0 ) ) ; end; :: deftheorem Def1 defines + ARYTM_0:def_1_:_ for x, y, b3 being Element of REAL holds ( ( x in REAL+ & y in REAL+ implies ( b3 = + (x,y) iff ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b3 = x9 + y9 ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] implies ( b3 = + (x,y) iff ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b3 = x9 - y9 ) ) ) & ( y in REAL+ & x in [:{0},REAL+:] implies ( b3 = + (x,y) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b3 = y9 - x9 ) ) ) & ( ( 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 ( b3 = + (x,y) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b3 = [0,(x9 + y9)] ) ) ) ); :: deftheorem Def2 defines * ARYTM_0:def_2_:_ for x, y, b3 being Element of REAL holds ( ( x in REAL+ & y in REAL+ implies ( b3 = * (x,y) iff ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b3 = x9 *' y9 ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ( b3 = * (x,y) iff ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b3 = [0,(x9 *' y9)] ) ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ( b3 = * (x,y) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b3 = [0,(y9 *' x9)] ) ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( b3 = * (x,y) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b3 = y9 *' x9 ) ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) implies ( b3 = * (x,y) iff b3 = 0 ) ) ); definition let x be Element of REAL ; func opp x -> Element of REAL means :Def3: :: ARYTM_0:def 3 + (x,it) = 0 ; existence ex b1 being Element of REAL st + (x,b1) = 0 proof reconsider z9 = 0 as Element of REAL+ by ARYTM_2:20; A1: x in REAL+ \/ [:{0},REAL+:] by NUMBERS:def_1, XBOOLE_0:def_5; percases ( x = 0 or ( x in REAL+ & x <> 0 ) or x in [:{0},REAL+:] ) by A1, XBOOLE_0:def_3; supposeA2: x = 0 ; ::_thesis: ex b1 being Element of REAL st + (x,b1) = 0 then reconsider x9 = x as Element of REAL+ by ARYTM_2:20; take x ; ::_thesis: + (x,x) = 0 x9 + x9 = 0 by A2, ARYTM_2:def_8; hence + (x,x) = 0 by Def1; ::_thesis: verum end; supposethat 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, XTUPLE_0:1; 0 in {0} by TARSKI:def_1; then A6: [0,x] in [:{0},REAL+:] by A3, ZFMISC_1:87; 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:56; 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, Def1; ::_thesis: verum end; supposeA8: 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:84; reconsider y = b as Element of REAL by A10, Th1; take y ; ::_thesis: + (x,y) = 0 now__::_thesis:_(_(_x_in_REAL+_&_y_in_REAL+_&_ex_x9,_y9_being_Element_of_REAL+_st_ (_x_=_x9_&_y_=_y9_&_0_=_x9_+_y9_)_)_or_(_x_in_REAL+_&_y_in_[:{0},REAL+:]_&_ex_x9,_y9_being_Element_of_REAL+_st_ (_x_=_x9_&_y_=_[0,y9]_&_0_=_x9_-_y9_)_)_or_(_y_in_REAL+_&_x_in_[:{0},REAL+:]_&_ex_x9,_y9_being_Element_of_REAL+_st_ (_x_=_[0,x9]_&_y_=_y9_&_0_=_y9_-_x9_)_)_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+:]_)_&_ex_x9,_y9_being_Element_of_REAL+_st_ (_x_=_[0,x9]_&_y_=_[0,y9]_&_0_=_[0,(y9_+_x9)]_)_)_) percases ( ( 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 Def1; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Element of REAL st + (x,b1) = 0 & + (x,b2) = 0 holds b1 = b2 proof let y, z be Element of REAL ; ::_thesis: ( + (x,y) = 0 & + (x,z) = 0 implies y = z ) assume that A12: + (x,y) = 0 and A13: + (x,z) = 0 ; ::_thesis: y = z percases ( ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & y in REAL+ & z in [:{0},REAL+:] ) or ( x in REAL+ & z in REAL+ & y in [:{0},REAL+:] ) or ( x in REAL+ & y in [:{0},REAL+:] & z in [:{0},REAL+:] ) or ( z in REAL+ & 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+:] ) ) or ( ( not x in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not z in [:{0},REAL+:] ) & ( not z in REAL+ or not x in [:{0},REAL+:] ) ) ) ; suppose ( x in REAL+ & y in REAL+ & z in REAL+ ) ; ::_thesis: y = z then ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & 0 = x9 + y9 ) & ex x9, y9 being Element of REAL+ st ( x = x9 & z = y9 & 0 = x9 + y9 ) ) by A12, A13, Def1; hence y = z by ARYTM_2:11; ::_thesis: verum end; supposethat A14: x in REAL+ and A15: y in REAL+ and A16: z in [:{0},REAL+:] ; ::_thesis: y = z consider x99, y99 being Element of REAL+ such that A17: x = x99 and A18: ( z = [0,y99] & 0 = x99 - y99 ) by A13, A14, A16, Def1; ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & 0 = x9 + y9 ) by A12, A14, A15, Def1; then A19: x99 = 0 by A17, ARYTM_2:5; [0,0] in {[0,0]} by TARSKI:def_1; then A20: not [0,0] in REAL by NUMBERS:def_1, XBOOLE_0:def_5; z in REAL ; hence y = z by A18, A19, A20, ARYTM_1:19; ::_thesis: verum end; supposethat A21: x in REAL+ and A22: z in REAL+ and A23: y in [:{0},REAL+:] ; ::_thesis: y = z consider x99, y9 being Element of REAL+ such that A24: x = x99 and A25: ( y = [0,y9] & 0 = x99 - y9 ) by A12, A21, A23, Def1; ex x9, z9 being Element of REAL+ st ( x = x9 & z = z9 & 0 = x9 + z9 ) by A13, A21, A22, Def1; then A26: x99 = 0 by A24, ARYTM_2:5; [0,0] in {[0,0]} by TARSKI:def_1; then A27: not [0,0] in REAL by NUMBERS:def_1, XBOOLE_0:def_5; y in REAL ; hence y = z by A25, A26, A27, ARYTM_1:19; ::_thesis: verum end; supposethat A28: x in REAL+ and A29: y in [:{0},REAL+:] and A30: z in [:{0},REAL+:] ; ::_thesis: y = z consider x99, z9 being Element of REAL+ such that A31: x = x99 and A32: z = [0,z9] and A33: 0 = x99 - z9 by A13, A28, A30, Def1; consider x9, y9 being Element of REAL+ such that A34: x = x9 and A35: y = [0,y9] and A36: 0 = x9 - y9 by A12, A28, A29, Def1; y9 = x9 by A36, Th6 .= z9 by A34, A31, A33, Th6 ; hence y = z by A35, A32; ::_thesis: verum end; supposethat A37: z in REAL+ and A38: y in REAL+ and A39: x in [:{0},REAL+:] ; ::_thesis: y = z consider x99, z9 being Element of REAL+ such that A40: x = [0,x99] and A41: z = z9 and A42: 0 = z9 - x99 by A13, A37, A39, Def1; consider x9, y9 being Element of REAL+ such that A43: x = [0,x9] and A44: y = y9 and A45: 0 = y9 - x9 by A12, A38, A39, Def1; x9 = x99 by A43, A40, XTUPLE_0:1; then z9 = x9 by A42, Th6 .= y9 by A45, Th6 ; hence y = z by A44, A41; ::_thesis: verum end; suppose ( ( 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: y = z then ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & 0 = [0,(x9 + y9)] ) by A12, Def1; hence y = z ; ::_thesis: verum end; suppose ( ( not x in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not z in [:{0},REAL+:] ) & ( not z in REAL+ or not x in [:{0},REAL+:] ) ) ; ::_thesis: y = z then ex x9, z9 being Element of REAL+ st ( x = [0,x9] & z = [0,z9] & 0 = [0,(x9 + z9)] ) by A13, Def1; hence y = z ; ::_thesis: verum end; end; end; involutiveness for b1, b2 being Element of REAL st + (b2,b1) = 0 holds + (b1,b2) = 0 ; func inv x -> Element of REAL means :Def4: :: ARYTM_0:def 4 * (x,it) = 1 if x <> 0 otherwise it = 0 ; existence ( ( x <> 0 implies ex b1 being Element of REAL st * (x,b1) = 1 ) & ( not x <> 0 implies ex b1 being Element of REAL st b1 = 0 ) ) proof thus ( x <> 0 implies ex y being Element of REAL st * (x,y) = 1 ) ::_thesis: ( not x <> 0 implies ex b1 being Element of REAL st b1 = 0 ) proof A46: x in REAL+ \/ [:{0},REAL+:] by NUMBERS:def_1, XBOOLE_0:def_5; assume A47: x <> 0 ; ::_thesis: ex y being Element of REAL st * (x,y) = 1 percases ( x in REAL+ or x in [:{0},REAL+:] ) by A46, XBOOLE_0:def_3; suppose x in REAL+ ; ::_thesis: ex y being Element of REAL st * (x,y) = 1 then reconsider x9 = x as Element of REAL+ ; consider y9 being Element of REAL+ such that A48: x9 *' y9 = 1 by A47, ARYTM_2:14; y9 in REAL+ ; then reconsider y = y9 as Element of REAL by Th1; take y ; ::_thesis: * (x,y) = 1 thus * (x,y) = 1 by A48, Def2; ::_thesis: verum end; supposeA49: x in [:{0},REAL+:] ; ::_thesis: ex y being Element of REAL st * (x,y) = 1 not x in {[0,0]} by NUMBERS:def_1, XBOOLE_0:def_5; then A50: x <> [0,0] by TARSKI:def_1; consider x1, x2 being set such that x1 in {0} and A51: x2 in REAL+ and A52: x = [x1,x2] by A49, ZFMISC_1:84; reconsider x2 = x2 as Element of REAL+ by A51; x1 in {0} by A49, A52, ZFMISC_1:87; then x2 <> 0 by A52, A50, TARSKI:def_1; then consider y2 being Element of REAL+ such that A53: x2 *' y2 = 1 by ARYTM_2:14; A54: now__::_thesis:_not_[0,y2]_in_{[0,0]} assume [0,y2] in {[0,0]} ; ::_thesis: contradiction then [0,y2] = [0,0] by TARSKI:def_1; then y2 = 0 by XTUPLE_0:1; hence contradiction by A53, ARYTM_2:4; ::_thesis: verum end; A55: [0,y2] in [:{0},REAL+:] by Lm1, ZFMISC_1:87; then [0,y2] in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def_3; then reconsider y = [0,y2] as Element of REAL by A54, NUMBERS:def_1, XBOOLE_0:def_5; take y ; ::_thesis: * (x,y) = 1 consider x9, y9 being Element of REAL+ such that A56: x = [0,x9] and A57: y = [0,y9] and A58: * (x,y) = y9 *' x9 by A49, A55, Def2; y9 = y2 by A57, XTUPLE_0:1; hence * (x,y) = 1 by A52, A53, A56, A58, XTUPLE_0:1; ::_thesis: verum end; end; end; thus ( not x <> 0 implies ex b1 being Element of REAL st b1 = 0 ) ; ::_thesis: verum end; uniqueness for b1, b2 being Element of REAL holds ( ( x <> 0 & * (x,b1) = 1 & * (x,b2) = 1 implies b1 = b2 ) & ( not x <> 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) ) proof let y, z be Element of REAL ; ::_thesis: ( ( x <> 0 & * (x,y) = 1 & * (x,z) = 1 implies y = z ) & ( not x <> 0 & y = 0 & z = 0 implies y = z ) ) thus ( x <> 0 & * (x,y) = 1 & * (x,z) = 1 implies y = z ) ::_thesis: ( not x <> 0 & y = 0 & z = 0 implies y = z ) proof assume that A59: x <> 0 and A60: * (x,y) = 1 and A61: * (x,z) = 1 ; ::_thesis: y = z A62: for x, y being Element of REAL st * (x,y) = 1 holds x <> 0 proof let x, y be Element of REAL ; ::_thesis: ( * (x,y) = 1 implies x <> 0 ) assume that A63: * (x,y) = 1 and A64: x = 0 ; ::_thesis: contradiction A65: not x in [:{0},REAL+:] by A64, Th5, ARYTM_2:20, XBOOLE_0:3; A66: y in REAL+ \/ [:{0},REAL+:] by NUMBERS:def_1, XBOOLE_0:def_5; percases ( y in REAL+ or y in [:{0},REAL+:] ) by A66, XBOOLE_0:def_3; suppose y in REAL+ ; ::_thesis: contradiction then ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & 1 = x9 *' y9 ) by A63, A64, Def2, ARYTM_2:20; hence contradiction by A64, ARYTM_2:4; ::_thesis: verum end; suppose y in [:{0},REAL+:] ; ::_thesis: contradiction then not y in REAL+ by Th5, XBOOLE_0:3; hence contradiction by A63, A64, A65, Def2; ::_thesis: verum end; end; end; then A67: y <> 0 by A60; A68: z <> 0 by A61, A62; percases ( ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & z in [:{0},REAL+:] ) or ( x in REAL+ & y in [:{0},REAL+:] ) or ( x in [:{0},REAL+:] & y in REAL+ ) or ( x in [:{0},REAL+:] & z in REAL+ ) or ( x in REAL+ & z in [:{0},REAL+:] ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) ) or ( ( not x in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not z in [:{0},REAL+:] or not x <> 0 ) & ( not z in REAL+ or not x in [:{0},REAL+:] or not z <> 0 ) & ( not x in [:{0},REAL+:] or not z in [:{0},REAL+:] ) ) ) ; suppose ( x in REAL+ & y in REAL+ & z in REAL+ ) ; ::_thesis: y = z then ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & 1 = x9 *' y9 ) & ex x9, y9 being Element of REAL+ st ( x = x9 & z = y9 & 1 = x9 *' y9 ) ) by A60, A61, Def2; hence y = z by A59, Th7; ::_thesis: verum end; supposethat A69: x in [:{0},REAL+:] and A70: y in [:{0},REAL+:] and A71: z in [:{0},REAL+:] ; ::_thesis: y = z consider x9, y9 being Element of REAL+ such that A72: x = [0,x9] and A73: ( y = [0,y9] & 1 = y9 *' x9 ) by A60, A69, A70, Def2; consider x99, z9 being Element of REAL+ such that A74: x = [0,x99] and A75: ( z = [0,z9] & 1 = z9 *' x99 ) by A61, A69, A71, Def2; x9 = x99 by A72, A74, XTUPLE_0:1; hence y = z by A72, A73, A75, Th3, Th7; ::_thesis: verum end; suppose ( x in REAL+ & y in [:{0},REAL+:] ) ; ::_thesis: y = z then ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & 1 = [0,(x9 *' y9)] ) by A59, A60, Def2; hence y = z by Lm2; ::_thesis: verum end; suppose ( x in [:{0},REAL+:] & y in REAL+ ) ; ::_thesis: y = z then ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & 1 = [0,(y9 *' x9)] ) by A60, A67, Def2; hence y = z by Lm2; ::_thesis: verum end; suppose ( x in [:{0},REAL+:] & z in REAL+ ) ; ::_thesis: y = z then ex x9, z9 being Element of REAL+ st ( x = [0,x9] & z = z9 & 1 = [0,(z9 *' x9)] ) by A61, A68, Def2; hence y = z by Lm2; ::_thesis: verum end; suppose ( x in REAL+ & z in [:{0},REAL+:] ) ; ::_thesis: y = z then ex x9, z9 being Element of REAL+ st ( x = x9 & z = [0,z9] & 1 = [0,(x9 *' z9)] ) by A59, A61, Def2; hence y = z by Lm2; ::_thesis: verum end; suppose ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) ) ; ::_thesis: y = z hence y = z by A60, Def2; ::_thesis: verum end; suppose ( ( not x in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not z in [:{0},REAL+:] or not x <> 0 ) & ( not z in REAL+ or not x in [:{0},REAL+:] or not z <> 0 ) & ( not x in [:{0},REAL+:] or not z in [:{0},REAL+:] ) ) ; ::_thesis: y = z hence y = z by A61, Def2; ::_thesis: verum end; end; end; thus ( not x <> 0 & y = 0 & z = 0 implies y = z ) ; ::_thesis: verum end; consistency for b1 being Element of REAL holds verum ; involutiveness for b1, b2 being Element of REAL st ( b2 <> 0 implies * (b2,b1) = 1 ) & ( not b2 <> 0 implies b1 = 0 ) holds ( ( b1 <> 0 implies * (b1,b2) = 1 ) & ( not b1 <> 0 implies b2 = 0 ) ) proof let x, y be Element of REAL ; ::_thesis: ( ( y <> 0 implies * (y,x) = 1 ) & ( not y <> 0 implies x = 0 ) implies ( ( x <> 0 implies * (x,y) = 1 ) & ( not x <> 0 implies y = 0 ) ) ) assume that A76: ( y <> 0 implies * (y,x) = 1 ) and A77: ( y = 0 implies x = 0 ) ; ::_thesis: ( ( x <> 0 implies * (x,y) = 1 ) & ( not x <> 0 implies y = 0 ) ) thus ( x <> 0 implies * (x,y) = 1 ) by A76, A77; ::_thesis: ( not x <> 0 implies y = 0 ) assume A78: x = 0 ; ::_thesis: y = 0 A79: y in REAL+ \/ [:{0},REAL+:] by NUMBERS:def_1, XBOOLE_0:def_5; assume A80: y <> 0 ; ::_thesis: contradiction percases ( y in REAL+ or y in [:{0},REAL+:] ) by A79, XBOOLE_0:def_3; suppose y in REAL+ ; ::_thesis: contradiction then ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & 1 = x9 *' y9 ) by A76, A78, A80, Def2, ARYTM_2:20; hence contradiction by A78, ARYTM_2:4; ::_thesis: verum end; supposeA81: y in [:{0},REAL+:] ; ::_thesis: contradiction A82: not x in [:{0},REAL+:] by A78, Th5, ARYTM_2:20, XBOOLE_0:3; not y in REAL+ by A81, Th5, XBOOLE_0:3; hence contradiction by A76, A78, A80, A82, Def2; ::_thesis: verum end; end; end; end; :: deftheorem Def3 defines opp ARYTM_0:def_3_:_ for x, b2 being Element of REAL holds ( b2 = opp x iff + (x,b2) = 0 ); :: deftheorem Def4 defines inv ARYTM_0:def_4_:_ for x, b2 being Element of REAL holds ( ( x <> 0 implies ( b2 = inv x iff * (x,b2) = 1 ) ) & ( not x <> 0 implies ( b2 = inv x iff b2 = 0 ) ) ); begin Lm3: for x, y, z being set st [x,y] = {z} holds ( z = {x} & x = y ) proof let x, y, z be set ; ::_thesis: ( [x,y] = {z} implies ( z = {x} & x = y ) ) assume [x,y] = {z} ; ::_thesis: ( z = {x} & x = y ) then A1: {{x,y},{x}} = {z} by TARSKI:def_5; then {x} in {z} by TARSKI:def_2; hence A2: z = {x} by TARSKI:def_1; ::_thesis: x = y {x,y} in {z} by A1, TARSKI:def_2; then {x,y} = z by TARSKI:def_1; hence x = y by A2, ZFMISC_1:5; ::_thesis: verum end; theorem Th8: :: ARYTM_0:8 for a, b being Element of REAL holds not (0,1) --> (a,b) in REAL proof let a, b be Element of REAL ; ::_thesis: not (0,1) --> (a,b) in REAL set IR = { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds ( ( for s being Element of RAT+ st s <=' r holds s in A ) & ex s being Element of RAT+ st ( s in A & r < s ) ) } ; set f = (0,1) --> (a,b); A1: now__::_thesis:_not_(0,1)_-->_(a,b)_in_[:{{}},REAL+:] (0,1) --> (a,b) = {[0,a],[1,b]} by FUNCT_4:67; then A2: [1,b] in (0,1) --> (a,b) by TARSKI:def_2; assume (0,1) --> (a,b) in [:{{}},REAL+:] ; ::_thesis: contradiction then consider x, y being set such that A3: x in {{}} and y in REAL+ and A4: (0,1) --> (a,b) = [x,y] by ZFMISC_1:84; x = 0 by A3, TARSKI:def_1; then (0,1) --> (a,b) = {{0,y},{0}} by A4, TARSKI:def_5; then A5: ( [1,b] = {0} or [1,b] = {0,y} ) by A2, TARSKI:def_2; percases ( {{1,b},{1}} = {0} or {{1,b},{1}} = {0,y} ) by A5, TARSKI:def_5; suppose {{1,b},{1}} = {0} ; ::_thesis: contradiction then 0 in {{1,b},{1}} by TARSKI:def_1; hence contradiction by TARSKI:def_2; ::_thesis: verum end; suppose {{1,b},{1}} = {0,y} ; ::_thesis: contradiction then 0 in {{1,b},{1}} by TARSKI:def_2; hence contradiction by TARSKI:def_2; ::_thesis: verum end; end; end; A6: (0,1) --> (a,b) = {[0,a],[1,b]} by FUNCT_4:67; now__::_thesis:_not_(0,1)_-->_(a,b)_in__{__[i,j]_where_i,_j_is_Element_of_NAT_:_(_i,j_are_relative_prime_&_j_<>_{}_)__}_ assume (0,1) --> (a,b) in { [i,j] where i, j is Element of NAT : ( i,j are_relative_prime & j <> {} ) } ; ::_thesis: contradiction then consider i, j being Element of NAT such that A7: (0,1) --> (a,b) = [i,j] and i,j are_relative_prime and j <> {} ; A8: (0,1) --> (a,b) = {{i,j},{i}} by A7, TARSKI:def_5; then A9: ( {i} in (0,1) --> (a,b) & {i,j} in (0,1) --> (a,b) ) by TARSKI:def_2; A10: now__::_thesis:_not_i_=_j assume i = j ; ::_thesis: contradiction then {i} = {i,j} by ENUMSET1:29; then A11: [i,j] = {{i}} by A7, A8, ENUMSET1:29; then [1,b] in {{i}} by A6, A7, TARSKI:def_2; then A12: [1,b] = {i} by TARSKI:def_1; [0,a] in {{i}} by A6, A7, A11, TARSKI:def_2; then [0,a] = {i} by TARSKI:def_1; hence contradiction by A12, XTUPLE_0:1; ::_thesis: verum end; A13: [1,b] = {{1,b},{1}} by TARSKI:def_5; A14: [0,a] = {{0,a},{0}} by TARSKI:def_5; percases ( ( {i,j} = [0,a] & {i} = [0,a] ) or ( {i,j} = [0,a] & {i} = [1,b] ) or ( {i,j} = [1,b] & {i} = [0,a] ) or ( {i,j} = [1,b] & {i} = [1,b] ) ) by A6, A9, TARSKI:def_2; suppose ( {i,j} = [0,a] & {i} = [0,a] ) ; ::_thesis: contradiction hence contradiction by A10, ZFMISC_1:5; ::_thesis: verum end; supposethat A15: {i,j} = [0,a] and A16: {i} = [1,b] ; ::_thesis: contradiction i in [0,a] by A15, TARSKI:def_2; then ( i = {0,a} or i = {0} ) by A14, TARSKI:def_2; then A17: 0 in i by TARSKI:def_1, TARSKI:def_2; i = {1} by A16, Lm3; hence contradiction by A17, TARSKI:def_1; ::_thesis: verum end; supposethat A18: {i,j} = [1,b] and A19: {i} = [0,a] ; ::_thesis: contradiction i in [1,b] by A18, TARSKI:def_2; then ( i = {1,b} or i = {1} ) by A13, TARSKI:def_2; then A20: 1 in i by TARSKI:def_1, TARSKI:def_2; i = {0} by A19, Lm3; hence contradiction by A20, TARSKI:def_1; ::_thesis: verum end; suppose ( {i,j} = [1,b] & {i} = [1,b] ) ; ::_thesis: contradiction hence contradiction by A10, ZFMISC_1:5; ::_thesis: verum end; end; end; then A21: not (0,1) --> (a,b) in { [i,j] where i, j is Element of NAT : ( i,j are_relative_prime & j <> {} ) } \ { [k,1] where k is Element of NAT : verum } ; for x, y being set holds not {[0,x],[1,y]} in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds ( ( for s being Element of RAT+ st s <=' r holds s in A ) & ex s being Element of RAT+ st ( s in A & r < s ) ) } proof given x, y being set such that A22: {[0,x],[1,y]} in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds ( ( for s being Element of RAT+ st s <=' r holds s in A ) & ex s being Element of RAT+ st ( s in A & r < s ) ) } ; ::_thesis: contradiction consider A being Subset of RAT+ such that A23: {[0,x],[1,y]} = A and A24: for r being Element of RAT+ st r in A holds ( ( for s being Element of RAT+ st s <=' r holds s in A ) & ex s being Element of RAT+ st ( s in A & r < s ) ) by A22; ( [0,x] in A & ( for r, s being Element of RAT+ st r in A & s <=' r holds s in A ) ) by A23, A24, TARSKI:def_2; then consider r1, r2, r3 being Element of RAT+ such that A25: r1 in A and A26: r2 in A and A27: ( r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1 ) by ARYTM_3:75; A28: ( r2 = [0,x] or r2 = [1,y] ) by A23, A26, TARSKI:def_2; ( r1 = [0,x] or r1 = [1,y] ) by A23, A25, TARSKI:def_2; hence contradiction by A23, A27, A28, TARSKI:def_2; ::_thesis: verum end; then A29: not (0,1) --> (a,b) in DEDEKIND_CUTS by A6, ARYTM_2:def_1; now__::_thesis:_not_(0,1)_-->_(a,b)_in_omega assume (0,1) --> (a,b) in omega ; ::_thesis: contradiction then {} in (0,1) --> (a,b) by ORDINAL3:8; hence contradiction by A6, TARSKI:def_2; ::_thesis: verum end; then not (0,1) --> (a,b) in RAT+ by A21, XBOOLE_0:def_3; then not (0,1) --> (a,b) in REAL+ by A29, ARYTM_2:def_2, XBOOLE_0:def_3; hence not (0,1) --> (a,b) in REAL by A1, NUMBERS:def_1, XBOOLE_0:def_3; ::_thesis: verum end; definition let x, y be Element of REAL ; func[*x,y*] -> Element of COMPLEX equals :Def5: :: ARYTM_0:def 5 x if y = 0 otherwise (0,1) --> (x,y); consistency for b1 being Element of COMPLEX holds verum ; coherence ( ( y = 0 implies x is Element of COMPLEX ) & ( not y = 0 implies (0,1) --> (x,y) is Element of COMPLEX ) ) proof set z = (0,1) --> (x,y); thus ( y = 0 implies x is Element of COMPLEX ) by NUMBERS:def_2, XBOOLE_0:def_3; ::_thesis: ( not y = 0 implies (0,1) --> (x,y) is Element of COMPLEX ) assume A1: y <> 0 ; ::_thesis: (0,1) --> (x,y) is Element of COMPLEX A2: now__::_thesis:_not_(0,1)_-->_(x,y)_in__{__r_where_r_is_Element_of_Funcs_({0,1},REAL)_:_r_._1_=_0__}_ assume (0,1) --> (x,y) in { r where r is Element of Funcs ({0,1},REAL) : r . 1 = 0 } ; ::_thesis: contradiction then ex r being Element of Funcs ({0,1},REAL) st ( (0,1) --> (x,y) = r & r . 1 = 0 ) ; hence contradiction by A1, FUNCT_4:63; ::_thesis: verum end; (0,1) --> (x,y) in Funcs ({0,1},REAL) by FUNCT_2:8; then (0,1) --> (x,y) in (Funcs ({0,1},REAL)) \ { r where r is Element of Funcs ({0,1},REAL) : r . 1 = 0 } by A2, XBOOLE_0:def_5; hence (0,1) --> (x,y) is Element of COMPLEX by NUMBERS:def_2, XBOOLE_0:def_3; ::_thesis: verum end; end; :: deftheorem Def5 defines [* ARYTM_0:def_5_:_ for x, y being Element of REAL holds ( ( y = 0 implies [*x,y*] = x ) & ( not y = 0 implies [*x,y*] = (0,1) --> (x,y) ) ); theorem :: ARYTM_0:9 for c being Element of COMPLEX ex r, s being Element of REAL st c = [*r,s*] proof let c be Element of COMPLEX ; ::_thesis: ex r, s being Element of REAL st c = [*r,s*] percases ( c in REAL or not c in REAL ) ; suppose c in REAL ; ::_thesis: ex r, s being Element of REAL st c = [*r,s*] then reconsider r = c, z = 0 as Element of REAL ; take r ; ::_thesis: ex s being Element of REAL st c = [*r,s*] take z ; ::_thesis: c = [*r,z*] thus c = [*r,z*] by Def5; ::_thesis: verum end; suppose not c in REAL ; ::_thesis: ex r, s being Element of REAL st c = [*r,s*] then A1: c in (Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } by NUMBERS:def_2, XBOOLE_0:def_3; then consider f being Function such that A2: c = f and A3: dom f = {0,1} and A4: rng f c= REAL by FUNCT_2:def_2; 1 in {0,1} by TARSKI:def_2; then A5: f . 1 in rng f by A3, FUNCT_1:3; 0 in {0,1} by TARSKI:def_2; then f . 0 in rng f by A3, FUNCT_1:3; then reconsider r = f . 0, s = f . 1 as Element of REAL by A4, A5; take r ; ::_thesis: ex s being Element of REAL st c = [*r,s*] take s ; ::_thesis: c = [*r,s*] A6: c = (0,1) --> (r,s) by A2, A3, FUNCT_4:66; now__::_thesis:_not_s_=_0 assume s = 0 ; ::_thesis: contradiction then ((0,1) --> (r,s)) . 1 = 0 by FUNCT_4:63; then c in { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } by A1, A6; hence contradiction by A1, XBOOLE_0:def_5; ::_thesis: verum end; hence c = [*r,s*] by A6, Def5; ::_thesis: verum end; end; end; theorem :: ARYTM_0:10 for x1, x2, y1, y2 being Element of REAL st [*x1,x2*] = [*y1,y2*] holds ( x1 = y1 & x2 = y2 ) proof let x1, x2, y1, y2 be Element of REAL ; ::_thesis: ( [*x1,x2*] = [*y1,y2*] implies ( x1 = y1 & x2 = y2 ) ) assume A1: [*x1,x2*] = [*y1,y2*] ; ::_thesis: ( x1 = y1 & x2 = y2 ) percases ( x2 = 0 or x2 <> 0 ) ; supposeA2: x2 = 0 ; ::_thesis: ( x1 = y1 & x2 = y2 ) then A3: [*x1,x2*] = x1 by Def5; A4: now__::_thesis:_not_y2_<>_0 assume y2 <> 0 ; ::_thesis: contradiction then x1 = (0,1) --> (y1,y2) by A1, A3, Def5; hence contradiction by Th8; ::_thesis: verum end; hence x1 = y1 by A1, A3, Def5; ::_thesis: x2 = y2 thus x2 = y2 by A2, A4; ::_thesis: verum end; suppose x2 <> 0 ; ::_thesis: ( x1 = y1 & x2 = y2 ) then A5: [*y1,y2*] = (0,1) --> (x1,x2) by A1, Def5; now__::_thesis:_not_y2_=_0 assume y2 = 0 ; ::_thesis: contradiction then [*y1,y2*] = y1 by Def5; hence contradiction by A5, Th8; ::_thesis: verum end; then [*y1,y2*] = (0,1) --> (y1,y2) by Def5; hence ( x1 = y1 & x2 = y2 ) by A5, FUNCT_4:68; ::_thesis: verum end; end; end; set RR = [:{0},REAL+:] \ {[0,0]}; reconsider o = 0 as Element of REAL ; theorem Th11: :: ARYTM_0:11 for x, o being Element of REAL st o = 0 holds + (x,o) = x proof reconsider y9 = 0 as Element of REAL+ by ARYTM_2:20; let x, o be Element of REAL ; ::_thesis: ( o = 0 implies + (x,o) = x ) assume A1: o = 0 ; ::_thesis: + (x,o) = x percases ( x in REAL+ or not x in REAL+ ) ; suppose x in REAL+ ; ::_thesis: + (x,o) = x then reconsider x9 = x as Element of REAL+ ; x9 = x9 + y9 by ARYTM_2:def_8; hence + (x,o) = x by A1, Def1; ::_thesis: verum end; supposeA2: not x in REAL+ ; ::_thesis: + (x,o) = x x in REAL+ \/ [:{{}},REAL+:] by NUMBERS:def_1, XBOOLE_0:def_5; then A3: x in [:{{}},REAL+:] by A2, XBOOLE_0:def_3; then consider x1, x2 being set such that A4: x1 in {{}} and A5: x2 in REAL+ and A6: x = [x1,x2] by ZFMISC_1:84; reconsider x9 = x2 as Element of REAL+ by A5; A7: x1 = 0 by A4, TARSKI:def_1; then x = y9 - x9 by A6, Th3, ARYTM_1:19; hence + (x,o) = x by A1, A3, A6, A7, Def1; ::_thesis: verum end; end; end; theorem Th12: :: ARYTM_0:12 for x, o being Element of REAL st o = 0 holds * (x,o) = 0 proof let x, o be Element of REAL ; ::_thesis: ( o = 0 implies * (x,o) = 0 ) assume A1: o = 0 ; ::_thesis: * (x,o) = 0 percases ( x in REAL+ or not x in REAL+ ) ; suppose x in REAL+ ; ::_thesis: * (x,o) = 0 then reconsider x9 = x, y9 = 0 as Element of REAL+ by ARYTM_2:20; 0 = x9 *' y9 by ARYTM_2:4; hence * (x,o) = 0 by A1, Def2; ::_thesis: verum end; supposeA2: not x in REAL+ ; ::_thesis: * (x,o) = 0 not o in [:{{}},REAL+:] by A1, Th5, ARYTM_2:20, XBOOLE_0:3; hence * (x,o) = 0 by A1, A2, Def2; ::_thesis: verum end; end; end; theorem Th13: :: ARYTM_0:13 for x, y, z being Element of REAL holds * (x,(* (y,z))) = * ((* (x,y)),z) proof let x, y, z be Element of REAL ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z) percases ( ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & x <> 0 & y in [:{0},REAL+:] \ {[0,0]} & z in REAL+ & z <> 0 ) or ( x in [:{0},REAL+:] \ {[0,0]} & y in REAL+ & y <> 0 & z in REAL+ & z <> 0 ) or ( x in [:{0},REAL+:] \ {[0,0]} & y in [:{0},REAL+:] \ {[0,0]} & z in REAL+ & z <> 0 ) or ( x in REAL+ & x <> 0 & y in REAL+ & y <> 0 & z in [:{0},REAL+:] \ {[0,0]} ) or ( x in REAL+ & x <> 0 & y in [:{0},REAL+:] \ {[0,0]} & z in [:{0},REAL+:] \ {[0,0]} ) or ( y in REAL+ & y <> 0 & x in [:{0},REAL+:] \ {[0,0]} & z in [:{0},REAL+:] \ {[0,0]} ) or ( x in [:{0},REAL+:] \ {[0,0]} & y in [:{0},REAL+:] \ {[0,0]} & z in [:{0},REAL+:] \ {[0,0]} ) or x = 0 or y = 0 or z = 0 or ( ( not x in REAL+ or not y in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not y in REAL+ or not x in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not x in REAL+ or not y in REAL+ or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in REAL+ or not y in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not y in REAL+ or not x in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) ) ) ; supposethat A1: x in REAL+ and A2: y in REAL+ and A3: z in REAL+ ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z) A4: ex x99, y99 being Element of REAL+ st ( x = x99 & y = y99 & * (x,y) = x99 *' y99 ) by A1, A2, Def2; then A5: ex xy99, z99 being Element of REAL+ st ( * (x,y) = xy99 & z = z99 & * ((* (x,y)),z) = xy99 *' z99 ) by A3, Def2; A6: ex y9, z9 being Element of REAL+ st ( y = y9 & z = z9 & * (y,z) = y9 *' z9 ) by A2, A3, Def2; then ex x9, yz9 being Element of REAL+ st ( x = x9 & * (y,z) = yz9 & * (x,(* (y,z))) = x9 *' yz9 ) by A1, Def2; hence * (x,(* (y,z))) = * ((* (x,y)),z) by A6, A4, A5, ARYTM_2:12; ::_thesis: verum end; supposethat A7: ( x in REAL+ & x <> 0 ) and A8: y in [:{0},REAL+:] \ {[0,0]} and A9: ( z in REAL+ & z <> 0 ) ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z) consider y9, z9 being Element of REAL+ such that A10: y = [0,y9] and A11: z = z9 and A12: * (y,z) = [0,(z9 *' y9)] by A8, A9, Def2; * (y,z) in [:{0},REAL+:] by A12, Lm1, ZFMISC_1:87; then consider x9, yz9 being Element of REAL+ such that A13: x = x9 and A14: ( * (y,z) = [0,yz9] & * (x,(* (y,z))) = [0,(x9 *' yz9)] ) by A7, Def2; consider x99, y99 being Element of REAL+ such that A15: x = x99 and A16: y = [0,y99] and A17: * (x,y) = [0,(x99 *' y99)] by A7, A8, Def2; A18: y9 = y99 by A10, A16, XTUPLE_0:1; * (x,y) in [:{0},REAL+:] by A17, Lm1, ZFMISC_1:87; then consider xy99, z99 being Element of REAL+ such that A19: * (x,y) = [0,xy99] and A20: z = z99 and A21: * ((* (x,y)),z) = [0,(z99 *' xy99)] by A9, Def2; thus * (x,(* (y,z))) = [0,(x9 *' (y9 *' z9))] by A12, A14, XTUPLE_0:1 .= [0,((x99 *' y99) *' z99)] by A11, A13, A15, A20, A18, ARYTM_2:12 .= * ((* (x,y)),z) by A17, A19, A21, XTUPLE_0:1 ; ::_thesis: verum end; supposethat A22: x in [:{0},REAL+:] \ {[0,0]} and A23: ( y in REAL+ & y <> 0 ) and A24: ( z in REAL+ & z <> 0 ) ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z) consider y9, z9 being Element of REAL+ such that A25: ( y = y9 & z = z9 ) and A26: * (y,z) = y9 *' z9 by A23, A24, Def2; y9 *' z9 <> 0 by A23, A24, A25, ARYTM_1:2; then consider x9, yz9 being Element of REAL+ such that A27: x = [0,x9] and A28: ( * (y,z) = yz9 & * (x,(* (y,z))) = [0,(yz9 *' x9)] ) by A22, A26, Def2; consider x99, y99 being Element of REAL+ such that A29: x = [0,x99] and A30: y = y99 and A31: * (x,y) = [0,(y99 *' x99)] by A22, A23, Def2; * (x,y) in [:{0},REAL+:] by A31, Lm1, ZFMISC_1:87; then consider xy99, z99 being Element of REAL+ such that A32: * (x,y) = [0,xy99] and A33: z = z99 and A34: * ((* (x,y)),z) = [0,(z99 *' xy99)] by A24, Def2; x9 = x99 by A27, A29, XTUPLE_0:1; hence * (x,(* (y,z))) = [0,((x99 *' y99) *' z99)] by A25, A26, A28, A30, A33, ARYTM_2:12 .= * ((* (x,y)),z) by A31, A32, A34, XTUPLE_0:1 ; ::_thesis: verum end; supposethat A35: x in [:{0},REAL+:] \ {[0,0]} and A36: y in [:{0},REAL+:] \ {[0,0]} and A37: ( z in REAL+ & z <> 0 ) ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z) consider x99, y99 being Element of REAL+ such that A38: x = [0,x99] and A39: y = [0,y99] and A40: * (x,y) = y99 *' x99 by A35, A36, Def2; consider y9, z9 being Element of REAL+ such that A41: y = [0,y9] and A42: z = z9 and A43: * (y,z) = [0,(z9 *' y9)] by A36, A37, Def2; A44: y9 = y99 by A41, A39, XTUPLE_0:1; * (y,z) in [:{0},REAL+:] by A43, Lm1, ZFMISC_1:87; then consider x9, yz9 being Element of REAL+ such that A45: x = [0,x9] and A46: ( * (y,z) = [0,yz9] & * (x,(* (y,z))) = yz9 *' x9 ) by A35, Def2; A47: x9 = x99 by A45, A38, XTUPLE_0:1; A48: ex xy99, z99 being Element of REAL+ st ( * (x,y) = xy99 & z = z99 & * ((* (x,y)),z) = xy99 *' z99 ) by A37, A40, Def2; thus * (x,(* (y,z))) = x9 *' (y9 *' z9) by A43, A46, XTUPLE_0:1 .= * ((* (x,y)),z) by A42, A40, A48, A47, A44, ARYTM_2:12 ; ::_thesis: verum end; supposethat A49: ( x in REAL+ & x <> 0 ) and A50: ( y in REAL+ & y <> 0 ) and A51: z in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z) A52: ex x99, y99 being Element of REAL+ st ( x = x99 & y = y99 & * (x,y) = x99 *' y99 ) by A49, A50, Def2; then * (x,y) <> 0 by A49, A50, ARYTM_1:2; then consider xy99, z99 being Element of REAL+ such that A53: * (x,y) = xy99 and A54: z = [0,z99] and A55: * ((* (x,y)),z) = [0,(xy99 *' z99)] by A51, A52, Def2; consider y9, z9 being Element of REAL+ such that A56: y = y9 and A57: z = [0,z9] and A58: * (y,z) = [0,(y9 *' z9)] by A50, A51, Def2; A59: z9 = z99 by A57, A54, XTUPLE_0:1; * (y,z) in [:{0},REAL+:] by A58, Lm1, ZFMISC_1:87; then consider x9, yz9 being Element of REAL+ such that A60: x = x9 and A61: ( * (y,z) = [0,yz9] & * (x,(* (y,z))) = [0,(x9 *' yz9)] ) by A49, Def2; thus * (x,(* (y,z))) = [0,(x9 *' (y9 *' z9))] by A58, A61, XTUPLE_0:1 .= * ((* (x,y)),z) by A56, A60, A52, A53, A55, A59, ARYTM_2:12 ; ::_thesis: verum end; supposethat A62: ( x in REAL+ & x <> 0 ) and A63: y in [:{0},REAL+:] \ {[0,0]} and A64: z in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z) consider y9, z9 being Element of REAL+ such that A65: y = [0,y9] and A66: z = [0,z9] and A67: * (y,z) = z9 *' y9 by A63, A64, Def2; A68: ex x9, yz9 being Element of REAL+ st ( x = x9 & * (y,z) = yz9 & * (x,(* (y,z))) = x9 *' yz9 ) by A62, A67, Def2; consider x99, y99 being Element of REAL+ such that A69: x = x99 and A70: y = [0,y99] and A71: * (x,y) = [0,(x99 *' y99)] by A62, A63, Def2; A72: y9 = y99 by A65, A70, XTUPLE_0:1; * (x,y) in [:{0},REAL+:] by A71, Lm1, ZFMISC_1:87; then consider xy99, z99 being Element of REAL+ such that A73: * (x,y) = [0,xy99] and A74: z = [0,z99] and A75: * ((* (x,y)),z) = z99 *' xy99 by A64, Def2; z9 = z99 by A66, A74, XTUPLE_0:1; hence * (x,(* (y,z))) = (x99 *' y99) *' z99 by A67, A68, A69, A72, ARYTM_2:12 .= * ((* (x,y)),z) by A71, A73, A75, XTUPLE_0:1 ; ::_thesis: verum end; supposethat A76: ( y in REAL+ & y <> 0 ) and A77: x in [:{0},REAL+:] \ {[0,0]} and A78: z in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z) consider x99, y99 being Element of REAL+ such that A79: x = [0,x99] and A80: y = y99 and A81: * (x,y) = [0,(y99 *' x99)] by A76, A77, Def2; consider y9, z9 being Element of REAL+ such that A82: y = y9 and A83: z = [0,z9] and A84: * (y,z) = [0,(y9 *' z9)] by A76, A78, Def2; [0,(y9 *' z9)] in [:{0},REAL+:] by Lm1, ZFMISC_1:87; then consider x9, yz9 being Element of REAL+ such that A85: x = [0,x9] and A86: ( * (y,z) = [0,yz9] & * (x,(* (y,z))) = yz9 *' x9 ) by A77, A84, Def2; A87: x9 = x99 by A85, A79, XTUPLE_0:1; * (x,y) in [:{0},REAL+:] by A81, Lm1, ZFMISC_1:87; then consider xy99, z99 being Element of REAL+ such that A88: * (x,y) = [0,xy99] and A89: z = [0,z99] and A90: * ((* (x,y)),z) = z99 *' xy99 by A78, Def2; A91: z9 = z99 by A83, A89, XTUPLE_0:1; thus * (x,(* (y,z))) = x9 *' (y9 *' z9) by A84, A86, XTUPLE_0:1 .= (x99 *' y99) *' z99 by A82, A80, A87, A91, ARYTM_2:12 .= * ((* (x,y)),z) by A81, A88, A90, XTUPLE_0:1 ; ::_thesis: verum end; supposethat A92: x in [:{0},REAL+:] \ {[0,0]} and A93: y in [:{0},REAL+:] \ {[0,0]} and A94: z in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z) consider y9, z9 being Element of REAL+ such that A95: y = [0,y9] and A96: z = [0,z9] and A97: * (y,z) = z9 *' y9 by A93, A94, Def2; not y in {[0,0]} by A93, XBOOLE_0:def_5; then A98: y9 <> 0 by A95, TARSKI:def_1; not z in {[0,0]} by A94, XBOOLE_0:def_5; then z9 <> 0 by A96, TARSKI:def_1; then * (z,y) <> 0 by A97, A98, ARYTM_1:2; then consider x9, yz9 being Element of REAL+ such that A99: x = [0,x9] and A100: ( * (y,z) = yz9 & * (x,(* (y,z))) = [0,(yz9 *' x9)] ) by A92, A97, Def2; consider x99, y99 being Element of REAL+ such that A101: x = [0,x99] and A102: y = [0,y99] and A103: * (x,y) = y99 *' x99 by A92, A93, Def2; A104: x9 = x99 by A99, A101, XTUPLE_0:1; A105: y9 = y99 by A95, A102, XTUPLE_0:1; not y in {[0,0]} by A93, XBOOLE_0:def_5; then A106: y9 <> 0 by A95, TARSKI:def_1; not x in {[0,0]} by A92, XBOOLE_0:def_5; then x9 <> 0 by A99, TARSKI:def_1; then * (x,y) <> 0 by A103, A104, A105, A106, ARYTM_1:2; then consider xy99, z99 being Element of REAL+ such that A107: * (x,y) = xy99 and A108: z = [0,z99] and A109: * ((* (x,y)),z) = [0,(xy99 *' z99)] by A94, A103, Def2; z9 = z99 by A96, A108, XTUPLE_0:1; hence * (x,(* (y,z))) = * ((* (x,y)),z) by A97, A100, A103, A104, A105, A107, A109, ARYTM_2:12; ::_thesis: verum end; supposeA110: x = 0 ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z) hence * (x,(* (y,z))) = 0 by Th12 .= * (o,z) by Th12 .= * ((* (x,y)),z) by A110, Th12 ; ::_thesis: verum end; supposeA111: y = 0 ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z) hence * (x,(* (y,z))) = * (x,o) by Th12 .= 0 by Th12 .= * (o,z) by Th12 .= * ((* (x,y)),z) by A111, Th12 ; ::_thesis: verum end; supposeA112: z = 0 ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z) hence * (x,(* (y,z))) = * (x,o) by Th12 .= 0 by Th12 .= * ((* (x,y)),z) by A112, Th12 ; ::_thesis: verum end; supposeA113: ( ( not x in REAL+ or not y in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not y in REAL+ or not x in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not x in REAL+ or not y in REAL+ or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in REAL+ or not y in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not y in REAL+ or not x in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) ) ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z) A114: not [0,0] in REAL+ by ARYTM_2:3; REAL = (REAL+ \ {[{},{}]}) \/ ([:{{}},REAL+:] \ {[{},{}]}) by NUMBERS:def_1, XBOOLE_1:42 .= REAL+ \/ ([:{0},REAL+:] \ {[0,0]}) by A114, ZFMISC_1:57 ; hence * (x,(* (y,z))) = * ((* (x,y)),z) by A113, XBOOLE_0:def_3; ::_thesis: verum end; end; end; theorem Th14: :: ARYTM_0:14 for x, y, z being Element of REAL holds * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) proof let x, y, z be Element of REAL ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) percases ( x = 0 or ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & x <> 0 & y in REAL+ & z in [:{0},REAL+:] \ {[0,0]} ) or ( x in REAL+ & x <> 0 & z in REAL+ & y in [:{0},REAL+:] \ {[0,0]} ) or ( x in REAL+ & x <> 0 & y in [:{0},REAL+:] \ {[0,0]} & z in [:{0},REAL+:] \ {[0,0]} ) or ( x in [:{0},REAL+:] \ {[0,0]} & y in REAL+ & z in REAL+ ) or ( x in [:{0},REAL+:] \ {[0,0]} & y in REAL+ & z in [:{0},REAL+:] \ {[0,0]} ) or ( x in [:{0},REAL+:] \ {[0,0]} & z in REAL+ & y in [:{0},REAL+:] \ {[0,0]} ) or ( x in [:{0},REAL+:] \ {[0,0]} & y in [:{0},REAL+:] \ {[0,0]} & z in [:{0},REAL+:] \ {[0,0]} ) or ( ( not x in REAL+ or not y in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not y in REAL+ or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in REAL+ or not y in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in REAL+ or not z in REAL+ ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in REAL+ or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) ) ) ; supposeA1: x = 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) hence * (x,(+ (y,z))) = 0 by Th12 .= + (o,o) by Th11 .= + ((* (x,y)),o) by A1, Th12 .= + ((* (x,y)),(* (x,z))) by A1, Th12 ; ::_thesis: verum end; supposethat A2: x in REAL+ and A3: ( y in REAL+ & z in REAL+ ) ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) A4: ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & * (x,y) = x9 *' y9 ) & ex x99, z9 being Element of REAL+ st ( x = x99 & z = z9 & * (x,z) = x99 *' z9 ) ) by A2, A3, Def2; then A5: ex xy9, xz9 being Element of REAL+ st ( * (x,y) = xy9 & * (x,z) = xz9 & + ((* (x,y)),(* (x,z))) = xy9 + xz9 ) by Def1; A6: ex y99, z99 being Element of REAL+ st ( y = y99 & z = z99 & + (y,z) = y99 + z99 ) by A3, Def1; then ex x999, yz9 being Element of REAL+ st ( x = x999 & + (y,z) = yz9 & * (x,(+ (y,z))) = x999 *' yz9 ) by A2, Def2; hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) by A4, A5, A6, ARYTM_2:13; ::_thesis: verum end; supposethat A7: ( x in REAL+ & x <> 0 ) and A8: y in REAL+ and A9: z in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) consider y99, z99 being Element of REAL+ such that A10: y = y99 and A11: z = [0,z99] and A12: + (y,z) = y99 - z99 by A8, A9, Def1; consider x9, y9 being Element of REAL+ such that A13: ( x = x9 & y = y9 ) and A14: * (x,y) = x9 *' y9 by A7, A8, Def2; consider x99, z9 being Element of REAL+ such that A15: x = x99 and A16: z = [0,z9] and A17: * (x,z) = [0,(x99 *' z9)] by A7, A9, Def2; * (x,z) in [:{0},REAL+:] by A17, Lm1, ZFMISC_1:87; then A18: ex xy9, xz9 being Element of REAL+ st ( * (x,y) = xy9 & * (x,z) = [0,xz9] & + ((* (x,y)),(* (x,z))) = xy9 - xz9 ) by A14, Def1; A19: z9 = z99 by A16, A11, XTUPLE_0:1; now__::_thesis:_*_(x,(+_(y,z)))_=_+_((*_(x,y)),(*_(x,z))) percases ( z99 <=' y99 or not z99 <=' y99 ) ; supposeA20: z99 <=' y99 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) then A21: + (y,z) = y99 -' z99 by A12, ARYTM_1:def_2; then ex x999, yz9 being Element of REAL+ st ( x = x999 & + (y,z) = yz9 & * (x,(+ (y,z))) = x999 *' yz9 ) by A7, Def2; hence * (x,(+ (y,z))) = (x9 *' y9) - (x99 *' z9) by A13, A15, A10, A19, A20, A21, ARYTM_1:26 .= + ((* (x,y)),(* (x,z))) by A14, A17, A18, XTUPLE_0:1 ; ::_thesis: verum end; supposeA22: not z99 <=' y99 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) then A23: + (y,z) = [0,(z99 -' y99)] by A12, ARYTM_1:def_2; then + (y,z) in [:{0},REAL+:] by Lm1, ZFMISC_1:87; then consider x999, yz9 being Element of REAL+ such that A24: x = x999 and A25: ( + (y,z) = [0,yz9] & * (x,(+ (y,z))) = [0,(x999 *' yz9)] ) by A7, Def2; thus * (x,(+ (y,z))) = [0,(x999 *' (z99 -' y99))] by A23, A25, XTUPLE_0:1 .= (x9 *' y9) - (x99 *' z9) by A7, A13, A15, A10, A19, A22, A24, ARYTM_1:27 .= + ((* (x,y)),(* (x,z))) by A14, A17, A18, XTUPLE_0:1 ; ::_thesis: verum end; end; end; hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; ::_thesis: verum end; supposethat A26: ( x in REAL+ & x <> 0 ) and A27: z in REAL+ and A28: y in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) consider z99, y99 being Element of REAL+ such that A29: z = z99 and A30: y = [0,y99] and A31: + (z,y) = z99 - y99 by A27, A28, Def1; consider x9, z9 being Element of REAL+ such that A32: ( x = x9 & z = z9 ) and A33: * (x,z) = x9 *' z9 by A26, A27, Def2; consider x99, y9 being Element of REAL+ such that A34: x = x99 and A35: y = [0,y9] and A36: * (x,y) = [0,(x99 *' y9)] by A26, A28, Def2; * (x,y) in [:{0},REAL+:] by A36, Lm1, ZFMISC_1:87; then A37: ex xz9, xy9 being Element of REAL+ st ( * (x,z) = xz9 & * (x,y) = [0,xy9] & + ((* (x,z)),(* (x,y))) = xz9 - xy9 ) by A33, Def1; A38: y9 = y99 by A35, A30, XTUPLE_0:1; now__::_thesis:_*_(x,(+_(z,y)))_=_+_((*_(x,z)),(*_(x,y))) percases ( y99 <=' z99 or not y99 <=' z99 ) ; supposeA39: y99 <=' z99 ; ::_thesis: * (x,(+ (z,y))) = + ((* (x,z)),(* (x,y))) then A40: + (z,y) = z99 -' y99 by A31, ARYTM_1:def_2; then ex x999, zy9 being Element of REAL+ st ( x = x999 & + (z,y) = zy9 & * (x,(+ (z,y))) = x999 *' zy9 ) by A26, Def2; hence * (x,(+ (z,y))) = (x9 *' z9) - (x99 *' y9) by A32, A34, A29, A38, A39, A40, ARYTM_1:26 .= + ((* (x,z)),(* (x,y))) by A33, A36, A37, XTUPLE_0:1 ; ::_thesis: verum end; supposeA41: not y99 <=' z99 ; ::_thesis: * (x,(+ (z,y))) = + ((* (x,z)),(* (x,y))) then A42: + (z,y) = [0,(y99 -' z99)] by A31, ARYTM_1:def_2; then + (z,y) in [:{0},REAL+:] by Lm1, ZFMISC_1:87; then consider x999, zy9 being Element of REAL+ such that A43: x = x999 and A44: ( + (z,y) = [0,zy9] & * (x,(+ (z,y))) = [0,(x999 *' zy9)] ) by A26, Def2; thus * (x,(+ (z,y))) = [0,(x999 *' (y99 -' z99))] by A42, A44, XTUPLE_0:1 .= (x9 *' z9) - (x99 *' y9) by A26, A32, A34, A29, A38, A41, A43, ARYTM_1:27 .= + ((* (x,z)),(* (x,y))) by A33, A36, A37, XTUPLE_0:1 ; ::_thesis: verum end; end; end; hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; ::_thesis: verum end; supposethat A45: ( x in REAL+ & x <> 0 ) and A46: y in [:{0},REAL+:] \ {[0,0]} and A47: z in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ( ( not y in REAL+ or not z in [:{0},REAL+:] ) & ( not y in [:{0},REAL+:] or not z in REAL+ ) ) by A46, A47, Th5, XBOOLE_0:3; then consider y99, z99 being Element of REAL+ such that A48: y = [0,y99] and A49: z = [0,z99] and A50: + (y,z) = [0,(y99 + z99)] by A46, Def1; + (y,z) in [:{0},REAL+:] by A50, Lm1, ZFMISC_1:87; then consider x999, yz9 being Element of REAL+ such that A51: x = x999 and A52: ( + (y,z) = [0,yz9] & * (x,(+ (y,z))) = [0,(x999 *' yz9)] ) by A45, Def2; consider x9, y9 being Element of REAL+ such that A53: x = x9 and A54: y = [0,y9] and A55: * (x,y) = [0,(x9 *' y9)] by A45, A46, Def2; A56: y9 = y99 by A54, A48, XTUPLE_0:1; consider x99, z9 being Element of REAL+ such that A57: x = x99 and A58: z = [0,z9] and A59: * (x,z) = [0,(x99 *' z9)] by A45, A47, Def2; * (x,z) in [:{0},REAL+:] by A59, Lm1, ZFMISC_1:87; then A60: ( not * (x,y) in [:{0},REAL+:] or not * (x,z) in REAL+ ) by Th5, XBOOLE_0:3; * (x,y) in [:{0},REAL+:] by A55, Lm1, ZFMISC_1:87; then ( not * (x,y) in REAL+ or not * (x,z) in [:{0},REAL+:] ) by Th5, XBOOLE_0:3; then consider xy9, xz9 being Element of REAL+ such that A61: * (x,y) = [0,xy9] and A62: ( * (x,z) = [0,xz9] & + ((* (x,y)),(* (x,z))) = [0,(xy9 + xz9)] ) by A55, A60, Def1, Lm1, ZFMISC_1:87; A63: xy9 = x9 *' y9 by A55, A61, XTUPLE_0:1; A64: z9 = z99 by A58, A49, XTUPLE_0:1; thus * (x,(+ (y,z))) = [0,(x999 *' (y99 + z99))] by A50, A52, XTUPLE_0:1 .= [0,((x9 *' y9) + (x9 *' z9))] by A53, A51, A56, A64, ARYTM_2:13 .= + ((* (x,y)),(* (x,z))) by A53, A57, A59, A62, A63, XTUPLE_0:1 ; ::_thesis: verum end; supposethat A65: x in [:{0},REAL+:] \ {[0,0]} and A66: y in REAL+ and A67: z in REAL+ ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) consider y99, z99 being Element of REAL+ such that A68: y = y99 and A69: z = z99 and A70: + (y,z) = y99 + z99 by A66, A67, Def1; now__::_thesis:_*_(x,(+_(y,z)))_=_+_((*_(x,y)),(*_(x,z))) percases ( ( y <> 0 & z <> 0 ) or x = 0 or z = 0 or y = 0 ) ; supposethat A71: y <> 0 and A72: z <> 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) consider x99, z9 being Element of REAL+ such that A73: x = [0,x99] and A74: z = z9 and A75: * (x,z) = [0,(z9 *' x99)] by A65, A67, A72, Def2; y99 + z99 <> 0 by A69, A72, ARYTM_2:5; then consider x999, yz9 being Element of REAL+ such that A76: x = [0,x999] and A77: ( + (y,z) = yz9 & * (x,(+ (y,z))) = [0,(yz9 *' x999)] ) by A65, A70, Def2; consider x9, y9 being Element of REAL+ such that A78: x = [0,x9] and A79: y = y9 and A80: * (x,y) = [0,(y9 *' x9)] by A65, A66, A71, Def2; A81: x99 = x999 by A73, A76, XTUPLE_0:1; * (x,z) in [:{0},REAL+:] by A75, Lm1, ZFMISC_1:87; then A82: ( not * (x,y) in [:{0},REAL+:] or not * (x,z) in REAL+ ) by Th5, XBOOLE_0:3; * (x,y) in [:{0},REAL+:] by A80, Lm1, ZFMISC_1:87; then ( not * (x,y) in REAL+ or not * (x,z) in [:{0},REAL+:] ) by Th5, XBOOLE_0:3; then consider xy9, xz9 being Element of REAL+ such that A83: * (x,y) = [0,xy9] and A84: ( * (x,z) = [0,xz9] & + ((* (x,y)),(* (x,z))) = [0,(xy9 + xz9)] ) by A80, A82, Def1, Lm1, ZFMISC_1:87; A85: xy9 = x9 *' y9 by A80, A83, XTUPLE_0:1; x9 = x99 by A78, A73, XTUPLE_0:1; hence * (x,(+ (y,z))) = [0,((x9 *' y9) + (x99 *' z9))] by A68, A69, A70, A79, A74, A77, A81, ARYTM_2:13 .= + ((* (x,y)),(* (x,z))) by A75, A84, A85, XTUPLE_0:1 ; ::_thesis: verum end; supposeA86: x = 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) hence * (x,(+ (y,z))) = 0 by Th12 .= + (o,o) by Th11 .= + ((* (x,y)),o) by A86, Th12 .= + ((* (x,y)),(* (x,z))) by A86, Th12 ; ::_thesis: verum end; supposeA87: z = 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) hence * (x,(+ (y,z))) = * (x,y) by Th11 .= + ((* (x,y)),(* (x,z))) by A87, Th11, Th12 ; ::_thesis: verum end; supposeA88: y = 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) hence * (x,(+ (y,z))) = * (x,z) by Th11 .= + ((* (x,y)),(* (x,z))) by A88, Th11, Th12 ; ::_thesis: verum end; end; end; hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; ::_thesis: verum end; supposethat A89: x in [:{0},REAL+:] \ {[0,0]} and A90: y in REAL+ and A91: z in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) consider x99, z9 being Element of REAL+ such that A92: x = [0,x99] and A93: z = [0,z9] and A94: * (x,z) = z9 *' x99 by A89, A91, Def2; now__::_thesis:_*_(x,(+_(y,z)))_=_+_((*_(x,y)),(*_(x,z))) percases ( y <> 0 or y = 0 ) ; suppose y <> 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) then consider x9, y9 being Element of REAL+ such that A95: x = [0,x9] and A96: y = y9 and A97: * (x,y) = [0,(y9 *' x9)] by A89, A90, Def2; * (x,y) in [:{0},REAL+:] by A97, Lm1, ZFMISC_1:87; then consider xy9, xz9 being Element of REAL+ such that A98: * (x,y) = [0,xy9] and A99: ( * (x,z) = xz9 & + ((* (x,y)),(* (x,z))) = xz9 - xy9 ) by A94, Def1; consider y99, z99 being Element of REAL+ such that A100: y = y99 and A101: z = [0,z99] and A102: + (y,z) = y99 - z99 by A91, A96, Def1; A103: z9 = z99 by A93, A101, XTUPLE_0:1; now__::_thesis:_*_(x,(+_(y,z)))_=_+_((*_(x,y)),(*_(x,z))) percases ( z99 <=' y99 or not z99 <=' y99 ) ; supposeA104: z99 <=' y99 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) then A105: + (y,z) = y99 -' z99 by A102, ARYTM_1:def_2; now__::_thesis:_*_(x,(+_(y,z)))_=_+_((*_(x,y)),(*_(x,z))) percases ( + (y,z) <> 0 or + (y,z) = 0 ) ; supposeA106: + (y,z) <> 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) then consider x999, yz9 being Element of REAL+ such that A107: x = [0,x999] and A108: ( + (y,z) = yz9 & * (x,(+ (y,z))) = [0,(yz9 *' x999)] ) by A89, A105, Def2; not x in {[0,0]} by NUMBERS:def_1, XBOOLE_0:def_5; then A109: x999 <> 0 by A107, TARSKI:def_1; A110: z9 = z99 by A93, A101, XTUPLE_0:1; A111: x9 = x99 by A92, A95, XTUPLE_0:1; x99 = x999 by A92, A107, XTUPLE_0:1; hence * (x,(+ (y,z))) = (x9 *' z9) - (x9 *' y9) by A96, A100, A104, A105, A106, A108, A111, A110, A109, ARYTM_1:28 .= + ((* (x,y)),(* (x,z))) by A94, A97, A98, A99, A111, XTUPLE_0:1 ; ::_thesis: verum end; supposeA112: + (y,z) = 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) then A113: y99 = z99 by A104, A105, ARYTM_1:10; A114: ( xy9 = x9 *' y9 & x9 = x99 ) by A92, A95, A97, A98, XTUPLE_0:1; thus * (x,(+ (y,z))) = 0 by A112, Th12 .= + ((* (x,y)),(* (x,z))) by A94, A96, A100, A99, A103, A113, A114, ARYTM_1:18 ; ::_thesis: verum end; end; end; hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; ::_thesis: verum end; supposeA115: not z99 <=' y99 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) then A116: + (y,z) = [0,(z99 -' y99)] by A102, ARYTM_1:def_2; then + (y,z) in [:{0},REAL+:] by Lm1, ZFMISC_1:87; then consider x999, yz9 being Element of REAL+ such that A117: x = [0,x999] and A118: ( + (y,z) = [0,yz9] & * (x,(+ (y,z))) = yz9 *' x999 ) by A89, Def2; A119: x99 = x999 by A92, A117, XTUPLE_0:1; A120: x9 = x99 by A92, A95, XTUPLE_0:1; thus * (x,(+ (y,z))) = x999 *' (z99 -' y99) by A116, A118, XTUPLE_0:1 .= (x99 *' z9) - (x9 *' y9) by A96, A100, A103, A115, A120, A119, ARYTM_1:26 .= + ((* (x,y)),(* (x,z))) by A94, A97, A98, A99, XTUPLE_0:1 ; ::_thesis: verum end; end; end; hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; ::_thesis: verum end; supposeA121: y = 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) hence * (x,(+ (y,z))) = * (x,z) by Th11 .= + ((* (x,y)),(* (x,z))) by A121, Th11, Th12 ; ::_thesis: verum end; end; end; hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; ::_thesis: verum end; supposethat A122: x in [:{0},REAL+:] \ {[0,0]} and A123: z in REAL+ and A124: y in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) consider x99, y9 being Element of REAL+ such that A125: x = [0,x99] and A126: y = [0,y9] and A127: * (x,y) = y9 *' x99 by A122, A124, Def2; now__::_thesis:_*_(x,(+_(y,z)))_=_+_((*_(x,y)),(*_(x,z))) percases ( z <> 0 or z = 0 ) ; suppose z <> 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) then consider x9, z9 being Element of REAL+ such that A128: x = [0,x9] and A129: z = z9 and A130: * (x,z) = [0,(z9 *' x9)] by A122, A123, Def2; * (x,z) in [:{0},REAL+:] by A130, Lm1, ZFMISC_1:87; then consider xz9, xy9 being Element of REAL+ such that A131: * (x,z) = [0,xz9] and A132: ( * (x,y) = xy9 & + ((* (x,z)),(* (x,y))) = xy9 - xz9 ) by A127, Def1; consider z99, y99 being Element of REAL+ such that A133: z = z99 and A134: y = [0,y99] and A135: + (z,y) = z99 - y99 by A124, A129, Def1; A136: y9 = y99 by A126, A134, XTUPLE_0:1; now__::_thesis:_*_(x,(+_(y,z)))_=_+_((*_(x,y)),(*_(x,z))) percases ( y99 <=' z99 or not y99 <=' z99 ) ; supposeA137: y99 <=' z99 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) then A138: + (z,y) = z99 -' y99 by A135, ARYTM_1:def_2; now__::_thesis:_*_(x,(+_(z,y)))_=_+_((*_(x,z)),(*_(x,y))) percases ( + (z,y) <> 0 or + (z,y) = 0 ) ; supposeA139: + (z,y) <> 0 ; ::_thesis: * (x,(+ (z,y))) = + ((* (x,z)),(* (x,y))) then consider x999, zy9 being Element of REAL+ such that A140: x = [0,x999] and A141: ( + (z,y) = zy9 & * (x,(+ (z,y))) = [0,(zy9 *' x999)] ) by A122, A138, Def2; not x in {[0,0]} by NUMBERS:def_1, XBOOLE_0:def_5; then A142: x999 <> 0 by A140, TARSKI:def_1; A143: y9 = y99 by A126, A134, XTUPLE_0:1; A144: x9 = x99 by A125, A128, XTUPLE_0:1; x99 = x999 by A125, A140, XTUPLE_0:1; hence * (x,(+ (z,y))) = (x9 *' y9) - (x9 *' z9) by A129, A133, A137, A138, A139, A141, A144, A143, A142, ARYTM_1:28 .= + ((* (x,z)),(* (x,y))) by A127, A130, A131, A132, A144, XTUPLE_0:1 ; ::_thesis: verum end; supposeA145: + (z,y) = 0 ; ::_thesis: * (x,(+ (z,y))) = + ((* (x,z)),(* (x,y))) then A146: z99 = y99 by A137, A138, ARYTM_1:10; A147: ( xz9 = x9 *' z9 & x9 = x99 ) by A125, A128, A130, A131, XTUPLE_0:1; thus * (x,(+ (z,y))) = 0 by A145, Th12 .= + ((* (x,z)),(* (x,y))) by A127, A129, A133, A132, A136, A146, A147, ARYTM_1:18 ; ::_thesis: verum end; end; end; hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; ::_thesis: verum end; supposeA148: not y99 <=' z99 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) then A149: + (z,y) = [0,(y99 -' z99)] by A135, ARYTM_1:def_2; then + (z,y) in [:{0},REAL+:] by Lm1, ZFMISC_1:87; then consider x999, zy9 being Element of REAL+ such that A150: x = [0,x999] and A151: ( + (z,y) = [0,zy9] & * (x,(+ (z,y))) = zy9 *' x999 ) by A122, Def2; A152: x99 = x999 by A125, A150, XTUPLE_0:1; A153: x9 = x99 by A125, A128, XTUPLE_0:1; thus * (x,(+ (y,z))) = x999 *' (y99 -' z99) by A149, A151, XTUPLE_0:1 .= (x99 *' y9) - (x9 *' z9) by A129, A133, A136, A148, A153, A152, ARYTM_1:26 .= + ((* (x,y)),(* (x,z))) by A127, A130, A131, A132, XTUPLE_0:1 ; ::_thesis: verum end; end; end; hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; ::_thesis: verum end; supposeA154: z = 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) hence * (x,(+ (y,z))) = * (x,y) by Th11 .= + ((* (x,y)),(* (x,z))) by A154, Th11, Th12 ; ::_thesis: verum end; end; end; hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; ::_thesis: verum end; supposethat A155: x in [:{0},REAL+:] \ {[0,0]} and A156: y in [:{0},REAL+:] \ {[0,0]} and A157: z in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ( ( not y in REAL+ or not z in [:{0},REAL+:] ) & ( not y in [:{0},REAL+:] or not z in REAL+ ) ) by A156, A157, Th5, XBOOLE_0:3; then consider y99, z99 being Element of REAL+ such that A158: y = [0,y99] and A159: z = [0,z99] and A160: + (y,z) = [0,(y99 + z99)] by A156, Def1; consider x99, z9 being Element of REAL+ such that A161: x = [0,x99] and A162: z = [0,z9] and A163: * (x,z) = z9 *' x99 by A155, A157, Def2; A164: z9 = z99 by A162, A159, XTUPLE_0:1; consider x9, y9 being Element of REAL+ such that A165: x = [0,x9] and A166: y = [0,y9] and A167: * (x,y) = y9 *' x9 by A155, A156, Def2; A168: y9 = y99 by A166, A158, XTUPLE_0:1; + (y,z) in [:{0},REAL+:] by A160, Lm1, ZFMISC_1:87; then consider x999, yz9 being Element of REAL+ such that A169: x = [0,x999] and A170: ( + (y,z) = [0,yz9] & * (x,(+ (y,z))) = yz9 *' x999 ) by A155, Def2; A171: x9 = x999 by A165, A169, XTUPLE_0:1; A172: ( ex xy9, xz9 being Element of REAL+ st ( * (x,y) = xy9 & * (x,z) = xz9 & + ((* (x,y)),(* (x,z))) = xy9 + xz9 ) & x9 = x99 ) by A165, A167, A161, A163, Def1, XTUPLE_0:1; thus * (x,(+ (y,z))) = x999 *' (y99 + z99) by A160, A170, XTUPLE_0:1 .= + ((* (x,y)),(* (x,z))) by A167, A163, A172, A171, A168, A164, ARYTM_2:13 ; ::_thesis: verum end; supposeA173: ( ( not x in REAL+ or not y in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not y in REAL+ or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in REAL+ or not y in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in REAL+ or not z in REAL+ ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in REAL+ or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) ) ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) A174: not [0,0] in REAL+ by ARYTM_2:3; REAL = (REAL+ \ {[0,0]}) \/ ([:{0},REAL+:] \ {[0,0]}) by NUMBERS:def_1, XBOOLE_1:42 .= REAL+ \/ ([:{0},REAL+:] \ {[0,0]}) by A174, ZFMISC_1:57 ; hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) by A173, XBOOLE_0:def_3; ::_thesis: verum end; end; end; theorem :: ARYTM_0:15 for x, y being Element of REAL holds * ((opp x),y) = opp (* (x,y)) proof let x, y be Element of REAL ; ::_thesis: * ((opp x),y) = opp (* (x,y)) + ((* ((opp x),y)),(* (x,y))) = * ((+ ((opp x),x)),y) by Th14 .= * (o,y) by Def3 .= 0 by Th12 ; hence * ((opp x),y) = opp (* (x,y)) by Def3; ::_thesis: verum end; theorem Th16: :: ARYTM_0:16 for x being Element of REAL holds * (x,x) in REAL+ proof let x be Element of REAL ; ::_thesis: * (x,x) in REAL+ A1: x in REAL+ \/ [:{{}},REAL+:] by NUMBERS:def_1, XBOOLE_0:def_5; percases ( x in REAL+ or x in [:{0},REAL+:] ) by A1, XBOOLE_0:def_3; suppose x in REAL+ ; ::_thesis: * (x,x) in REAL+ then ex x9, y9 being Element of REAL+ st ( x = x9 & x = y9 & * (x,x) = x9 *' y9 ) by Def2; hence * (x,x) in REAL+ ; ::_thesis: verum end; suppose x in [:{0},REAL+:] ; ::_thesis: * (x,x) in REAL+ then ex x9, y9 being Element of REAL+ st ( x = [0,x9] & x = [0,y9] & * (x,x) = y9 *' x9 ) by Def2; hence * (x,x) in REAL+ ; ::_thesis: verum end; end; end; theorem :: ARYTM_0:17 for x, y being Element of REAL st + ((* (x,x)),(* (y,y))) = 0 holds x = 0 proof let x, y be Element of REAL ; ::_thesis: ( + ((* (x,x)),(* (y,y))) = 0 implies x = 0 ) assume A1: + ((* (x,x)),(* (y,y))) = 0 ; ::_thesis: x = 0 ( * (x,x) in REAL+ & * (y,y) in REAL+ ) by Th16; then consider x9, y9 being Element of REAL+ such that A2: * (x,x) = x9 and * (y,y) = y9 and A3: 0 = x9 + y9 by A1, Def1; A4: x9 = 0 by A3, ARYTM_2:5; A5: x in REAL+ \/ [:{{}},REAL+:] by NUMBERS:def_1, XBOOLE_0:def_5; percases ( x in REAL+ or x in [:{0},REAL+:] ) by A5, XBOOLE_0:def_3; suppose x in REAL+ ; ::_thesis: x = 0 then ex x9, y9 being Element of REAL+ st ( x = x9 & x = y9 & 0 = x9 *' y9 ) by A2, A4, Def2; hence x = 0 by ARYTM_1:2; ::_thesis: verum end; suppose x in [:{0},REAL+:] ; ::_thesis: x = 0 then consider x9, y9 being Element of REAL+ such that A6: x = [0,x9] and A7: x = [0,y9] and A8: 0 = y9 *' x9 by A2, A4, Def2; x9 = y9 by A6, A7, XTUPLE_0:1; then x9 = 0 by A8, ARYTM_1:2; then x in {[0,0]} by A6, TARSKI:def_1; hence x = 0 by NUMBERS:def_1, XBOOLE_0:def_5; ::_thesis: verum end; end; end; theorem Th18: :: ARYTM_0:18 for x, y, z being Element of REAL st x <> 0 & * (x,y) = 1 & * (x,z) = 1 holds y = z proof let x, y, z be Element of REAL ; ::_thesis: ( x <> 0 & * (x,y) = 1 & * (x,z) = 1 implies y = z ) assume that A1: x <> 0 and A2: * (x,y) = 1 and A3: * (x,z) = 1 ; ::_thesis: y = z thus y = inv x by A1, A2, Def4 .= z by A1, A3, Def4 ; ::_thesis: verum end; theorem Th19: :: ARYTM_0:19 for x, y being Element of REAL st y = 1 holds * (x,y) = x proof let x, y be Element of REAL ; ::_thesis: ( y = 1 implies * (x,y) = x ) assume A1: y = 1 ; ::_thesis: * (x,y) = x percases ( x = 0 or x <> 0 ) ; suppose x = 0 ; ::_thesis: * (x,y) = x hence * (x,y) = x by Th12; ::_thesis: verum end; supposeA2: x <> 0 ; ::_thesis: * (x,y) = x A3: now__::_thesis:_(_inv_x_=_0_implies_1_=_0_) assume A4: inv x = 0 ; ::_thesis: 1 = 0 thus 1 = * (x,(inv x)) by A2, Def4 .= 0 by A4, Th12 ; ::_thesis: verum end; A5: ex x9, y9 being Element of REAL+ st ( y = x9 & y = y9 & * (y,y) = x9 *' y9 ) by A1, Def2, ARYTM_2:20; A6: * (x,(inv x)) = 1 by A2, Def4; * ((* (x,y)),(inv x)) = * ((* (x,(inv x))),y) by Th13 .= * (y,y) by A1, A2, Def4 .= 1 by A1, A5, ARYTM_2:15 ; hence * (x,y) = x by A3, A6, Th18; ::_thesis: verum end; end; end; reconsider j = 1 as Element of REAL ; theorem :: ARYTM_0:20 for x, y being Element of REAL st y <> 0 holds * ((* (x,y)),(inv y)) = x proof let x, y be Element of REAL ; ::_thesis: ( y <> 0 implies * ((* (x,y)),(inv y)) = x ) assume A1: y <> 0 ; ::_thesis: * ((* (x,y)),(inv y)) = x thus * ((* (x,y)),(inv y)) = * (x,(* (y,(inv y)))) by Th13 .= * (x,j) by A1, Def4 .= x by Th19 ; ::_thesis: verum end; theorem Th21: :: ARYTM_0:21 for x, y being Element of REAL holds ( not * (x,y) = 0 or x = 0 or y = 0 ) proof let x, y be Element of REAL ; ::_thesis: ( not * (x,y) = 0 or x = 0 or y = 0 ) assume that A1: * (x,y) = 0 and A2: x <> 0 ; ::_thesis: y = 0 A3: * (x,(inv x)) = 1 by A2, Def4; thus y = * (j,y) by Th19 .= * ((* (x,y)),(inv x)) by A3, Th13 .= 0 by A1, Th12 ; ::_thesis: verum end; theorem :: ARYTM_0:22 for x, y being Element of REAL holds inv (* (x,y)) = * ((inv x),(inv y)) proof let x, y be Element of REAL ; ::_thesis: inv (* (x,y)) = * ((inv x),(inv y)) percases ( x = 0 or y = 0 or ( x <> 0 & y <> 0 ) ) ; supposeA1: ( x = 0 or y = 0 ) ; ::_thesis: inv (* (x,y)) = * ((inv x),(inv y)) then A2: ( inv x = 0 or inv y = 0 ) by Def4; * (x,y) = 0 by A1, Th12; hence inv (* (x,y)) = 0 by Def4 .= * ((inv x),(inv y)) by A2, Th12 ; ::_thesis: verum end; supposethat A3: x <> 0 and A4: y <> 0 ; ::_thesis: inv (* (x,y)) = * ((inv x),(inv y)) A5: * (x,y) <> 0 by A3, A4, Th21; A6: * (x,(inv x)) = 1 by A3, Def4; A7: * (y,(inv y)) = 1 by A4, Def4; * ((* (x,y)),(* ((inv x),(inv y)))) = * ((* ((* (x,y)),(inv x))),(inv y)) by Th13 .= * ((* (j,y)),(inv y)) by A6, Th13 .= 1 by A7, Th19 ; hence inv (* (x,y)) = * ((inv x),(inv y)) by A5, Def4; ::_thesis: verum end; end; end; theorem Th23: :: ARYTM_0:23 for x, y, z being Element of REAL holds + (x,(+ (y,z))) = + ((+ (x,y)),z) proof let x, y, z be Element of REAL ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) A1: ( x in REAL+ \/ [:{0},REAL+:] & y in REAL+ \/ [:{0},REAL+:] ) by NUMBERS:def_1, XBOOLE_0:def_5; A2: z in REAL+ \/ [:{0},REAL+:] by NUMBERS:def_1, XBOOLE_0:def_5; percases ( ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & y in REAL+ & z in [:{0},REAL+:] ) or ( x in REAL+ & y in [:{0},REAL+:] & z in REAL+ ) or ( x in REAL+ & y in [:{0},REAL+:] & z in [:{0},REAL+:] ) or ( z in REAL+ & y in REAL+ & x in [:{0},REAL+:] ) or ( x in [:{0},REAL+:] & y in REAL+ & z in [:{0},REAL+:] ) or ( z in REAL+ & y in [:{0},REAL+:] & x in [:{0},REAL+:] ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & z in [:{0},REAL+:] ) ) by A1, A2, XBOOLE_0:def_3; supposethat A3: x in REAL+ and A4: y in REAL+ and A5: z in REAL+ ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) A6: ex x99, y99 being Element of REAL+ st ( x = x99 & y = y99 & + (x,y) = x99 + y99 ) by A3, A4, Def1; then A7: ex xy99, z99 being Element of REAL+ st ( + (x,y) = xy99 & z = z99 & + ((+ (x,y)),z) = xy99 + z99 ) by A5, Def1; A8: ex y9, z9 being Element of REAL+ st ( y = y9 & z = z9 & + (y,z) = y9 + z9 ) by A4, A5, Def1; then ex x9, yz9 being Element of REAL+ st ( x = x9 & + (y,z) = yz9 & + (x,(+ (y,z))) = x9 + yz9 ) by A3, Def1; hence + (x,(+ (y,z))) = + ((+ (x,y)),z) by A8, A6, A7, ARYTM_2:6; ::_thesis: verum end; supposethat A9: x in REAL+ and A10: y in REAL+ and A11: z in [:{0},REAL+:] ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) A12: ex x99, y99 being Element of REAL+ st ( x = x99 & y = y99 & + (x,y) = x99 + y99 ) by A9, A10, Def1; then consider xy99, z99 being Element of REAL+ such that A13: + (x,y) = xy99 and A14: z = [0,z99] and A15: + ((+ (x,y)),z) = xy99 - z99 by A11, Def1; consider y9, z9 being Element of REAL+ such that A16: y = y9 and A17: z = [0,z9] and A18: + (y,z) = y9 - z9 by A10, A11, Def1; A19: z9 = z99 by A17, A14, XTUPLE_0:1; now__::_thesis:_+_(x,(+_(y,z)))_=_+_((+_(x,y)),z) percases ( z9 <=' y9 or not z9 <=' y9 ) ; supposeA20: z9 <=' y9 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) then A21: + (y,z) = y9 -' z9 by A18, ARYTM_1:def_2; then ex x9, yz9 being Element of REAL+ st ( x = x9 & + (y,z) = yz9 & + (x,(+ (y,z))) = x9 + yz9 ) by A9, Def1; hence + (x,(+ (y,z))) = + ((+ (x,y)),z) by A16, A12, A13, A15, A19, A20, A21, ARYTM_1:20; ::_thesis: verum end; supposeA22: not z9 <=' y9 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) then A23: + (y,z) = [0,(z9 -' y9)] by A18, ARYTM_1:def_2; then + (y,z) in [:{0},REAL+:] by Lm1, ZFMISC_1:87; then consider x9, yz9 being Element of REAL+ such that A24: x = x9 and A25: ( + (y,z) = [0,yz9] & + (x,(+ (y,z))) = x9 - yz9 ) by A9, Def1; thus + (x,(+ (y,z))) = x9 - (z9 -' y9) by A23, A25, XTUPLE_0:1 .= + ((+ (x,y)),z) by A16, A12, A13, A15, A19, A22, A24, ARYTM_1:21 ; ::_thesis: verum end; end; end; hence + (x,(+ (y,z))) = + ((+ (x,y)),z) ; ::_thesis: verum end; supposethat A26: x in REAL+ and A27: y in [:{0},REAL+:] and A28: z in REAL+ ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) consider x99, y99 being Element of REAL+ such that A29: x = x99 and A30: y = [0,y99] and A31: + (x,y) = x99 - y99 by A26, A27, Def1; consider z9, y9 being Element of REAL+ such that A32: z = z9 and A33: y = [0,y9] and A34: + (y,z) = z9 - y9 by A27, A28, Def1; A35: y9 = y99 by A33, A30, XTUPLE_0:1; now__::_thesis:_+_(x,(+_(y,z)))_=_+_((+_(x,y)),z) percases ( ( y9 <=' x99 & y9 <=' z9 ) or ( y9 <=' x99 & not y9 <=' z9 ) or ( not y9 <=' x99 & y9 <=' z9 ) or ( not y9 <=' x99 & not y9 <=' z9 ) ) ; supposethat A36: y9 <=' x99 and A37: y9 <=' z9 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) A38: + (y,z) = z9 -' y9 by A34, A37, ARYTM_1:def_2; then consider x9, yz9 being Element of REAL+ such that A39: x = x9 and A40: ( + (y,z) = yz9 & + (x,(+ (y,z))) = x9 + yz9 ) by A26, Def1; A41: + (x,y) = x9 -' y9 by A29, A31, A35, A36, A39, ARYTM_1:def_2; then ex z99, xy99 being Element of REAL+ st ( z = z99 & + (x,y) = xy99 & + (z,(+ (x,y))) = z99 + xy99 ) by A28, Def1; hence + (x,(+ (y,z))) = + ((+ (x,y)),z) by A32, A29, A36, A37, A38, A39, A40, A41, ARYTM_1:12; ::_thesis: verum end; supposethat A42: y9 <=' x99 and A43: not y9 <=' z9 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) A44: + (x,y) = x99 -' y9 by A31, A35, A42, ARYTM_1:def_2; then A45: ex z99, xy99 being Element of REAL+ st ( z = z99 & + (x,y) = xy99 & + (z,(+ (x,y))) = z99 + xy99 ) by A28, Def1; A46: + (y,z) = [0,(y9 -' z9)] by A34, A43, ARYTM_1:def_2; then + (y,z) in [:{0},REAL+:] by Lm1, ZFMISC_1:87; then consider x9, yz9 being Element of REAL+ such that A47: x = x9 and A48: ( + (y,z) = [0,yz9] & + (x,(+ (y,z))) = x9 - yz9 ) by A26, Def1; thus + (x,(+ (y,z))) = x9 - (y9 -' z9) by A46, A48, XTUPLE_0:1 .= + ((+ (x,y)),z) by A32, A29, A42, A43, A47, A44, A45, ARYTM_1:22 ; ::_thesis: verum end; supposethat A49: not y9 <=' x99 and A50: y9 <=' z9 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) A51: + (y,x) = [0,(y9 -' x99)] by A31, A35, A49, ARYTM_1:def_2; then + (y,x) in [:{0},REAL+:] by Lm1, ZFMISC_1:87; then consider z99, yx99 being Element of REAL+ such that A52: z = z99 and A53: ( + (y,x) = [0,yx99] & + (z,(+ (y,x))) = z99 - yx99 ) by A28, Def1; A54: + (z,y) = z9 -' y9 by A34, A50, ARYTM_1:def_2; then ex x9, zy99 being Element of REAL+ st ( x = x9 & + (z,y) = zy99 & + (x,(+ (z,y))) = x9 + zy99 ) by A26, Def1; hence + (x,(+ (y,z))) = z99 - (y9 -' x99) by A32, A29, A49, A50, A52, A54, ARYTM_1:22 .= + ((+ (x,y)),z) by A51, A53, XTUPLE_0:1 ; ::_thesis: verum end; supposethat A55: not y9 <=' x99 and A56: not y9 <=' z9 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) A57: + (y,z) = [0,(y9 -' z9)] by A34, A56, ARYTM_1:def_2; then + (y,z) in [:{0},REAL+:] by Lm1, ZFMISC_1:87; then consider x9, yz9 being Element of REAL+ such that A58: x = x9 and A59: ( + (y,z) = [0,yz9] & + (x,(+ (y,z))) = x9 - yz9 ) by A26, Def1; A60: + (y,x) = [0,(y9 -' x99)] by A31, A35, A55, ARYTM_1:def_2; then + (y,x) in [:{0},REAL+:] by Lm1, ZFMISC_1:87; then consider z99, yx99 being Element of REAL+ such that A61: z = z99 and A62: ( + (y,x) = [0,yx99] & + (z,(+ (y,x))) = z99 - yx99 ) by A28, Def1; thus + (x,(+ (y,z))) = x9 - (y9 -' z9) by A57, A59, XTUPLE_0:1 .= z99 - (y9 -' x99) by A32, A29, A55, A56, A61, A58, ARYTM_1:23 .= + ((+ (x,y)),z) by A60, A62, XTUPLE_0:1 ; ::_thesis: verum end; end; end; hence + (x,(+ (y,z))) = + ((+ (x,y)),z) ; ::_thesis: verum end; supposethat A63: x in REAL+ and A64: y in [:{0},REAL+:] and A65: z in [:{0},REAL+:] ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) ( ( not z in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not z in [:{0},REAL+:] ) ) by A64, A65, Th5, XBOOLE_0:3; then consider y9, z9 being Element of REAL+ such that A66: y = [0,y9] and A67: z = [0,z9] and A68: + (y,z) = [0,(y9 + z9)] by A64, Def1; + (y,z) in [:{0},REAL+:] by A68, Lm1, ZFMISC_1:87; then consider x9, yz9 being Element of REAL+ such that A69: x = x9 and A70: + (y,z) = [0,yz9] and A71: + (x,(+ (y,z))) = x9 - yz9 by A63, Def1; consider x99, y99 being Element of REAL+ such that A72: x = x99 and A73: y = [0,y99] and A74: + (x,y) = x99 - y99 by A63, A64, Def1; A75: y9 = y99 by A66, A73, XTUPLE_0:1; now__::_thesis:_+_(x,(+_(y,z)))_=_+_((+_(x,y)),z) percases ( y99 <=' x99 or not y99 <=' x99 ) ; supposeA76: y99 <=' x99 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) then A77: + (x,y) = x99 -' y99 by A74, ARYTM_1:def_2; then consider xy99, z99 being Element of REAL+ such that A78: + (x,y) = xy99 and A79: z = [0,z99] and A80: + ((+ (x,y)),z) = xy99 - z99 by A65, Def1; A81: z9 = z99 by A67, A79, XTUPLE_0:1; thus + (x,(+ (y,z))) = x9 - (y9 + z9) by A68, A70, A71, XTUPLE_0:1 .= + ((+ (x,y)),z) by A72, A69, A75, A76, A77, A78, A80, A81, ARYTM_1:24 ; ::_thesis: verum end; supposeA82: not y99 <=' x99 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) A83: ( not z in REAL+ or not + (x,y) in [:{0},REAL+:] ) by A65, Th5, XBOOLE_0:3; A84: + (x,y) = [0,(y99 -' x99)] by A74, A82, ARYTM_1:def_2; then + (x,y) in [:{0},REAL+:] by Lm1, ZFMISC_1:87; then ( not + (x,y) in REAL+ or not z in [:{0},REAL+:] ) by Th5, XBOOLE_0:3; then consider xy99, z99 being Element of REAL+ such that A85: + (x,y) = [0,xy99] and A86: z = [0,z99] and A87: + ((+ (x,y)),z) = [0,(xy99 + z99)] by A84, A83, Def1, Lm1, ZFMISC_1:87; A88: z9 = z99 by A67, A86, XTUPLE_0:1; A89: yz9 = z9 + y9 by A68, A70, XTUPLE_0:1; then y99 <=' yz9 by A75, ARYTM_2:19; then not yz9 <=' x9 by A72, A69, A82, ARYTM_1:3; hence + (x,(+ (y,z))) = [0,((z9 + y9) -' x9)] by A71, A89, ARYTM_1:def_2 .= [0,(z99 + (y99 -' x99))] by A72, A69, A75, A82, A88, ARYTM_1:13 .= + ((+ (x,y)),z) by A84, A85, A87, XTUPLE_0:1 ; ::_thesis: verum end; end; end; hence + (x,(+ (y,z))) = + ((+ (x,y)),z) ; ::_thesis: verum end; supposethat A90: z in REAL+ and A91: y in REAL+ and A92: x in [:{0},REAL+:] ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) A93: ex z99, y99 being Element of REAL+ st ( z = z99 & y = y99 & + (z,y) = z99 + y99 ) by A90, A91, Def1; then consider zy99, x99 being Element of REAL+ such that A94: + (z,y) = zy99 and A95: x = [0,x99] and A96: + ((+ (z,y)),x) = zy99 - x99 by A92, Def1; consider y9, x9 being Element of REAL+ such that A97: y = y9 and A98: x = [0,x9] and A99: + (y,x) = y9 - x9 by A91, A92, Def1; A100: x9 = x99 by A98, A95, XTUPLE_0:1; now__::_thesis:_+_(z,(+_(y,x)))_=_+_((+_(z,y)),x) percases ( x9 <=' y9 or not x9 <=' y9 ) ; supposeA101: x9 <=' y9 ; ::_thesis: + (z,(+ (y,x))) = + ((+ (z,y)),x) then A102: + (y,x) = y9 -' x9 by A99, ARYTM_1:def_2; then ex z9, yx9 being Element of REAL+ st ( z = z9 & + (y,x) = yx9 & + (z,(+ (y,x))) = z9 + yx9 ) by A90, Def1; hence + (z,(+ (y,x))) = + ((+ (z,y)),x) by A97, A93, A94, A96, A100, A101, A102, ARYTM_1:20; ::_thesis: verum end; supposeA103: not x9 <=' y9 ; ::_thesis: + (z,(+ (y,x))) = + ((+ (z,y)),x) then A104: + (y,x) = [0,(x9 -' y9)] by A99, ARYTM_1:def_2; then + (y,x) in [:{0},REAL+:] by Lm1, ZFMISC_1:87; then consider z9, yx9 being Element of REAL+ such that A105: z = z9 and A106: ( + (y,x) = [0,yx9] & + (z,(+ (y,x))) = z9 - yx9 ) by A90, Def1; thus + (z,(+ (y,x))) = z9 - (x9 -' y9) by A104, A106, XTUPLE_0:1 .= + ((+ (z,y)),x) by A97, A93, A94, A96, A100, A103, A105, ARYTM_1:21 ; ::_thesis: verum end; end; end; hence + (x,(+ (y,z))) = + ((+ (x,y)),z) ; ::_thesis: verum end; supposethat A107: x in [:{0},REAL+:] and A108: y in REAL+ and A109: z in [:{0},REAL+:] ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) consider y9, z9 being Element of REAL+ such that A110: y = y9 and A111: z = [0,z9] and A112: + (y,z) = y9 - z9 by A108, A109, Def1; consider x99, y99 being Element of REAL+ such that A113: x = [0,x99] and A114: y = y99 and A115: + (x,y) = y99 - x99 by A107, A108, Def1; now__::_thesis:_+_(x,(+_(y,z)))_=_+_((+_(x,y)),z) percases ( ( x99 <=' y99 & z9 <=' y9 ) or ( not x99 <=' y99 & z9 <=' y9 ) or ( not z9 <=' y9 & x99 <=' y99 ) or ( not x99 <=' y99 & not z9 <=' y9 ) ) ; supposethat A116: x99 <=' y99 and A117: z9 <=' y9 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) A118: + (y,z) = y9 -' z9 by A112, A117, ARYTM_1:def_2; then consider x9, yz9 being Element of REAL+ such that A119: x = [0,x9] and A120: ( + (y,z) = yz9 & + (x,(+ (y,z))) = yz9 - x9 ) by A107, Def1; A121: x9 = x99 by A113, A119, XTUPLE_0:1; then A122: + (x,y) = y9 -' x9 by A110, A114, A115, A116, ARYTM_1:def_2; then consider z99, xy99 being Element of REAL+ such that A123: z = [0,z99] and A124: ( + (x,y) = xy99 & + (z,(+ (x,y))) = xy99 - z99 ) by A109, Def1; z9 = z99 by A111, A123, XTUPLE_0:1; hence + (x,(+ (y,z))) = + ((+ (x,y)),z) by A110, A114, A116, A117, A118, A120, A121, A122, A124, ARYTM_1:25; ::_thesis: verum end; supposethat A125: not x99 <=' y99 and A126: z9 <=' y9 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) A127: ( not z in REAL+ or not + (x,y) in [:{0},REAL+:] ) by A109, Th5, XBOOLE_0:3; A128: + (y,x) = [0,(x99 -' y99)] by A115, A125, ARYTM_1:def_2; then + (y,x) in [:{0},REAL+:] by Lm1, ZFMISC_1:87; then ( not + (x,y) in REAL+ or not z in [:{0},REAL+:] ) by Th5, XBOOLE_0:3; then consider z99, yx9 being Element of REAL+ such that A129: z = [0,z99] and A130: ( + (y,x) = [0,yx9] & + (z,(+ (y,x))) = [0,(z99 + yx9)] ) by A128, A127, Def1, Lm1, ZFMISC_1:87; A131: z9 = z99 by A111, A129, XTUPLE_0:1; A132: + (y,z) = y9 -' z9 by A112, A126, ARYTM_1:def_2; then consider x9, yz9 being Element of REAL+ such that A133: x = [0,x9] and A134: + (y,z) = yz9 and A135: + (x,(+ (y,z))) = yz9 - x9 by A107, Def1; A136: x9 = x99 by A113, A133, XTUPLE_0:1; yz9 <=' y9 by A132, A134, ARYTM_1:11; then not x9 <=' yz9 by A110, A114, A125, A136, ARYTM_1:3; hence + (x,(+ (y,z))) = [0,(x9 -' (y9 -' z9))] by A132, A134, A135, ARYTM_1:def_2 .= [0,((x99 -' y99) + z99)] by A110, A114, A125, A126, A136, A131, ARYTM_1:14 .= + ((+ (x,y)),z) by A128, A130, XTUPLE_0:1 ; ::_thesis: verum end; supposethat A137: not z9 <=' y9 and A138: x99 <=' y99 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) A139: ( not x in REAL+ or not + (z,y) in [:{0},REAL+:] ) by A107, Th5, XBOOLE_0:3; A140: + (y,z) = [0,(z9 -' y9)] by A112, A137, ARYTM_1:def_2; then + (y,z) in [:{0},REAL+:] by Lm1, ZFMISC_1:87; then ( not + (z,y) in REAL+ or not x in [:{0},REAL+:] ) by Th5, XBOOLE_0:3; then consider x9, yz99 being Element of REAL+ such that A141: x = [0,x9] and A142: ( + (y,z) = [0,yz99] & + (x,(+ (y,z))) = [0,(x9 + yz99)] ) by A140, A139, Def1, Lm1, ZFMISC_1:87; A143: x99 = x9 by A113, A141, XTUPLE_0:1; A144: + (y,x) = y99 -' x99 by A115, A138, ARYTM_1:def_2; then consider z99, yx99 being Element of REAL+ such that A145: z = [0,z99] and A146: + (y,x) = yx99 and A147: + (z,(+ (y,x))) = yx99 - z99 by A109, Def1; A148: z99 = z9 by A111, A145, XTUPLE_0:1; yx99 <=' y99 by A144, A146, ARYTM_1:11; then A149: not z99 <=' yx99 by A110, A114, A137, A148, ARYTM_1:3; thus + (x,(+ (y,z))) = [0,((z9 -' y9) + x9)] by A140, A142, XTUPLE_0:1 .= [0,(z99 -' (y99 -' x99))] by A110, A114, A137, A138, A148, A143, ARYTM_1:14 .= + ((+ (x,y)),z) by A144, A146, A147, A149, ARYTM_1:def_2 ; ::_thesis: verum end; supposethat A150: not x99 <=' y99 and A151: not z9 <=' y9 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) A152: ( not x in REAL+ or not + (z,y) in [:{0},REAL+:] ) by A107, Th5, XBOOLE_0:3; A153: ( not z in REAL+ or not + (x,y) in [:{0},REAL+:] ) by A109, Th5, XBOOLE_0:3; A154: + (y,x) = [0,(x99 -' y99)] by A115, A150, ARYTM_1:def_2; then + (y,x) in [:{0},REAL+:] by Lm1, ZFMISC_1:87; then ( not + (x,y) in REAL+ or not z in [:{0},REAL+:] ) by Th5, XBOOLE_0:3; then consider z99, yx9 being Element of REAL+ such that A155: z = [0,z99] and A156: ( + (y,x) = [0,yx9] & + (z,(+ (y,x))) = [0,(z99 + yx9)] ) by A154, A153, Def1, Lm1, ZFMISC_1:87; A157: z9 = z99 by A111, A155, XTUPLE_0:1; A158: + (y,z) = [0,(z9 -' y9)] by A112, A151, ARYTM_1:def_2; then + (y,z) in [:{0},REAL+:] by Lm1, ZFMISC_1:87; then ( not + (z,y) in REAL+ or not x in [:{0},REAL+:] ) by Th5, XBOOLE_0:3; then consider x9, yz99 being Element of REAL+ such that A159: x = [0,x9] and A160: ( + (y,z) = [0,yz99] & + (x,(+ (y,z))) = [0,(x9 + yz99)] ) by A158, A152, Def1, Lm1, ZFMISC_1:87; A161: x9 = x99 by A113, A159, XTUPLE_0:1; thus + (x,(+ (y,z))) = [0,((z9 -' y9) + x9)] by A158, A160, XTUPLE_0:1 .= [0,((x99 -' y99) + z99)] by A110, A114, A150, A151, A157, A161, ARYTM_1:15 .= + ((+ (x,y)),z) by A154, A156, XTUPLE_0:1 ; ::_thesis: verum end; end; end; hence + (x,(+ (y,z))) = + ((+ (x,y)),z) ; ::_thesis: verum end; supposethat A162: z in REAL+ and A163: y in [:{0},REAL+:] and A164: x in [:{0},REAL+:] ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) ( ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) ) by A163, A164, Th5, XBOOLE_0:3; then consider y9, x9 being Element of REAL+ such that A165: y = [0,y9] and A166: x = [0,x9] and A167: + (y,x) = [0,(y9 + x9)] by A163, Def1; + (y,x) in [:{0},REAL+:] by A167, Lm1, ZFMISC_1:87; then consider z9, yx9 being Element of REAL+ such that A168: z = z9 and A169: + (y,x) = [0,yx9] and A170: + (z,(+ (y,x))) = z9 - yx9 by A162, Def1; consider z99, y99 being Element of REAL+ such that A171: z = z99 and A172: y = [0,y99] and A173: + (z,y) = z99 - y99 by A162, A163, Def1; A174: y9 = y99 by A165, A172, XTUPLE_0:1; now__::_thesis:_+_(z,(+_(y,x)))_=_+_((+_(z,y)),x) percases ( y99 <=' z99 or not y99 <=' z99 ) ; supposeA175: y99 <=' z99 ; ::_thesis: + (z,(+ (y,x))) = + ((+ (z,y)),x) then A176: + (z,y) = z99 -' y99 by A173, ARYTM_1:def_2; then consider zy99, x99 being Element of REAL+ such that A177: + (z,y) = zy99 and A178: x = [0,x99] and A179: + ((+ (z,y)),x) = zy99 - x99 by A164, Def1; A180: x9 = x99 by A166, A178, XTUPLE_0:1; thus + (z,(+ (y,x))) = z9 - (y9 + x9) by A167, A169, A170, XTUPLE_0:1 .= + ((+ (z,y)),x) by A171, A168, A174, A175, A176, A177, A179, A180, ARYTM_1:24 ; ::_thesis: verum end; supposeA181: not y99 <=' z99 ; ::_thesis: + (z,(+ (y,x))) = + ((+ (z,y)),x) A182: ( not x in REAL+ or not + (z,y) in [:{0},REAL+:] ) by A164, Th5, XBOOLE_0:3; A183: + (z,y) = [0,(y99 -' z99)] by A173, A181, ARYTM_1:def_2; then + (z,y) in [:{0},REAL+:] by Lm1, ZFMISC_1:87; then ( not + (z,y) in REAL+ or not x in [:{0},REAL+:] ) by Th5, XBOOLE_0:3; then consider zy99, x99 being Element of REAL+ such that A184: + (z,y) = [0,zy99] and A185: x = [0,x99] and A186: + ((+ (z,y)),x) = [0,(zy99 + x99)] by A183, A182, Def1, Lm1, ZFMISC_1:87; A187: x9 = x99 by A166, A185, XTUPLE_0:1; A188: yx9 = x9 + y9 by A167, A169, XTUPLE_0:1; then y99 <=' yx9 by A174, ARYTM_2:19; then not yx9 <=' z9 by A171, A168, A181, ARYTM_1:3; hence + (z,(+ (y,x))) = [0,((x9 + y9) -' z9)] by A170, A188, ARYTM_1:def_2 .= [0,(x99 + (y99 -' z99))] by A171, A168, A174, A181, A187, ARYTM_1:13 .= + ((+ (z,y)),x) by A183, A184, A186, XTUPLE_0:1 ; ::_thesis: verum end; end; end; hence + (x,(+ (y,z))) = + ((+ (x,y)),z) ; ::_thesis: verum end; supposethat A189: x in [:{0},REAL+:] and A190: y in [:{0},REAL+:] and A191: z in [:{0},REAL+:] ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z) A192: ( not x in REAL+ or not + (z,y) in [:{0},REAL+:] ) by A189, Th5, XBOOLE_0:3; ( ( not z in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not z in [:{0},REAL+:] ) ) by A190, A191, Th5, XBOOLE_0:3; then consider y9, z9 being Element of REAL+ such that A193: y = [0,y9] and A194: z = [0,z9] and A195: + (y,z) = [0,(y9 + z9)] by A190, Def1; + (z,y) in [:{0},REAL+:] by A195, Lm1, ZFMISC_1:87; then ( not + (z,y) in REAL+ or not x in [:{0},REAL+:] ) by Th5, XBOOLE_0:3; then consider x9, yz9 being Element of REAL+ such that A196: x = [0,x9] and A197: ( + (y,z) = [0,yz9] & + (x,(+ (y,z))) = [0,(x9 + yz9)] ) by A195, A192, Def1, Lm1, ZFMISC_1:87; A198: ( not z in REAL+ or not + (x,y) in [:{0},REAL+:] ) by A191, Th5, XBOOLE_0:3; ( ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) ) by A189, A190, Th5, XBOOLE_0:3; then consider x99, y99 being Element of REAL+ such that A199: x = [0,x99] and A200: y = [0,y99] and A201: + (x,y) = [0,(x99 + y99)] by A189, Def1; A202: x9 = x99 by A199, A196, XTUPLE_0:1; + (x,y) in [:{0},REAL+:] by A201, Lm1, ZFMISC_1:87; then ( not + (x,y) in REAL+ or not z in [:{0},REAL+:] ) by Th5, XBOOLE_0:3; then consider xy99, z99 being Element of REAL+ such that A203: + (x,y) = [0,xy99] and A204: z = [0,z99] and A205: + ((+ (x,y)),z) = [0,(xy99 + z99)] by A201, A198, Def1, Lm1, ZFMISC_1:87; A206: z9 = z99 by A194, A204, XTUPLE_0:1; A207: y9 = y99 by A193, A200, XTUPLE_0:1; thus + (x,(+ (y,z))) = [0,((z9 + y9) + x9)] by A195, A197, XTUPLE_0:1 .= [0,(z99 + (y99 + x99))] by A206, A202, A207, ARYTM_2:6 .= + ((+ (x,y)),z) by A201, A203, A205, XTUPLE_0:1 ; ::_thesis: verum end; end; end; theorem :: ARYTM_0:24 for x, y being Element of REAL st [*x,y*] in REAL holds y = 0 proof let x, y be Element of REAL ; ::_thesis: ( [*x,y*] in REAL implies y = 0 ) assume A1: [*x,y*] in REAL ; ::_thesis: y = 0 assume y <> 0 ; ::_thesis: contradiction then [*x,y*] = (0,1) --> (x,y) by Def5; hence contradiction by A1, Th8; ::_thesis: verum end; theorem :: ARYTM_0:25 for x, y being Element of REAL holds opp (+ (x,y)) = + ((opp x),(opp y)) proof let x, y be Element of REAL ; ::_thesis: opp (+ (x,y)) = + ((opp x),(opp y)) + ((+ (x,y)),(+ ((opp x),(opp y)))) = + (x,(+ (y,(+ ((opp x),(opp y)))))) by Th23 .= + (x,(+ ((opp x),(+ (y,(opp y)))))) by Th23 .= + (x,(+ ((opp x),o))) by Def3 .= + (x,(opp x)) by Th11 .= 0 by Def3 ; hence opp (+ (x,y)) = + ((opp x),(opp y)) by Def3; ::_thesis: verum end;