The abstract of the Mizar article:

Arithmetic of Non-Negative Rational Numbers

by

Grzegorz Bancerek

Received March 7, 1998

MML identifier: ARYTM_3

[ Mizar article, MML identifier index ]

environ

 vocabulary ORDINAL1, ORDINAL2, BOOLE, ORDINAL3, ARYTM_3, QUOFIELD;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, ORDINAL3;
 constructors ORDINAL3, SUBSET_1, XBOOLE_0;
 clusters ORDINAL1, ORDINAL2, SUBSET_1, ZFMISC_1, XBOOLE_0;
 requirements BOOLE, SUBSET;


begin :: Natural ordinals

reserve A,B,C for Ordinal;

definition
 let A be Ordinal;
 cluster -> ordinal Element of A;
end;

definition
 cluster empty -> natural Ordinal;
 cluster one -> natural non empty;
 cluster -> natural Element of omega;
end;

definition
 cluster non empty natural Ordinal;
end;

definition let a be natural Ordinal;
 cluster succ a -> natural;
end;

scheme Omega_Ind {P[set]}:
 for a being natural Ordinal holds P[a]
provided
   P[{}]
and
   for a being natural Ordinal st P[a] holds P[succ a];

definition
 let a, b be natural Ordinal;
 cluster a +^ b -> natural;
end;

theorem :: ARYTM_3:1
 for a,b being Ordinal st a+^b is natural holds a in omega & b in omega;

definition
 let a, b be natural Ordinal;
 cluster a -^ b -> natural;
 cluster a *^ b -> natural;
end;

theorem :: ARYTM_3:2
 for a,b being Ordinal st a*^b is natural non empty
  holds a in omega & b in omega;

theorem :: ARYTM_3:3
 for a,b being natural Ordinal holds a+^b = b+^a;

theorem :: ARYTM_3:4
 for a,b being natural Ordinal holds a*^b = b*^a;

definition redefine
 let a,b be natural Ordinal;
 func a+^b; commutativity;
 func a*^b; commutativity;
end;

begin :: Relative prime numbers and divisibility

definition
 let a,b be Ordinal;
 pred a,b are_relative_prime means
:: ARYTM_3:def 1

  for c,d1,d2 being Ordinal st a = c *^ d1 & b = c *^ d2
   holds c = one;
 symmetry;
end;

theorem :: ARYTM_3:5
 not {},{} are_relative_prime;

theorem :: ARYTM_3:6
 one,A are_relative_prime;

theorem :: ARYTM_3:7
 {},A are_relative_prime implies A = one;

reserve a,b,c,d for natural Ordinal;

theorem :: ARYTM_3:8
   a <> {} or b <> {} implies
  ex c,d1,d2 being natural Ordinal st
   d1,d2 are_relative_prime & a = c *^ d1 & b = c *^ d2;

reserve l,m,n for natural Ordinal;

definition let m,n;
 cluster m div^ n -> natural;
 cluster m mod^ n -> natural;
end;

definition
 let k,n be Ordinal;
 pred k divides n means
:: ARYTM_3:def 2
ex a being Ordinal st n = k*^a;
 reflexivity;
end;

theorem :: ARYTM_3:9
 a divides b iff ex c st b = a*^c;

theorem :: ARYTM_3:10
 for m,n st {} in m holds n mod^ m in m;

theorem :: ARYTM_3:11
 for n,m holds m divides n iff n = m *^ (n div^ m);

canceled;

theorem :: ARYTM_3:13
 for n,m st n divides m & m divides n holds n = m;

theorem :: ARYTM_3:14
 n divides {} & one divides n;

theorem :: ARYTM_3:15
 for n,m st {} in m & n divides m holds n c= m;

theorem :: ARYTM_3:16
 for n,m,l st n divides m & n divides m +^ l holds n divides l;

definition let k,n be natural Ordinal;
 func k lcm n -> Element of omega means
:: ARYTM_3:def 3
  k divides it & n divides it & for m st k divides m & n divides
 m holds it divides m;
  commutativity;
