:: Introduction to Arithmetics :: by Andrzej Trybulec :: :: Received January 9, 2003 :: Copyright (c) 2003-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, ARYTM_2, TARSKI, NUMBERS, ZFMISC_1, SUBSET_1, ARYTM_1, ARYTM_3, CARD_1, RELAT_1, FUNCOP_1, ORDINAL1, FUNCT_2, FUNCT_1, ARYTM_0, XCMPLX_0; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, ORDINAL1, ARYTM_3, ARYTM_2, ARYTM_1, NUMBERS; constructors FUNCT_4, ARYTM_1, NUMBERS, XTUPLE_0; registrations XBOOLE_0, ORDINAL1, FUNCT_2, FUNCT_4, ARYTM_2, FUNCT_1, NUMBERS; requirements BOOLE, SUBSET, NUMERALS; definitions ORDINAL1; equalities NUMBERS, TARSKI, ARYTM_3, ORDINAL1; expansions TARSKI, ORDINAL1; theorems XBOOLE_0, ARYTM_1, ZFMISC_1, TARSKI, ARYTM_2, XBOOLE_1, ORDINAL3, ARYTM_3, FUNCT_2, FUNCT_4, FUNCT_1, ENUMSET1, NUMBERS, XTUPLE_0; begin :: Arithmetics Lm1: for x being Element of REAL+ holds [0,x] in [:{0},REAL+:] proof 0 in {0} by TARSKI:def 1; hence thesis by ZFMISC_1:87; end; theorem Th1: REAL+ c= REAL proof REAL+ c= REAL+ \/ [:{{}},REAL+:] by XBOOLE_1:7; hence thesis by ARYTM_2:3,ZFMISC_1:34; end; theorem Th2: for x being Element of REAL+ st x <> {} holds [{},x] in REAL proof let x be Element of REAL+ such that A1: x <> {}; A2: now assume [{},x] in {[{},{}]}; then [{},x] = [{},{}] by TARSKI:def 1; hence contradiction by A1,XTUPLE_0:1; 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 thesis by A2,XBOOLE_0:def 5; end; theorem Th3: for y being set st [{},y] in REAL holds y <> {} proof let y be set such that A1: [{},y] in REAL and A2: y = {}; [{},y] in {[{},{}]} by A2,TARSKI:def 1; hence contradiction by A1,XBOOLE_0:def 5; end; theorem Th4: for x,y being Element of REAL+ holds x - y in REAL proof let x,y be Element of REAL+; per cases; suppose y <=' x; then x - y = x -' y by ARYTM_1:def 2; then x - y in REAL+; hence thesis by Th1; end; suppose A1: not y <=' x; then x - y = [{},y -' x] by ARYTM_1:def 2; hence thesis by A1,Th2,ARYTM_1:9; end; end; theorem Th5: REAL+ misses [:{{}},REAL+:] proof assume REAL+ meets [:{{}},REAL+:]; then consider x being object such that A1: x in REAL+ and A2: x in [:{{}},REAL+:] by XBOOLE_0:3; consider x1,x2 being object 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; end; begin :: Real numbers registration let x,y be object; cluster [x,y] -> non zero; coherence; end; theorem Th6: for x,y being Element of REAL+ st x - y = {} holds x = y proof let x,y be Element of REAL+; assume A1: x - y = {}; 0 <> [{},y -' x]; then y <=' x & x -' y = {} by A1,ARYTM_1:def 2; hence thesis by ARYTM_1:10; end; Lm2: not ex a,b being set st 1 = [a,b] proof let a,b be set; assume A1: 1 = [a,b]; {a} in {{a,b},{a}} by TARSKI:def 2; hence contradiction by A1,ORDINAL3:15,TARSKI:def 1; end; theorem Th7: 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+; assume that A1: x <> {} and A2: x *' y = x *' z; per cases; suppose A3: z <=' y; 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 thesis by Th6; end; suppose A4: 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 thesis by Th6; end; end; begin Lm3: 0 in REAL by NUMBERS:19; definition let x,y be Element of REAL; func +(x,y) -> Element of REAL means :Def1: 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 proof hereby assume x in REAL+ & y in REAL+; then reconsider x9=x, y9=y as Element of REAL+; reconsider IT = x9 + y9 as Element of REAL by Th1; take IT,x9,y9; thus x = x9 & y = y9 & IT = x9 + y9; end; A1: y in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5; hereby assume x in REAL+; then reconsider x9=x as Element of REAL+; assume y in [:{0},REAL+:]; then consider z,y9 being object such that A2: z in{0} and A3: y9 in REAL+ and A4: y = [z,y9] by ZFMISC_1:84; reconsider y9 as Element of REAL+ by A3; reconsider IT = x9 - y9 as Element of REAL by Th4; take IT,x9,y9; thus x = x9 & y = [0,y9] & IT = x9 - y9 by A2,A4,TARSKI:def 1; end; hereby assume y in REAL+; then reconsider y9=y as Element of REAL+; assume x in [:{0},REAL+:]; then consider z,x9 being object such that A5: z in{0} and A6: x9 in REAL+ and A7: x = [z,x9] by ZFMISC_1:84; reconsider x9 as Element of REAL+ by A6; reconsider IT = y9 - x9 as Element of REAL by Th4; take IT,x9,y9; thus x = [0,x9] & y = y9 & IT = y9 - x9 by A5,A7,TARSKI:def 1; end; assume that A8: not(x in REAL+ & y in REAL+) and A9: not(x in REAL+ & y in [:{0},REAL+:]) and A10: not(y in REAL+ & x in [:{0},REAL+:]); A11: x in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5; then x in REAL+ or x in [:{0},REAL+:] by XBOOLE_0:def 3; then consider z1,x9 being object 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 object 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 as Element of REAL+ by A13; reconsider 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,x9,y9; thus thesis by A12,A14,A15,A17,TARSKI:def 1; end; uniqueness proof let IT1,IT2 be Element of REAL; 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; 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; 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; assume that not(x in REAL+ & y in REAL+) and not(x in REAL+ & y in [:{0},REAL+:]) and not(y in REAL+ & x in [:{0},REAL+:]); given x9,y9 being Element of REAL+ such that A18: x = [0,x9] and A19: y = [0,y9] & IT1 = [0,x9+y9]; given x99,y99 being Element of REAL+ such that A20: x = [0,x99] and A21: y = [0,y99] & IT2 = [0,x99+y99]; x9 = x99 by A18,A20,XTUPLE_0:1; hence thesis by A19,A21,XTUPLE_0:1; end; consistency by Th5,XBOOLE_0:3; commutativity; func *(x,y) -> Element of REAL means :Def2: 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 proof hereby assume x in REAL+ & y in REAL+; then reconsider x9=x, y9=y as Element of REAL+; reconsider IT = x9 *' y9 as Element of REAL by Th1; take IT,x9,y9; thus x = x9 & y = y9 & IT = x9 *' y9; end; hereby assume x in REAL+; then reconsider x9=x as Element of REAL+; assume y in [:{0},REAL+:]; then consider z,y9 being object such that A22: z in{0} and A23: y9 in REAL+ and A24: y = [z,y9] by ZFMISC_1:84; reconsider 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; then reconsider IT = [0,x9 *' y9] as Element of REAL by A25,Th2,ARYTM_1:2 ; take IT,x9,y9; thus x = x9 & y = [0,y9] & IT = [0,x9 *' y9] by A22,A24,TARSKI:def 1; end; hereby assume y in REAL+; then reconsider y9=y as Element of REAL+; assume x in [:{0},REAL+:]; then consider z,x9 being object such that A26: z in{0} and A27: x9 in REAL+ and A28: x = [z,x9] by ZFMISC_1:84; reconsider 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; then reconsider IT = [0,y9 *' x9] as Element of REAL by A29,Th2,ARYTM_1:2 ; take IT,x9,y9; thus x = [0,x9] & y = y9 & IT = [0,y9 *' x9] by A26,A28,TARSKI:def 1; end; hereby assume x in [:{0},REAL+:]; then consider z1,x9 being object such that A30: z1 in{0} and A31: x9 in REAL+ and A32: x = [z1,x9] by ZFMISC_1:84; reconsider x9 as Element of REAL+ by A31; assume y in [:{0},REAL+:]; then consider z2,y9 being object such that A33: z2 in{0} and A34: y9 in REAL+ and A35: y = [z2,y9] by ZFMISC_1:84; reconsider y9 as Element of REAL+ by A34; reconsider IT = y9 *' x9 as Element of REAL by Th1; take IT,x9,y9; thus x = [0,x9] & y = [0,y9] & IT = y9 *' x9 by A30,A32,A33,A35, TARSKI:def 1; end; thus thesis by Lm3; end; uniqueness proof let IT1,IT2 be Element of REAL; 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; 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; 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; hereby assume that x in [:{0},REAL+:] and y in [:{0},REAL+:]; given x9,y9 being Element of REAL+ such that A36: x = [0,x9] and A37: y = [0,y9] & IT1 = y9 *' x9; given x99,y99 being Element of REAL+ such that A38: x = [0,x99] and A39: y = [0,y99] & IT2 = y99 *' x99; x9 = x99 by A36,A38,XTUPLE_0:1; hence IT1 = IT2 by A37,A39,XTUPLE_0:1; end; thus thesis; end; consistency by Th5,XBOOLE_0:3; commutativity; end; reserve x,y for Element of REAL; definition let x be Element of REAL; func opp x -> Element of REAL means :Def3: +(x,it) = 0; existence proof reconsider z9 = 0 as Element of REAL+ by ARYTM_2:20; A1: x in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5; per cases by A1,XBOOLE_0:def 3; suppose A2: x = 0; then reconsider x9 = x as Element of REAL+ by ARYTM_2:20; take x; x9 + x9 = 0 by A2,ARYTM_2:def 8; hence thesis by Def1,Lm3; end; suppose that A3: x in REAL+ and A4: x <> 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 ,ZFMISC_1:56; reconsider x9 = x as Element of REAL+ by A3; A7: x9 <=' x9; take y; 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 thesis by A6,Def1,Lm3; end; suppose A8: x in [:{0},REAL+:]; then consider a,b being object 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; now per cases; case x in REAL+ & y in REAL+; hence ex x9,y9 being Element of REAL+ st x = x9 & y = y9 & 0 = x9 + y9 by A8,Th5,XBOOLE_0:3; end; case x in REAL+ & y in [:{0},REAL+:]; hence ex x9,y9 being Element of REAL+ st x = x9 & y = [0,y9] & 0 = x9 - y9 by A10,Th5,XBOOLE_0:3; end; case y in REAL+ & x in [:{0},REAL+:]; reconsider x9 = b, y9 = y as Element of REAL+ by A10; take x9, y9; thus x = [0,x9] by A9,A11,TARSKI:def 1; thus y = y9; thus 0 = y9 - x9 by ARYTM_1:18; end; case not(x in REAL+ & y in REAL+) & not(x in REAL+ & y in [:{0}, REAL+:]) & not (y in REAL+ & x in [:{0},REAL+:]); hence ex x9,y9 being Element of REAL+ st x = [0,x9] & y = [0,y9] & 0 = [0,y9+x9] by A8,A10; end; end; hence thesis by Def1,Lm3; end; end; uniqueness proof let y,z be Element of REAL such that A12: +(x,y) = 0 and A13: +(x,z) = 0; per cases; suppose x in REAL+ & y in REAL+ & z in REAL+; 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 thesis by ARYTM_2:11; end; suppose that A14: x in REAL+ and A15: y in REAL+ and A16: z in [:{0},REAL+:]; 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 XBOOLE_0:def 5; z in REAL; hence thesis by A18,A19,A20,ARYTM_1:19; end; suppose that A21: x in REAL+ and A22: z in REAL+ and A23: y in [:{0},REAL+:]; 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 XBOOLE_0:def 5; y in REAL; hence thesis by A25,A26,A27,ARYTM_1:19; end; suppose that A28: x in REAL+ and A29: y in [:{0},REAL+:] and A30: z in [:{0},REAL+:]; 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 thesis by A35,A32; end; suppose that A37: z in REAL+ and A38: y in REAL+ and A39: x in [:{0},REAL+:]; 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 thesis by A44,A41; end; suppose not(x in REAL+ & y in REAL+) & not(x in REAL+ & y in [:{0}, REAL+:]) & not(y in REAL+ & x in [:{0},REAL+:]); then ex x9,y9 being Element of REAL+ st x = [0,x9] & y = [0,y9] & 0 = [0 ,x9+y9] by A12,Def1; hence thesis; end; suppose not(x in REAL+ & z in REAL+) & not(x in REAL+ & z in [:{0}, REAL+:]) & not(z in REAL+ & x in [:{0},REAL+:]); then ex x9,z9 being Element of REAL+ st x = [0,x9] & z = [0,z9] & 0 = [0 ,x9+z9] by A13,Def1; hence thesis; end; end; involutiveness; func inv x -> Element of REAL means :Def4: *(x,it) = 1 if x <> 0 otherwise it = 0; existence proof thus x <> 0 implies ex y st *(x,y) = 1 proof A46: x in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5; assume A47: x <> 0; per cases by A46,XBOOLE_0:def 3; suppose x in REAL+; then reconsider x9 = x as Element of REAL+; reconsider jj = 1 as Element of REAL by NUMBERS:19; consider y9 being Element of REAL+ such that A48: x9 *' y9 = jj by A47,ARYTM_2:14; reconsider y = y9 as Element of REAL by Th1; take y; thus thesis by A48,Def2; end; suppose A49: x in [:{0},REAL+:]; not x in {[0,0]} by XBOOLE_0:def 5; then A50: x <> [0,0] by TARSKI:def 1; consider x1,x2 being object such that x1 in {0} and A51: x2 in REAL+ and A52: x = [x1,x2] by A49,ZFMISC_1:84; reconsider 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 assume [0,y2] in {[0,0]}; then [0,y2] = [0,0] by TARSKI:def 1; then y2 = 0 by XTUPLE_0:1; hence contradiction by A53,ARYTM_2:4; end; A55: [0,y2] in [:{0},REAL+:] by Lm1; then [0,y2] in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 3; then reconsider y = [0,y2] as Element of REAL by A54 ,XBOOLE_0:def 5; take y; 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 thesis by A52,A53,A56,A58,XTUPLE_0:1; end; end; thus thesis; end; uniqueness proof let y,z be Element of REAL; thus x <> 0 & *(x,y) = 1 & *(x,z) = 1 implies y = z proof assume that A59: x <> 0 and A60: *(x,y) = 1 and A61: *(x,z) = 1; A62: for x,y being Element of REAL st *(x,y) =1 holds x <> 0 proof let x,y be Element of REAL such that A63: *(x,y) =1 and A64: x = 0; A65: not x in [:{0},REAL+:] by A64,Th5,ARYTM_2:20,XBOOLE_0:3; A66: y in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5; per cases by A66,XBOOLE_0:def 3; suppose y in REAL+; 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; end; suppose y in [:{0},REAL+:]; then not y in REAL+ by Th5,XBOOLE_0:3; hence contradiction by A63,A64,A65,Def2; end; end; then A67: y <> 0 by A60; A68: z <> 0 by A61,A62; per cases; suppose x in REAL+ & y in REAL+ & z in REAL+; 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 thesis by A59,Th7; end; suppose that A69: x in [:{0},REAL+:] and A70: y in [:{0},REAL+:] and A71: z in [:{0},REAL+:]; 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 thesis by A72,A73,A75,Th3,Th7; end; suppose x in REAL+ & y in [:{0},REAL+:]; then ex x9,y9 being Element of REAL+ st x = x9 & y = [0,y9] & 1 = [0, x9 *' y9] by A59,A60,Def2; hence thesis by Lm2; end; suppose x in [:{0},REAL+:] & y in REAL+; then ex x9,y9 being Element of REAL+ st x = [0,x9] & y = y9 & 1 = [0, y9 *' x9] by A60,A67,Def2; hence thesis by Lm2; end; suppose x in [:{0},REAL+:] & z in REAL+; then ex x9,z9 being Element of REAL+ st x = [0,x9] & z = z9 & 1 = [0, z9 *' x9] by A61,A68,Def2; hence thesis by Lm2; end; suppose x in REAL+ & z in [:{0},REAL+:]; then ex x9,z9 being Element of REAL+ st x = x9 & z = [0,z9] & 1 = [0, x9 *' z9] by A59,A61,Def2; hence thesis by Lm2; end; suppose not (x in REAL+ & y in REAL+) & not (x in REAL+ & y in [:{0} ,REAL+:] & x <> 0) & not (y in REAL+ & x in [:{0},REAL+:] & y <> 0) & not (x in [:{0},REAL+:] & y in [:{0},REAL+:]); hence thesis by A60,Def2; end; suppose not (x in REAL+ & z in REAL+) & not (x in REAL+ & z in [:{0} ,REAL+:] & x <> 0) & not (z in REAL+ & x in [:{0},REAL+:] & z <> 0) & not (x in [:{0},REAL+:] & z in [:{0},REAL+:]); hence thesis by A61,Def2; end; end; thus thesis; end; consistency; involutiveness proof let x,y be Element of REAL; assume that A76: y <> 0 implies *(y,x) = 1 and A77: y = 0 implies x = 0; thus x <> 0 implies *(x,y) = 1 by A76,A77; assume A78: x = 0; A79: y in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5; assume A80: y <> 0; per cases by A79,XBOOLE_0:def 3; suppose y in REAL+; 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; end; suppose A81: y in [:{0},REAL+:]; 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; end; end; end; begin :: from COMPLEX1 Lm4: for x,y,z being set st [x,y] = {z} holds z = {x} & x = y proof let x,y,z be set; assume A1: [x,y] = {z}; then {x} in {z} by TARSKI:def 2; hence A2: z = {x} by TARSKI:def 1; {x,y} in {z} by A1,TARSKI:def 2; then {x,y} = z by TARSKI:def 1; hence thesis by A2,ZFMISC_1:5; end; reserve i,j,k for Element of NAT; reserve a,b for Element of REAL; theorem Th8: not (0,1)-->(a,b) in REAL proof 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 f = {[0,a],[1,b]} by FUNCT_4:67; then A2: [1,b] in f by TARSKI:def 2; assume f in [:{{}},REAL+:]; then consider x,y being object such that A3: x in {{}} and y in REAL+ and A4: f = [x,y] by ZFMISC_1:84; x = 0 by A3,TARSKI:def 1; then per cases by A4,A2,TARSKI:def 2; suppose {{1,b},{1}} = {0}; then 0 in {{1,b},{1}} by TARSKI:def 1; hence contradiction by TARSKI:def 2; end; suppose {{1,b},{1}} = {0,y}; then 0 in {{1,b},{1}} by TARSKI:def 2; hence contradiction by TARSKI:def 2; end; end; A5: f = {[0,a],[1,b]} by FUNCT_4:67; now assume f in {[i,j]: i,j are_coprime & j <> {}}; then consider i,j such that A6: f = [i,j] and i,j are_coprime and j <> {}; A7: {i} in f & {i,j} in f by A6,TARSKI:def 2; A8: now assume i = j; then {i} = {i,j} by ENUMSET1:29; then A9: [i,j] = {{i}} by ENUMSET1:29; then [1,b] in {{i}} by A5,A6,TARSKI:def 2; then A10: [1,b] = {i} by TARSKI:def 1; [0,a] in {{i}} by A5,A6,A9,TARSKI:def 2; then [0,a] = {i} by TARSKI:def 1; hence contradiction by A10,XTUPLE_0:1; end; per cases by A5,A7,TARSKI:def 2; suppose {i,j} = [0,a] & {i} = [0,a]; hence contradiction by A8,ZFMISC_1:5; end; suppose that A11: {i,j} = [0,a] and A12: {i} = [1,b]; i in {i,j} by TARSKI:def 2; then i = {0,a} or i = {0} by A11,TARSKI:def 2; then A13: 0 in i by TARSKI:def 1,def 2; i = {1} by A12,Lm4; hence contradiction by A13,TARSKI:def 1; end; suppose that A14: {i,j} = [1,b] and A15: {i} = [0,a]; i in {i,j} by TARSKI:def 2; then i = {1,b} or i = {1} by A14,TARSKI:def 2; then A16: 1 in i by TARSKI:def 1,def 2; i = {0} by A15,Lm4; hence contradiction by A16,TARSKI:def 1; end; suppose {i,j} = [1,b] & {i} = [1,b]; hence contradiction by A8,ZFMISC_1:5; end; end; then A17: not f in {[i,j]: i,j are_coprime & j <> {}} \ the set of all [k,1]; not ex x,y being set st {[0,x],[1,y]} in IR proof given x,y being set such that A18: {[0,x],[1,y]} in IR; consider A being Subset of RAT+ such that A19: {[0,x],[1,y]} = A and A20: 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 A18; [0,x] in A & for r,s being Element of RAT+ st r in A & s <=' r holds s in A by A19,A20,TARSKI:def 2; then consider r1,r2,r3 being Element of RAT+ such that A21: r1 in A and A22: r2 in A and A23: r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1 by ARYTM_3:75; A24: r2 = [0,x] or r2 = [1,y] by A19,A22,TARSKI:def 2; r1 = [0,x] or r1 = [1,y] by A19,A21,TARSKI:def 2; hence contradiction by A19,A23,A24,TARSKI:def 2; end; then A25: not f in DEDEKIND_CUTS by A5,ARYTM_2:def 1; now assume f in omega; then {} in f by ORDINAL3:8; hence contradiction by A5,TARSKI:def 2; end; then not f in RAT+ by A17,XBOOLE_0:def 3; then not f in REAL+ by A25,ARYTM_2:def 2,XBOOLE_0:def 3; hence thesis by A1,XBOOLE_0:def 3; end; definition let x,y be Element of REAL; func [*x,y*] -> Element of COMPLEX equals :Def5: x if y = 0 otherwise (0,1) --> (x,y); consistency; coherence proof set z = (0,1)-->(x,y); thus y = 0 implies x is Element of COMPLEX by XBOOLE_0:def 3; assume A1: y <> 0; A2: now assume z in { r where r is Element of Funcs({0,1},REAL): r.1 = 0 }; then ex r being Element of Funcs({0,1},REAL) st z = r & r.1 = 0; hence contradiction by A1,FUNCT_4:63; end; z in Funcs({0,1},REAL) by FUNCT_2:8; then z 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 thesis by XBOOLE_0:def 3; end; end; theorem for c being Element of COMPLEX ex r,s being Element of REAL st c = [*r ,s*] proof let c be Element of COMPLEX; per cases; suppose c in REAL; then reconsider r=c, z=0 as Element of REAL by Lm3; take r,z; thus thesis by Def5; end; suppose not c in REAL; then A1: c in Funcs({0,1},REAL) \ { x where x is Element of Funcs({0,1},REAL): x.1 = 0} by 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,s; A6: c = (0,1)-->(r,s) by A2,A3,FUNCT_4:66; now assume s = 0; 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; end; hence thesis by A6,Def5; end; end; theorem 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 such that A1: [*x1,x2*] = [*y1,y2*]; per cases; suppose A2: x2 = 0; then A3: [*x1,x2*] = x1 by Def5; A4: now assume y2 <> 0; then x1 = (0,1) --> (y1,y2) by A1,A3,Def5; hence contradiction by Th8; end; hence x1 = y1 by A1,A3,Def5; thus thesis by A2,A4; end; suppose x2 <> 0; then A5: [*y1,y2*] = (0,1) --> (x1,x2) by A1,Def5; now assume y2 = 0; then [*y1,y2*] = y1 by Def5; hence contradiction by A5,Th8; end; then [*y1,y2*] = (0,1) --> (y1,y2) by Def5; hence thesis by A5,FUNCT_4:68; end; end; set RR = [:{0},REAL+:] \ {[0,0]}; theorem Th11: 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 being Element of REAL such that A1: o = 0; per cases; suppose x in REAL+; then reconsider x9 = x as Element of REAL+; x9 = x9 + y9 by ARYTM_2:def 8; hence thesis by A1,Def1; end; suppose A2: not x in REAL+; x in REAL+ \/ [:{{}},REAL+:] by XBOOLE_0:def 5; then A3: x in [:{{}},REAL+:] by A2,XBOOLE_0:def 3; then consider x1,x2 being object 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 thesis by A1,A3,A6,A7,Def1; end; end; theorem Th12: for x,o being Element of REAL st o = 0 holds *(x,o) = 0 proof let x,o being Element of REAL such that A1: o = 0; per cases; suppose x in REAL+; then reconsider x9 = x, y9 = 0 as Element of REAL+ by ARYTM_2:20; 0 = x9 *' y9 by ARYTM_2:4; hence thesis by A1,Def2; end; suppose A2: not x in REAL+; not o in [:{{}},REAL+:] by A1,Th5,ARYTM_2:20,XBOOLE_0:3; hence thesis by A1,A2,Def2; end; end; theorem Th13: for x,y,z being Element of REAL holds *(x,*(y,z)) = *(*(x,y),z) proof let x,y,z be Element of REAL; reconsider o = 0 as Element of REAL by Lm3; per cases; suppose that A1: x in REAL+ and A2: y in REAL+ and A3: z in REAL+; 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 thesis by A6,A4,A5,ARYTM_2:12; end; suppose that A7: x in REAL+ & x <> 0 and A8: y in RR and A9: z in REAL+ & z <> 0; 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; 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; 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; end; suppose that A22: x in RR and A23: y in REAL+ & y <> 0 and A24: z in REAL+ & z <> 0; 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; 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; end; suppose that A35: x in RR and A36: y in RR and A37: z in REAL+ & z <> 0; 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; 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; end; suppose that A49: x in REAL+ & x <> 0 and A50: y in REAL+ & y <> 0 and A51: z in RR; 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; 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; end; suppose that A62: x in REAL+ & x <> 0 and A63: y in RR and A64: z in RR; 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; 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; end; suppose that A76: y in REAL+ & y <> 0 and A77: x in RR and A78: z in RR; 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; 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; 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; end; suppose that A92: x in RR and A93: y in RR and A94: z in RR; 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 XBOOLE_0:def 5; then A98: y9 <> 0 by A95,TARSKI:def 1; not z in {[0,0]} by 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 XBOOLE_0:def 5; then A106: y9 <> 0 by A95,TARSKI:def 1; not x in {[0,0]} by 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 thesis by A97,A100,A103,A104,A105,A107,A109,ARYTM_2:12; end; suppose A110: x = 0; hence *(x,*(y,z)) = 0 by Th12 .= *(o,z) by Th12 .= *(*(x,y),z) by A110,Th12; end; suppose A111: y = 0; hence *(x,*(y,z)) = *(x,o) by Th12 .= 0 by Th12 .= *(o,z) by Th12 .= *(*(x,y),z) by A111,Th12; end; suppose A112: z = 0; hence *(x,*(y,z)) = *(x,o) by Th12 .= 0 by Th12 .= *(*(x,y),z) by A112,Th12; end; suppose A113: not( x in REAL+ & y in REAL+ & z in REAL+) & not(x in REAL+ & y in RR & z in REAL+) & not(y in REAL+ & x in RR & z in REAL+) & not(x in RR & y in RR & z in REAL+) & not( x in REAL+ & y in REAL+ & z in RR) & not(x in REAL+ & y in RR & z in RR) & not(y in REAL+ & x in RR & z in RR) & not(x in RR & y in RR & z in RR); REAL = (REAL+ \ {[{},{}]}) \/ ([:{{}},REAL+:] \ {[{},{}]}) by XBOOLE_1:42 .= REAL+ \/ RR by ARYTM_2:3,ZFMISC_1:57; hence thesis by A113,XBOOLE_0:def 3; end; end; theorem Th14: 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; reconsider o = 0 as Element of REAL by Lm3; per cases; suppose A1: x = 0; hence *(x,+(y,z)) = 0 by Th12 .= +(o,o) by Th11 .= +(*(x,y),o) by A1,Th12 .= +(*(x,y),*(x,z)) by A1,Th12; end; suppose that A2: x in REAL+ and A3: y in REAL+ & z in REAL+; 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 thesis by A4,A5,A6,ARYTM_2:13; end; suppose that A7: x in REAL+ & x <> 0 and A8: y in REAL+ and A9: z in RR; 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; 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 per cases; suppose A20: z99 <=' y99; 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; end; suppose A22: not z99 <=' y99; then A23: +(y,z) = [0,z99 -' y99] by A12,ARYTM_1:def 2; then +(y,z) in [:{0},REAL+:] by Lm1; 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; end; end; hence thesis; end; suppose that A26: x in REAL+ & x <> 0 and A27: z in REAL+ and A28: y in RR; 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; 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 per cases; suppose A39: y99 <=' z99; 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; end; suppose A41: not y99 <=' z99; then A42: +(z,y) = [0,y99 -' z99] by A31,ARYTM_1:def 2; then +(z,y) in [:{0},REAL+:] by Lm1; 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; end; end; hence thesis; end; suppose that A45: x in REAL+ & x <> 0 and A46: y in RR and A47: z in RR; ( not(y in REAL+ & z in [:{0},REAL+:]))& not(y in [:{0},REAL+:] & 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; 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; then A60: not(*(x,y) in [:{0},REAL+:] & *(x,z) in REAL+) by Th5,XBOOLE_0:3; *(x,y) in [:{0},REAL+:] by A55,Lm1; then not(*(x,y) in REAL+ & *(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; 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; end; suppose that A65: x in RR and A66: y in REAL+ and A67: z in REAL+; 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 per cases; suppose that A71: y <> 0 and A72: z <> 0; 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; then A82: not(*(x,y) in [:{0},REAL+:] & *(x,z) in REAL+) by Th5,XBOOLE_0:3; *(x,y) in [:{0},REAL+:] by A80,Lm1; then not(*(x,y) in REAL+ & *(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; 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; end; suppose A86: x = 0; hence *(x,+(y,z)) = 0 by Th12 .= +(o,o) by Th11 .= +(*(x,y),o) by A86,Th12 .= +(*(x,y),*(x,z)) by A86,Th12; end; suppose A87: z = 0; hence *(x,+(y,z)) = *(x,y) by Th11 .= +(*(x,y),*(x,z)) by A87,Th11,Th12; end; suppose A88: y = 0; hence *(x,+(y,z)) = *(x,z) by Th11 .= +(*(x,y),*(x,z)) by A88,Th11,Th12; end; end; hence thesis; end; suppose that A89: x in RR and A90: y in REAL+ and A91: z in RR; 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 per cases; suppose y <> 0; 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; 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 per cases; suppose A104: z99 <=' y99; then A105: +(y,z) = y99 -' z99 by A102,ARYTM_1:def 2; now per cases; suppose A106: +(y,z) <> 0; 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 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; end; suppose A112: +(y,z) = 0; 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; end; end; hence thesis; end; suppose A115: not z99 <=' y99; then A116: +(y,z) = [0,z99 -' y99] by A102,ARYTM_1:def 2; then +(y,z) in [:{0},REAL+:] by Lm1; 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; end; end; hence thesis; end; suppose A121: y = 0; hence *(x,+(y,z)) = *(x,z) by Th11 .= +(*(x,y),*(x,z)) by A121,Th11,Th12; end; end; hence thesis; end; suppose that A122: x in RR and A123: z in REAL+ and A124: y in RR; 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 per cases; suppose z <> 0; 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; 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 per cases; suppose A137: y99 <=' z99; then A138: +(z,y) = z99 -' y99 by A135,ARYTM_1:def 2; now per cases; suppose A139: +(z,y) <> 0; 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 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; end; suppose A145: +(z,y) = 0; 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; end; end; hence thesis; end; suppose A148: not y99 <=' z99; then A149: +(z,y) = [0,y99 -' z99] by A135,ARYTM_1:def 2; then +(z,y) in [:{0},REAL+:] by Lm1; 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; end; end; hence thesis; end; suppose A154: z = 0; hence *(x,+(y,z)) = *(x,y) by Th11 .= +(*(x,y),*(x,z)) by A154,Th11,Th12; end; end; hence thesis; end; suppose that A155: x in RR and A156: y in RR and A157: z in RR; ( not(y in REAL+ & z in [:{0},REAL+:]))& not(y in [:{0},REAL+:] & 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; 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; end; suppose A173: not(x in REAL+ & y in REAL+ & z in REAL+) & not(x in REAL+ & y in REAL+ & z in RR) & not(x in REAL+ & y in RR & z in REAL+) & not(x in REAL+ & y in RR & z in RR) & not(x in RR & y in REAL+ & z in REAL+) & not(x in RR & y in REAL+ & z in RR) & not(x in RR & y in RR & z in REAL+) & not(x in RR & y in RR & z in RR); REAL = (REAL+ \ {[0,0]}) \/ ([:{0},REAL+:] \ {[0,0]}) by XBOOLE_1:42 .= REAL+ \/ RR by ARYTM_2:3,ZFMISC_1:57; hence thesis by A173,XBOOLE_0:def 3; end; end; theorem for x,y being Element of REAL holds *(opp x,y) = opp *(x,y) proof let x,y be Element of REAL; +(*(opp x,y),*(x,y)) = *(+(opp x,x), y) by Th14 .= 0 by Th12,Def3; hence thesis by Def3; end; theorem Th16: for x being Element of REAL holds *(x,x) in REAL+ proof let x be Element of REAL; A1: x in REAL+ \/ [:{{}},REAL+:] by XBOOLE_0:def 5; per cases by A1,XBOOLE_0:def 3; suppose x in REAL+; then ex x9,y9 being Element of REAL+ st x = x9 & x = y9 & *(x,x) = x9 *' y9 by Def2; hence thesis; end; suppose x in [:{0},REAL+:]; then ex x9,y9 being Element of REAL+ st x = [0,x9] & x = [0,y9] & *(x,x) = y9 *' x9 by Def2; hence thesis; end; end; theorem for x,y st +(*(x,x),*(y,y)) = 0 holds x = 0 proof let x,y such that A1: +(*(x,x),*(y,y)) = 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 XBOOLE_0:def 5; per cases by A5,XBOOLE_0:def 3; suppose x in REAL+; then ex x9,y9 being Element of REAL+ st x = x9 & x = y9 & 0 = x9 *' y9 by A2,A4,Def2; hence thesis by ARYTM_1:2; end; suppose x in [:{0},REAL+:]; 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 thesis by XBOOLE_0:def 5; end; end; theorem Th18: 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; assume that A1: x <> 0 and A2: *(x,y) = 1 and A3: *(x,z) = 1; thus y = inv x by A1,A2,Def4 .= z by A1,A3,Def4; end; theorem Th19: for x,y st y = 1 holds *(x,y) = x proof let x,y such that A1: y = 1; per cases; suppose x = 0; hence thesis by Th12; end; suppose A2: x <> 0; A3: now assume A4: inv x = 0; thus 1 = *(x, inv x) by A2,Def4 .= 0 by A4,Th12; 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 thesis by A3,A6,Th18; end; end; theorem for x,y st y <> 0 holds *(*(x,y),inv y) = x proof reconsider jj = 1 as Element of REAL by NUMBERS:19; let x,y such that A1: y <> 0; thus *(*(x,y),inv y) = *(x,*(y,inv y)) by Th13 .= *(x,jj) by A1,Def4 .= x by Th19; end; theorem Th21: for x,y st *(x,y) = 0 holds x = 0 or y = 0 proof reconsider jj = 1 as Element of REAL by NUMBERS:19; let x,y such that A1: *(x,y) = 0 and A2: x <> 0; A3: *(x, inv x) = 1 by A2,Def4; thus y = *(jj,y) by Th19 .= *(*(x,y),inv x) by A3,Th13 .= 0 by A1,Th12; end; theorem for x,y holds inv *(x,y) = *(inv x, inv y) proof reconsider jj = 1 as Element of REAL by NUMBERS:19; let x,y; per cases; suppose A1: x = 0 or y = 0; 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; end; suppose that A3: x <> 0 and A4: y <> 0; 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 .= *(*(jj,y), inv y) by A6,Th13 .= 1 by A7,Th19; hence thesis by A5,Def4; end; end; theorem Th23: for x,y,z being Element of REAL holds +(x,+(y,z)) = +(+(x,y),z) proof let x,y,z be Element of REAL; A1: x in REAL+ \/ [:{0},REAL+:] & y in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5; A2: z in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5; per cases by A1,A2,XBOOLE_0:def 3; suppose that A3: x in REAL+ and A4: y in REAL+ and A5: z in REAL+; 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 thesis by A8,A6,A7,ARYTM_2:6; end; suppose that A9: x in REAL+ and A10: y in REAL+ and A11: z in [:{0},REAL+:]; 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 per cases; suppose A20: z9 <=' y9; 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 thesis by A16,A12,A13,A15,A19,A20,A21,ARYTM_1:20; end; suppose A22: not z9 <=' y9; then A23: +(y,z) = [0,z9 -' y9] by A18,ARYTM_1:def 2; then +(y,z) in [:{0},REAL+:] by Lm1; 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; end; end; hence thesis; end; suppose that A26: x in REAL+ and A27: y in [:{0},REAL+:] and A28: z in REAL+; 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 per cases; suppose that A36: y9 <=' x99 and A37: y9 <=' z9; 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 thesis by A32,A29,A36,A37,A38,A39,A40,A41,ARYTM_1:12; end; suppose that A42: y9 <=' x99 and A43: not y9 <=' z9; 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; 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; end; suppose that A49: not y9 <=' x99 and A50: y9 <=' z9; A51: +(y,x) = [0,y9 -' x99] by A31,A35,A49,ARYTM_1:def 2; then +(y,x) in [:{0},REAL+:] by Lm1; 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; end; suppose that A55: not y9 <=' x99 and A56: not y9 <=' z9; A57: +(y,z) = [0,y9 -' z9] by A34,A56,ARYTM_1:def 2; then +(y,z) in [:{0},REAL+:] by Lm1; 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; 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; end; end; hence thesis; end; suppose that A63: x in REAL+ and A64: y in [:{0},REAL+:] and A65: z in [:{0},REAL+:]; ( not(z in REAL+ & y in [:{0},REAL+:]))& not(y in REAL+ & 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; 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 per cases; suppose A76: y99 <=' x99; 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; end; suppose A82: not y99 <=' x99; A83: not(z in REAL+ & +(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; then not(+(x,y) in REAL+ & 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; 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; end; end; hence thesis; end; suppose that A90: z in REAL+ and A91: y in REAL+ and A92: x in [:{0},REAL+:]; 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 per cases; suppose A101: x9 <=' y9; 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; end; suppose A103: not x9 <=' y9; then A104: +(y,x) = [0,x9 -' y9] by A99,ARYTM_1:def 2; then +(y,x) in [:{0},REAL+:] by Lm1; 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; end; end; hence thesis; end; suppose that A107: x in [:{0},REAL+:] and A108: y in REAL+ and A109: z in [:{0},REAL+:]; 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 per cases; suppose that A116: x99 <=' y99 and A117: z9 <=' y9; 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 thesis by A110,A114,A116,A117,A118,A120,A121,A122,A124,ARYTM_1:25 ; end; suppose that A125: not x99 <=' y99 and A126: z9 <=' y9; A127: not(z in REAL+ & +(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; then not(+(x,y) in REAL+ & 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; 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; end; suppose that A137: not z9 <=' y9 and A138: x99 <=' y99; A139: not(x in REAL+ & +(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; then not(+(z,y) in REAL+ & 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; 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; end; suppose that A150: not x99 <=' y99 and A151: not z9 <=' y9; A152: not(x in REAL+ & +(z,y) in [:{0},REAL+:]) by A107,Th5,XBOOLE_0:3; A153: not(z in REAL+ & +(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; then not(+(x,y) in REAL+ & 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; 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; then not(+(z,y) in REAL+ & 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; 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; end; end; hence thesis; end; suppose that A162: z in REAL+ and A163: y in [:{0},REAL+:] and A164: x in [:{0},REAL+:]; ( not(x in REAL+ & y in [:{0},REAL+:]))& not(y in REAL+ & 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; 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 per cases; suppose A175: y99 <=' z99; 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; end; suppose A181: not y99 <=' z99; A182: not(x in REAL+ & +(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; then not(+(z,y) in REAL+ & 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; 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; end; end; hence thesis; end; suppose that A189: x in [:{0},REAL+:] and A190: y in [:{0},REAL+:] and A191: z in [:{0},REAL+:]; A192: not(x in REAL+ & +(z,y) in [:{0},REAL+:]) by A189,Th5,XBOOLE_0:3; ( not(z in REAL+ & y in [:{0},REAL+:]))& not(y in REAL+ & 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; then not(+(z,y) in REAL+ & 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; A198: not(z in REAL+ & +(x,y) in [:{0},REAL+:]) by A191,Th5,XBOOLE_0:3; ( not(x in REAL+ & y in [:{0},REAL+:]))& not(y in REAL+ & 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; then not(+(x,y) in REAL+ & 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; 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; end; end; theorem [*x,y*] in REAL implies y = 0 proof assume A1: [*x,y*] in REAL; assume y <> 0; then [*x,y*] = (0,1) --> (x,y) by Def5; hence contradiction by A1,Th8; end; theorem for x,y being Element of REAL holds opp +(x,y) = +(opp x, opp y) proof reconsider o = 0 as Element of REAL by Lm3; let x,y be Element of REAL; +(+(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 thesis by Def3; end;