Journal of Formalized Mathematics
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

### Introduction to Arithmetics

by
Andrzej Trybulec

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);

```