end;

theorem :: ARYTM_3:17
 m lcm n divides m*^n;

theorem :: ARYTM_3:18
 n <> {} implies (m*^n) div^ (m lcm n) divides m;

definition let k,n be natural Ordinal;
 func k hcf n -> Element of omega means
:: ARYTM_3:def 4
  it divides k & it divides n & for m st m divides k & m divides
 n holds m divides it;
  commutativity;
end;

theorem :: ARYTM_3:19
 a hcf {} = a & a lcm {} = {};

theorem :: ARYTM_3:20
 a hcf b = {} implies a = {};

theorem :: ARYTM_3:21
 a hcf a = a & a lcm a = a;

theorem :: ARYTM_3:22
 (a*^c) hcf (b*^c) = (a hcf b)*^c;

theorem :: ARYTM_3:23
 b <> {} implies a hcf b <> {} & b div^ (a hcf b) <> {};

theorem :: ARYTM_3:24
 a <> {} or b <> {} implies
  a div^ (a hcf b), b div^ (a hcf b) are_relative_prime;

theorem :: ARYTM_3:25
 a,b are_relative_prime iff a hcf b = one;

definition let a,b be natural Ordinal;
 func RED(a,b) -> Element of omega equals
:: ARYTM_3:def 5

  a div^ (a hcf b);
end;

theorem :: ARYTM_3:26
 RED(a,b)*^(a hcf b) = a;

theorem :: ARYTM_3:27
 a <> {} or b <> {} implies RED(a,b), RED(b,a) are_relative_prime;

theorem :: ARYTM_3:28
 a,b are_relative_prime implies RED(a,b) = a;

theorem :: ARYTM_3:29
 RED(a,one) = a & RED(one,a) = one;

theorem :: ARYTM_3:30
 b <> {} implies RED(b,a) <> {};

theorem :: ARYTM_3:31
 RED({},a) = {} & (a <> {} implies RED(a,{}) = one);

theorem :: ARYTM_3:32
 a <> {} implies RED(a,a) = one;

theorem :: ARYTM_3:33
 c <> {} implies RED(a*^c, b*^c) = RED(a, b);

begin :: Non negative rationals

reserve i,j,k for Element of omega;

definition
 func RAT+ equals
:: ARYTM_3:def 6

  ({[i,j]: i,j are_relative_prime & j <> {}} \ {[k,one]: not contradiction})
  \/ omega;
end;

theorem :: ARYTM_3:34
 omega c= RAT+;

reserve x,y,z for Element of RAT+;

definition
 cluster RAT+ -> non empty;
end;

definition
 cluster non empty ordinal Element of RAT+;
end;

theorem :: ARYTM_3:35
 x in
 omega or ex i,j st x = [i,j] & i,j are_relative_prime & j <> {} & j <> one;

theorem :: ARYTM_3:36
 not ex i,j being set st [i,j] is Ordinal;

theorem :: ARYTM_3:37
 A in RAT+ implies A in omega;

definition
 cluster -> natural (ordinal Element of RAT+);
end;

theorem :: ARYTM_3:38
 not ex i,j being set st [i,j] in omega;

theorem :: ARYTM_3:39
 [i,j] in RAT+ iff i,j are_relative_prime & j <> {} & j <> one;

definition
 let x be Element of RAT+;
 func numerator x -> Element of omega means
:: ARYTM_3:def 7

  it = x if x in omega otherwise ex a st x = [it,a];
 func denominator x -> Element of omega means
:: ARYTM_3:def 8

  it = one if x in omega otherwise ex a st x = [a,it];
end;

theorem :: ARYTM_3:40
 numerator x, denominator x are_relative_prime;

theorem :: ARYTM_3:41
 denominator x <> {};

theorem :: ARYTM_3:42
 not x in omega implies x = [numerator x, denominator x] & denominator x <> one
;

theorem :: ARYTM_3:43
 x <> {} iff numerator x <> {};

