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