### The Mizar article:

### Introduction to Arithmetics

**by****Andrzej Trybulec**

- Received January 9, 2003
Copyright (c) 2003 Association of Mizar Users

- MML identifier: ARYTM_0
- [ MML identifier index ]

environ vocabulary ARYTM_0, COMPLEX1, FUNCT_2, FUNCT_1, FUNCOP_1, ARYTM_2, BOOLE, ARYTM_1, ARYTM_3, ORDINAL2, ORDINAL1, OPPCAT_1, RELAT_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, ORDINAL1, ARYTM_3, ARYTM_2, ARYTM_1, NUMBERS; constructors ARYTM_1, FRAENKEL, FUNCT_4, XBOOLE_0, NUMBERS; clusters XBOOLE_0, ARYTM_2, SUBSET_1, ORDINAL2, ARYTM_3, FRAENKEL, FUNCT_2, FUNCT_4, ZFMISC_1, NUMBERS; requirements BOOLE, SUBSET; theorems XBOOLE_0, ARYTM_1, ZFMISC_1, TARSKI, ARYTM_2, ORDINAL2, XBOOLE_1, ORDINAL1, ORDINAL3, ARYTM_3, FUNCT_2, FUNCT_4, FUNCT_1, ENUMSET1, NUMBERS; begin :: Arithmetics Lm1: {} in {{}} by TARSKI:def 1; Lm2: now let e be set; assume A1: one = [0,e]; {0} = 0 \/ {0} .= succ 0 by ORDINAL1:def 1 .= {{0},{0,e}} by A1,ORDINAL2:def 4,TARSKI:def 5; then {0} in {0} by TARSKI:def 2; hence contradiction; end; theorem Th1: REAL+ c= REAL proof A1: REAL+ c= REAL+ \/ [:{{}},REAL+:] by XBOOLE_1:7; not [{},{}] in REAL+ by ARYTM_2:3; hence thesis by A1,NUMBERS:def 1,ZFMISC_1:40; 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,ZFMISC_1:33; end; {} in {{}} by TARSKI:def 1; then [{},x] in [:{{}},REAL+:] by ZFMISC_1:106; then [{},x] in REAL+ \/ [:{{}},REAL+:] by XBOOLE_0:def 2; hence [{},x] in REAL by A2,NUMBERS:def 1,XBOOLE_0:def 4; 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,NUMBERS:def 1,XBOOLE_0:def 4; 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 x - y in REAL by Th1; suppose A1: not y <=' x; then A2: x - y = [{},y -' x] by ARYTM_1:def 2; y -' x <> {} by A1,ARYTM_1:9; hence x - y in REAL by A2,Th2; end; theorem Th5: REAL+ misses [:{{}},REAL+:] proof assume REAL+ meets [:{{}},REAL+:]; 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 A4: x2 in REAL+ & x = [x1,x2] by A2,ZFMISC_1:103; x1 = {} by A3,TARSKI:def 1; hence contradiction by A1,A4,ARYTM_2:3; end; begin :: Real numbers theorem Th6: for x,y being Element of REAL+ st x - y = {} holds x = y proof let x,y be Element of REAL+; A1: {} <> [{},y -' x]; assume A2: x - y = {}; then A3: y <=' x by A1,ARYTM_1:def 2; then x -' y = {} by A2,ARYTM_1:def 2; hence x = y by A3,ARYTM_1:10; end; theorem Th7: not ex a,b being set st one = [a,b] proof let a,b be set; assume one = [a,b]; then A1: {{}} = {{a,b},{a}} by ORDINAL3:18,TARSKI:def 5; {a} in {{a,b},{a}} by TARSKI:def 2; hence contradiction by A1,TARSKI:def 1; end; theorem Th8: 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 y = z by Th6; 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 y = z by Th6; end; canceled; begin :: from XREAL_0 definition let x,y be Element of REAL; canceled; func +(x,y) -> Element of REAL means :Def2: ex x',y' being Element of REAL+ st x = x' & y = y' & it = x' + y' if x in REAL+ & y in REAL+, ex x',y' being Element of REAL+ st x = x' & y = [0,y'] & it = x' - y' if x in REAL+ & y in [:{0},REAL+:], ex x',y' being Element of REAL+ st x = [0,x'] & y = y' & it = y' - x' if y in REAL+ & x in [:{0},REAL+:] otherwise ex x',y' being Element of REAL+ st x = [0,x'] & y = [0,y'] & it = [0,x'+y']; existence proof hereby assume x in REAL+ & y in REAL+; then reconsider x'=x, y'=y as Element of REAL+; x' + y' in REAL+; then reconsider IT = x' + y' as Element of REAL by Th1; take IT,x',y'; thus x = x' & y = y' & IT = x' + y'; end; hereby assume x in REAL+; then reconsider x'=x as Element of REAL+; assume y in [:{0},REAL+:]; then consider z,y' being set such that A1: z in{0} and A2: y' in REAL+ and A3: y = [z,y'] by ZFMISC_1:103; reconsider y' as Element of REAL+ by A2; reconsider IT = x' - y' as Element of REAL by Th4; take IT,x',y'; thus x = x' & y = [0,y'] & IT = x' - y' by A1,A3,TARSKI:def 1; end; hereby assume y in REAL+; then reconsider y'=y as Element of REAL+; assume x in [:{0},REAL+:]; then consider z,x' being set such that A4: z in{0} and A5: x' in REAL+ and A6: x = [z,x'] by ZFMISC_1:103; reconsider x' as Element of REAL+ by A5; reconsider IT = y' - x' as Element of REAL by Th4; take IT,x',y'; thus x = [0,x'] & y = y' & IT = y' - x' by A4,A6,TARSKI:def 1; end; x in REAL+ \/ [:{0},REAL+:] & y in REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1,XBOOLE_0:def 4; then A7: (x in REAL+ or x in [:{0},REAL+:]) & (y in REAL+ or y in [:{0},REAL+:]) by XBOOLE_0:def 2; assume A8: not(x in REAL+ & y in REAL+) & not(x in REAL+ & y in [:{0},REAL+:]) & not(y in REAL+ & x in [:{0},REAL+:]); then consider z1,x' being set such that A9: z1 in{0} and A10: x' in REAL+ and A11: x = [z1,x'] by A7,ZFMISC_1:103; reconsider x' as Element of REAL+ by A10; consider z2,y' being set such that A12: z2 in{0} and A13: y' in REAL+ and A14: y = [z2,y'] by A7,A8,ZFMISC_1:103; reconsider y' as Element of REAL+ by A13; x = [0,x'] by A9,A11,TARSKI:def 1; then x' <> 0 by Th3; then x' + y' <> 0 by ARYTM_2:6; then reconsider IT = [0,y' + x'] as Element of REAL by Th2; take IT,x',y'; thus x = [0,x'] & y = [0,y'] & IT = [0,x' + y'] by A9,A11,A12,A14,TARSKI:def 1; end; uniqueness proof let IT1,IT2 be Element of REAL; thus x in REAL+ & y in REAL+ & (ex x',y' being Element of REAL+ st x = x' & y = y' & IT1 = x' + y') & (ex x',y' being Element of REAL+ st x = x' & y = y' & IT2 = x' + y') implies IT1 = IT2; thus x in REAL+ & y in [:{0},REAL+:] & (ex x',y' being Element of REAL+ st x = x' & y = [0,y'] &IT1 = x' - y') & (ex x'',y'' being Element of REAL+ st x = x'' & y = [0,y''] & IT2 = x'' - y'') implies IT1 = IT2 by ZFMISC_1:33; thus y in REAL+ & x in [:{0},REAL+:] & (ex x',y' being Element of REAL+ st x = [0,x'] & y = y' & IT1 = y' - x') & (ex x'',y'' being Element of REAL+ st x = [0,x''] & y = y'' & IT2 = y'' - x'') implies IT1 = IT2 by ZFMISC_1:33; assume not(x in REAL+ & y in REAL+) & not(x in REAL+ & y in [:{0},REAL+:]) & not(y in REAL+ & x in [:{0},REAL+:]); given x',y' being Element of REAL+ such that A15: x = [0,x'] & y = [0,y'] and A16: IT1 = [0,x'+y']; given x'',y'' being Element of REAL+ such that A17: x = [0,x''] & y = [0,y''] and A18: IT2 = [0,x''+y'']; x' = x'' & y' = y'' by A15,A17,ZFMISC_1:33; hence thesis by A16,A18; end; consistency by Th5,XBOOLE_0:3; commutativity; func *(x,y) -> Element of REAL means :Def3: ex x',y' being Element of REAL+ st x = x' & y = y' & it = x' *' y' if x in REAL+ & y in REAL+, ex x',y' being Element of REAL+ st x = x' & y = [0,y'] & it = [0,x' *' y'] if x in REAL+ & y in [:{0},REAL+:] & x <> 0, ex x',y' being Element of REAL+ st x = [0,x'] & y = y' & it = [0,y' *' x'] if y in REAL+ & x in [:{0},REAL+:] & y <> 0, ex x',y' being Element of REAL+ st x = [0,x'] & y = [0,y'] & it = y' *' x' if x in [:{0},REAL+:] & y in [:{0},REAL+:] otherwise it = 0; existence proof hereby assume x in REAL+ & y in REAL+; then reconsider x'=x, y'=y as Element of REAL+; x' *' y' in REAL+; then reconsider IT = x' *' y' as Element of REAL by Th1; take IT,x',y'; thus x = x' & y = y' & IT = x' *' y'; end; hereby assume x in REAL+; then reconsider x'=x as Element of REAL+; assume y in [:{0},REAL+:]; then consider z,y' being set such that A19: z in{0} and A20: y' in REAL+ and A21: y = [z,y'] by ZFMISC_1:103; reconsider y' as Element of REAL+ by A20; assume A22: x <> 0; y = [0,y'] by A19,A21,TARSKI:def 1; then y' <> 0 by Th3; then x' *' y' <> 0 by A22,ARYTM_1:2; then reconsider IT = [0,x' *' y'] as Element of REAL by Th2; take IT,x',y'; thus x = x' & y = [0,y'] & IT = [0,x' *' y'] by A19,A21,TARSKI:def 1; end; hereby assume y in REAL+; then reconsider y'=y as Element of REAL+; assume x in [:{0},REAL+:]; then consider z,x' being set such that A23: z in{0} and A24: x' in REAL+ and A25: x = [z,x'] by ZFMISC_1:103; reconsider x' as Element of REAL+ by A24; assume A26: y <> 0; x = [0,x'] by A23,A25,TARSKI:def 1; then x' <> 0 by Th3; then x' *' y' <> 0 by A26,ARYTM_1:2; then reconsider IT = [0,y' *' x'] as Element of REAL by Th2; take IT,x',y'; thus x = [0,x'] & y = y' & IT = [0,y' *' x'] by A23,A25,TARSKI:def 1; end; hereby assume x in [:{0},REAL+:]; then consider z1,x' being set such that A27: z1 in{0} and A28: x' in REAL+ and A29: x = [z1,x'] by ZFMISC_1:103; reconsider x' as Element of REAL+ by A28; assume y in [:{0},REAL+:]; then consider z2,y' being set such that A30: z2 in{0} and A31: y' in REAL+ and A32: y = [z2,y'] by ZFMISC_1:103; reconsider y' as Element of REAL+ by A31; x' *' y' in REAL+; then reconsider IT = y' *' x' as Element of REAL by Th1; take IT,x',y'; thus x = [0,x'] & y = [0,y'] & IT = y' *' x' by A27,A29,A30,A32,TARSKI:def 1; end; thus thesis by Th1,ARYTM_2:21; end; uniqueness proof let IT1,IT2 be Element of REAL; thus x in REAL+ & y in REAL+ & (ex x',y' being Element of REAL+ st x = x' & y = y' & IT1 = x' *' y') & (ex x',y' being Element of REAL+ st x = x' & y = y' & IT2 = x' *' y') implies IT1 = IT2; thus x in REAL+ & y in [:{0},REAL+:] & x <> 0 & (ex x',y' being Element of REAL+ st x = x' & y = [0,y'] & IT1 = [0,x' *' y']) & (ex x'',y'' being Element of REAL+ st x = x'' & y = [0,y''] & IT2 = [0,x'' *' y'']) implies IT1 = IT2 by ZFMISC_1:33; thus y in REAL+ & x in [:{0},REAL+:] & y <> 0 & (ex x',y' being Element of REAL+ st x = [0,x'] & y = y' & IT1 = [0,y' *' x']) & (ex x'',y'' being Element of REAL+ st x = [0,x''] & y = y'' & IT2 = [0,y'' *' x'']) implies IT1 = IT2 by ZFMISC_1:33; hereby assume x in [:{0},REAL+:] & y in [:{0},REAL+:]; given x',y' being Element of REAL+ such that A33: x = [0,x'] & y = [0,y'] and A34: IT1 = y' *' x'; given x'',y'' being Element of REAL+ such that A35: x = [0,x''] & y = [0,y''] and A36: IT2 = y'' *' x''; x' = x'' & y' = y'' by A33,A35,ZFMISC_1:33; hence IT1 = IT2 by A34,A36; 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 :Def4: +(x,it) = 0; existence proof reconsider z' = 0 as Element of REAL+ by ARYTM_2:21; A1: x in REAL+ \/ [:{0},REAL+:] & not x in {[0,0]} by NUMBERS:def 1,XBOOLE_0:def 4; per cases by A1,XBOOLE_0:def 2; suppose A2: x = 0; then reconsider x' = x as Element of REAL+ by ARYTM_2:21; take x; x' + x' = 0 by A2,ARYTM_2:def 8; hence thesis by Def2,Th1,ARYTM_2:21; suppose that A3: x in REAL+ and A4: x <> 0; 0 in {0} by TARSKI:def 1; then A5: [0,x] in [:{0},REAL+:] by A3,ZFMISC_1:106; then A6: [0,x] in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 2; [0,x] <> [0,0] by A4,ZFMISC_1:33; then reconsider y = [0,x] as Element of REAL by A6,NUMBERS:def 1,ZFMISC_1:64; take y; reconsider x' = x as Element of REAL+ by A3; A7: x' <=' x'; z' + x' = x' by ARYTM_2:def 8; then z' = x' -' x' by A7,ARYTM_1:def 1; then 0 = x' - x' by A7,ARYTM_1:def 2; hence thesis by A5,Def2,Th1,ARYTM_2:21; suppose A8: x in [:{0},REAL+:]; then consider a,b being set such that A9: a in {0} and A10: b in REAL+ and A11: x = [a,b] by ZFMISC_1:103; reconsider y = b as Element of REAL by A10,Th1; take y; now per cases; case x in REAL+ & y in REAL+; hence ex x',y' being Element of REAL+ st x = x' & y = y' & 0 = x' + y' by A8,Th5,XBOOLE_0:3; case x in REAL+ & y in [:{0},REAL+:]; hence ex x',y' being Element of REAL+ st x = x' & y = [0,y'] & 0 = x' - y' by A10,Th5,XBOOLE_0:3; case y in REAL+ & x in [:{0},REAL+:]; reconsider x' = b, y' = y as Element of REAL+ by A10; take x', y'; thus x = [0,x'] by A9,A11,TARSKI:def 1; thus y = y'; thus 0 = y' - x' by ARYTM_1:18; 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 x',y' being Element of REAL+ st x = [0,x'] & y = [0,y'] & 0 = [0,y'+x'] by A8,A10; end; hence thesis by Def2,Th1,ARYTM_2:21; 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 x',y' being Element of REAL+ st x = x' & y = y' & 0 = x' + y') & ex x',y' being Element of REAL+ st x = x' & z = y' & 0 = x' + y' by A12,A13,Def2; hence y = z by ARYTM_2:12; suppose that A14: x in REAL+ and A15: y in REAL+ and A16: z in [:{0},REAL+:]; consider x',y' being Element of REAL+ such that A17: x = x' and y = y' and A18: 0 = x' + y' by A12,A14,A15,Def2; consider x'',y'' being Element of REAL+ such that A19: x = x'' and A20: z = [0,y''] and A21: 0 = x'' - y'' by A13,A14,A16,Def2; A22: x'' = 0 by A17,A18,A19,ARYTM_2:6; [0,0] in {[0,0]} by TARSKI:def 1; then A23: not [0,0] in REAL by NUMBERS:def 1,XBOOLE_0:def 4; z in REAL; hence y = z by A20,A21,A22,A23,ARYTM_1:19; suppose that A24: x in REAL+ and A25: z in REAL+ and A26: y in [:{0},REAL+:]; consider x',z' being Element of REAL+ such that A27: x = x' and z = z' and A28: 0 = x' + z' by A13,A24,A25,Def2; consider x'',y' being Element of REAL+ such that A29: x = x'' and A30: y = [0,y'] and A31: 0 = x'' - y' by A12,A24,A26,Def2; A32: x'' = 0 by A27,A28,A29,ARYTM_2:6; [0,0] in {[0,0]} by TARSKI:def 1; then A33: not [0,0] in REAL by NUMBERS:def 1,XBOOLE_0:def 4; y in REAL; hence z = y by A30,A31,A32,A33,ARYTM_1:19; suppose that A34: x in REAL+ and A35: y in [:{0},REAL+:] and A36: z in [:{0},REAL+:]; consider x',y' being Element of REAL+ such that A37: x = x' and A38: y = [0,y'] and A39: 0 = x' - y' by A12,A34,A35,Def2; consider x'',z' being Element of REAL+ such that A40: x = x'' and A41: z = [0,z'] and A42: 0 = x'' - z' by A13,A34,A36,Def2; y' = x' by A39,Th6 .= z' by A37,A40,A42,Th6; hence y = z by A38,A41; suppose that A43: z in REAL+ and A44: y in REAL+ and A45: x in [:{0},REAL+:]; consider x',y' being Element of REAL+ such that A46: x = [0,x'] and A47: y = y' and A48: 0 = y' - x' by A12,A44,A45,Def2; consider x'',z' being Element of REAL+ such that A49: x = [0,x''] and A50: z = z' and A51: 0 = z' - x'' by A13,A43,A45,Def2; x' = x'' by A46,A49,ZFMISC_1:33; then z' = x' by A51,Th6 .= y' by A48,Th6; hence y = z by A47,A50; 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 x',y' being Element of REAL+ st x = [0,x'] & y = [0,y'] & 0 = [0,x'+y'] by A12,Def2; hence y = z; 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 x',z' being Element of REAL+ st x = [0,x'] & z = [0,z'] & 0 = [0,x'+z'] by A13,Def2; hence y = z; end; involutiveness; func inv x -> Element of REAL means :Def5: *(x,it) = one if x <> 0 otherwise it = 0; existence proof thus x <> 0 implies ex y st *(x,y) = one proof assume A52: x <> 0; A53: x in REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1,XBOOLE_0:def 4; per cases by A53,XBOOLE_0:def 2; suppose A54: x in REAL+; then reconsider x' = x as Element of REAL+; consider y' being Element of REAL+ such that A55: x' *' y' = one by A52,ARYTM_2:15; y' in REAL+; then reconsider y = y' as Element of REAL by Th1; take y; consider x'',y'' being Element of REAL+ such that A56: x = x'' and A57: y = y'' and A58: *(x,y) = x'' *' y'' by A54,Def3; thus *(x,y) = one by A55,A56,A57,A58; suppose A59: x in [:{0},REAL+:]; then consider x1,x2 being set such that x1 in {0} and A60: x2 in REAL+ and A61: x = [x1,x2] by ZFMISC_1:103; reconsider x2 as Element of REAL+ by A60; not x in {[0,0]} by NUMBERS:def 1,XBOOLE_0:def 4; then A62: x <> [0,0] by TARSKI:def 1; x1 in {0} by A59,A61,ZFMISC_1:106; then x2 <> 0 by A61,A62,TARSKI:def 1; then consider y2 being Element of REAL+ such that A63: x2 *' y2 = one by ARYTM_2:15; A64: [0,y2] in [:{0},REAL+:] by Lm1,ZFMISC_1:106; then A65: [0,y2] in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 2; now assume [0,y2] in {[0,0]}; then [0,y2] = [0,0] by TARSKI:def 1; then y2 = 0 by ZFMISC_1:33; hence contradiction by A63,ARYTM_2:4; end; then reconsider y = [0,y2] as Element of REAL by A65,NUMBERS:def 1,XBOOLE_0:def 4; consider x',y' being Element of REAL+ such that A66: x = [0,x'] and A67: y = [0,y'] and A68: *(x,y) = y' *' x' by A59,A64,Def3; take y; y' = y2 & x' = x2 by A61,A66,A67,ZFMISC_1:33; hence *(x,y) = one by A63,A68; end; thus thesis; end; uniqueness proof let y,z be Element of REAL; thus x <> 0 & *(x,y) = one & *(x,z) = one implies y = z proof assume that A69: x <> 0 and A70: *(x,y) = one and A71: *(x,z) = one; A72: for x,y being Element of REAL st *(x,y) =one holds x <> 0 proof let x,y be Element of REAL such that A73: *(x,y) =one and A74: x = 0; A75: not x in [:{0},REAL+:] by A74,Th5,ARYTM_2:21,XBOOLE_0:3; A76: y in REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1,XBOOLE_0:def 4; per cases by A76,XBOOLE_0:def 2; suppose y in REAL+; then ex x',y' being Element of REAL+ st x = x' & y = y' & one = x' *' y' by A73,A74,Def3,ARYTM_2:21; hence contradiction by A74,ARYTM_2:4; suppose y in [:{0},REAL+:]; then not y in REAL+ by Th5,XBOOLE_0:3; hence contradiction by A73,A74,A75,Def3; end; then A77: y <> 0 by A70; A78: z <> 0 by A71,A72; per cases; suppose x in REAL+ & y in REAL+ & z in REAL+; then (ex x',y' being Element of REAL+ st x = x' & y = y' & one = x' *' y') & ex x',y' being Element of REAL+ st x = x' & z = y' & one = x' *' y' by A70,A71,Def3; hence y = z by A69,Th8; suppose that A79: x in [:{0},REAL+:] and A80: y in [:{0},REAL+:] and A81: z in [:{0},REAL+:]; consider x',y' being Element of REAL+ such that A82: x = [0,x'] and A83: y = [0,y'] and A84: one = y' *' x' by A70,A79,A80,Def3; consider x'',z' being Element of REAL+ such that A85: x = [0,x''] and A86: z = [0,z'] and A87: one = z' *' x'' by A71,A79,A81,Def3; A88: x' = x'' by A82,A85,ZFMISC_1:33; x' <> 0 by A82,Th3; hence y = z by A83,A84,A86,A87,A88,Th8; suppose x in REAL+ & y in [:{0},REAL+:]; then ex x',y' being Element of REAL+ st x = x' & y = [0,y'] & one = [0,x' *' y'] by A69,A70,Def3; hence y = z by Th7; suppose x in [:{0},REAL+:] & y in REAL+; then ex x',y' being Element of REAL+ st x = [0,x'] & y = y' & one = [0,y' *' x'] by A70,A77,Def3; hence y = z by Th7; suppose x in [:{0},REAL+:] & z in REAL+; then ex x',z' being Element of REAL+ st x = [0,x'] & z = z' & one = [0,z' *' x'] by A71,A78,Def3; hence y = z by Th7; suppose x in REAL+ & z in [:{0},REAL+:]; then ex x',z' being Element of REAL+ st x = x' & z = [0,z'] & one = [0,x' *' z'] by A69,A71,Def3; hence y = z by Th7; 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 A70,Def3; 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 A71,Def3; end; thus thesis; end; consistency; involutiveness proof let x,y be Element of REAL; assume that A89: y <> 0 implies *(y,x) = one and A90: y = 0 implies x = 0; thus x <> 0 implies *(x,y) = one by A89,A90; assume A91: x = 0; assume A92: y <> 0; A93: y in REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1,XBOOLE_0:def 4; per cases by A93,XBOOLE_0:def 2; suppose y in REAL+; then ex x',y' being Element of REAL+ st x = x' & y = y' & one = x' *' y' by A89,A91,A92,Def3,ARYTM_2:21; hence contradiction by A91,ARYTM_2:4; suppose y in [:{0},REAL+:]; then not y in REAL+ & not x in [:{0},REAL+:] by A91,Th5,ARYTM_2:21,XBOOLE_0:3; hence contradiction by A89,A91,A92,Def3; end; end; begin :: from COMPLEX1 Lm3: for x,y,z being set st [x,y] = {z} holds z = {x} & x = y proof let x,y,z be set; assume [x,y] = {z}; then {{x,y},{x}} = {z} by TARSKI:def 5; then A1: {x,y} in {z} & {x} in {z} by TARSKI:def 2; hence A2: z = {x} by TARSKI:def 1; {x,y} = z by A1,TARSKI:def 1; hence x = y by A2,ZFMISC_1:9; end; reserve i,j,k for Element of NAT; reserve a,b for Element of REAL; theorem Th10: not (0,one)-->(a,b) in REAL proof set f = (0,one)-->(a,b); A1: f = {[0,a],[one,b]} by FUNCT_4:71; now assume f in {[i,j]: i,j are_relative_prime & j <> {}}; then consider i,j such that A2: f = [i,j] and i,j are_relative_prime and j <> {}; A3: f = {{i,j},{i}} by A2,TARSKI:def 5; then A4: {i} in f by TARSKI:def 2; A5: {i,j} in f by A3,TARSKI:def 2; A6: [0,a] = {{0,a},{0}} by TARSKI:def 5; A7: [one,b] = {{one,b},{one}} by TARSKI:def 5; A8: now assume i = j; then {i} = {i,j} by ENUMSET1:69; then [i,j] = {{i}} by A2,A3,ENUMSET1:69; then [0,a] in {{i}} & [one,b] in {{i}} by A1,A2,TARSKI:def 2; then [0,a] = {i} & [one,b] = {i} by TARSKI:def 1; hence contradiction by ZFMISC_1:33; end; per cases by A1,A4,A5,TARSKI:def 2; suppose {i,j} = [0,a] & {i} = [0,a]; hence contradiction by A8,ZFMISC_1:9; suppose that A9: {i,j} = [0,a] and A10: {i} = [one,b]; A11: i = {one} by A10,Lm3; i in [0,a] by A9,TARSKI:def 2; then i = {0,a} or i = {0} by A6,TARSKI:def 2; then 0 in i by TARSKI:def 1,def 2; hence contradiction by A11,TARSKI:def 1; suppose that A12: {i,j} = [one,b] and A13: {i} = [0,a]; A14: i = {0} by A13,Lm3; i in [one,b] by A12,TARSKI:def 2; then i = {one,b} or i = {one} by A7,TARSKI:def 2; then one in i by TARSKI:def 1,def 2; hence contradiction by A14,TARSKI:def 1; suppose {i,j} = [one,b] & {i} = [one,b]; hence contradiction by A8,ZFMISC_1:9; end; then A15: not f in {[i,j]: i,j are_relative_prime & j <> {}} \ {[k,one]: not contradiction} by XBOOLE_0:def 4; now assume f in omega; then f is ordinal by ORDINAL1:23; then {} in f by A1,ORDINAL3:10; hence contradiction by A1,TARSKI:def 2; end; then A16: not f in RAT+ by A15,ARYTM_3:def 6,XBOOLE_0:def 2; 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}; not ex x,y being set st {[0,x],[one,y]} in IR proof given x,y being set such that A17: {[0,x],[one,y]} in IR; consider A being Subset of RAT+ such that A18: {[0,x],[one,y]} = A and A19: 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 A17; A20: [0,x] in A by A18,TARSKI:def 2; for r,s being Element of RAT+ st r in A & s <=' r holds s in A by A19; then consider r1,r2,r3 being Element of RAT+ such that A21: r1 in A & r2 in A & r3 in A and A22: r1 <> r2 & r2 <> r3 & r3 <> r1 by A20,ARYTM_3:82; (r1 = [0,x] or r1 = [one,y]) & (r2 = [0,x] or r2 = [one,y]) & (r3 = [0,x] or r3 = [one,y]) by A18,A21,TARSKI:def 2; hence contradiction by A22; end; then not f in IR by A1; then not f in DEDEKIND_CUTS by ARYTM_2:def 1,XBOOLE_0:def 4; then not f in RAT+ \/ DEDEKIND_CUTS by A16,XBOOLE_0:def 2; then A23: not f in REAL+ by ARYTM_2:def 2,XBOOLE_0:def 4; now assume f in [:{{}},REAL+:]; then consider x,y being set such that A24: x in {{}} and y in REAL+ and A25: f = [x,y] by ZFMISC_1:103; x = 0 by A24,TARSKI:def 1; then A26: f = {{0,y},{0}} by A25,TARSKI:def 5; f = {[0,a],[one,b]} by FUNCT_4:71; then [one,b] in f by TARSKI:def 2; then A27: [one,b] = {0} or [one,b] = {0,y} by A26,TARSKI:def 2; per cases by A27,TARSKI:def 5; suppose {{one,b},{one}} = {0}; then 0 in {{one,b},{one}} by TARSKI:def 1; hence contradiction by TARSKI:def 2; suppose {{one,b},{one}} = {0,y}; then 0 in {{one,b},{one}} by TARSKI:def 2; hence contradiction by TARSKI:def 2; end; then not f in REAL+ \/ [:{{}},REAL+:] by A23,XBOOLE_0:def 2; hence thesis by NUMBERS:def 1,XBOOLE_0:def 4; end; definition let x,y be Element of REAL; canceled; func [*x,y*] -> Element of COMPLEX equals :Def7: x if y = 0 otherwise (0,one) --> (x,y); consistency; coherence proof thus y = 0 implies x is Element of COMPLEX by NUMBERS:def 2,XBOOLE_0:def 2; set z = (0,one)-->(x,y); assume A1: y <> 0; A2: z in Funcs({0,one},REAL) by FUNCT_2:11; now assume z in { r where r is Element of Funcs({0,one},REAL): r.one = 0 } ; then ex r being Element of Funcs({0,one},REAL) st z = r & r.one = 0; hence contradiction by A1,FUNCT_4:66; end; then z in Funcs({0,one},REAL) \ { r where r is Element of Funcs({0,one},REAL): r.one = 0} by A2,XBOOLE_0:def 4; hence thesis by NUMBERS:def 2,XBOOLE_0:def 2; 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 Th1,ARYTM_2:21; take r,z; thus c = [*r,z*] by Def7; suppose not c in REAL; then A1: c in Funcs({0,one},REAL) \ { x where x is Element of Funcs({0,one},REAL): x.one = 0} by NUMBERS:def 2,XBOOLE_0:def 2; then A2: c in Funcs({0,one},REAL) by XBOOLE_0:def 4; then consider f being Function such that A3: c = f and A4: dom f = {0,one} and A5: rng f c= REAL by FUNCT_2:def 2; 0 in {0,one} & one in {0,one} by TARSKI:def 2; then f.0 in rng f & f.one in rng f by A4,FUNCT_1:12; then reconsider r = f.0, s = f.one as Element of REAL by A5; A6: c = (0,one)-->(r,s) by A3,A4,FUNCT_4:69; take r,s; now assume s = 0; then (0,one)-->(r,s).one = 0 by FUNCT_4:66; then c in { x where x is Element of Funcs({0,one},REAL): x.one = 0} by A2,A6; hence contradiction by A1,XBOOLE_0:def 4; end; hence c = [*r,s*] by A6,Def7; 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 Def7; A4: now assume y2 <> 0; then x1 = (0,one) --> (y1,y2) by A1,A3,Def7; hence contradiction by Th10; end; hence x1 = y1 by A1,A3,Def7; thus x2 = y2 by A2,A4; suppose x2 <> 0; then A5: [*y1,y2*] = (0,one) --> (x1,x2) by A1,Def7; now assume y2 = 0; then [*y1,y2*] = y1 by Def7; hence contradiction by A5,Th10; end; then [*y1,y2*] = (0,one) --> (y1,y2) by Def7; hence x1 = y1 & x2 = y2 by A5,FUNCT_4:72; end; set RR = [:{0},REAL+:] \ {[0,0]}; reconsider o = 0 as Element of REAL by Th1,ARYTM_2:21; theorem Th13: for x,o being Element of REAL st o = 0 holds +(x,o) = x proof let x,o being Element of REAL such that A1: o = 0; reconsider y' = 0 as Element of REAL+ by ARYTM_2:21; per cases; suppose x in REAL+; then reconsider x' = x as Element of REAL+; x' = x' + y' by ARYTM_2:def 8; hence +(x,o) = x by A1,Def2; suppose A2: not x in REAL+; x in REAL+ \/ [:{{}},REAL+:] by NUMBERS:def 1,XBOOLE_0:def 4; then A3: x in [:{{}},REAL+:] by A2,XBOOLE_0:def 2; then consider x1,x2 being set such that A4: x1 in {{}} and A5: x2 in REAL+ and A6: x = [x1,x2] by ZFMISC_1:103; reconsider x' = x2 as Element of REAL+ by A5; A7: x1 = 0 by A4,TARSKI:def 1; then x' <> 0 by A6,Th3; then x = y' - x' by A6,A7,ARYTM_1:19; hence thesis by A1,A3,A6,A7,Def2; end; theorem Th14: 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 x' = x, y' = 0 as Element of REAL+ by ARYTM_2:21; 0 = x' *' y' by ARYTM_2:4; hence *(x,o) = 0 by A1,Def3; suppose A2: not x in REAL+; not o in [:{{}},REAL+:] by A1,Th5,ARYTM_2:21,XBOOLE_0:3; hence thesis by A1,A2,Def3; end; theorem Th15: for x,y,z being Element of REAL holds *(x,*(y,z)) = *(*(x,y),z) proof let x,y,z be Element of REAL; per cases; suppose that A1: x in REAL+ and A2: y in REAL+ and A3: z in REAL+; consider y',z' being Element of REAL+ such that A4: y = y' and A5: z = z' and A6: *(y,z) = y' *' z' by A2,A3,Def3; consider x',yz' being Element of REAL+ such that A7: x = x' and A8: *(y,z) = yz' and A9: *(x,*(y,z)) = x' *' yz' by A1,A6,Def3; consider x'',y'' being Element of REAL+ such that A10: x = x'' and A11: y = y'' and A12: *(x,y) = x'' *' y'' by A1,A2,Def3; consider xy'',z'' being Element of REAL+ such that A13: *(x,y) = xy'' and A14: z = z'' and A15: *(*(x,y),z) = xy'' *' z'' by A3,A12,Def3; thus *(x,*(y,z)) = *(*(x,y),z) by A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,A15, ARYTM_2:13; suppose that A16: x in REAL+ & x <> 0 and A17: y in RR and A18: z in REAL+ & z <> 0; A19: y in [:{0},REAL+:] by A17,XBOOLE_0:def 4; then consider y',z' being Element of REAL+ such that A20: y = [0,y'] and A21: z = z' and A22: *(y,z) = [0,z' *' y'] by A18,Def3; *(y,z) in [:{0},REAL+:] by A22,Lm1,ZFMISC_1:106; then consider x',yz' being Element of REAL+ such that A23: x = x' and A24: *(y,z) = [0,yz'] and A25: *(x,*(y,z) ) = [0,x' *' yz'] by A16,Def3; consider x'',y'' being Element of REAL+ such that A26: x = x'' and A27: y = [0,y''] and A28: *(x,y) = [0,x'' *' y''] by A16,A19,Def3; *(x,y) in [:{0},REAL+:] by A28,Lm1,ZFMISC_1:106; then consider xy'',z'' being Element of REAL+ such that A29: *(x,y) = [0,xy''] and A30: z = z'' and A31: *(*(x,y),z) = [0,z'' *' xy''] by A18,Def3; A32: y' = y'' by A20,A27,ZFMISC_1:33; thus *(x,*(y,z)) = [0,x' *' (y' *' z')] by A22,A24,A25,ZFMISC_1:33 .= [0,(x'' *' y'') *' z''] by A21,A23,A26,A30,A32,ARYTM_2:13 .= *(*(x,y),z) by A28,A29,A31,ZFMISC_1:33; suppose that A33: x in RR and A34: y in REAL+ & y <> 0 and A35: z in REAL+ & z <> 0; A36: x in [:{0},REAL+:] by A33,XBOOLE_0:def 4; consider y',z' being Element of REAL+ such that A37: y = y' and A38: z = z' and A39: *(y,z) = y' *' z' by A34,A35,Def3; y' *' z' <> 0 by A34,A35,A37,A38,ARYTM_1:2; then consider x',yz' being Element of REAL+ such that A40: x = [0,x'] and A41: *(y,z) = yz' and A42: *(x,*(y,z)) = [0,yz' *' x'] by A36,A39,Def3; consider x'',y'' being Element of REAL+ such that A43: x = [0,x''] and A44: y = y'' and A45: *(x,y) = [0,y'' *' x''] by A34,A36,Def3; *(x,y) in [:{0},REAL+:] by A45,Lm1,ZFMISC_1:106; then consider xy'',z'' being Element of REAL+ such that A46: *(x,y) = [0,xy''] and A47: z = z'' and A48: *(*(x,y),z) = [0,z'' *' xy''] by A35,Def3; x' = x'' by A40,A43,ZFMISC_1:33; hence *(x,*(y,z)) = [0,(x'' *' y'') *' z''] by A37,A38,A39,A41,A42,A44,A47, ARYTM_2:13 .= *(*(x,y),z) by A45,A46,A48,ZFMISC_1:33; suppose that A49: x in RR and A50: y in RR and A51: z in REAL+ & z <> 0; A52: x in [:{0},REAL+:] by A49,XBOOLE_0:def 4; A53: y in [:{0},REAL+:] by A50,XBOOLE_0:def 4; then consider y',z' being Element of REAL+ such that A54: y = [0,y'] and A55: z = z' and A56: *(y,z) = [0,z' *' y'] by A51,Def3; *(y,z) in [:{0},REAL+:] by A56,Lm1,ZFMISC_1:106; then consider x',yz' being Element of REAL+ such that A57: x = [0,x'] and A58: *(y,z) = [0,yz'] and A59: *(x,*(y,z)) = yz' *' x' by A52,Def3; consider x'',y'' being Element of REAL+ such that A60: x = [0,x''] and A61: y = [0,y''] and A62: *(x,y) = y'' *' x'' by A52,A53,Def3; consider xy'',z'' being Element of REAL+ such that A63: *(x,y) = xy'' and A64: z = z'' and A65: *(*(x,y),z) = xy'' *' z'' by A51,A62,Def3; A66: x' = x'' by A57,A60,ZFMISC_1:33; A67: y' = y'' by A54,A61,ZFMISC_1:33; thus *(x,*(y,z)) = x' *' (y' *' z') by A56,A58,A59,ZFMISC_1:33 .= *(*(x,y),z) by A55,A62,A63,A64,A65,A66,A67,ARYTM_2:13; suppose that A68: x in REAL+ & x <> 0 and A69: y in REAL+ & y <> 0 and A70: z in RR; A71: z in [:{0},REAL+:] by A70,XBOOLE_0:def 4; then consider y',z' being Element of REAL+ such that A72: y = y' and A73: z = [0,z'] and A74: *(y,z) = [0,y' *' z'] by A69,Def3; *(y,z) in [:{0},REAL+:] by A74,Lm1,ZFMISC_1:106; then consider x',yz' being Element of REAL+ such that A75: x = x' and A76: *(y,z) = [0,yz'] and A77: *(x,*(y,z)) = [0,x' *' yz'] by A68,Def3; consider x'',y'' being Element of REAL+ such that A78: x = x'' and A79: y = y'' and A80: *(x,y) = x'' *' y'' by A68,A69,Def3; *(x,y) <> 0 by A68,A69,A78,A79,A80,ARYTM_1:2; then consider xy'',z'' being Element of REAL+ such that A81: *(x,y) = xy'' and A82: z = [0,z''] and A83: *(*(x,y),z) = [0,xy'' *' z''] by A71,A80,Def3; A84: z' = z'' by A73,A82,ZFMISC_1:33; thus *(x,*(y,z)) = [0,x' *' (y' *' z')] by A74,A76,A77,ZFMISC_1:33 .= *(*(x,y),z) by A72,A75,A78,A79,A80,A81,A83,A84,ARYTM_2:13; suppose that A85: x in REAL+ & x <> 0 and A86: y in RR and A87: z in RR; A88: y in [:{0},REAL+:] by A86,XBOOLE_0:def 4; A89: z in [:{0},REAL+:] by A87,XBOOLE_0:def 4; then consider y',z' being Element of REAL+ such that A90: y = [0,y'] and A91: z = [0,z'] and A92: *(y,z) = z' *' y' by A88,Def3; consider x',yz' being Element of REAL+ such that A93: x = x' and A94: *(y,z) = yz' and A95: *(x,*(y,z)) = x' *' yz' by A85,A92,Def3; consider x'',y'' being Element of REAL+ such that A96: x = x'' and A97: y = [0,y''] and A98: *(x,y) = [0,x'' *' y''] by A85,A88,Def3; *(x,y) in [:{0},REAL+:] by A98,Lm1,ZFMISC_1:106; then consider xy'',z'' being Element of REAL+ such that A99: *(x,y) = [0,xy''] and A100: z = [0,z''] and A101: *(*(x,y),z) = z'' *' xy'' by A89,Def3; A102: y' = y'' by A90,A97,ZFMISC_1:33; z' = z'' by A91,A100,ZFMISC_1:33; hence *(x,*(y,z)) = (x'' *' y'') *' z'' by A92,A93,A94,A95,A96,A102,ARYTM_2:13 .= *(*(x,y),z) by A98,A99,A101,ZFMISC_1:33; suppose that A103: y in REAL+ & y <> 0 and A104: x in RR and A105: z in RR; A106: x in [:{0},REAL+:] by A104,XBOOLE_0:def 4; A107: z in [:{0},REAL+:] by A105,XBOOLE_0:def 4; then consider y',z' being Element of REAL+ such that A108: y = y' and A109: z = [0,z'] and A110: *(y,z) = [0,y' *' z'] by A103,Def3; [0,y' *' z'] in [:{0},REAL+:] by Lm1,ZFMISC_1:106; then consider x',yz' being Element of REAL+ such that A111: x = [0,x'] and A112: *(y,z) = [0,yz'] and A113: *(x,*(y,z)) = yz' *' x' by A106,A110,Def3; consider x'',y'' being Element of REAL+ such that A114: x = [0,x''] and A115: y = y'' and A116: *(x,y) = [0,y'' *' x''] by A103,A106,Def3; *(x,y) in [:{0},REAL+:] by A116,Lm1,ZFMISC_1:106; then consider xy'',z'' being Element of REAL+ such that A117: *(x,y) = [0,xy''] and A118: z = [0,z''] and A119: *(*(x,y),z) = z'' *' xy'' by A107,Def3; A120: x' = x'' by A111,A114,ZFMISC_1:33; A121: z' = z'' by A109,A118,ZFMISC_1:33; thus *(x,*(y,z)) = x' *' (y' *' z') by A110,A112,A113,ZFMISC_1:33 .= (x'' *' y'') *' z'' by A108,A115,A120,A121,ARYTM_2:13 .= *(*(x,y),z) by A116,A117,A119,ZFMISC_1:33; suppose that A122: x in RR and A123: y in RR and A124: z in RR; A125: x in [:{0},REAL+:] by A122,XBOOLE_0:def 4; A126: y in [:{0},REAL+:] by A123,XBOOLE_0:def 4; A127: z in [:{0},REAL+:] by A124,XBOOLE_0:def 4; then consider y',z' being Element of REAL+ such that A128: y = [0,y'] and A129: z = [0,z'] and A130: *(y,z) = z' *' y' by A126,Def3; not z in {[0,0]} & not y in {[0,0]} by A123,A124,XBOOLE_0:def 4; then z' <> 0 & y' <> 0 by A128,A129,TARSKI:def 1; then *(z,y) <> 0 by A130,ARYTM_1:2; then consider x',yz' being Element of REAL+ such that A131: x = [0,x'] and A132: *(y,z) = yz' and A133: *(x,*(y,z)) = [0,yz' *' x'] by A125,A130,Def3; consider x'',y'' being Element of REAL+ such that A134: x = [0,x''] and A135: y = [0,y''] and A136: *(x,y) = y'' *' x'' by A125,A126,Def3; A137: x' = x'' by A131,A134,ZFMISC_1:33; A138: y' = y'' by A128,A135,ZFMISC_1:33; not x in {[0,0]} & not y in {[0,0]} by A122,A123,XBOOLE_0:def 4; then x' <> 0 & y' <> 0 by A128,A131,TARSKI:def 1; then *(x,y) <> 0 by A136,A137,A138,ARYTM_1:2; then consider xy'',z'' being Element of REAL+ such that A139: *(x,y) = xy'' and A140: z = [0,z''] and A141: *(*(x,y),z) = [0,xy'' *' z''] by A127,A136,Def3; z' = z'' by A129,A140,ZFMISC_1:33; hence *(x,*(y,z)) = *(*(x,y),z) by A130,A132,A133,A136,A137,A138,A139,A141, ARYTM_2:13; suppose A142: x = 0; hence *(x,*(y,z)) = 0 by Th14 .= *(o,z) by Th14 .= *(*(x,y),z) by A142,Th14; suppose A143: y = 0; hence *(x,*(y,z)) = *(x,o) by Th14 .= 0 by Th14 .= *(o,z) by Th14 .= *(*(x,y),z) by A143,Th14; suppose A144: z = 0; hence *(x,*(y,z)) = *(x,o) by Th14 .= 0 by Th14 .= *(*(x,y),z) by A144,Th14; suppose A145: 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); A146: not [0,0] in REAL+ by ARYTM_2:3; REAL = (REAL+ \ {[{},{}]}) \/ ([:{{}},REAL+:] \ {[{},{}]}) by NUMBERS:def 1,XBOOLE_1:42 .= REAL+ \/ RR by A146,ZFMISC_1:65; hence thesis by A145,XBOOLE_0:def 2; end; theorem Th16: 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; per cases; suppose A1: x = 0; hence *(x,+(y,z)) = 0 by Th14 .= +(o,o) by Th13 .= +(*(x,y),o) by A1,Th14 .= +(*(x,y),*(x,z)) by A1,Th14; suppose that A2: x in REAL+ and A3: y in REAL+ and A4: z in REAL+; consider x',y' being Element of REAL+ such that A5: x = x' and A6: y = y' and A7: *(x,y) = x' *' y' by A2,A3,Def3; consider x'',z' being Element of REAL+ such that A8: x = x'' and A9: z = z' and A10: *(x,z) = x'' *' z' by A2,A4,Def3; consider xy',xz' being Element of REAL+ such that A11: *(x,y) = xy' and A12: *(x,z) = xz' and A13: +(*(x,y),*(x,z)) = xy' + xz' by A7,A10,Def2; consider y'',z'' being Element of REAL+ such that A14: y = y'' and A15: z = z'' and A16: +(y,z) = y'' + z'' by A3,A4,Def2; consider x''',yz' being Element of REAL+ such that A17: x = x''' and A18: +(y,z) = yz' and A19: *(x,+(y,z)) = x''' *' yz' by A2,A16,Def3; thus *(x,+(y,z)) = +(*(x,y),*(x,z)) by A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,A15, A16,A17,A18,A19,ARYTM_2:14; suppose that A20: x in REAL+ & x <> 0 and A21: y in REAL+ and A22: z in RR; A23: z in [:{0},REAL+:] by A22,XBOOLE_0:def 4; consider x',y' being Element of REAL+ such that A24: x = x' and A25: y = y' and A26: *(x,y) = x' *' y' by A20,A21,Def3; consider x'',z' being Element of REAL+ such that A27: x = x'' and A28: z = [0,z'] and A29: *(x,z) = [0,x'' *' z'] by A20,A23,Def3; consider y'',z'' being Element of REAL+ such that A30: y = y'' and A31: z = [0,z''] and A32: +(y,z) = y'' - z'' by A21,A23,Def2; A33: z' = z'' by A28,A31,ZFMISC_1:33; *(x,z) in [:{0},REAL+:] by A29,Lm1,ZFMISC_1:106; then consider xy',xz' being Element of REAL+ such that A34: *(x,y) = xy' and A35: *(x,z) = [0,xz'] and A36: +(*(x,y),*(x,z)) = xy' - xz' by A26,Def2; now per cases; suppose A37: z'' <=' y''; then A38: +(y,z) = y'' -' z'' by A32,ARYTM_1:def 2; then consider x''',yz' being Element of REAL+ such that A39: x = x''' and A40: +(y,z) = yz' and A41: *(x,+(y,z)) = x''' *' yz' by A20,Def3; thus *(x,+(y,z)) = (x' *' y') - (x'' *' z') by A24,A25,A27,A30,A33,A37,A38, A39,A40,A41,ARYTM_1:26 .= +(*(x,y),*(x,z)) by A26,A29,A34,A35,A36,ZFMISC_1:33; suppose A42: not z'' <=' y''; then A43: +(y,z) = [0,z'' -' y''] by A32,ARYTM_1:def 2; then +(y,z) in [:{0},REAL+:] by Lm1,ZFMISC_1:106; then consider x''',yz' being Element of REAL+ such that A44: x = x''' and A45: +(y,z) = [0,yz'] and A46: *(x,+(y,z)) = [0,x''' *' yz'] by A20,Def3; thus *(x,+(y,z)) = [0,x''' *' (z'' -' y'')] by A43,A45,A46,ZFMISC_1:33 .= (x' *' y') - (x'' *' z') by A20,A24,A25,A27,A30,A33,A42,A44,ARYTM_1:27 .= +(*(x,y),*(x,z)) by A26,A29,A34,A35,A36,ZFMISC_1:33; end; hence thesis; suppose that A47: x in REAL+ & x <> 0 and A48: z in REAL+ and A49: y in RR; A50: y in [:{0},REAL+:] by A49,XBOOLE_0:def 4; consider x',z' being Element of REAL+ such that A51: x = x' and A52: z = z' and A53: *(x,z) = x' *' z' by A47,A48,Def3; consider x'',y' being Element of REAL+ such that A54: x = x'' and A55: y = [0,y'] and A56: *(x,y) = [0,x'' *' y'] by A47,A50,Def3; consider z'',y'' being Element of REAL+ such that A57: z = z'' and A58: y = [0,y''] and A59: +(z,y) = z'' - y'' by A48,A50,Def2; A60: y' = y'' by A55,A58,ZFMISC_1:33; *(x,y) in [:{0},REAL+:] by A56,Lm1,ZFMISC_1:106; then consider xz',xy' being Element of REAL+ such that A61: *(x,z) = xz' and A62: *(x,y) = [0,xy'] and A63: +(*(x,z),*(x,y)) = xz' - xy' by A53,Def2; now per cases; suppose A64: y'' <=' z''; then A65: +(z,y) = z'' -' y'' by A59,ARYTM_1:def 2; then consider x''',zy' being Element of REAL+ such that A66: x = x''' and A67: +(z,y) = zy' and A68: *(x,+(z,y)) = x''' *' zy' by A47,Def3; thus *(x,+(z,y)) = (x' *' z') - (x'' *' y') by A51,A52,A54,A57,A60,A64,A65, A66,A67,A68,ARYTM_1:26 .= +(*(x,z),*(x,y)) by A53,A56,A61,A62,A63,ZFMISC_1:33; suppose A69: not y'' <=' z''; then A70: +(z,y) = [0,y'' -' z''] by A59,ARYTM_1:def 2; then +(z,y) in [:{0},REAL+:] by Lm1,ZFMISC_1:106; then consider x''',zy' being Element of REAL+ such that A71: x = x''' and A72: +(z,y) = [0,zy'] and A73: *(x,+(z,y)) = [0,x''' *' zy'] by A47,Def3; thus *(x,+(z,y)) = [0,x''' *' (y'' -' z'')] by A70,A72,A73,ZFMISC_1:33 .= (x' *' z') - (x'' *' y') by A47,A51,A52,A54,A57,A60,A69,A71,ARYTM_1:27 .= +(*(x,z),*(x,y)) by A53,A56,A61,A62,A63,ZFMISC_1:33; end; hence thesis; suppose that A74: x in REAL+ & x <> 0 and A75: y in RR and A76: z in RR; A77: y in [:{0},REAL+:] by A75,XBOOLE_0:def 4; A78: z in [:{0},REAL+:] by A76,XBOOLE_0:def 4; consider x',y' being Element of REAL+ such that A79: x = x' and A80: y = [0,y'] and A81: *(x,y) = [0,x' *' y'] by A74,A77,Def3; consider x'',z' being Element of REAL+ such that A82: x = x'' and A83: z = [0,z'] and A84: *(x,z) = [0,x'' *' z'] by A74,A78,Def3; *(x,y) in [:{0},REAL+:] & *(x,z) in [:{0},REAL+:] by A81,A84,Lm1,ZFMISC_1:106; then not(*(x,y) in REAL+ & *(x,z) in REAL+) & not(*(x,y) in REAL+ & *(x,z) in [:{0},REAL+:]) & not(*(x,y) in [:{0},REAL+:] & *(x,z) in REAL+) by Th5,XBOOLE_0:3; then consider xy',xz' being Element of REAL+ such that A85: *(x,y) = [0,xy'] and A86: *(x,z) = [0,xz'] and A87: +(*(x,y),*(x,z)) = [0,xy' + xz'] by Def2; not(y in REAL+ & z in REAL+) & not(y in REAL+ & z in [:{0},REAL+:]) & not(y in [:{0},REAL+:] & z in REAL+) by A77,A78,Th5,XBOOLE_0:3; then consider y'',z'' being Element of REAL+ such that A88: y = [0,y''] and A89: z = [0,z''] and A90: +(y,z) = [0,y'' + z''] by Def2; +(y,z) in [:{0},REAL+:] by A90,Lm1,ZFMISC_1:106; then consider x''',yz' being Element of REAL+ such that A91: x = x''' and A92: +(y,z) = [0,yz'] and A93: *(x,+(y,z)) = [0,x''' *' yz'] by A74,Def3; A94: xy' = x' *' y' by A81,A85,ZFMISC_1:33; A95: y' = y'' by A80,A88,ZFMISC_1:33; A96: z' = z'' by A83,A89,ZFMISC_1:33; thus *(x,+(y,z)) = [0,x''' *' (y'' + z'')] by A90,A92,A93,ZFMISC_1:33 .= [0,(x' *' y') + (x' *' z')] by A79,A91,A95,A96,ARYTM_2:14 .= +(*(x,y),*(x,z)) by A79,A82,A84,A86,A87,A94,ZFMISC_1:33; suppose that A97: x in RR and A98: y in REAL+ and A99: z in REAL+; A100: x in [:{0},REAL+:] by A97,XBOOLE_0:def 4; consider y'',z'' being Element of REAL+ such that A101: y = y'' and A102: z = z'' and A103: +(y,z) = y'' + z'' by A98,A99,Def2; now per cases; suppose that A104: y <> 0 and A105: z <> 0; consider x',y' being Element of REAL+ such that A106: x = [0,x'] and A107: y = y' and A108: *(x,y) = [0,y' *' x'] by A98,A100,A104,Def3; consider x'',z' being Element of REAL+ such that A109: x = [0,x''] and A110: z = z' and A111: *(x,z) = [0,z' *' x''] by A99,A100,A105,Def3; *(x,y) in [:{0},REAL+:] & *(x,z) in [:{0},REAL+:] by A108,A111,Lm1,ZFMISC_1:106; then not(*(x,y) in REAL+ & *(x,z) in REAL+) & not(*(x,y) in REAL+ & *(x,z) in [:{0},REAL+:]) & not(*(x,y) in [:{0},REAL+:] & *(x,z) in REAL+) by Th5,XBOOLE_0:3; then consider xy',xz' being Element of REAL+ such that A112: *(x,y) = [0,xy'] and A113: *(x,z) = [0,xz'] and A114: +(*(x,y),*(x,z)) = [0,xy' + xz'] by Def2; y'' + z'' <> 0 by A102,A105,ARYTM_2:6; then consider x''',yz' being Element of REAL+ such that A115: x = [0,x'''] and A116: +(y,z) = yz' and A117: *(x,+(y,z)) = [0,yz' *' x'''] by A100,A103,Def3; A118: xy' = x' *' y' by A108,A112,ZFMISC_1:33; A119: x' = x'' by A106,A109,ZFMISC_1:33; x'' = x''' by A109,A115,ZFMISC_1:33; hence *(x,+(y,z)) = [0,(x' *' y') + (x'' *' z')] by A101,A102,A103,A107,A110, A116,A117,A119,ARYTM_2:14 .= +(*(x,y),*(x,z)) by A111,A113,A114,A118,ZFMISC_1:33; suppose A120: x = 0; hence *(x,+(y,z)) = 0 by Th14 .= +(o,o) by Th13 .= +(*(x,y),o) by A120,Th14 .= +(*(x,y),*(x,z)) by A120,Th14; suppose A121: z = 0; hence *(x,+(y,z)) = *(x,y) by Th13 .= +(*(x,y),o) by Th13 .= +(*(x,y),*(x,z)) by A121,Th14; suppose A122: y = 0; hence *(x,+(y,z)) = *(x,z) by Th13 .= +(o,*(x,z)) by Th13 .= +(*(x,y),*(x,z)) by A122,Th14; end; hence thesis; suppose that A123: x in RR and A124: y in REAL+ and A125: z in RR; A126: x in [:{0},REAL+:] by A123,XBOOLE_0:def 4; A127: z in [:{0},REAL+:] by A125,XBOOLE_0:def 4; then consider x'',z' being Element of REAL+ such that A128: x = [0,x''] and A129: z = [0,z'] and A130: *(x,z) = z' *' x'' by A126,Def3; now per cases; suppose y <> 0; then consider x',y' being Element of REAL+ such that A131: x = [0,x'] and A132: y = y' and A133: *(x,y) = [0,y' *' x'] by A124,A126,Def3; consider y'',z'' being Element of REAL+ such that A134: y = y'' and A135: z = [0,z''] and A136: +(y,z) = y'' - z'' by A127,A132,Def2; *(x,y) in [:{0},REAL+:] by A133,Lm1,ZFMISC_1:106; then consider xy',xz' being Element of REAL+ such that A137: *(x,y) = [0,xy'] and A138: *(x,z) = xz' and A139: +(*(x,y),*(x,z)) = xz' - xy' by A130,Def2; A140: z' = z'' by A129,A135,ZFMISC_1:33; now per cases; suppose A141: z'' <=' y''; then A142: +(y,z) = y'' -' z'' by A136,ARYTM_1:def 2; now per cases; suppose A143: +(y,z) <> 0; then consider x''',yz' being Element of REAL+ such that A144: x = [0,x'''] and A145: +(y,z) = yz' and A146: *(x,+(y,z)) = [0,yz' *' x'''] by A126,A142,Def3; A147: x' = x'' by A128,A131,ZFMISC_1:33; A148: x'' = x''' by A128,A144,ZFMISC_1:33; A149: z' = z'' by A129,A135,ZFMISC_1:33; not x in {[0,0]} by NUMBERS:def 1,XBOOLE_0:def 4; then x''' <> 0 by A144,TARSKI:def 1; hence *(x,+(y,z)) = (x' *' z') - (x' *' y') by A132,A134,A141,A142,A143,A145, A146,A147,A148,A149,ARYTM_1:28 .= +(*(x,y),*(x,z)) by A130,A133,A137,A138,A139,A147,ZFMISC_1:33; suppose A150: +(y,z) = 0; then A151: y'' = z'' by A141,A142,ARYTM_1:10; A152: xy' = x' *' y' by A133,A137,ZFMISC_1:33; A153: x' = x'' by A128,A131,ZFMISC_1:33; thus *(x,+(y,z)) = 0 by A150,Th14 .= +(*(x,y),*(x,z)) by A130,A132,A134,A138,A139,A140,A151,A152,A153, ARYTM_1:18; end; hence thesis; suppose A154: not z'' <=' y''; then A155: +(y,z) = [0,z'' -' y''] by A136,ARYTM_1:def 2; then +(y,z) in [:{0},REAL+:] by Lm1,ZFMISC_1:106; then consider x''',yz' being Element of REAL+ such that A156: x = [0,x'''] and A157: +(y,z) = [0,yz'] and A158: *(x,+(y,z)) = yz' *' x''' by A126,Def3; A159: x' = x'' by A128,A131,ZFMISC_1:33; A160: x'' = x''' by A128,A156,ZFMISC_1:33; thus *(x,+(y,z)) = x''' *' (z'' -' y'') by A155,A157,A158,ZFMISC_1:33 .= (x'' *' z') - (x' *' y') by A132,A134,A140,A154,A159,A160,ARYTM_1:26 .= +(*(x,y),*(x,z)) by A130,A133,A137,A138,A139,ZFMISC_1:33; end; hence thesis; suppose A161: y = 0; hence *(x,+(y,z)) = *(x,z) by Th13 .= +(o,*(x,z)) by Th13 .= +(*(x,y),*(x,z)) by A161,Th14; end; hence thesis; suppose that A162: x in RR and A163: z in REAL+ and A164: y in RR; A165: x in [:{0},REAL+:] by A162,XBOOLE_0:def 4; A166: y in [:{0},REAL+:] by A164,XBOOLE_0:def 4; then consider x'',y' being Element of REAL+ such that A167: x = [0,x''] and A168: y = [0,y'] and A169: *(x,y) = y' *' x'' by A165,Def3; now per cases; suppose z <> 0; then consider x',z' being Element of REAL+ such that A170: x = [0,x'] and A171: z = z' and A172: *(x,z) = [0,z' *' x'] by A163,A165,Def3; consider z'',y'' being Element of REAL+ such that A173: z = z'' and A174: y = [0,y''] and A175: +(z,y) = z'' - y'' by A166,A171,Def2; *(x,z) in [:{0},REAL+:] by A172,Lm1,ZFMISC_1:106; then consider xz',xy' being Element of REAL+ such that A176: *(x,z) = [0,xz'] and A177: *(x,y) = xy' and A178: +(*(x,z),*(x,y)) = xy' - xz' by A169,Def2; A179: y' = y'' by A168,A174,ZFMISC_1:33; now per cases; suppose A180: y'' <=' z''; then A181: +(z,y) = z'' -' y'' by A175,ARYTM_1:def 2; now per cases; suppose A182: +(z,y) <> 0; then consider x''',zy' being Element of REAL+ such that A183: x = [0,x'''] and A184: +(z,y) = zy' and A185: *(x,+(z,y)) = [0,zy' *' x'''] by A165,A181,Def3; A186: x' = x'' by A167,A170,ZFMISC_1:33; A187: x'' = x''' by A167,A183,ZFMISC_1:33; A188: y' = y'' by A168,A174,ZFMISC_1:33; not x in {[0,0]} by NUMBERS:def 1,XBOOLE_0:def 4; then x''' <> 0 by A183,TARSKI:def 1; hence *(x,+(z,y)) = (x' *' y') - (x' *' z') by A171,A173,A180,A181,A182,A184, A185,A186,A187,A188,ARYTM_1:28 .= +(*(x,z),*(x,y)) by A169,A172,A176,A177,A178,A186,ZFMISC_1:33; suppose A189: +(z,y) = 0; then A190: z'' = y'' by A180,A181,ARYTM_1:10; A191: xz' = x' *' z' by A172,A176,ZFMISC_1:33; A192: x' = x'' by A167,A170,ZFMISC_1:33; thus *(x,+(z,y)) = 0 by A189,Th14 .= +(*(x,z),*(x,y)) by A169,A171,A173,A177,A178,A179,A190,A191,A192,ARYTM_1 :18; end; hence thesis; suppose A193: not y'' <=' z''; then A194: +(z,y) = [0,y'' -' z''] by A175,ARYTM_1:def 2; then +(z,y) in [:{0},REAL+:] by Lm1,ZFMISC_1:106; then consider x''',zy' being Element of REAL+ such that A195: x = [0,x'''] and A196: +(z,y) = [0,zy'] and A197: *(x,+(z,y)) = zy' *' x''' by A165,Def3; A198: x' = x'' by A167,A170,ZFMISC_1:33; A199: x'' = x''' by A167,A195,ZFMISC_1:33; thus *(x,+(y,z)) = x''' *' (y'' -' z'') by A194,A196,A197,ZFMISC_1:33 .= (x'' *' y') - (x' *' z') by A171,A173,A179,A193,A198,A199,ARYTM_1:26 .= +(*(x,y),*(x,z)) by A169,A172,A176,A177,A178,ZFMISC_1:33; end; hence thesis; suppose A200: z = 0; hence *(x,+(y,z)) = *(x,y) by Th13 .= +(*(x,y),o) by Th13 .= +(*(x,y),*(x,z)) by A200,Th14; end; hence thesis; suppose that A201: x in RR and A202: y in RR and A203: z in RR; A204: x in [:{0},REAL+:] by A201,XBOOLE_0:def 4; A205: y in [:{0},REAL+:] by A202,XBOOLE_0:def 4; A206: z in [:{0},REAL+:] by A203,XBOOLE_0:def 4; consider x',y' being Element of REAL+ such that A207: x = [0,x'] and A208: y = [0,y'] and A209: *(x,y) = y' *' x' by A204,A205,Def3; consider x'',z' being Element of REAL+ such that A210: x = [0,x''] and A211: z = [0,z'] and A212: *(x,z) = z' *' x'' by A204,A206,Def3; consider xy',xz' being Element of REAL+ such that A213: *(x,y) = xy' and A214: *(x,z) = xz' and A215: +(*(x,y),*(x,z)) = xy' + xz' by A209,A212,Def2; not(y in REAL+ & z in REAL+) & not(y in REAL+ & z in [:{0},REAL+:]) & not(y in [:{0},REAL+:] & z in REAL+) by A205,A206,Th5,XBOOLE_0:3; then consider y'',z'' being Element of REAL+ such that A216: y = [0,y''] and A217: z = [0,z''] and A218: +(y,z) = [0,y'' + z''] by Def2; +(y,z) in [:{0},REAL+:] by A218,Lm1,ZFMISC_1:106; then consider x''',yz' being Element of REAL+ such that A219: x = [0,x'''] and A220: +(y,z) = [0,yz'] and A221: *(x,+(y,z)) = yz' *' x''' by A204,Def3; A222: x' = x'' by A207,A210,ZFMISC_1:33; A223: x' = x''' by A207,A219,ZFMISC_1:33; A224: y' = y'' by A208,A216,ZFMISC_1:33; A225: z' = z'' by A211,A217,ZFMISC_1:33; thus *(x,+(y,z)) = x''' *' (y'' + z'') by A218,A220,A221,ZFMISC_1:33 .= +(*(x,y),*(x,z)) by A209,A212,A213,A214,A215,A222,A223,A224,A225, ARYTM_2:14; suppose A226: 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); A227: 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+ \/ RR by A227,ZFMISC_1:65; hence *(x,+(y,z)) = +(*(x,y),*(x,z)) by A226,XBOOLE_0:def 2; 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 Th16 .= *(o,y) by Def4 .= 0 by Th14; hence *(opp x,y) = opp *(x,y) by Def4; end; theorem Th18: for x being Element of REAL holds *(x,x) in REAL+ proof let x be Element of REAL; A1: x in REAL+ \/ [:{{}},REAL+:] by NUMBERS:def 1,XBOOLE_0:def 4; per cases by A1,XBOOLE_0:def 2; suppose x in REAL+; then ex x',y' being Element of REAL+ st x = x' & x = y' & *(x,x) = x' *' y' by Def3; hence *(x,x) in REAL+; suppose x in [:{0},REAL+:]; then ex x',y' being Element of REAL+ st x = [0,x'] & x = [0,y'] & *(x,x) = y' *' x' by Def3; hence *(x,x) in REAL+; 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 Th18; then consider x',y' being Element of REAL+ such that A2: *(x,x) = x' & *(y,y) = y' and A3: 0 = x' + y' by A1,Def2; A4: x' = 0 by A3,ARYTM_2:6; A5: x in REAL+ \/ [:{{}},REAL+:] by NUMBERS:def 1,XBOOLE_0:def 4; per cases by A5,XBOOLE_0:def 2; suppose x in REAL+; then ex x',y' being Element of REAL+ st x = x' & x = y' & 0 = x' *' y' by A2,A4,Def3; hence x = 0 by ARYTM_1:2; suppose x in [:{0},REAL+:]; then consider x',y' being Element of REAL+ such that A6: x = [0,x'] & x = [0,y'] and A7: 0 = y' *' x' by A2,A4,Def3; x' = y' by A6,ZFMISC_1:33; then x' = 0 by A7,ARYTM_1:2; then x in {[0,0]} by A6,TARSKI:def 1; hence x = 0 by NUMBERS:def 1,XBOOLE_0:def 4; end; theorem Th20: for x,y,z being Element of REAL st x <> 0 & *(x,y) = one & *(x,z) = one holds y = z proof let x,y,z be Element of REAL; assume that A1: x <> 0 and A2: *(x,y) = one and A3: *(x,z) = one; A4: for x,y being Element of REAL st *(x,y) =one holds x <> 0 proof let x,y be Element of REAL such that A5: *(x,y) = one and A6: x = 0; A7: not x in [:{0},REAL+:] by A6,Th5,ARYTM_2:21,XBOOLE_0:3; A8: y in REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1,XBOOLE_0:def 4; per cases by A8,XBOOLE_0:def 2; suppose y in REAL+; then ex x',y' being Element of REAL+ st x = x' & y = y' & one = x' *' y' by A5,A6,Def3,ARYTM_2:21; hence contradiction by A6,ARYTM_2:4; suppose y in [:{0},REAL+:]; then not y in REAL+ by Th5,XBOOLE_0:3; hence contradiction by A5,A6,A7,Def3; end; then A9: y <> 0 by A2; A10: z <> 0 by A3,A4; per cases; suppose x in REAL+ & y in REAL+ & z in REAL+; then (ex x',y' being Element of REAL+ st x = x' & y = y' & one = x' *' y') & ex x',y' being Element of REAL+ st x = x' & z = y' & one = x' *' y' by A2,A3,Def3; hence y = z by A1,Th8; suppose that A11: x in [:{0},REAL+:] and A12: y in [:{0},REAL+:] and A13: z in [:{0},REAL+:]; consider x',y' being Element of REAL+ such that A14: x = [0,x'] and A15: y = [0,y'] and A16: one = y' *' x' by A2,A11,A12,Def3; consider x'',z' being Element of REAL+ such that A17: x = [0,x''] and A18: z = [0,z'] and A19: one = z' *' x'' by A3,A11,A13,Def3; A20: x' = x'' by A14,A17,ZFMISC_1:33; x' <> 0 by A14,Th3; hence y = z by A15,A16,A18,A19,A20,Th8; suppose x in REAL+ & y in [:{0},REAL+:]; then ex x',y' being Element of REAL+ st x = x' & y = [0,y'] & one = [0,x' *' y'] by A1,A2,Def3; hence y = z by Lm2; suppose x in [:{0},REAL+:] & y in REAL+; then ex x',y' being Element of REAL+ st x = [0,x'] & y = y' & one = [0,y' *' x'] by A2,A9,Def3; hence y = z by Lm2; suppose x in [:{0},REAL+:] & z in REAL+; then ex x',z' being Element of REAL+ st x = [0,x'] & z = z' & one = [0,z' *' x'] by A3,A10,Def3; hence y = z by Lm2; suppose x in REAL+ & z in [:{0},REAL+:]; then ex x',z' being Element of REAL+ st x = x' & z = [0,z'] & one = [0,x' *' z'] by A1,A3,Def3; hence y = z by Lm2; 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 A2,Def3; 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 A3,Def3; end; theorem Th21: for x,y st y = one holds *(x,y) = x proof let x,y such that A1: y = one; per cases; suppose x = 0; hence thesis by Th14; suppose A2: x <> 0; A3: now assume A4: inv x = 0; thus one = *(x, inv x) by A2,Def5 .= 0 by A4,Th14; end; A5: *(x,inv x) = one by A2,Def5; A6: ex x',y' being Element of REAL+ st y = x' & y = y' & *(y,y) = x' *' y' by A1,Def3,ARYTM_2:21; *(*(x,y), inv x) = *(*(x,inv x), y) by Th15 .= *(y,y) by A1,A2,Def5 .= one by A1,A6,ARYTM_2:16; hence *(x,y) = x by A3,A5,Th20; end; reconsider j = one as Element of REAL by Th1,ARYTM_2:21; theorem for x,y st y <> 0 holds *(*(x,y),inv y) = x proof let x,y such that A1: y <> 0; thus *(*(x,y),inv y) = *(x,*(y,inv y)) by Th15 .= *(x,j) by A1,Def5 .= x by Th21; end; theorem Th23: for x,y st *(x,y) = 0 holds x = 0 or y = 0 proof let x,y such that A1: *(x,y) = 0 and A2: x <> 0; A3: *(x, inv x) = one by A2,Def5; thus y = *(j,y) by Th21 .= *(*(x,y),inv x) by A3,Th15 .= 0 by A1,Th14; end; theorem for x,y holds inv *(x,y) = *(inv x, inv y) proof let x,y; per cases; suppose A1: x = 0 or y = 0; then A2: *(x,y) = 0 by Th14; A3: inv x = 0 or inv y = 0 by A1,Def5; thus inv *(x,y) = 0 by A2,Def5 .= *(inv x, inv y) by A3,Th14; suppose that A4: x <> 0 and A5: y <> 0; A6: *(y,inv y) = one by A5,Def5; A7: *(x,inv x) = one by A4,Def5; A8: *(x,y) <> 0 by A4,A5,Th23; *(*(x,y),*(inv x, inv y)) = *(*(*(x,y),inv x), inv y) by Th15 .= *(*(j,y), inv y) by A7,Th15 .= one by A6,Th21; hence inv *(x,y) = *(inv x, inv y) by A8,Def5; end; theorem Th25: 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+:] & z in REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1,XBOOLE_0:def 4; per cases by A1,XBOOLE_0:def 2; suppose that A2: x in REAL+ and A3: y in REAL+ and A4: z in REAL+; consider y',z' being Element of REAL+ such that A5: y = y' and A6: z = z' and A7: +(y,z) = y' + z' by A3,A4,Def2; consider x',yz' being Element of REAL+ such that A8: x = x' and A9: +(y,z) = yz' and A10: +(x,+(y,z)) = x' + yz' by A2,A7,Def2; consider x'',y'' being Element of REAL+ such that A11: x = x'' and A12: y = y'' and A13: +(x,y) = x'' + y'' by A2,A3,Def2; consider xy'',z'' being Element of REAL+ such that A14: +(x,y) = xy'' and A15: z = z'' and A16: +(+(x,y),z) = xy'' + z'' by A4,A13,Def2; thus +(x,+(y,z)) = +(+(x,y),z) by A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,A15,A16, ARYTM_2:7; suppose that A17: x in REAL+ and A18: y in REAL+ and A19: z in [:{0},REAL+:]; consider y',z' being Element of REAL+ such that A20: y = y' and A21: z = [0,z'] and A22: +(y,z) = y' - z' by A18,A19,Def2; consider x'',y'' being Element of REAL+ such that A23: x = x'' and A24: y = y'' and A25: +(x,y) = x'' + y'' by A17,A18,Def2; consider xy'',z'' being Element of REAL+ such that A26: +(x,y) = xy'' and A27: z = [0,z''] and A28: +(+(x,y),z) = xy'' - z'' by A19,A25,Def2; A29: z' = z'' by A21,A27,ZFMISC_1:33; now per cases; suppose A30: z' <=' y'; then A31: +(y,z) = y' -' z' by A22,ARYTM_1:def 2; then consider x',yz' being Element of REAL+ such that A32: x = x' and A33: +(y,z) = yz' and A34: +(x,+(y,z)) = x' + yz' by A17,Def2; thus +(x,+(y,z)) = +(+(x,y),z) by A20,A23,A24,A25,A26,A28,A29,A30,A31,A32, A33,A34,ARYTM_1:20; suppose A35: not z' <=' y'; then A36: +(y,z) = [0,z' -' y'] by A22,ARYTM_1:def 2; then +(y,z) in [:{0},REAL+:] by Lm1,ZFMISC_1:106; then consider x',yz' being Element of REAL+ such that A37: x = x' and A38: +(y,z) = [0,yz'] and A39: +(x,+(y,z)) = x' - yz' by A17,Def2; thus +(x,+(y,z)) = x' - (z' -' y') by A36,A38,A39,ZFMISC_1:33 .= +(+(x,y),z) by A20,A23,A24,A25,A26,A28,A29,A35,A37,ARYTM_1:21; end; hence thesis; suppose that A40: x in REAL+ and A41: y in [:{0},REAL+:] and A42: z in REAL+; consider z',y' being Element of REAL+ such that A43: z = z' and A44: y = [0,y'] and A45: +(y,z) = z' - y' by A41,A42,Def2; consider x'',y'' being Element of REAL+ such that A46: x = x'' and A47: y = [0,y''] and A48: +(x,y) = x'' - y'' by A40,A41,Def2; A49: y' = y'' by A44,A47,ZFMISC_1:33; now per cases; suppose that A50: y' <=' x'' and A51: y' <=' z'; A52: +(y,z) = z' -' y' by A45,A51,ARYTM_1:def 2; then consider x',yz' being Element of REAL+ such that A53: x = x' and A54: +(y,z) = yz' and A55: +(x,+(y,z)) = x' + yz' by A40,Def2; A56: +(x,y) = x' -' y' by A46,A48,A49,A50,A53,ARYTM_1:def 2; then consider z'',xy'' being Element of REAL+ such that A57: z = z'' and A58: +(x,y) = xy'' and A59: +(z,+(x,y)) = z'' + xy'' by A42,Def2; thus +(x,+(y,z)) = +(+(x,y),z) by A43,A46,A50,A51,A52,A53,A54,A55,A56,A57, A58,A59,ARYTM_1:12; suppose that A60: y' <=' x'' and A61: not y' <=' z'; A62: +(y,z) = [0,y' -' z'] by A45,A61,ARYTM_1:def 2; then +(y,z) in [:{0},REAL+:] by Lm1,ZFMISC_1:106; then consider x',yz' being Element of REAL+ such that A63: x = x' and A64: +(y,z) = [0,yz'] and A65: +(x,+(y,z)) = x' - yz' by A40,Def2; A66: +(x,y) = x'' -' y' by A48,A49,A60,ARYTM_1:def 2; then consider z'',xy'' being Element of REAL+ such that A67: z = z'' and A68: +(x,y) = xy'' and A69: +(z,+(x,y)) = z'' + xy'' by A42,Def2; thus +(x,+(y,z)) = x' - (y' -' z') by A62,A64,A65,ZFMISC_1:33 .= +(+(x,y),z) by A43,A46,A60,A61,A63,A66,A67,A68,A69,ARYTM_1:22; suppose that A70: not y' <=' x'' and A71: y' <=' z'; A72: +(y,x) = [0,y' -' x''] by A48,A49,A70,ARYTM_1:def 2; then +(y,x) in [:{0},REAL+:] by Lm1,ZFMISC_1:106; then consider z'',yx'' being Element of REAL+ such that A73: z = z'' and A74: +(y,x) = [0,yx''] and A75: +(z,+(y,x)) = z'' - yx'' by A42,Def2; A76: +(z,y) = z' -' y' by A45,A71,ARYTM_1:def 2; then consider x',zy'' being Element of REAL+ such that A77: x = x' and A78: +(z,y) = zy'' and A79: +(x,+(z,y)) = x' + zy'' by A40,Def2; thus +(x,+(y,z)) = z'' - (y' -' x'') by A43,A46,A70,A71,A73,A76,A77,A78,A79, ARYTM_1:22 .= +(+(x,y),z) by A72,A74,A75,ZFMISC_1:33; suppose that A80: not y' <=' x'' and A81: not y' <=' z'; A82: +(y,x) = [0,y' -' x''] by A48,A49,A80,ARYTM_1:def 2; then +(y,x) in [:{0},REAL+:] by Lm1,ZFMISC_1:106; then consider z'',yx'' being Element of REAL+ such that A83: z = z'' and A84: +(y,x) = [0,yx''] and A85: +(z,+(y,x)) = z'' - yx'' by A42,Def2; A86: +(y,z) = [0,y' -' z'] by A45,A81,ARYTM_1:def 2; then +(y,z) in [:{0},REAL+:] by Lm1,ZFMISC_1:106; then consider x',yz' being Element of REAL+ such that A87: x = x' and A88: +(y,z) = [0,yz'] and A89: +(x,+(y,z)) = x' - yz' by A40,Def2; thus +(x,+(y,z)) = x' - (y' -' z') by A86,A88,A89,ZFMISC_1:33 .= z'' - (y' -' x'') by A43,A46,A80,A81,A83,A87,ARYTM_1:23 .= +(+(x,y),z) by A82,A84,A85,ZFMISC_1:33; end; hence thesis; suppose that A90: x in REAL+ and A91: y in [:{0},REAL+:] and A92: z in [:{0},REAL+:]; not(z in REAL+ & y in REAL+) & not(z in REAL+ & y in [:{0},REAL+:]) & not(y in REAL+ & z in [:{0},REAL+:]) by A91,A92,Th5,XBOOLE_0:3; then consider y',z' being Element of REAL+ such that A93: y = [0,y'] and A94: z = [0,z'] and A95: +(y,z) = [0,y' + z'] by Def2; consider x'',y'' being Element of REAL+ such that A96: x = x'' and A97: y = [0,y''] and A98: +(x,y) = x'' - y'' by A90,A91,Def2; +(y,z) in [:{0},REAL+:] by A95,Lm1,ZFMISC_1:106; then consider x',yz' being Element of REAL+ such that A99: x = x' and A100: +(y,z) = [0,yz'] and A101: +(x,+(y,z)) = x' - yz' by A90,Def2; A102: y' = y'' by A93,A97,ZFMISC_1:33; now per cases; suppose A103: y'' <=' x''; then A104: +(x,y) = x'' -' y'' by A98,ARYTM_1:def 2; then consider xy'',z'' being Element of REAL+ such that A105: +(x,y) = xy'' and A106: z = [0,z''] and A107: +(+(x,y),z) = xy'' - z'' by A92,Def2; A108: z' = z'' by A94,A106,ZFMISC_1:33; thus +(x,+(y,z)) = x' - (y' + z') by A95,A100,A101,ZFMISC_1:33 .= +(+(x,y),z) by A96,A99,A102,A103,A104,A105,A107,A108,ARYTM_1:24; suppose A109: not y'' <=' x''; then A110: +(x,y) = [0,y'' -' x''] by A98,ARYTM_1:def 2; then +(x,y) in [:{0},REAL+:] by Lm1,ZFMISC_1:106; then not(z in REAL+ & +(x,y) in REAL+) & not(z in REAL+ & +(x,y) in [:{0},REAL+:]) & not(+(x,y) in REAL+ & z in [:{0},REAL+:]) by A92,Th5,XBOOLE_0:3; then consider xy'',z'' being Element of REAL+ such that A111: +(x,y) = [0,xy''] and A112: z = [0,z''] and A113: +(+(x,y),z) = [0,xy'' + z''] by Def2; A114: z' = z'' by A94,A112,ZFMISC_1:33; A115: yz' = z' + y' by A95,A100,ZFMISC_1:33; then y'' <=' yz' by A102,ARYTM_2:20; then not yz' <=' x' by A96,A99,A109,ARYTM_1:3; hence +(x,+(y,z)) = [0,z' + y' -' x'] by A101,A115,ARYTM_1:def 2 .= [0,z'' + (y'' -' x'')] by A96,A99,A102,A109,A114,ARYTM_1:13 .= +(+(x,y),z) by A110,A111,A113,ZFMISC_1:33; end; hence thesis; suppose that A116: z in REAL+ and A117: y in REAL+ and A118: x in [:{0},REAL+:]; consider y',x' being Element of REAL+ such that A119: y = y' and A120: x = [0,x'] and A121: +(y,x) = y' - x' by A117,A118,Def2; consider z'',y'' being Element of REAL+ such that A122: z = z'' and A123: y = y'' and A124: +(z,y) = z'' + y'' by A116,A117,Def2; consider zy'',x'' being Element of REAL+ such that A125: +(z,y) = zy'' and A126: x = [0,x''] and A127: +(+(z,y),x) = zy'' - x'' by A118,A124,Def2; A128: x' = x'' by A120,A126,ZFMISC_1:33; now per cases; suppose A129: x' <=' y'; then A130: +(y,x) = y' -' x' by A121,ARYTM_1:def 2; then consider z',yx' being Element of REAL+ such that A131: z = z' and A132: +(y,x) = yx' and A133: +(z,+(y,x)) = z' + yx' by A116,Def2; thus +(z,+(y,x)) = +(+(z,y),x) by A119,A122,A123,A124,A125,A127,A128,A129, A130,A131,A132,A133,ARYTM_1:20; suppose A134: not x' <=' y'; then A135: +(y,x) = [0,x' -' y'] by A121,ARYTM_1:def 2; then +(y,x) in [:{0},REAL+:] by Lm1,ZFMISC_1:106; then consider z',yx' being Element of REAL+ such that A136: z = z' and A137: +(y,x) = [0,yx'] and A138: +(z,+(y,x)) = z' - yx' by A116,Def2; thus +(z,+(y,x)) = z' - (x' -' y') by A135,A137,A138,ZFMISC_1:33 .= +(+(z,y),x) by A119,A122,A123,A124,A125,A127,A128,A134,A136, ARYTM_1:21; end; hence thesis; suppose that A139: x in [:{0},REAL+:] and A140: y in REAL+ and A141: z in [:{0},REAL+:]; consider y',z' being Element of REAL+ such that A142: y = y' and A143: z = [0,z'] and A144: +(y,z) = y' - z' by A140,A141,Def2; consider x'',y'' being Element of REAL+ such that A145: x = [0,x''] and A146: y = y'' and A147: +(x,y) = y'' - x'' by A139,A140,Def2; now per cases; suppose that A148: x'' <=' y'' and A149: z' <=' y'; A150: +(y,z) = y' -' z' by A144,A149,ARYTM_1:def 2; then consider x',yz' being Element of REAL+ such that A151: x = [0,x'] and A152: +(y,z) = yz' and A153: +(x,+(y,z)) = yz' - x' by A139,Def2; A154: x' = x'' by A145,A151,ZFMISC_1:33; then A155: +(x,y) = y' -' x' by A142,A146,A147,A148,ARYTM_1:def 2; then consider z'',xy'' being Element of REAL+ such that A156: z = [0,z''] and A157: +(x,y) = xy'' and A158: +(z,+(x,y)) = xy'' - z'' by A141,Def2; z' = z'' by A143,A156,ZFMISC_1:33; hence +(x,+(y,z)) = +(+(x,y),z) by A142,A146,A148,A149,A150,A152,A153,A154, A155,A157,A158,ARYTM_1:25; suppose that A159: not x'' <=' y'' and A160: z' <=' y'; A161: +(y,z) = y' -' z' by A144,A160,ARYTM_1:def 2; then consider x',yz' being Element of REAL+ such that A162: x = [0,x'] and A163: +(y,z) = yz' and A164: +(x,+(y,z)) = yz' - x' by A139,Def2; A165: x' = x'' by A145,A162,ZFMISC_1:33; A166: +(y,x) = [0,x'' -' y''] by A147,A159,ARYTM_1:def 2; then +(y,x) in [:{0},REAL+:] by Lm1,ZFMISC_1:106; then not(z in REAL+ & +(x,y) in REAL+) & not(z in REAL+ & +(x,y) in [:{0},REAL+:]) & not(+(x,y) in REAL+ & z in [:{0},REAL+:]) by A141,Th5,XBOOLE_0:3; then consider z'',yx' being Element of REAL+ such that A167: z = [0,z''] and A168: +(y,x) = [0,yx'] and A169: +(z,+(y,x)) = [0,z'' + yx'] by Def2; A170: z' = z'' by A143,A167,ZFMISC_1:33; yz' <=' y' by A161,A163,ARYTM_1:11; then not x' <=' yz' by A142,A146,A159,A165,ARYTM_1:3; hence +(x,+(y,z)) = [0,x' -' (y' -' z')] by A161,A163,A164,ARYTM_1:def 2 .= [0,x'' -' y'' + z''] by A142,A146,A159,A160,A165,A170,ARYTM_1:14 .= +(+(x,y),z) by A166,A168,A169,ZFMISC_1:33; suppose that A171: not z' <=' y' and A172: x'' <=' y''; A173: +(y,x) = y'' -' x'' by A147,A172,ARYTM_1:def 2; then consider z'',yx'' being Element of REAL+ such that A174: z = [0,z''] and A175: +(y,x) = yx'' and A176: +(z,+(y,x)) = yx'' - z'' by A141,Def2; A177: z'' = z' by A143,A174,ZFMISC_1:33; A178: +(y,z) = [0,z' -' y'] by A144,A171,ARYTM_1:def 2; then +(y,z) in [:{0},REAL+:] by Lm1,ZFMISC_1:106; then not(x in REAL+ & +(z,y) in REAL+) & not(x in REAL+ & +(z,y) in [:{0},REAL+:]) & not(+(z,y) in REAL+ & x in [:{0},REAL+:]) by A139,Th5,XBOOLE_0:3; then consider x',yz'' being Element of REAL+ such that A179: x = [0,x'] and A180: +(y,z) = [0,yz''] and A181: +(x,+(y,z)) = [0,x' + yz''] by Def2; A182: x'' = x' by A145,A179,ZFMISC_1:33; yx'' <=' y'' by A173,A175,ARYTM_1:11; then A183: not z'' <=' yx'' by A142,A146,A171,A177,ARYTM_1:3; thus +(x,+(y,z)) = [0,z' -' y' + x'] by A178,A180,A181,ZFMISC_1:33 .= [0,z'' -' (y'' -' x'')] by A142,A146,A171,A172,A177,A182,ARYTM_1: 14 .= +(+(x,y),z) by A173,A175,A176,A183,ARYTM_1:def 2; suppose that A184: not x'' <=' y'' and A185: not z' <=' y'; A186: +(y,z) = [0,z' -' y'] by A144,A185,ARYTM_1:def 2; then +(y,z) in [:{0},REAL+:] by Lm1,ZFMISC_1:106; then not(x in REAL+ & +(z,y) in REAL+) & not(x in REAL+ & +(z,y) in [:{0},REAL+:]) & not(+(z,y) in REAL+ & x in [:{0},REAL+:]) by A139,Th5,XBOOLE_0:3; then consider x',yz'' being Element of REAL+ such that A187: x = [0,x'] and A188: +(y,z) = [0,yz''] and A189: +(x,+(y,z)) = [0,x' + yz''] by Def2; A190: +(y,x) = [0,x'' -' y''] by A147,A184,ARYTM_1:def 2; then +(y,x) in [:{0},REAL+:] by Lm1,ZFMISC_1:106; then not(z in REAL+ & +(x,y) in REAL+) & not(z in REAL+ & +(x,y) in [:{0},REAL+:]) & not(+(x,y) in REAL+ & z in [:{0},REAL+:]) by A141,Th5,XBOOLE_0:3; then consider z'',yx' being Element of REAL+ such that A191: z = [0,z''] and A192: +(y,x) = [0,yx'] and A193: +(z,+(y,x)) = [0,z'' + yx'] by Def2; A194: z' = z'' by A143,A191,ZFMISC_1:33; A195: x' = x'' by A145,A187,ZFMISC_1:33; thus +(x,+(y,z)) = [0,z' -' y' + x'] by A186,A188,A189,ZFMISC_1:33 .= [0,x'' -' y'' + z''] by A142,A146,A184,A185,A194,A195,ARYTM_1:15 .= +(+(x,y),z) by A190,A192,A193,ZFMISC_1:33; end; hence thesis; suppose that A196: z in REAL+ and A197: y in [:{0},REAL+:] and A198: x in [:{0},REAL+:]; not(x in REAL+ & y in REAL+) & not(x in REAL+ & y in [:{0},REAL+:]) & not(y in REAL+ & x in [:{0},REAL+:]) by A197,A198,Th5,XBOOLE_0:3; then consider y',x' being Element of REAL+ such that A199: y = [0,y'] and A200: x = [0,x'] and A201: +(y,x) = [0,y' + x'] by Def2; consider z'',y'' being Element of REAL+ such that A202: z = z'' and A203: y = [0,y''] and A204: +(z,y) = z'' - y'' by A196,A197,Def2; +(y,x) in [:{0},REAL+:] by A201,Lm1,ZFMISC_1:106; then consider z',yx' being Element of REAL+ such that A205: z = z' and A206: +(y,x) = [0,yx'] and A207: +(z,+(y,x)) = z' - yx' by A196,Def2; A208: y' = y'' by A199,A203,ZFMISC_1:33; now per cases; suppose A209: y'' <=' z''; then A210: +(z,y) = z'' -' y'' by A204,ARYTM_1:def 2; then consider zy'',x'' being Element of REAL+ such that A211: +(z,y) = zy'' and A212: x = [0,x''] and A213: +(+(z,y),x) = zy'' - x'' by A198,Def2; A214: x' = x'' by A200,A212,ZFMISC_1:33; thus +(z,+(y,x)) = z' - (y' + x') by A201,A206,A207,ZFMISC_1:33 .= +(+(z,y),x) by A202,A205,A208,A209,A210,A211,A213,A214,ARYTM_1:24; suppose A215: not y'' <=' z''; then A216: +(z,y) = [0,y'' -' z''] by A204,ARYTM_1:def 2; then +(z,y) in [:{0},REAL+:] by Lm1,ZFMISC_1:106; then not(x in REAL+ & +(z,y) in REAL+) & not(x in REAL+ & +(z,y) in [:{0},REAL+:]) & not(+(z,y) in REAL+ & x in [:{0},REAL+:]) by A198,Th5,XBOOLE_0:3; then consider zy'',x'' being Element of REAL+ such that A217: +(z,y) = [0,zy''] and A218: x = [0,x''] and A219: +(+(z,y),x) = [0,zy'' + x''] by Def2; A220: x' = x'' by A200,A218,ZFMISC_1:33; A221: yx' = x' + y' by A201,A206,ZFMISC_1:33; then y'' <=' yx' by A208,ARYTM_2:20; then not yx' <=' z' by A202,A205,A215,ARYTM_1:3; hence +(z,+(y,x)) = [0,x' + y' -' z'] by A207,A221,ARYTM_1:def 2 .= [0,x'' + (y'' -' z'')] by A202,A205,A208,A215,A220,ARYTM_1:13 .= +(+(z,y),x) by A216,A217,A219,ZFMISC_1:33; end; hence thesis; suppose that A222: x in [:{0},REAL+:] and A223: y in [:{0},REAL+:] and A224: z in [:{0},REAL+:]; not(z in REAL+ & y in REAL+) & not(z in REAL+ & y in [:{0},REAL+:]) & not(y in REAL+ & z in [:{0},REAL+:]) by A223,A224,Th5,XBOOLE_0:3; then consider y',z' being Element of REAL+ such that A225: y = [0,y'] and A226: z = [0,z'] and A227: +(y,z) = [0,y' + z'] by Def2; not(x in REAL+ & y in REAL+) & not(x in REAL+ & y in [:{0},REAL+:]) & not(y in REAL+ & x in [:{0},REAL+:]) by A222,A223,Th5,XBOOLE_0:3; then consider x'',y'' being Element of REAL+ such that A228: x = [0,x''] and A229: y = [0,y''] and A230: +(x,y) = [0,x'' + y''] by Def2; +(z,y) in [:{0},REAL+:] by A227,Lm1,ZFMISC_1:106; then not(x in REAL+ & +(z,y) in REAL+) & not(x in REAL+ & +(z,y) in [:{0},REAL+:]) & not(+(z,y) in REAL+ & x in [:{0},REAL+:]) by A222,Th5,XBOOLE_0:3; then consider x',yz' being Element of REAL+ such that A231: x = [0,x'] and A232: +(y,z) = [0,yz'] and A233: +(x,+(y,z)) = [0,x' + yz'] by Def2; +(x,y) in [:{0},REAL+:] by A230,Lm1,ZFMISC_1:106; then not(z in REAL+ & +(x,y) in REAL+) & not(z in REAL+ & +(x,y) in [:{0},REAL+:]) & not(+(x,y) in REAL+ & z in [:{0},REAL+:]) by A224,Th5,XBOOLE_0:3; then consider xy'',z'' being Element of REAL+ such that A234: +(x,y) = [0,xy''] and A235: z = [0,z''] and A236: +(+(x,y),z) = [0,xy'' + z''] by Def2; A237: z' = z'' by A226,A235,ZFMISC_1:33; A238: x' = x'' by A228,A231,ZFMISC_1:33; A239: y' = y'' by A225,A229,ZFMISC_1:33; thus +(x,+(y,z)) = [0,z' + y' + x'] by A227,A232,A233,ZFMISC_1:33 .= [0,z'' + (y'' + x'')] by A237,A238,A239,ARYTM_2:7 .= +(+(x,y),z) by A230,A234,A236,ZFMISC_1:33; end; theorem [*x,y*] in REAL implies y = 0 proof assume A1: [*x,y*] in REAL; assume y <> 0; then [*x,y*] = (0,one) --> (x,y) by Def7; hence contradiction by A1,Th10; end; theorem for x,y being Element of REAL holds opp +(x,y) = +(opp x, opp y) proof let x,y be Element of REAL; +(+(x,y),+(opp x, opp y)) = +(x,+(y,+(opp x, opp y))) by Th25 .= +(x,+(opp x,+(y, opp y))) by Th25 .= +(x,+(opp x,o)) by Def4 .= +(x,opp x) by Th13 .= 0 by Def4; hence thesis by Def4; end;

Back to top