theorem :: ARYTM_3:44
  x in omega iff denominator x = one;

definition
 let i,j be natural Ordinal;
 func i/j -> Element of RAT+ equals
:: ARYTM_3:def 9

  {} if j = {},
  RED(i,j) if RED(j,i) = one otherwise
  [RED(i,j), RED(j,i)];
 synonym quotient(i,j);
end;

theorem :: ARYTM_3:45
 (numerator x)/(denominator x) = x;

theorem :: ARYTM_3:46
 {}/b = {} & a/one = a;

theorem :: ARYTM_3:47
 a <> {} implies a/a = one;

theorem :: ARYTM_3:48
 b <> {} implies numerator (a/b) = RED(a,b) & denominator (a/b) = RED(b,a);

theorem :: ARYTM_3:49
 i,j are_relative_prime & j <> {} implies
   numerator (i/j) = i & denominator (i/j) = j;

theorem :: ARYTM_3:50
 c <> {} implies (a*^c)/(b*^c) = a/b;

reserve i,j,k for natural Ordinal;

theorem :: ARYTM_3:51
 j <> {} & l <> {} implies (i/j = k/l iff i*^l = j*^k);

definition
 let x,y be Element of RAT+;
 func x+y -> Element of RAT+ equals
:: ARYTM_3:def 10

  ((numerator x)*^(denominator y)+^(numerator y)*^(denominator x))
   / ((denominator x)*^(denominator y));
 commutativity;
 func x*'y -> Element of RAT+ equals
:: ARYTM_3:def 11

  ((numerator x)*^(numerator y)) / ((denominator x)*^(denominator y));
 commutativity;
end;

theorem :: ARYTM_3:52
 j <> {} & l <> {} implies (i/j)+(k/l) = (i*^l+^j*^k)/(j*^l);

theorem :: ARYTM_3:53
 k <> {} implies (i/k)+(j/k) = (i+^j)/k;

definition
 cluster empty Element of RAT+;
end;

definition
 redefine
 func {} -> empty Element of RAT+;
 func one -> non empty ordinal Element of RAT+;
end;

theorem :: ARYTM_3:54
 x*'{} = {};

theorem :: ARYTM_3:55
 (i/j)*'(k/l) = (i*^k)/(j*^l);

theorem :: ARYTM_3:56
 x+{} = x;

theorem :: ARYTM_3:57
 (x+y)+z = x+(y+z);

theorem :: ARYTM_3:58
 (x*'y)*'z = x*'(y*'z);

theorem :: ARYTM_3:59
 x*'one = x;

theorem :: ARYTM_3:60
 x <> {} implies ex y st x*'y = one;

theorem :: ARYTM_3:61
 x <> {} implies ex z st y = x*'z;

theorem :: ARYTM_3:62
 x <> {} & x*'y = x*'z implies y = z;

theorem :: ARYTM_3:63
 x*'(y+z) = x*'y+x*'z;

theorem :: ARYTM_3:64
 for i,j being ordinal Element of RAT+ holds i+j = i+^j;

theorem :: ARYTM_3:65
   for i,j being ordinal Element of RAT+ holds i*'j = i*^j;

theorem :: ARYTM_3:66
 ex y st x = y+y;

definition
 let x,y be Element of RAT+;
 pred x <=' y means
:: ARYTM_3:def 12

  ex z being Element of RAT+ st y = x+z;
 connectedness;
 antonym y < x;
end;

reserve r,s,t for Element of RAT+;

canceled;

theorem :: ARYTM_3:68
   not ex y being set st [{},y] in RAT+;

theorem :: ARYTM_3:69
 s + t = r + t implies s = r;

theorem :: ARYTM_3:70
 r+s = {} implies r = {};

theorem :: ARYTM_3:71
 {} <=' s;

theorem :: ARYTM_3:72
   s <=' {} implies s = {};

theorem :: ARYTM_3:73
 r <=' s & s <=' r implies r = s;

