:: Introduction to Arithmetics :: by Andrzej Trybulec :: :: Received January 9, 2003 :: Copyright (c) 2003-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, ARYTM_2, TARSKI, NUMBERS, ZFMISC_1, SUBSET_1, ARYTM_1, ARYTM_3, CARD_1, RELAT_1, FUNCOP_1, ORDINAL1, FUNCT_2, FUNCT_1, ARYTM_0, XCMPLX_0; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, ORDINAL1, ARYTM_3, ARYTM_2, ARYTM_1, NUMBERS; constructors FUNCT_4, ARYTM_1, NUMBERS, XTUPLE_0; registrations XBOOLE_0, ORDINAL1, FUNCT_2, FUNCT_4, ARYTM_2, FUNCT_1, NUMBERS; requirements BOOLE, SUBSET, NUMERALS; begin theorem :: ARYTM_0:1 REAL+ c= REAL; theorem :: ARYTM_0:2 for x being Element of REAL+ st x <> {} holds [{},x] in REAL; theorem :: ARYTM_0:3 for y being set st [{},y] in REAL holds y <> {}; theorem :: ARYTM_0:4 for x,y being Element of REAL+ holds x - y in REAL; theorem :: ARYTM_0:5 REAL+ misses [:{{}},REAL+:]; begin :: Real numbers registration let x,y be object; cluster [x,y] -> non zero; end; theorem :: ARYTM_0:6 for x,y being Element of REAL+ st x - y = {} holds x = y; theorem :: ARYTM_0:7 for x,y,z being Element of REAL+ st x <> {} & x *' y = x *' z holds y = z; begin definition let x,y be Element of REAL; func +(x,y) -> Element of REAL means :: ARYTM_0:def 1 ex x9,y9 being Element of REAL+ st x = x9 & y = y9 & it = x9 + y9 if x in REAL+ & y in REAL+, ex x9,y9 being Element of REAL+ st x = x9 & y = [0,y9] & it = x9 - y9 if x in REAL+ & y in [:{ 0},REAL+:], ex x9,y9 being Element of REAL+ st x = [0,x9] & y = y9 & it = y9 - x9 if y in REAL+ & x in [:{0},REAL+:] otherwise ex x9,y9 being Element of REAL+ st x = [0,x9] & y = [0,y9] & it = [0,x9+y9]; commutativity; func *(x,y) -> Element of REAL means :: ARYTM_0:def 2 ex x9,y9 being Element of REAL+ st x = x9 & y = y9 & it = x9 *' y9 if x in REAL+ & y in REAL+, ex x9,y9 being Element of REAL+ st x = x9 & y = [0,y9] & it = [0,x9 *' y9] if x in REAL+ & y in [:{0},REAL+:] & x <> 0, ex x9,y9 being Element of REAL+ st x = [0,x9] & y = y9 & it = [0,y9 *' x9] if y in REAL+ & x in [:{0},REAL+:] & y <> 0, ex x9,y9 being Element of REAL+ st x = [0,x9] & y = [0,y9] & it = y9 *' x9 if x in [:{0} ,REAL+:] & y in [:{0},REAL+:] otherwise it = 0; commutativity; end; reserve x,y for Element of REAL; definition let x be Element of REAL; func opp x -> Element of REAL means :: ARYTM_0:def 3 +(x,it) = 0; involutiveness; func inv x -> Element of REAL means :: ARYTM_0:def 4 *(x,it) = 1 if x <> 0 otherwise it = 0; involutiveness; end; begin reserve i,j,k for Element of NAT; reserve a,b for Element of REAL; theorem :: ARYTM_0:8 not (0,1)-->(a,b) in REAL; definition let x,y be Element of REAL; func [*x,y*] -> Element of COMPLEX equals :: ARYTM_0:def 5 x if y = 0 otherwise (0,1) --> (x,y); end; theorem :: ARYTM_0:9 for c being Element of COMPLEX ex r,s being Element of REAL st c = [*r ,s*]; theorem :: ARYTM_0:10 for x1,x2,y1,y2 being Element of REAL st [*x1,x2*] = [*y1,y2*] holds x1 = y1 & x2 = y2; theorem :: ARYTM_0:11 for x,o being Element of REAL st o = 0 holds +(x,o) = x; theorem :: ARYTM_0:12 for x,o being Element of REAL st o = 0 holds *(x,o) = 0; theorem :: ARYTM_0:13 for x,y,z being Element of REAL holds *(x,*(y,z)) = *(*(x,y),z); theorem :: ARYTM_0:14 for x,y,z being Element of REAL holds *(x,+(y,z)) = +(*(x,y),*(x ,z)); theorem :: ARYTM_0:15 for x,y being Element of REAL holds *(opp x,y) = opp *(x,y); theorem :: ARYTM_0:16 for x being Element of REAL holds *(x,x) in REAL+; theorem :: ARYTM_0:17 for x,y st +(*(x,x),*(y,y)) = 0 holds x = 0; theorem :: ARYTM_0:18 for x,y,z being Element of REAL st x <> 0 & *(x,y) = 1 & *(x,z) = 1 holds y = z; theorem :: ARYTM_0:19 for x,y st y = 1 holds *(x,y) = x; theorem :: ARYTM_0:20 for x,y st y <> 0 holds *(*(x,y),inv y) = x; theorem :: ARYTM_0:21 for x,y st *(x,y) = 0 holds x = 0 or y = 0; theorem :: ARYTM_0:22 for x,y holds inv *(x,y) = *(inv x, inv y); theorem :: ARYTM_0:23 for x,y,z being Element of REAL holds +(x,+(y,z)) = +(+(x,y),z); theorem :: ARYTM_0:24 [*x,y*] in REAL implies y = 0; theorem :: ARYTM_0:25 for x,y being Element of REAL holds opp +(x,y) = +(opp x, opp y);