:: Introduction to Arithmetics
:: by Andrzej Trybulec
::
:: Received January 9, 2003
:: Copyright (c) 2003-2016 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);