theorem :: ARYTM_3:74
 r <=' s & s <=' t implies r <=' t;

theorem :: ARYTM_3:75
   r < s iff r <=' s & r <> s;

theorem :: ARYTM_3:76
  r < s & s <=' t or r <=' s & s < t implies r < t;

theorem :: ARYTM_3:77
   r < s & s < t implies r < t;

theorem :: ARYTM_3:78
 x in omega & x+y in omega implies y in omega;

theorem :: ARYTM_3:79
 for i being ordinal Element of RAT+
  st i < x & x < i+one
  holds not x in omega;

theorem :: ARYTM_3:80
 t <> {} implies ex r st r < t & not r in omega;

theorem :: ARYTM_3:81
   {s: s < t} in RAT+ iff t = {};

theorem :: ARYTM_3:82
   for A being Subset of RAT+ st
  (ex t st t in A & t <> {}) &   ::  dodany warunek ?!
  for r,s st r in A & s <=' r holds s in A
 ex r1,r2,r3 being Element of RAT+ st
  r1 in A & r2 in A & r3 in A &
  r1 <> r2 & r2 <> r3 & r3 <> r1;

theorem :: ARYTM_3:83
 s + t <=' r + t iff s <=' r;

canceled;

theorem :: ARYTM_3:85
   s <=' s + t;

theorem :: ARYTM_3:86
 r*'s = {} implies r = {} or s = {};

theorem :: ARYTM_3:87
 r <=' s *' t implies
  ex t0 being Element of RAT+ st r = s *' t0 & t0 <=' t;

theorem :: ARYTM_3:88
   t <> {} & s *' t <=' r *' t implies s <=' r;

theorem :: ARYTM_3:89
   for r1,r2,s1,s2 being Element of RAT+ st r1+r2 = s1+s2
  holds r1 <=' s1 or r2 <=' s2;

theorem :: ARYTM_3:90
 s <=' r implies s *' t <=' r *' t;

theorem :: ARYTM_3:91
   for r1,r2,s1,s2 being Element of RAT+ st r1*'r2 = s1*'s2
  holds r1 <=' s1 or r2 <=' s2;

theorem :: ARYTM_3:92
   r = {} iff r + s = s;

theorem :: ARYTM_3:93
   for s1,t1,s2,t2 being Element of RAT+ st s1 + t1 = s2 + t2 & s1 <=' s2
  holds t2 <=' t1;

theorem :: ARYTM_3:94
 r <=' s & s <=' r + t implies
  ex t0 being Element of RAT+ st s = r + t0 & t0 <=' t;

theorem :: ARYTM_3:95
   r <=' s + t implies
  ex s0,t0 being Element of RAT+ st r = s0 + t0 & s0 <=' s & t0 <=' t;

theorem :: ARYTM_3:96
   r < s & r < t implies
  ex t0 being Element of RAT+ st t0 <=' s & t0 <=' t & r < t0;

theorem :: ARYTM_3:97
   r <=' s & s <=' t & s <> t implies r <> t;

theorem :: ARYTM_3:98
   s < r + t & t <> {} implies
  ex r0,t0 being Element of RAT+ st s = r0 + t0 &
    r0 <=' r & t0 <=' t & t0 <> t;

theorem :: ARYTM_3:99
   for A being non empty Subset of RAT+ st A in RAT+
  ex s st s in A & for r st r in A holds r <=' s;

theorem :: ARYTM_3:100
   ex t st r + t = s or s + t = r;

theorem :: ARYTM_3:101
   r < s implies ex t st r < t & t < s;

theorem :: ARYTM_3:102
   ex s st r < s;

theorem :: ARYTM_3:103
   t <> {} implies ex s st s in omega & r <=' s *' t;

scheme DisNat { n0,n1,n2() -> Element of RAT+, P[set] }:
 ex s st s in omega & P[s] & not P[s + n1()]
provided
 n1() = one and
 n0() = {} and
 n2() in omega and
 P[n0()] and
 not P[n2()];