Addenda , 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

### The abstract of the Mizar article:

### Introduction to Arithmetics

**by****Andrzej Trybulec**- Received January 9, 2003
- MML identifier: ARYTM_0

- [ Mizar article, 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; 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 theorem :: ARYTM_0:6 for x,y being Element of REAL+ st x - y = {} holds x = y; theorem :: ARYTM_0:7 not ex a,b being set st one = [a,b]; theorem :: ARYTM_0:8 for x,y,z being Element of REAL+ st x <> {} & x *' y = x *' z holds y = z; canceled; begin :: from XREAL_0 definition let x,y be Element of REAL; canceled; func +(x,y) -> Element of REAL means :: ARYTM_0:def 2 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']; commutativity; func *(x,y) -> Element of REAL means :: ARYTM_0:def 3 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; 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 4 +(x,it) = 0; involutiveness; func inv x -> Element of REAL means :: ARYTM_0:def 5 *(x,it) = one 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:10 not (0,one)-->(a,b) in REAL; definition let x,y be Element of REAL; canceled; func [*x,y*] -> Element of COMPLEX equals :: ARYTM_0:def 7 x if y = 0 otherwise (0,one) --> (x,y); end; theorem :: ARYTM_0:11 for c being Element of COMPLEX ex r,s being Element of REAL st c = [*r,s*]; theorem :: ARYTM_0:12 for x1,x2,y1,y2 being Element of REAL st [*x1,x2*] = [*y1,y2*] holds x1 = y1 & x2 = y2; theorem :: ARYTM_0:13 for x,o being Element of REAL st o = 0 holds +(x,o) = x; theorem :: ARYTM_0:14 for x,o being Element of REAL st o = 0 holds *(x,o) = 0; theorem :: ARYTM_0:15 for x,y,z being Element of REAL holds *(x,*(y,z)) = *(*(x,y),z); theorem :: ARYTM_0:16 for x,y,z being Element of REAL holds *(x,+(y,z)) = +(*(x,y),*(x,z)); theorem :: ARYTM_0:17 for x,y being Element of REAL holds *(opp x,y) = opp *(x,y); theorem :: ARYTM_0:18 for x being Element of REAL holds *(x,x) in REAL+; theorem :: ARYTM_0:19 for x,y st +(*(x,x),*(y,y)) = 0 holds x = 0; theorem :: ARYTM_0:20 for x,y,z being Element of REAL st x <> 0 & *(x,y) = one & *(x,z) = one holds y = z; theorem :: ARYTM_0:21 for x,y st y = one holds *(x,y) = x; theorem :: ARYTM_0:22 for x,y st y <> 0 holds *(*(x,y),inv y) = x; theorem :: ARYTM_0:23 for x,y st *(x,y) = 0 holds x = 0 or y = 0; theorem :: ARYTM_0:24 for x,y holds inv *(x,y) = *(inv x, inv y); theorem :: ARYTM_0:25 for x,y,z being Element of REAL holds +(x,+(y,z)) = +(+(x,y),z); theorem :: ARYTM_0:26 [*x,y*] in REAL implies y = 0; theorem :: ARYTM_0:27 for x,y being Element of REAL holds opp +(x,y) = +(opp x, opp y);

Back to top