### The Mizar article:

### Introduction to Arithmetic of Real Numbers

**by****Library Committee**

- Received February 11, 2003
Copyright (c) 2003 Association of Mizar Users

- MML identifier: XREAL_0
- [ MML identifier index ]

environ vocabulary XREAL_0, ARYTM_2, BOOLE, ARYTM_1, ARYTM_3, ORDINAL2, ARYTM, RELAT_1, ASYMPT_0, ZF_LANG, XCMPLX_0, COMPLEX1, FUNCOP_1, OPPCAT_1, ORDINAL1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_4, ORDINAL1, ORDINAL2, ARYTM_2, ARYTM_1, NUMBERS, ARYTM_0, XCMPLX_0; constructors ARYTM_1, ARYTM_0, ORDINAL2, XCMPLX_0, FUNCT_4, XBOOLE_0, TARSKI; clusters ARYTM_2, NUMBERS, ARYTM_3, ORDINAL2, SUBSET_1, XBOOLE_0, XCMPLX_0, ZFMISC_1; requirements NUMERALS, BOOLE, SUBSET, ARITHM; definitions XCMPLX_0; theorems XBOOLE_0, ARYTM_1, ZFMISC_1, TARSKI, ARYTM_2, ORDINAL2, ARYTM_0, XCMPLX_0, NUMBERS; begin definition let r be number; attr r is real means :Def1: r in REAL; end; definition cluster natural -> real number; coherence proof let x be number; assume x is natural; then x in NAT by ORDINAL2:def 21; hence x in REAL; end; cluster real -> complex number; coherence proof let x be number; assume x is real; then x in REAL by Def1; hence x in COMPLEX by NUMBERS:def 2,XBOOLE_0:def 2; end; end; definition cluster real number; existence proof consider r being Element of REAL; take r; thus r in REAL; end; end; definition let x,y be real number; pred x <= y means :Def2: ex x',y' being Element of REAL+ st x = x' & y = y' & x' <=' y' if x in REAL+ & y in REAL+, ex x',y' being Element of REAL+ st x = [0,x'] & y = [0,y'] & y' <=' x' if x in [:{0},REAL+:] & y in [:{0},REAL+:] otherwise y in REAL+ & x in [:{0},REAL+:]; consistency by ARYTM_0:5,XBOOLE_0:3; reflexivity proof let x be real number such that A1: not((x in REAL+ & x in REAL+ implies ex x',y' being Element of REAL+ st x = x' & x = y' & x' <=' y') & (x in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x',y' being Element of REAL+ st x = [0,x'] & x = [0,y'] & y' <=' x') & (not(x in REAL+ & x in REAL+) & not(x in [:{0},REAL+:] & x in [:{0},REAL+:]) implies x in REAL+ & x in [:{0},REAL+:])); x in REAL by Def1; then A2: x in REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1,XBOOLE_0:def 4; per cases by A1; suppose that A3: x in REAL+ and A4: not ex x',y' being Element of REAL+ st x = x' & x = y' & x' <=' y'; reconsider x' = x as Element of REAL+ by A3; not x' <=' x' by A4; hence thesis; suppose that A5: x in [:{0},REAL+:] and A6: not ex x',y' being Element of REAL+ st x = [0,x'] & x = [0,y'] & y' <=' x'; consider z,x' being set such that A7: z in {0} and A8: x' in REAL+ and A9: x = [z,x'] by A5,ZFMISC_1:103; reconsider x' as Element of REAL+ by A8; x = [0,x'] by A7,A9,TARSKI:def 1; then not x' <=' x' by A6; hence thesis; suppose not(not x in REAL+ & not x in [:{0},REAL+:] implies x in REAL+ & x in [:{0},REAL+:]); hence thesis by A2,XBOOLE_0:def 2; end; connectedness proof let x,y be real number such that A10: not((x in REAL+ & y in REAL+ implies ex x',y' being Element of REAL+ st x = x' & y = y' & x' <=' y') & (x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ex x',y' being Element of REAL+ st x = [0,x'] & y = [0,y'] & y' <=' x') & (not(x in REAL+ & y in REAL+) & not(x in [:{0},REAL+:] & y in [:{0},REAL+:]) implies y in REAL+ & x in [:{0},REAL+:])); x in REAL & y in REAL by Def1; then A11: x in REAL+ \/ [:{0},REAL+:] & y in REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1,XBOOLE_0:def 4; per cases by A10; suppose that A12: x in REAL+ & y in REAL+ and A13: not ex x',y' being Element of REAL+ st x = x' & y = y' & x' <=' y'; hereby assume y in REAL+ & x in REAL+; then reconsider x' = x, y' = y as Element of REAL+; take y',x'; thus y = y' & x = x'; thus y' <=' x' by A13; end; thus thesis by A12,ARYTM_0:5,XBOOLE_0:3; suppose that A14: x in [:{0},REAL+:] & y in [:{0},REAL+:] and A15: not ex x',y' being Element of REAL+ st x = [0,x'] & y = [0,y'] & y' <=' x'; now assume y in [:{0},REAL+:]; then consider z,y' being set such that A16: z in {0} and A17: y' in REAL+ and A18: y = [z,y'] by ZFMISC_1:103; A19: z = 0 by A16,TARSKI:def 1; assume x in [:{0},REAL+:]; then consider z,x' being set such that A20: z in {0} and A21: x' in REAL+ and A22: x = [z,x'] by ZFMISC_1:103; A23: z = 0 by A20,TARSKI:def 1; reconsider x',y' as Element of REAL+ by A17,A21; take y',x'; thus y = [0,y'] & x = [0,x'] by A16,A18,A20,A22,TARSKI:def 1; thus x' <=' y' by A15,A18,A19,A22,A23; end; hence thesis by A14,ARYTM_0:5,XBOOLE_0:3; suppose not(not(x in REAL+ & y in REAL+) & not(x in [:{0},REAL+:] & y in [:{0},REAL+:]) implies y in REAL+ & x in [:{0},REAL+:]); hence thesis by A11,XBOOLE_0:def 2; end; synonym y >= x; antonym y < x; antonym x > y; end; definition let x be real number; attr x is positive means :Def3: x > 0; attr x is negative means :Def4: x < 0; end; Lm1: for x being real number, x1,x2 being Element of REAL st x = [*x1,x2*] holds x2 = 0 & x = x1 proof let x be real number, x1,x2 being Element of REAL; assume A1: x = [*x1,x2*]; A2: x in REAL by Def1; hereby assume x2 <> 0; then x = (0,one) --> (x1,x2) by A1,ARYTM_0:def 7; hence contradiction by A2,ARYTM_0:10; end; hence x = x1 by A1,ARYTM_0:def 7; end; definition let x be real number; cluster -x -> real; coherence proof x + -x = 0 by XCMPLX_0:def 6; then consider x1,x2,y1,y2 being Element of REAL such that A1: x = [*x1,x2*] and A2: -x = [*y1,y2*] and A3: 0 = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4; A4: +(x2,y2) = 0 by A3,Lm1; x2 = 0 by A1,Lm1; then y2 = 0 by A4,ARYTM_0:13; then -x = y1 by A2,ARYTM_0:def 7; hence thesis by Def1; end; cluster x" -> real; coherence proof A5:one = succ 0 by ORDINAL2:def 4 .= 1; per cases; suppose x = 0; hence thesis by XCMPLX_0:def 7; suppose A6: x <> 0; then x * x" = one by A5,XCMPLX_0:def 7; then consider x1,x2,y1,y2 being Element of REAL such that A7: x = [*x1,x2*] and A8: x" = [*y1,y2*] and A9: one = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *] by XCMPLX_0:def 5; A10: +(*(x1,y2),*(x2,y1)) = 0 by A9,Lm1; x2 = 0 by A7,Lm1; then *(x2,y1) = 0 by ARYTM_0:14; then 0 = *(x1,y2) by A10,ARYTM_0:13; then x1 = 0 or y2 = 0 by ARYTM_0:23; then x" = y1 by A6,A7,A8,Lm1,ARYTM_0:def 7; hence thesis by Def1; end; let y be real number; cluster x + y -> real; coherence proof consider x1,x2,y1,y2 being Element of REAL such that A11: x = [*x1,x2*] and A12: y = [*y1,y2*] and A13: x+y = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4; x2 = 0 & y2 = 0 by A11,A12,Lm1; then +(x2,y2) = 0 by ARYTM_0:13; then x + y = +(x1,y1) by A13,ARYTM_0:def 7; hence thesis by Def1; end; cluster x * y -> real; coherence proof consider x1,x2,y1,y2 being Element of REAL such that A14: x = [*x1,x2*] and A15: y = [*y1,y2*] and A16: x*y = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *] by XCMPLX_0:def 5; A17: x2 = 0 & y2 = 0 by A14,A15,Lm1; then *(x2,y1) = 0 & *(x1,y2) = 0 by ARYTM_0:14; then A18: +(*(x1,y2),*(x2,y1)) = 0 by ARYTM_0:13; *(opp x2,y2) = 0 by A17,ARYTM_0:14; then opp*(x2,y2) = 0 by ARYTM_0:17; then x * y = +(*(x1,y1),0) by A16,A18,ARYTM_0:def 7 .= *(x1,y1) by ARYTM_0:13; hence thesis by Def1; end; end; definition let x,y be real number; cluster x-y -> real; coherence proof x-y = x+-y by XCMPLX_0:def 8; hence thesis; end; cluster x/y -> real; coherence proof x/y = x*y" by XCMPLX_0:def 9; hence thesis; end; end; begin reserve r,s,t for real number; Lm2: one = succ 0 by ORDINAL2:def 4 .= 1; Lm3: {} in {{}} by TARSKI:def 1; Lm4: r <= s & s <= r implies r = s proof assume that A1: r <= s and A2: s <= r; r in REAL & s in REAL by Def1; then A3: r in REAL+ \/ [:{0},REAL+:] & s in REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1,XBOOLE_0:def 4; per cases by A3,XBOOLE_0:def 2; suppose that A4: r in REAL+ and A5: s in REAL+; consider r',s' being Element of REAL+ such that A6: r = r' and A7: s = s' and A8: r' <=' s' by A1,A4,A5,Def2; consider s'',r'' being Element of REAL+ such that A9: s = s'' and A10: r = r'' and A11: s'' <=' r'' by A2,A4,A5,Def2; thus thesis by A6,A7,A8,A9,A10,A11,ARYTM_1:4; suppose A12: r in REAL+ & s in [:{0},REAL+:]; then not(r in REAL+ & s in REAL+) & not(r in [:{0},REAL+:] & s in [:{0},REAL+:]) by ARYTM_0:5,XBOOLE_0:3; hence thesis by A1,A12,Def2; suppose A13: s in REAL+ & r in [:{0},REAL+:]; then not(r in REAL+ & s in REAL+) & not(r in [:{0},REAL+:] & s in [:{0},REAL+:]) by ARYTM_0:5,XBOOLE_0:3; hence thesis by A2,A13,Def2; suppose that A14: r in [:{0},REAL+:] and A15: s in [:{0},REAL+:]; consider r',s' being Element of REAL+ such that A16: r = [0,r'] and A17: s = [0,s'] and A18: s' <=' r' by A1,A14,A15,Def2; consider s'',r'' being Element of REAL+ such that A19: s = [0,s''] and A20: r = [0,r''] and A21: r'' <=' s'' by A2,A14,A15,Def2; r' = r'' & s' = s'' by A16,A17,A19,A20,ZFMISC_1:33; hence thesis by A18,A19,A20,A21,ARYTM_1:4; end; Lm5: r <= s implies r + t <= s + t proof assume A1: r <= s; reconsider x1=r, y1=s, z1=t as Element of REAL by Def1; for x' being Element of REAL, r st x' = r holds +(x',z1) = r + t proof let x' be Element of REAL, r such that A2: x' = r; consider x1,x2,y1,y2 being Element of REAL such that A3: r = [* x1,x2 *] and A4: t = [*y1,y2*] and A5: r+t = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4; A6: r = x1 & t = y1 by A3,A4,Lm1; x2 = 0 & y2 = 0 by A3,A4,Lm1; then +(x2,y2) = 0 by ARYTM_0:13; hence +(x',z1) = r + t by A2,A5,A6,ARYTM_0:def 7; end; then A7: +(y1,z1) = s + t & +(x1,z1) = r + t; per cases by A1,Def2; suppose that A8: r in REAL+ and A9: s in REAL+ and A10: t in REAL+; consider x'',s'' being Element of REAL+ such that A11: r = x'' and A12: s = s'' and A13: x'' <=' s'' by A1,A8,A9,Def2; consider x',t' being Element of REAL+ such that A14: r = x' and A15: t = t' and A16: +(x1,z1) = x' + t' by A8,A10,ARYTM_0:def 2; consider s',t'' being Element of REAL+ such that A17: s = s' and A18: t = t'' and A19: +(y1,z1) = s' + t'' by A9,A10,ARYTM_0:def 2; x' + t' <=' s' + t'' by A11,A12,A13,A14,A15,A17,A18,ARYTM_1:7; hence r + t <= s + t by A7,A16,A19,Def2; suppose that A20: r in [:{0},REAL+:] and A21: s in REAL+ and A22: t in REAL+; consider x',t' being Element of REAL+ such that r = [0,x'] and A23: t = t' and A24: +(x1,z1) = t' - x' by A20,A22,ARYTM_0:def 2; consider s',t'' being Element of REAL+ such that s = s' and A25: t = t'' and A26: +(y1,z1) = s' + t'' by A21,A22,ARYTM_0:def 2; now per cases; suppose x' <=' t'; then A27: t' - x' = t' -' x' by ARYTM_1:def 2; A28: t' -' x' <=' t' by ARYTM_1:11; t' <=' s' + t'' by A23,A25,ARYTM_2:20; then t' -' x' <=' s' + t'' by A28,ARYTM_1:3; hence r + t <= s + t by A7,A24,A26,A27,Def2; suppose not x' <=' t'; then t' - x' = [0,x' -' t'] by ARYTM_1:def 2; then t' - x' in [:{0},REAL+:] by Lm3,ZFMISC_1:106; then not r + t in REAL+ & not s + t in [:{0},REAL+:] by A7,A24,A26,ARYTM_0:5,XBOOLE_0:3; hence r + t <= s + t by Def2; end; hence thesis; suppose that A29: r in [:{0},REAL+:] and A30: s in [:{0},REAL+:] and A31: t in REAL+; consider x'',s'' being Element of REAL+ such that A32: r = [0,x''] and A33: s = [0,s''] and A34: s'' <=' x'' by A1,A29,A30,Def2; consider x',t' being Element of REAL+ such that A35: r = [0,x'] and A36: t = t' and A37: +(x1,z1) = t' - x' by A29,A31,ARYTM_0:def 2; consider s',t'' being Element of REAL+ such that A38: s = [0,s'] and A39: t = t'' and A40: +(y1,z1) = t'' - s' by A30,A31,ARYTM_0:def 2; A41: x' = x'' by A32,A35,ZFMISC_1:33; A42: s' = s'' by A33,A38,ZFMISC_1:33; now per cases; suppose A43: x' <=' t'; then A44: t' - x' = t' -' x' by ARYTM_1:def 2; s' <=' t' by A34,A41,A42,A43,ARYTM_1:3; then A45: t' - s' = t' -' s' by ARYTM_1:def 2; t' -' x' <=' t'' -' s' by A34,A36,A39,A41,A42,ARYTM_1:16; hence r + t <= s + t by A7,A36,A37,A39,A40,A44,A45,Def2; suppose not x' <=' t'; then A46: +(x1,z1) = [0,x' -' t'] by A37,ARYTM_1:def 2; then A47: +(x1,z1) in [:{0},REAL+:] by Lm3,ZFMISC_1:106; now per cases; suppose s' <=' t'; then t' - s' = t' -' s' by ARYTM_1:def 2; then not +(x1,z1) in REAL+ & not +(y1,z1) in [:{0},REAL+:] by A36,A39,A40,A47,ARYTM_0:5,XBOOLE_0:3; hence r + t <= s + t by A7,Def2; suppose not s' <=' t'; then A48: +(y1,z1) = [0,s' -' t'] by A36,A39,A40,ARYTM_1:def 2; then A49: +(y1,z1) in [:{0},REAL+:] by Lm3,ZFMISC_1:106; s' -' t' <=' x' -' t' by A34,A41,A42,ARYTM_1:17; hence r + t <= s + t by A7,A46,A47,A48,A49,Def2; end; hence thesis; end; hence thesis; suppose that A50: r in REAL+ and A51: s in REAL+ and A52: t in [:{0},REAL+:]; consider x'',s'' being Element of REAL+ such that A53: r = x'' and A54: s = s'' and A55: x'' <=' s'' by A1,A50,A51,Def2; consider x',t' being Element of REAL+ such that A56: r = x' and A57: t = [0,t'] and A58: +(x1,z1) = x' - t' by A50,A52,ARYTM_0:def 2; consider s',t'' being Element of REAL+ such that A59: s = s' and A60: t = [0,t''] and A61: +(y1,z1) = s' - t'' by A51,A52,ARYTM_0:def 2; A62: t' = t'' by A57,A60,ZFMISC_1:33; now per cases; suppose A63: t' <=' x'; then A64: x' - t' = x' -' t' by ARYTM_1:def 2; t' <=' s' by A53,A54,A55,A56,A59,A63,ARYTM_1:3; then A65: s' - t' = s' -' t' by ARYTM_1:def 2; x' -' t' <=' s' -' t'' by A53,A54,A55,A56,A59,A62,ARYTM_1:17; hence r + t <= s + t by A7,A58,A61,A62,A64,A65,Def2; suppose not t' <=' x'; then A66: +(x1,z1) = [0,t' -' x'] by A58,ARYTM_1:def 2; then A67: +(x1,z1) in [:{0},REAL+:] by Lm3,ZFMISC_1:106; now per cases; suppose t' <=' s'; then s' - t' = s' -' t' by ARYTM_1:def 2; then not +(x1,z1) in REAL+ & not +(y1,z1) in [:{0},REAL+:] by A61,A62,A67,ARYTM_0:5,XBOOLE_0:3; hence r + t <= s + t by A7,Def2; suppose not t' <=' s'; then A68: +(y1,z1) = [0,t' -' s'] by A61,A62,ARYTM_1:def 2; then A69: +(y1,z1) in [:{0},REAL+:] by Lm3,ZFMISC_1:106; t' -' s' <=' t' -' x' by A53,A54,A55,A56,A59,ARYTM_1:16; hence r + t <= s + t by A7,A66,A67,A68,A69,Def2; end; hence thesis; end; hence thesis; suppose that A70: r in [:{0},REAL+:] and A71: s in REAL+ and A72: t in [:{0},REAL+:]; not r in REAL+ & not t in REAL+ by A70,A72,ARYTM_0:5,XBOOLE_0:3; then consider x',t' being Element of REAL+ such that r = [0,x'] and A73: t = [0,t'] and A74: +(x1,z1) = [0,x' + t'] by ARYTM_0:def 2; consider s',t'' being Element of REAL+ such that s = s' and A75: t = [0,t''] and A76: +(y1,z1) = s' - t'' by A71,A72,ARYTM_0:def 2; A77: t' = t'' by A73,A75,ZFMISC_1:33; A78: +(x1,z1) in [:{0},REAL+:] by A74,Lm3,ZFMISC_1:106; now per cases; suppose t' <=' s'; then s' - t'' = s' -' t'' by A77,ARYTM_1:def 2; then not +(x1,z1) in REAL+ & not +(y1,z1) in [:{0},REAL+:] by A76,A78,ARYTM_0:5,XBOOLE_0:3; hence r + t <= s + t by A7,Def2; suppose not t' <=' s'; then A79: +(y1,z1) = [0,t' -' s'] by A76,A77,ARYTM_1:def 2; then A80: +(y1,z1) in [:{0},REAL+:] by Lm3,ZFMISC_1:106; A81: t' -' s' <=' t' by ARYTM_1:11; t' <=' t' + x' by ARYTM_2:20; then t' -' s' <=' t' + x' by A81,ARYTM_1:3; hence r + t <= s + t by A7,A74,A78,A79,A80,Def2; end; hence thesis; suppose that A82: r in [:{0},REAL+:] and A83: s in [:{0},REAL+:] and A84: t in [:{0},REAL+:]; consider x'',s'' being Element of REAL+ such that A85: r = [0,x''] and A86: s = [0,s''] and A87: s'' <=' x'' by A1,A82,A83,Def2; not r in REAL+ & not t in REAL+ by A82,A84,ARYTM_0:5,XBOOLE_0:3; then consider x',t' being Element of REAL+ such that A88: r = [0,x'] and A89: t = [0,t'] and A90: +(x1,z1) = [0,x' + t'] by ARYTM_0:def 2; not s in REAL+ & not t in REAL+ by A83,A84,ARYTM_0:5,XBOOLE_0:3; then consider s',t'' being Element of REAL+ such that A91: s = [0,s'] and A92: t = [0,t''] and A93: +(y1,z1) = [0,s' + t''] by ARYTM_0:def 2; A94: x' = x'' by A85,A88,ZFMISC_1:33; A95: s' = s'' by A86,A91,ZFMISC_1:33; A96: t' = t'' by A89,A92,ZFMISC_1:33; then A97: s' + t' <=' x' + t'' by A87,A94,A95,ARYTM_1:7; A98: +(x1,z1) in [:{0},REAL+:] by A90,Lm3,ZFMISC_1:106; +(y1,z1) in [:{0},REAL+:] by A93,Lm3,ZFMISC_1:106; hence r + t <= s + t by A7,A90,A93,A96,A97,A98,Def2; end; Lm6: r <= s & s <= t implies r <= t proof assume that A1: r <= s and A2: s <= t; r in REAL & s in REAL & t in REAL by Def1; then A3: r in REAL+ \/ [:{0},REAL+:] & s in REAL+ \/ [:{0},REAL+:] & t in REAL+ \/ [:{0},REAL+:] by NUMBERS:def 1,XBOOLE_0:def 4; per cases by A3,XBOOLE_0:def 2; suppose that A4: r in REAL+ and A5: s in REAL+ and A6: t in REAL+; consider x',s' being Element of REAL+ such that A7: r = x' and A8: s = s' and A9: x' <=' s' by A1,A4,A5,Def2; consider s'',t' being Element of REAL+ such that A10: s = s'' and A11: t = t' and A12: s'' <=' t' by A2,A5,A6,Def2; x' <=' t' by A8,A9,A10,A12,ARYTM_1:3; hence thesis by A7,A11,Def2; suppose A13: r in REAL+ & s in [:{0},REAL+:]; then not(r in REAL+ & s in REAL+) & not(r in [:{0},REAL+:] & s in [:{0},REAL+:]) by ARYTM_0:5,XBOOLE_0:3; hence thesis by A1,A13,Def2; suppose A14: s in REAL+ & t in [:{0},REAL+:]; then not(t in REAL+ & s in REAL+) & not(t in [:{0},REAL+:] & s in [:{0},REAL+:]) by ARYTM_0:5,XBOOLE_0:3; hence thesis by A2,A14,Def2; suppose that A15: r in [:{0},REAL+:] and A16: t in REAL+; not(r in REAL+ & t in REAL+) & not(r in [:{0},REAL+:] & t in [:{0},REAL+:]) by A15,A16,ARYTM_0:5,XBOOLE_0:3; hence thesis by A16,Def2; suppose that A17: r in [:{0},REAL+:] and A18: s in [:{0},REAL+:] and A19: t in [:{0},REAL+:]; consider x',s' being Element of REAL+ such that A20: r = [0,x'] and A21: s = [0,s'] and A22: s' <=' x' by A1,A17,A18,Def2; consider s'',t' being Element of REAL+ such that A23: s = [0,s''] and A24: t = [0,t'] and A25: t' <=' s'' by A2,A18,A19,Def2; s' = s'' by A21,A23,ZFMISC_1:33; then t' <=' x' by A22,A25,ARYTM_1:3; hence thesis by A17,A19,A20,A24,Def2; end; reconsider z = 0 as Element of REAL+ by ARYTM_2:21; Lm7: not 0 in [:{0},REAL+:] by ARYTM_0:5,ARYTM_2:21,XBOOLE_0:3; reconsider j = 1 as Element of REAL+ by Lm2,ARYTM_2:21; z <=' j by ARYTM_1:6; then Lm8:0 <= 1 by Def2; 1 + -1 = 0; then consider x1,x2,y1,y2 being Element of REAL such that Lm9: 1 = [*x1,x2*] and Lm10: -1 = [*y1,y2*] and Lm11: 0 = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4; Lm12: x1 = 1 by Lm1,Lm9; Lm13: y1 = -1 by Lm1,Lm10; Lm14: +(x1,y1) = 0 by Lm1,Lm11; Lm15: now assume -1 in REAL+; then ex x',y' being Element of REAL+ st x1 = x' & y1 = y' & z = x' + y' by Lm2,Lm12,Lm13,Lm14,ARYTM_0:def 2, ARYTM_2:21; hence contradiction by Lm12,ARYTM_2:6; end; Lm16: r >= 0 & s > 0 implies r + s > 0 proof assume r >= 0; then r + s >= 0 + s by Lm5; hence thesis by Lm6; end; Lm17: r <= 0 & s < 0 implies r + s < 0 proof assume r <= 0; then r + s <= 0 + s by Lm5; hence thesis by Lm6; end; reconsider o = 0 as Element of REAL+ by ARYTM_2:21; Lm18: r <= s & 0 <= t implies r * t <= s * t proof assume that A1: r <= s and A2: 0 <= t; reconsider x1=r, y1=s, z1=t as Element of REAL by Def1; for x' being Element of REAL, r st x' = r holds *(x',z1) = r * t proof let x' be Element of REAL, r such that A3: x' = r; consider x1,x2,y1,y2 being Element of REAL such that A4: r = [* x1,x2 *] and A5: t = [*y1,y2*] and A6: r*t = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *] by XCMPLX_0:def 5; A7: r = x1 & t = y1 by A4,A5,Lm1; A8: x2 = 0 & y2 = 0 by A4,A5,Lm1; then *(x1,y2) = 0 & *(x2,y1) = 0 by ARYTM_0:14; then A9: +(*(x1,y2),*(x2,y1)) = 0 by ARYTM_0:13; thus *(x',z1) = +(*(x1,y1),0) by A3,A7,ARYTM_0:13 .= +(*(x1,y1),*(opp x2,y2)) by A8,ARYTM_0:14 .= +(*(x1,y1),opp*(x2,y2)) by ARYTM_0:17 .= r * t by A6,A9,ARYTM_0:def 7; end; then A10: *(y1,z1) = s * t & *(x1,z1) = r * t; not o in [:{0},REAL+:] by ARYTM_0:5,XBOOLE_0:3; then A11: t in REAL+ by A2,Def2; assume A12: not thesis; then A13: t <> 0; per cases by A1,Def2; suppose that A14: r in REAL+ and A15: s in REAL+; consider x'',s'' being Element of REAL+ such that A16: r = x'' and A17: s = s'' and A18: x'' <=' s'' by A1,A14,A15,Def2; consider x',t' being Element of REAL+ such that A19: r = x' and A20: t = t' and A21: *(x1,z1) = x' *' t' by A11,A14,ARYTM_0:def 3; consider s',t'' being Element of REAL+ such that A22: s = s' and A23: t = t'' and A24: *(y1,z1) = s' *' t'' by A11,A15,ARYTM_0:def 3; x' *' t' <=' s' *' t' by A16,A17,A18,A19,A22,ARYTM_1:8; hence contradiction by A10,A12,A20,A21,A23,A24,Def2; suppose that A25: r in [:{0},REAL+:] and A26: s in REAL+; consider x',t' being Element of REAL+ such that r = [0,x'] and t = t' and A27: *(x1,z1) = [0,t' *' x'] by A11,A13,A25,ARYTM_0:def 3; consider s',t'' being Element of REAL+ such that s = s' and t = t'' and A28: *(y1,z1) = s' *' t'' by A11,A26,ARYTM_0:def 3; *(x1,z1) in [:{0},REAL+:] by A27,Lm3,ZFMISC_1:106; then not *(x1,z1) in REAL+ & not *(y1,z1) in [:{0},REAL+:] by A28,ARYTM_0:5,XBOOLE_0:3; hence contradiction by A10,A12,Def2; suppose that A29: r in [:{0},REAL+:] and A30: s in [:{0},REAL+:]; consider x'',s'' being Element of REAL+ such that A31: r = [0,x''] and A32: s = [0,s''] and A33: s'' <=' x'' by A1,A29,A30,Def2; consider x',t' being Element of REAL+ such that A34: r = [0,x'] and A35: t = t' and A36: *(x1,z1) = [0,t' *' x'] by A11,A13,A29,ARYTM_0:def 3; consider s',t'' being Element of REAL+ such that A37: s = [0,s'] and A38: t = t'' and A39: *(y1,z1) = [0,t'' *' s'] by A11,A13,A30,ARYTM_0:def 3; A40: x' = x'' by A31,A34,ZFMISC_1:33; A41: s' = s'' by A32,A37,ZFMISC_1:33; A42: *(x1,z1) in [:{0},REAL+:] & *(y1,z1) in [:{0},REAL+:] by A36,A39,Lm3,ZFMISC_1:106; s' *' t' <=' x' *' t' by A33,A40,A41,ARYTM_1:8; hence contradiction by A10,A12,A35,A36,A38,A39,A42,Def2; end; Lm19: (r * s) * t = r * (s * t) proof consider x1,x2,y1,y2 being Element of REAL such that A1: r = [*x1,x2*] and A2: s = [*y1,y2*] and A3: r*s = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *] by XCMPLX_0:def 5; consider y3,y4,z1,z2 being Element of REAL such that A4: s = [*y3,y4*] and A5: t = [*z1,z2*] and A6: s*t = [* +(*(y3,z1),opp*(y4,z2)), +(*(y3,z2),*(y4,z1)) *] by XCMPLX_0:def 5; A7: y1 = y3 & y2 = y4 by A2,A4,ARYTM_0:12; consider x3,x4,yz1,yz2 being Element of REAL such that A8: r = [*x3,x4*] and A9: s*t = [*yz1,yz2*] and A10: r*(s*t) = [* +(*(x3,yz1),opp*(x4,yz2)), +(*(x3,yz2),*(x4,yz1)) *] by XCMPLX_0:def 5; A11: x1 = x3 & x2 = x4 by A1,A8,ARYTM_0:12; consider xy1,xy2,z3,z4 being Element of REAL such that A12: r*s = [*xy1,xy2*] and A13: t = [*z3,z4*] and A14: (r*s)*t = [* +(*(xy1,z3),opp*(xy2,z4)), +(*(xy1,z4),*(xy2,z3)) *] by XCMPLX_0:def 5; A15: z1 = z3 & z2 = z4 by A5,A13,ARYTM_0:12; A16: xy1 = +(*(x1,y1),opp*(x2,y2)) & xy2 = +(*(x1,y2),*(x2,y1)) by A3,A12,ARYTM_0:12; A17: yz1 = +(*(y3,z1),opp*(y4,z2)) & yz2 = +(*(y3,z2),*(y4,z1)) by A6,A9,ARYTM_0:12; +(*(opp x4,*(y3,z2)),*(opp x4,*(y4,z1))) = +(*(opp x4,*(y4,z1)),*(*(opp x2,y1),z4)) by A7,A11,A15,ARYTM_0:15 .= +(*(*(opp x2,y2),z3),*(*(opp x2,y1),z4)) by A7,A11,A15,ARYTM_0:15; then A18: +(*(x3,*(opp y4,z2)),+(*(opp x4,*(y3,z2)),*(opp x4,*(y4,z1)))) = +(*(*(x1,opp y2),z4), +(*(*(opp x2,y2),z3),*(*(opp x2,y1),z4))) by A7,A11,A15,ARYTM_0:15 .= +(*(opp *(x1,y2),z4), +(*(*(opp x2,y2),z3),*(*(opp x2,y1),z4))) by ARYTM_0:17 .= +(*(*(opp x1,y2),z4), +(*(*(opp x2,y2),z3),*(*(opp x2,y1),z4))) by ARYTM_0:17 .= +(*(*(opp x2,y2),z3), +(*(*(opp x1,y2),z4),*(*(opp x2,y1),z4))) by ARYTM_0:25; A19: +(*(x3,yz1),opp*(x4,yz2)) = +(*(x3,yz1),*(opp x4,yz2)) by ARYTM_0:17 .= +(*(x3,+(*(y3,z1),*(opp y4,z2))),*(opp x4,yz2)) by A17,ARYTM_0:17 .= +(+(*(x3,*(y3,z1)),*(x3,*(opp y4,z2))), *(opp x4,+(*(y3,z2),*(y4,z1)))) by A17,ARYTM_0:16 .= +(+(*(x3,*(y3,z1)),*(x3,*(opp y4,z2))), +(*(opp x4,*(y3,z2)),*(opp x4,*(y4,z1)))) by ARYTM_0:16 .= +(*(x3,*(y3,z1)),+(*(*(opp x2,y2),z3), +(*(*(opp x1,y2),z4),*(*(opp x2,y1),z4)))) by A18,ARYTM_0:25 .= +(+(*(x3,*(y3,z1)),*(*(opp x2,y2),z3)), +(*(*(opp x1,y2),z4),*(*(opp x2,y1),z4))) by ARYTM_0:25 .= +(+(*(*(x1,y1),z3),*(*(opp x2,y2),z3)), +(*(*(opp x1,y2),z4),*(*(opp x2,y1),z4))) by A7,A11,A15,ARYTM_0:15 .= +(*(+(*(x1,y1),*(opp x2,y2)),z3), +(*(*(opp x1,y2),z4),*(*(opp x2,y1),z4))) by ARYTM_0:16 .= +(*(+(*(x1,y1),*(opp x2,y2)),z3), +(*(*(opp x1,y2),z4),*(opp *(x2,y1),z4))) by ARYTM_0:17 .= +(*(+(*(x1,y1),*(opp x2,y2)),z3), +(*(*(opp x1,y2),z4),opp *(*(x2,y1),z4))) by ARYTM_0:17 .= +(*(+(*(x1,y1),*(opp x2,y2)),z3), +(*(opp *(x1,y2),z4),opp *(*(x2,y1),z4))) by ARYTM_0:17 .= +(*(+(*(x1,y1),*(opp x2,y2)),z3), +(opp *(*(x1,y2),z4),opp *(*(x2,y1),z4))) by ARYTM_0:17 .= +(*(+(*(x1,y1),*(opp x2,y2)),z3), opp +(*(*(x1,y2),z4),*(*(x2,y1),z4))) by ARYTM_0:27 .= +(*(+(*(x1,y1),*(opp x2,y2)),z3), opp*( +(*(x1,y2),*(x2,y1)),z4)) by ARYTM_0:16 .= +(*(+(*(x1,y1),*(opp x2,y2)),z3),*(opp xy2,z4)) by A16,ARYTM_0:17 .= +(*(xy1,z3),*(opp xy2,z4)) by A16,ARYTM_0:17 .= +(*(xy1,z3),opp*(xy2,z4)) by ARYTM_0:17; A20: +(*(opp*(x2,y2),z4),*(*(x2,y1),z3)) = +(opp*(*(x2,y2),z4),*(*(x2,y1),z3)) by ARYTM_0:17 .= +(*(x4,*(y3,z1)),opp*(*(x2,y2),z4)) by A7,A11,A15,ARYTM_0:15 .= +(*(x4,*(y3,z1)),opp*(x4,*(y4,z2))) by A7,A11,A15,ARYTM_0:15 .= +(*(x4,*(y3,z1)),*(x4,opp*(y4,z2))) by ARYTM_0:17; A21: +(*(opp*(x2,y2),z4),*(xy2,z3)) = +(*(opp*(x2,y2),z4),+(*(*(x1,y2),z3),*(*(x2,y1),z3))) by A16,ARYTM_0:16 .= +(*(*(x1,y2),z3),+(*(opp*(x2,y2),z4),*(*(x2,y1),z3))) by ARYTM_0:25 .= +(*(x3,*(y4,z1)),+(*(x4,*(y3,z1)),*(x4,opp*(y4,z2)))) by A7,A11,A15,A20,ARYTM_0:15 .= +(*(x3,*(y4,z1)),*(x4,yz1)) by A17,ARYTM_0:16; +(*(xy1,z4),*(xy2,z3)) = +(+(*(*(x1,y1),z4),*(opp*(x2,y2),z4)),*(xy2,z3)) by A16,ARYTM_0:16 .= +(*(*(x1,y1),z4),+(*(opp*(x2,y2),z4),*(xy2,z3))) by ARYTM_0:25 .= +(*(x3,*(y3,z2)),+(*(x3,*(y4,z1)),*(x4,yz1))) by A7,A11,A15,A21,ARYTM_0:15 .= +(+(*(x3,*(y3,z2)),*(x3,*(y4,z1))),*(x4,yz1)) by ARYTM_0:25 .= +(*(x3,yz2),*(x4,yz1)) by A17,ARYTM_0:16; hence thesis by A10,A14,A19; end; Lm20: r*s = 0 implies r = 0 or s = 0 proof assume A1:r*s=0; assume A2:r<>0; r"*r*s=r"*0 by A1,Lm19; then 1*s=0 by A2,XCMPLX_0:def 7; hence thesis; end; Lm21: r > 0 & s > 0 implies r*s > 0 proof assume A1: r > 0 & s > 0; then A2: r * s >= 0 * s by Lm18; assume 0 >= r * s; then r * s = 0 by A2,Lm4; hence thesis by A1,Lm20; end; Lm22: r > 0 & s < 0 implies r*s < 0 proof assume A1: r > 0 & s < 0; then A2: r * s <= r * 0 by Lm18; assume 0 <= r * s; then r * s = 0 by A2,Lm4; hence thesis by A1,Lm20; end; Lm23: r <= s implies r - t <= s - t proof r <= s implies r + -t <= s + -t by Lm5; then r <= s implies r - t <= s + -t by XCMPLX_0:def 8; hence thesis by XCMPLX_0:def 8; end; Lm24: 0 - r = -r proof thus 0-r=0+ -r by XCMPLX_0:def 8 .=-r; end; Lm25: r + (s + t) = (r + s) + t proof consider x1,x2,y1,y2 being Element of REAL such that A1: r = [*x1,x2*] and A2: s = [*y1,y2*] and A3: r+s = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4; consider y3,y4,z1,z2 being Element of REAL such that A4: s = [*y3,y4*] and A5: t = [*z1,z2*] and A6: s+t = [*+(y3,z1),+(y4,z2)*] by XCMPLX_0:def 4; A7: y1 = y3 & y2 = y4 by A2,A4,ARYTM_0:12; consider x3,x4,yz1,yz2 being Element of REAL such that A8: r = [*x3,x4*] and A9: s+t = [*yz1,yz2*] and A10: r+(s+t) = [*+(x3,yz1),+(x4,yz2)*] by XCMPLX_0:def 4; A11: x1 = x3 & x2 = x4 by A1,A8,ARYTM_0:12; consider xy1,xy2,z3,z4 being Element of REAL such that A12: r+s = [*xy1,xy2*] and A13: t = [*z3,z4*] and A14: (r+s)+t = [*+(xy1,z3),+(xy2,z4)*] by XCMPLX_0:def 4; A15: z1 = z3 & z2 = z4 by A5,A13,ARYTM_0:12; A16: xy1 = +(x1,y1) & xy2 = +(x2,y2) by A3,A12,ARYTM_0:12; A17: yz1 = +(y1,z1) & yz2 = +(y2,z2) by A6,A7,A9,ARYTM_0:12; then +(x3,yz1) = +(xy1,z3) by A11,A15,A16,ARYTM_0:25; hence thesis by A10,A11,A14,A15,A16,A17,ARYTM_0:25; end; Lm26: s<=t implies -t<=-s proof assume s<=t; then s-t<=t-t by Lm23; then s-t<=t+ -t by XCMPLX_0:def 8; then s-t<=0 by XCMPLX_0:def 6; then s-t-s<=0-s by Lm23; then s-t-s<=-s by Lm24; then -s+(s-t)<=-s by XCMPLX_0:def 8; then -s+(s+ -t)<=-s by XCMPLX_0:def 8; then -s+s+ -t<=-s by Lm25; then 0+ -t<=-s by XCMPLX_0:def 6; hence thesis; end; Lm27: r <= 0 & s >= 0 implies r*s <= 0 proof assume that A1: r <= 0 and A2: s >= 0; per cases by A1,A2,Lm4; suppose r = 0 or s = 0; hence r * s <= 0; suppose r < 0 & s > 0; hence r * s <= 0 by Lm22; end; definition cluster positive -> non negative non zero (real number); coherence proof let r be real number; assume r > 0; hence r >= 0 & r <> 0; end; cluster non negative non zero -> positive (real number); coherence proof let r be real number; assume r >= 0 & r <> 0; hence r > 0 by Lm4; end; cluster negative -> non positive non zero (real number); coherence proof let r be real number; assume r < 0; hence r <= 0 & r <> 0; end; cluster non positive non zero -> negative (real number); coherence proof let r be real number; assume r <= 0 & r <> 0; hence r < 0 by Lm4; end; cluster zero -> non negative non positive (real number); coherence proof let r be real number; assume r = 0; hence r >= 0 & 0 >= r; end; cluster non negative non positive -> zero (real number); coherence proof let r be real number; assume r >= 0 & 0 >= r; hence r = 0 by Lm4; end; end; definition cluster positive (real number); existence proof take r = 1; thus 0 < r by Lm4,Lm8; end; cluster negative (real number); existence proof take r = -1; thus 0 > r by Def2,Lm7,Lm15; end; cluster zero (real number); existence proof take 0; thus thesis; end; end; definition let r,s be non negative (real number); cluster r + s -> non negative; coherence proof A1: r >= 0 & s >= 0 by Def4; per cases by A1,Lm4; suppose r = 0; hence r + s >= 0 by Def4; suppose r > 0; hence r+s >= 0 by A1,Lm16; end; end; definition let r,s be non positive (real number); cluster r + s -> non positive; coherence proof A1: r <= 0 & s <= 0 by Def3; per cases by A1,Lm4; suppose r = 0; hence r + s <= 0 by Def3; suppose r < 0; hence r + s <= 0 by A1,Lm17; end; end; definition let r be positive (real number); let s be non negative (real number); cluster r + s -> positive; coherence proof r > 0 & s >= 0 by Def3,Def4; hence r+s > 0 by Lm16; end; cluster s + r -> positive; coherence proof r > 0 & s >= 0 by Def3,Def4; hence s+r > 0 by Lm16; end; end; definition let r be negative (real number); let s be non positive (real number); cluster r + s -> negative; coherence proof r < 0 & s <= 0 by Def3,Def4; hence r+s < 0 by Lm17; end; cluster s + r -> negative; coherence proof r < 0 & s <= 0 by Def3,Def4; hence s+r < 0 by Lm17; end; end; definition let r be non positive (real number); cluster -r -> non negative; coherence proof A1: --r <= 0 by Def3; assume -r < 0; then -r+--r < 0 by A1,Lm17; hence contradiction by XCMPLX_0:def 6; end; end; definition let r be non negative (real number); cluster -r -> non positive; coherence proof A1: --r >= 0 by Def4; assume -r > 0; then -r+--r > 0 by A1,Lm16; hence contradiction by XCMPLX_0:def 6; end; end; definition let r be non negative (real number), s be non positive (real number); cluster r - s -> non negative; coherence proof r - s = r + -s by XCMPLX_0:def 8; hence thesis; end; cluster s - r -> non positive; coherence proof s - r = s + -r by XCMPLX_0:def 8; hence thesis; end; end; definition let r be positive (real number); let s be non positive (real number); cluster r - s -> positive; coherence proof r - s = r + -s by XCMPLX_0:def 8; hence thesis; end; cluster s - r -> negative; coherence proof s - r = s + -r by XCMPLX_0:def 8; hence thesis; end; end; definition let r be negative (real number); let s be non negative (real number); cluster r - s -> negative; coherence proof r - s = r + -s by XCMPLX_0:def 8; hence thesis; end; cluster s - r -> positive; coherence proof s - r = s + -r by XCMPLX_0:def 8; hence thesis; end; end; definition let r be non positive (real number), s be non negative (real number); cluster r*s -> non positive; coherence proof r <= 0 & s >= 0 by Def3,Def4; hence r*s <= 0 by Lm27; end; cluster s*r -> non positive; coherence proof r <= 0 & s >= 0 by Def3,Def4; hence s*r <= 0 by Lm27; end; end; Lm28: r * (s + t) = r * s + r * t proof consider y3,y4,z1,z2 being Element of REAL such that A1: s = [*y3,y4*] and A2: t = [*z1,z2*] and A3: s+t = [*+(y3,z1),+(y4,z2)*] by XCMPLX_0:def 4; consider x3,x4,yz1,yz2 being Element of REAL such that A4: r = [*x3,x4*] and A5: s+t = [*yz1,yz2*] and A6: r*(s+t) = [* +(*(x3,yz1),opp*(x4,yz2)), +(*(x3,yz2),*(x4,yz1)) *] by XCMPLX_0:def 5; consider x1,x2,y1,y2 being Element of REAL such that A7: r = [*x1,x2*] and A8: s = [*y1,y2*] and A9: r*s = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *] by XCMPLX_0:def 5; A10: y1 = y3 & y2 = y4 by A1,A8,ARYTM_0:12; consider x5,x6,z3,z4 being Element of REAL such that A11: r = [*x5,x6*] and A12: t = [*z3,z4*] and A13: r*t = [* +(*(x5,z3),opp*(x6,z4)), +(*(x5,z4),*(x6,z3)) *] by XCMPLX_0:def 5; A14: x1 = x3 & x2 = x4 & x1 = x5 & x2 = x6 by A4,A7,A11,ARYTM_0:12; A15: z1 = z3 & z2 = z4 by A2,A12,ARYTM_0:12; consider xy3,xy4,xz1,xz2 being Element of REAL such that A16: r*s = [*xy3,xy4*] and A17: r*t = [*xz1,xz2*] and A18: r*s+r*t = [*+(xy3,xz1),+(xy4,xz2)*] by XCMPLX_0:def 4; A19: yz1 = +(y3,z1) & yz2 = +(y4,z2) by A3,A5,ARYTM_0:12; A20: xy3 = +(*(x1,y1),opp*(x2,y2)) & xy4 = +(*(x1,y2),*(x2,y1)) by A9,A16,ARYTM_0:12; A21: xz1 = +(*(x5,z3),opp*(x6,z4)) & xz2 = +(*(x5,z4),*(x6,z3)) by A13,A17,ARYTM_0:12; *(x4,yz2) = +(*(x2,y2),*(x6,z4)) by A10,A14,A15,A19,ARYTM_0:16; then opp*(x4,yz2) = +(opp*(x2,y2),opp*(x6,z4)) by ARYTM_0:27; then A22: +(*(x3,z1),opp*(x4,yz2)) = +(opp*(x2,y2),xz1) by A14,A15,A21,ARYTM_0:25; A23: +(*(x3,yz1),opp*(x4,yz2)) = +(+(*(x3,y3),*(x3,z1)),opp*(x4,yz2)) by A19,ARYTM_0:16 .= +(*(x1,y1),+(opp*(x2,y2),xz1)) by A10,A14,A22,ARYTM_0:25 .= +(xy3,xz1) by A20,ARYTM_0:25; *(x4,yz1) = +(*(x2,y1),*(x6,z3)) by A10,A14,A15,A19,ARYTM_0:16; then A24: +(*(x3,z2),*(x4,yz1)) = +(*(x2,y1),xz2) by A14,A15,A21,ARYTM_0:25; +(*(x3,yz2),*(x4,yz1)) = +(+(*(x3,y4),*(x3,z2)),*(x4,yz1)) by A19,ARYTM_0:16 .= +(*(x1,y2),+(*(x2,y1),xz2)) by A10,A14,A24,ARYTM_0:25 .= +(xy4,xz2) by A20,ARYTM_0:25; hence thesis by A6,A18,A23; end; Lm29: (- r) * s = -(r * s) proof thus (-r)*s = (-r)*s + 0 .= (-r)*s + (r*s + -(r*s)) by XCMPLX_0:def 6 .= (-r)*s + r*s + -(r*s) by Lm25 .= (-r + r)*s + -(r*s) by Lm28 .= 0*s+ -(r*s) by XCMPLX_0:def 6 .= -(r*s); end; definition let r,s be non positive (real number); cluster r*s -> non negative; coherence proof A1: r <= 0 & s <= 0 by Def3; per cases by A1,Lm4; suppose r = 0 or s = 0; hence r * s >= 0; suppose A2: --r < --0 & s < 0; then 0<-r by Lm26; then A3: s*(-r)<=0*(-r) by A2,Lm18; s*1 <> 0*((-r)*(-r)") by A2; then s*((-r)*(-r)") <> 0*(-r)*(-r)" by A2,XCMPLX_0:def 7; then s*(-r)<>0*(-r) by Lm19; then s*(-r)<0*(-r) by A3,Lm4; then -(s*r)<0*(-r) by Lm29; then --0*r<--s*r by Lm26; hence r * s >= 0; end; end; definition let r,s be non negative (real number); cluster r*s -> non negative; coherence proof A1: r >= 0 & s >= 0 by Def4; per cases by A1,Lm4; suppose r = 0 or s = 0; hence r * s >= 0; suppose r > 0 & s > 0; hence r * s >= 0 by Lm21; end; end; Lm30: r" = 0 implies r = 0 proof assume A1:r"=0; assume A2:r<>0; r"*r=0 by A1; hence contradiction by A2,XCMPLX_0:def 7; end; definition let r be non positive (real number); cluster r" -> non positive; coherence proof A1: r"" <= 0 by Def3; assume that A2: r" > 0; per cases by A1,Lm4; suppose r"" = 0; hence contradiction by A2,Lm30; suppose A3: r"" < 0; r"*r"" = 1 by A2,XCMPLX_0:def 7; hence contradiction by A2,A3,Lm8,Lm22; end; end; definition let r be non negative (real number); cluster r" -> non negative; coherence proof A1: r"" >= 0 by Def4; assume that A2: r" < 0; per cases by A1,Lm4; suppose r"" = 0; hence contradiction by A2,Lm30; suppose A3: r"" > 0; r"*r"" = 1 by A2,XCMPLX_0:def 7; hence contradiction by A2,A3,Lm8,Lm22; end; end; definition let r be non negative (real number), s be non positive (real number); cluster r/s -> non positive; coherence proof r/s = r*s" by XCMPLX_0:def 9; hence thesis; end; cluster s/r -> non positive; coherence proof s/r = s*r" by XCMPLX_0:def 9; hence thesis; end; end; definition let r,s be non negative (real number); cluster r/s -> non negative; coherence proof r/s = r*s" by XCMPLX_0:def 9; hence thesis; end; end; definition let r,s be non positive (real number); cluster r/s -> non negative; coherence proof r/s = r*s" by XCMPLX_0:def 9; hence thesis; end; end;

Back to top