:: Arithmetic of Non Negative Rational Numbers
::  by Grzegorz Bancerek
::
:: Received March 7, 1998
:: Copyright (c) 1998 Association of Mizar Users

environ

 vocabularies ORDINAL1, ORDINAL2, BOOLE, ORDINAL3, ARYTM_3, QUOFIELD;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, ORDINAL3;
 constructors SUBSET_1, ORDINAL3;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, ORDINAL3;
 requirements BOOLE, SUBSET, NUMERALS;
 definitions TARSKI, ORDINAL1;
 theorems TARSKI, XBOOLE_0, ZFMISC_1, ORDINAL1, ORDINAL2, ORDINAL3, XBOOLE_1;
 schemes ORDINAL1;

begin :: Natural ordinals

reserve A,B,C for Ordinal;

Lm1: {} in omega by ORDINAL1:def 12;

Lm2: 1 in omega;

definition
  func one equals

  1;
  correctness;
end;

begin :: Relative prime numbers and divisibility

definition
  let a,b be Ordinal;
  pred a,b are_relative_prime means
  :Def2:
  for c,d1,d2 being Ordinal st a = c *^ d1 & b = c *^ d2 holds c = 1;
  symmetry;
end;

canceled 4;

theorem Th5:
  not {},{} are_relative_prime
proof
  take {}, {}, {};
  thus thesis by ORDINAL2:52;
end;

theorem Th6:
  1,A are_relative_prime
proof
  let c,d1,d2 be Ordinal;
  thus thesis by ORDINAL3:41;
end;

theorem Th7:
  {},A are_relative_prime implies A = 1
proof
  assume
A1: {},A are_relative_prime & A <> 1;
  then A in 1 or 1 in A by ORDINAL1:24;
  then 1 in A & {} = A*^{} & A = A*^1 by A1,Th5,ORDINAL2:55,56,ORDINAL3:17;
  hence contradiction by A1,Def2;
end;

reserve a,b,c,d for natural Ordinal;
defpred PP[set] means ex B st B c= $1 & $1 in omega & $1 <> {} &
not ex c,d1,d2 being natural Ordinal st
d1,d2 are_relative_prime & $1 = c *^ d1 & B = c *^ d2;

theorem
  a <> {} or b <> {} implies ex c,d1,d2 being natural Ordinal st
  d1,d2 are_relative_prime & a = c *^ d1 & b = c *^ d2
proof
  assume that
A1: a <> {} or b <> {} and
A2: not ex c,d1,d2 being natural Ordinal st
  d1,d2 are_relative_prime & a = c *^ d1 & b = c *^ d2;
A3: ex A st PP[A]
  proof per cases;
    suppose
A4:   a c= b;
      take A = b, B = a;
      thus B c= A & A in omega & A <> {} by A1,A4,ORDINAL1:def 13;
      thus not ex c,d1,d2 being natural Ordinal st
      d1,d2 are_relative_prime & A = c *^ d1 & B = c *^ d2 by A2;
    end;
    suppose
A5:   b c= a;
      take A = a, B = b;
      thus B c= A & A in omega & A <> {} by A1,A5,ORDINAL1:def 13;
      thus not ex c,d1,d2 being natural Ordinal st
      d1,d2 are_relative_prime & A = c *^ d1 & B = c *^ d2 by A2;
    end;
  end;
  consider A such that
A6: PP[A] and
A7: for C st PP[C] holds A c= C from ORDINAL1:sch 1(A3);
  consider B such that
A8: B c= A & A in omega & A <> {} & not ex c,d1,d2 being natural Ordinal st
  d1,d2 are_relative_prime & A = c *^ d1 & B = c *^ d2 by A6;
  reconsider A,B as Element of omega by A8,ORDINAL1:22;
  A = 1 *^ A & B = 1 *^ B by ORDINAL2:56;
  then not A,B are_relative_prime by A8;
  then consider c,d1,d2 being Ordinal such that
A9: A = c *^ d1 & B = c *^ d2 & c <> 1 by Def2;
A10: d1 <> {} & c <> {} by A8,A9,ORDINAL2:52,55;
  then c c= A & d1 c= A & d2 c= B by A9,ORDINAL3:39;
  then reconsider c,d1,d2 as Element of omega by ORDINAL1:22;
  A = d1*^c & B = d2*^c by A9;
  then
A11: d2 c= d1 by A8,A10,ORDINAL3:38;
B13:
  now
    let c',d1',d2' be natural Ordinal;
    assume
A12: d1',d2' are_relative_prime & d1 = c' *^ d1' & d2 = c' *^ d2';
    then A = c*^c'*^d1' & B = c*^c'*^d2' by A9,ORDINAL3:58;
    hence contradiction by A8,A12;
  end;
  1 in c or c in 1 by A9,ORDINAL1:24;
  then 1*^d1 in A by A9,A10,ORDINAL3:17,22;
  then d1 in A by ORDINAL2:56;
  hence contradiction by B13,ORDINAL1:7,A7,A10,A11;
end;

reserve l,m,n for natural Ordinal;

registration
  let m,n;
  cluster m div^ n -> natural;
  coherence
  proof
A1: n in 1 or 1 c= n by ORDINAL1:26;
    n = {} implies m div^ n = {} & {}*^1 = {} by ORDINAL2:52,ORDINAL3:def 7;
    then (m div^ n)*^1 c= (m div^ n)*^n by A1,ORDINAL3:17,23;
    then m div^ n c= (m div^ n)*^n & (m div^ n)*^n c= m
    by ORDINAL2:56,ORDINAL3:77;
    then m div^ n c= m & m in omega by ORDINAL1:def 13,XBOOLE_1:1;
    hence m div^ n in omega by ORDINAL1:22;
  end;
  cluster m mod^ n -> natural;
  coherence
  proof
    (m div^ n)*^n+^(m mod^ n) = m by ORDINAL3:78;
    then m mod^ n c= m & m in omega by ORDINAL1:def 13,ORDINAL3:27;
    hence m mod^ n in omega by ORDINAL1:22;
  end;
end;

definition
  let k,n be Ordinal;
  pred k divides n means
  : Def3:
  ex a being Ordinal st n = k*^a;
  reflexivity
  proof
    let n be Ordinal;
    take 1;
    thus thesis by ORDINAL2:56;
  end;
end;

theorem Th9:
  a divides b iff ex c st b = a*^c
proof
  thus a divides b implies ex c st b = a*^c
  proof
    given c being Ordinal such that
A1: b = a*^c;
    per cases;
    suppose b = {};
      then b = a*^{} by ORDINAL2:55;
      hence ex c st b = a*^c;
    end;
    suppose b <> {};
      then c is Element of omega by A1,ORDINAL3:88;
      hence ex c st b = a*^c by A1;
    end;
  end;
  thus thesis by Def3;
end;

theorem Th10:
  for m,n st {} in m holds n mod^ m in m
proof
  let m,n;
  assume {} in m;
  then consider C such that
A1: n = (n div^ m)*^m+^C & C in m by ORDINAL3:def 7;
  n mod^ m = n-^(n div^ m)*^m by ORDINAL3:def 8;
  hence n mod^ m in m by A1,ORDINAL3:65;
end;

theorem Th11:
  for n,m holds m divides n iff n = m *^ (n div^ m)
proof
  let n,m;
  assume
A1: not thesis;
  then consider a such that
A2: n = m*^a by Th9;
  {}*^a = {} & {}*^(n div^ m) = {} by ORDINAL2:52;
  then {} <> m by A1,A2;
  then {} in m & n = a*^m+^{} by A2,ORDINAL2:44,ORDINAL3:10;
  hence thesis by A1,A2,Def3,ORDINAL3:def 7;
end;

canceled;

theorem Th13:
  for n,m st n divides m & m divides n holds n = m
proof
  let n,m;
  assume n divides m & m divides n;
  then
A1: m = n *^ (m div^ n) & n = m *^ (n div^ m) by Th11;
  then
A2: n *^ 1 = n & n = n *^ ((m div^ n) *^ (n div^ m))
  by ORDINAL2:56,ORDINAL3:58;
A3: n = {} implies n = m by A1,ORDINAL2:52;
  (m div^ n) *^ (n div^ m) = 1 implies n = m
  proof
    assume (m div^ n) *^ (n div^ m) = 1;
    then m div^ n = 1 by ORDINAL3:41;
    hence n = m by A1,ORDINAL2:56;
  end;
  hence n = m by A2,A3,ORDINAL3:36;
end;

theorem Th14:
  n divides {} & 1 divides n
proof
  {} = n *^ {} by ORDINAL2:52;
  hence n divides {} by Def3;
  n = 1 *^ n by ORDINAL2:56;
  hence thesis by Def3;
end;

theorem Th15:
  for n,m st {} in m & n divides m holds n c= m
proof
  let n,m such that
A1: {} in m;
  given a being Ordinal such that
A2: m = n*^a;
  a <> {} by A1,A2,ORDINAL2:55;
  hence thesis by A2,ORDINAL3:39;
end;

theorem Th16:
  for n,m,l st n divides m & n divides m +^ l holds n divides l
proof
  let n,m,l;
  assume n divides m;
  then consider a such that
A1: m = n*^a by Th9;
  assume n divides m +^ l;
  then consider b such that
A2: m +^ l = n*^b by Th9;
  assume
A3: not n divides l;
  l = n*^b -^ n*^a by A1,A2,ORDINAL3:65
    .= (b-^a)*^n by ORDINAL3:76;
  hence thesis by A3,Def3;
end;

Lm3: 1 = succ {};

definition
  let k,n be natural Ordinal;
  func k lcm n -> Element of omega means
  :
  Def4: k divides it & n divides it & for m st k divides m & n divides
  m holds it divides m;
  existence
  proof per cases;
    suppose
A1:   k = {} or n = {};
      reconsider w = {} as Element of omega by ORDINAL1:def 13;
      take w;
      thus k divides w & n divides w by Th14;
      let m;
      assume k divides m & n divides m;
      hence w divides m by A1;
    end;
    suppose
A2:   k <> {} & n <> {};
A3:   k divides k *^ n & n divides k *^ n by Def3;
      defpred P[Ordinal] means
      ex m st $1 = m & k divides m & n divides m & k c= m;
      {} c= n;
      then {} c< n by A2,XBOOLE_0:def 8;
      then {} in n by ORDINAL1:21;
      then 1 c= n by Lm3,ORDINAL1:33;
      then k*^1 = k & k *^ 1 c= k *^ n by ORDINAL2:56,58;
      then
A4:   ex A st P[A] by A3;
      consider A such that
A5:   P[A] and
A6:   for B st P[B] holds A c= B from ORDINAL1:sch 1(A4);
      consider l such that
A7:   A = l & k divides l & n divides l & k c= l by A5;
      reconsider l as Element of omega by ORDINAL1:def 13;
      take l;
      thus k divides l & n divides l by A7;
      let m such that
A8:   k divides m & n divides m;
      now {} c= k;
        then {} c< k by A2,XBOOLE_0:def 8;
        then
A9:     {} in k by ORDINAL1:21;
A10:    m = l*^(m div^ l)+^(m mod^ l) by ORDINAL3:78;
        l = k*^(l div^ k) & l = n*^(l div^ n) by A7,Th11;
        then l*^(m div^ l) = k*^((l div^ k)*^(m div^ l)) &
        l*^(m div^ l) = n*^((l div^ n)*^(m div^ l)) by ORDINAL3:58;
        then k divides l*^(m div^ l) & n divides l*^(m div^ l) by Def3;
        then
A11:    k divides m mod^ l & n divides m mod^ l by A8,A10,Th16;
        now
          assume
A12:      m mod^ l <> {};
          {} c= m mod^ l;
          then {} c< m mod^ l by A12,XBOOLE_0:def 8;
          then k c= m mod^ l by A11,Th15,ORDINAL1:21;
          then l c= m mod^ l by A6,A7,A11;
          hence contradiction by A7,A9,Th10,ORDINAL1:7;
        end;
        then m = l*^(m div^ l) by A10,ORDINAL2:44;
        hence l divides m by Th11;
      end;
      hence l divides m;
    end;
  end;
  uniqueness
  proof
    let m1,m2 be Element of omega such that
A13: k divides m1 & n divides m1 & for m st k divides m & n divides
    m holds m1 divides m and
A14: k divides m2 & n divides m2 & for m st k divides m & n divides
    m holds m2 divides m;
    m1 divides m2 & m2 divides m1 by A13,A14;
    hence m1 = m2 by Th13;
  end;
  commutativity;
end;

theorem Th17:
  m lcm n divides m*^n
proof m divides m*^n & n divides m*^n by Def3;
  hence thesis by Def4;
end;

theorem Th18:
  n <> {} implies (m*^n) div^ (m lcm n) divides m
proof
  assume
A1: n <> {};
  take ((m lcm n) div^ n);
  m lcm n divides m*^n & n divides m lcm n by Def4,Th17;
  then m*^n = (m lcm n)*^ ((m*^n) div^ (m lcm n)) &
  m lcm n = n*^((m lcm n) div^ n)by Th11;
  then n*^m = n*^(((m lcm n) div^ n)*^ ((m*^n) div^ (m lcm n))) by ORDINAL3:58;
  hence m = ((m*^n) div^ (m lcm n))*^((m lcm n) div^ n) by A1,ORDINAL3:36;
end;

definition
  let k,n be natural Ordinal;
  func k hcf n -> Element of omega means
  :
  Def5: it divides k & it divides n & for m st m divides k & m divides
  n holds m divides it;
  existence
  proof
    per cases;
    suppose
A1:   k = {} or n = {};
      then reconsider m = k \/ n as Element of omega by ORDINAL1:def 13;
      take m;
      thus m divides k & m divides n by A1,Th14;
      thus thesis by A1;
    end;
    suppose
A2:   k <> {} & n <> {};
      reconsider l = (k*^n) div^ (k lcm n) as Element of omega
      by ORDINAL1:def 13;
      take l;
      thus l divides k & l divides n by A2,Th18;
      let m;
      set mm = m*^((k div^ m)*^(n div^ m));
      assume m divides k & m divides n;
      then
A3:   k = m*^(k div^ m) & n = m*^(n div^ m) by Th11;
      then m*^(k div^ m)*^(n div^ m) = n*^(k div^ m) by ORDINAL3:58;
      then k divides m*^(k div^ m)*^(n div^ m) & n divides
      m*^(k div^ m)*^(n div^ m) by A3,Def3;
      then
A4:   k lcm n divides
      m*^(k div^ m)*^(n div^ m) & mm = m*^(k div^ m)*^(n div^ m)
      by Def4,ORDINAL3:58;
      then
A5:   mm = (k lcm n)*^(mm div^ (k lcm n)) by Th11;
      then
A6:   mm*^m = (k lcm n)*^(m*^(mm div^ (k lcm n))) by ORDINAL3:58;
A7:   m <> {} & k div^ m <> {} & n div^ m <> {} by A2,A3,ORDINAL2:52;
      then (k div^ m)*^(n div^ m) <> {} by ORDINAL3:34;
      then k lcm n <> {} by A5,A7,ORDINAL2:52,ORDINAL3:34;
      then k*^n = (k lcm n)*^(m*^(mm div^ (k lcm n))) & k*^n = k*^n+^{} &
      {} in k lcm n by A3,A4,A6,ORDINAL2:44,ORDINAL3:10,58;
      then l = m*^(mm div^ (k lcm n)) by ORDINAL3:79;
      hence m divides l by Def3;
    end;
  end;
  uniqueness
  proof
    let m1,m2 be Element of omega such that
A8: m1 divides k & m1 divides n & for m st m divides k & m divides
    n holds m divides m1 and
A9: m2 divides k & m2 divides n & for m st m divides k & m divides
    n holds m divides m2;
    m1 divides m2 & m2 divides m1 by A8,A9;
    hence m1 = m2 by Th13;
  end;
  commutativity;
end;

theorem Th19:
  a hcf {} = a & a lcm {} = {}
proof
  reconsider e = a, c = {} as Element of omega by ORDINAL1:def 13;
A1: e divides a & e divides {} & for n st n divides a & n divides
  {} holds n divides e by Th14;
  a divides c & {} divides c & for b st a divides b & {} divides
  b holds c divides b by Th14;
  hence thesis by A1,Def4,Def5;
end;

theorem Th20:
  a hcf b = {} implies a = {}
proof a hcf b divides a by Def5;
  then a = (a hcf b)*^(a div^ (a hcf b)) by Th11;
  hence thesis by ORDINAL2:52;
end;

theorem Th21:
  a hcf a = a & a lcm a = a
proof reconsider c = a as Element of omega by ORDINAL1:def 13;
  c divides a & for b st b divides a & b divides a holds b divides c;
  hence a hcf a = a by Def5;
  a divides c & for b st a divides b & a divides b holds c divides b;
  hence thesis by Def4;
end;

theorem Th22:
  (a*^c) hcf (b*^c) = (a hcf b)*^c
proof per cases;
  suppose c = {};
    then a*^c = {} & b*^c = {} & (a hcf b)*^c = {} by ORDINAL2:52;
    hence thesis by Th21;
  end;
  suppose
A1: c <> {} & a <> {};
    reconsider d = (a hcf b)*^c as Element of omega by ORDINAL1:def 13;
    set e = ((a*^c) hcf (b*^c)) div^ d;
    a hcf b divides a & a hcf b divides b by Def5;
    then a = (a hcf b)*^(a div^ (a hcf b)) & b = (a hcf b)*^(b div^ (a hcf b))
    by Th11;
    then a*^c = d*^(a div^ (a hcf b)) & b*^c = d*^(b div^ (a hcf b))
    by ORDINAL3:58;
    then d divides a*^c & d divides b*^c by Def3;
    then d divides (a*^c) hcf (b*^c) by Def5;
    then
A2: (a*^c) hcf (b*^c) = d*^e by Th11
      .= (a hcf b)*^e*^c by ORDINAL3:58;
    then (a hcf b)*^e*^c divides a*^c & (a hcf b)*^e*^c divides b*^c by Def5;
    then (a hcf b)*^e*^c*^((a*^c)div^((a hcf b)*^e*^c)) = a*^c &
    (a hcf b)*^e*^c*^((b*^c)div^((a hcf b)*^e*^c)) = b*^c by Th11;
    then (a hcf b)*^e*^((a*^c)div^((a hcf b)*^e*^c))*^c = a*^c &
    (a hcf b)*^e*^((b*^c)div^((a hcf b)*^e*^c))*^c = b*^c by ORDINAL3:58;
    then (a hcf b)*^e*^((a*^c)div^((a hcf b)*^e*^c)) = a &
    (a hcf b)*^e*^((b*^c)div^((a hcf b)*^e*^c)) = b by A1,ORDINAL3:36;
    then (a hcf b)*^e divides a & (a hcf b)*^e divides b by Def3;
    then (a hcf b)*^e divides a hcf b by Def5;
    then (a hcf b)*^e*^((a hcf b) div^ ((a hcf b)*^e)) = a hcf b by Th11;
    then (a hcf b)*^(e*^((a hcf b) div^ ((a hcf b)*^e))) = a hcf b by
    ORDINAL3:58
      .= (a hcf b)*^1 by ORDINAL2:56;
    then a hcf b = {} or e*^((a hcf b) div^ ((a hcf b)*^e)) = 1
    by ORDINAL3:36;
    then e = 1 by A1,Th20,ORDINAL3:41;
    hence thesis by A2,ORDINAL2:56;
  end;
  suppose a = {};
    then a hcf b = b & a*^c = {} by Th19,ORDINAL2:52;
    hence thesis by Th19;
  end;
end;

theorem Th23:
  b <> {} implies a hcf b <> {} & b div^ (a hcf b) <> {}
proof
  a hcf b divides b by Def5;
  then b = (a hcf b)*^(b div^ (a hcf b)) by Th11;
  hence thesis by ORDINAL2:52;
end;

theorem Th24:
  a <> {} or b <> {} implies
  a div^ (a hcf b), b div^ (a hcf b) are_relative_prime
proof
  assume
A1: a <> {} or b <> {};
A2: 1*^a = a & 1*^b = b by ORDINAL2:56;
  set ab = a hcf b;
  per cases;
  suppose a = {} or b = {};
    then ab = b & b div^ b = 1 or
    ab = a & a div^ a = 1 by A1,A2,Th19,ORDINAL3:81;
    hence thesis by Th6;
  end;
  suppose
A3: a <> {} & b <> {};
    ab divides a & ab divides b by Def5;
    then
A4: a = ab*^(a div^ ab) & b = ab*^(b div^ ab) by Th11;
    let c,d1,d2 be Ordinal such that
A5: a div^ (a hcf b) = c *^ d1 & b div^ (a hcf b) = c *^ d2;
    a div^ ab <> {} & b div^ ab <> {} by A3,A4,ORDINAL2:52;
    then reconsider c,d1,d2 as Element of omega by A5,ORDINAL3:88;
    a = ab*^c*^d1 & b = ab*^c*^d2 by A4,A5,ORDINAL3:58;
    then ab*^c divides a & ab*^c divides b by Def3;
    then ab*^c divides ab by Def5;
    then ab = (ab*^c)*^(ab div^ (ab*^c)) by Th11;
    then ab = ab*^(c*^(ab div^ (ab*^c))) by ORDINAL3:58;
    then ab*^1 = ab*^(c*^(ab div^ (ab*^c))) & ab <> {} by A3,A4,ORDINAL2:52,56;
    then 1 = c*^(ab div^ (ab*^c)) by ORDINAL3:36;
    hence thesis by ORDINAL3:41;
  end;
end;

theorem Th25:
  a,b are_relative_prime iff a hcf b = 1
proof
  a hcf b divides a & a hcf b divides b by Def5;
  then a = (a hcf b)*^(a div^ (a hcf b)) & b = (a hcf b)*^(b div^ (a hcf b))
  by Th11;
  hence a,b are_relative_prime implies a hcf b = 1 by Def2;
  assume
A1: a hcf b = 1;
  let c,d1,d2 be Ordinal such that
A2: a = c*^d1 & b = c*^d2;
  a <> {} or b <> {} by A1,Th19;
  then reconsider c as Element of omega by A2,ORDINAL3:88;
  c divides a & c divides b by A2,Def3;
  then c divides 1 by A1,Def5;
  then ex d st 1 = c*^d by Th9;
  hence thesis by ORDINAL3:41;
end;

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

  a div^ (a hcf b);
  coherence by ORDINAL1:def 13;
end;

theorem Th26:
  RED(a,b)*^(a hcf b) = a
proof
  RED(a,b) = a div^ (a hcf b) & a hcf b divides a by Def5;
  hence thesis by Th11;
end;

theorem
  a <> {} or b <> {} implies RED(a,b), RED(b,a) are_relative_prime by Th24;

theorem Th28:
  a,b are_relative_prime implies RED(a,b) = a
proof
  assume a,b are_relative_prime;
  then a hcf b = 1 by Th25;
  hence thesis by ORDINAL3:84;
end;

theorem Th29:
  RED(a,1) = a & RED(1,a) = 1
proof a,1 are_relative_prime by Th6;
  then a hcf 1 = 1 by Th25;
  hence thesis by ORDINAL3:84;
end;

theorem
  b <> {} implies RED(b,a) <> {} by Th23;

theorem Th31:
  RED({},a) = {} & (a <> {} implies RED(a,{}) = 1)
proof thus RED({},a) = {} by ORDINAL3:83;
  assume
A1: a <> {};
  thus RED(a,{}) = a div^ a by Th19
    .= a*^1 div^ a by ORDINAL2:56
    .= 1 by A1,ORDINAL3:81;
end;

theorem Th32:
  a <> {} implies RED(a,a) = 1
proof
  assume
A1: a <> {};
  thus RED(a,a) = a div^ a by Th21
    .= a*^1 div^ a by ORDINAL2:56
    .= 1 by A1,ORDINAL3:81;
end;

theorem Th33:
  c <> {} implies RED(a*^c, b*^c) = RED(a, b)
proof
A1: a hcf b divides a by Def5;
A2: a <> {} implies a hcf b <> {} by Th23;
  assume c <> {};
  then
A3: a <> {} implies (a hcf b)*^c <> {} by A2,ORDINAL3:34;
A4: RED({},b) = {} & {}*^((a hcf b)*^c) = {} & {} div^ ((a hcf b)*^c) = {}
  by ORDINAL2:52,ORDINAL3:83;
  thus RED(a*^c, b*^c) = (a*^c)div^((a hcf b)*^c) by Th22
    .= (((a div^(a hcf b))*^(a hcf b))*^c)div^((a hcf b)*^c) by A1,Th11
    .= (RED(a,b)*^((a hcf b)*^c))div^((a hcf b)*^c) by ORDINAL3:58
    .= RED(a, b) by A3,A4,ORDINAL3:81;
end;
set RATplus = {[a,b] where a,b is Element of omega:
a,b are_relative_prime & b <> {}};
1 <> {} & 1,1 are_relative_prime by Th6;
then [1,1] in RATplus;
then reconsider RATplus as non empty set;

Lm4: [a,b] in RATplus implies a,b are_relative_prime & b <> {}
proof
  assume [a,b] in RATplus;
  then consider c,d being Element of omega such that
A1: [a,b] = [c,d] & c,d are_relative_prime & d <> {};
  a = c & b = d by A1,ZFMISC_1:33;
  hence thesis by A1;
end;

begin :: Non negative rationals

reserve i,j,k for Element of omega;

definition
  func RAT+ equals
  ({[i,j]: i,j are_relative_prime & j <> {}} \ {[k,1]: not contradiction})
  \/ omega;
  correctness;
end;

Lm5: omega c= RAT+ by XBOOLE_1:7;

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

registration
  cluster RAT+ -> non empty;
  coherence;
end;

registration
  cluster non empty ordinal Element of RAT+;
  existence by Lm2,Lm5;
end;

canceled;

theorem Th35:
  x in
  omega or ex i,j st x = [i,j] & i,j are_relative_prime & j <> {} & j <> 1
proof
  assume not x in omega;
  then x in RATplus \ {[k,1]: not contradiction} by XBOOLE_0:def 2;
  then
A1: x in RATplus & not x in {[k,1]: not contradiction} by XBOOLE_0:def 4;
  then consider a,b being Element of omega such that
A2: x = [a,b] & a,b are_relative_prime & b <> {};
  [a,1] in {[k,1]: not contradiction};
  hence thesis by A1,A2;
end;

theorem Th36:
  not ex i,j being set st [i,j] is Ordinal
proof
  given i,j being set such that
A1: [i,j] is Ordinal;
  {} in [i,j] by A1,ORDINAL3:10;
  hence thesis by TARSKI:def 2;
end;

theorem Th37:
  A in RAT+ implies A in omega
proof
  assume A in RAT+ & not A in omega;
  then ex i,j st A = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 by Th35;
  hence thesis by Th36;
end;

registration
  cluster -> natural (ordinal Element of RAT+);
  coherence
  proof
    let x be ordinal Element of RAT+;
    assume not x in omega;
    then consider i,j such that
A1: x = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 by Th35;
    {} in x by A1,ORDINAL3:10;
    hence thesis by A1,TARSKI:def 2;
  end;
end;

theorem Th38:
  not ex i,j being set st [i,j] in omega
proof
  given i,j being set such that
A1: [i,j] in omega;
  reconsider a = [i,j] as Element of omega by A1;
  {} in a by ORDINAL3:10;
  hence thesis by TARSKI:def 2;
end;

theorem Th39:
  [i,j] in RAT+ iff i,j are_relative_prime & j <> {} & j <> 1
proof
A1: not [i,j] in omega by Th38;
  hereby
    assume [i,j] in RAT+;
    then
A2: [i,j] in RATplus \ {[k,1]: not contradiction} by A1,XBOOLE_0:def 2;
    then
A3: [i,j] in RATplus & not [i,j] in {[k,1]: not contradiction}
    by XBOOLE_0:def 4;
    thus i,j are_relative_prime & j <> {} by A2,Lm4;
    thus j <> 1 by A3;
  end;
  assume i,j are_relative_prime & j <> {};
  then
A4: [i,j] in RATplus;
  assume j <> 1;
  then not ex k st [i,j] = [k,1] by ZFMISC_1:33;
  then not [i,j] in {[k,1]: not contradiction};
  then [i,j] in RATplus \ {[k,1]: not contradiction} by A4,XBOOLE_0:def 4;
  hence thesis by XBOOLE_0:def 2;
end;

definition
  let x be Element of RAT+;
  func numerator x -> Element of omega means
  :Def8:
  it = x if x in omega otherwise ex a st x = [it,a];
  existence
  proof
    thus x in omega implies ex a being Element of omega st a = x;
    assume not x in omega;
    then x in RATplus \ {[k,1]: not contradiction} by XBOOLE_0:def 2;
    then x in RATplus;
    then consider a,b being Element of omega such that
A1: x = [a,b] & a,b are_relative_prime & b <> {};
    take a,b; thus thesis by A1;
  end;
  correctness by ZFMISC_1:33;
  func denominator x -> Element of omega means
  :
  Def9: it = 1 if x in omega otherwise ex a st x = [a,it];
  existence
  proof
    thus x in omega implies ex a being Element of omega st a = 1;
    assume not x in omega;
    then x in RATplus \ {[k,1]: not contradiction} by XBOOLE_0:def 2;
    then x in RATplus;
    then consider a,b being Element of omega such that
A2: x = [a,b] & a,b are_relative_prime & b <> {};
    take b,a; thus thesis by A2;
  end;
  correctness by ZFMISC_1:33;
end;

theorem Th40:
  numerator x, denominator x are_relative_prime
proof per cases;
  suppose x in omega;
    then denominator x = 1 by Def9;
    hence thesis by Th6;
  end;
  suppose
A1: not x in omega;
    then consider i,j such that
A2: x = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 by Th35;
    i = numerator x by A1,A2,Def8;
    hence thesis by A1,A2,Def9;
  end;
end;

theorem Th41:
  denominator x <> {}
proof per cases;
  suppose x in omega;
    hence thesis by Def9;
  end;
  suppose
A1: not x in omega;
    then consider i,j such that
A2: x = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 by Th35;
    thus thesis by A1,A2,Def9;
  end;
end;

theorem Th42:
  not x in omega implies x = [numerator x, denominator x] & denominator x <> 1
proof
  assume
A1: not x in omega;
  then consider i,j such that
A2: x = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 by Th35;
  i = numerator x & j = denominator x by A1,A2,Def8,Def9;
  hence thesis by A2;
end;

theorem Th43:
  x <> {} iff numerator x <> {}
proof
  hereby
    assume
A1: x <> {} & numerator x = {};
    then
A2: not x in omega by Def8;
    then consider i,j such that
A3: x = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 by Th35;
    i = {} by A1,A2,A3,Def8;
    hence contradiction by A3,Th7;
  end;
  {} in omega by ORDINAL1:def 12;
  hence thesis by Def8;
end;

theorem
  x in omega iff denominator x = 1 by Def9,Th42;

definition
  let i,j be natural Ordinal;
  func i/j -> Element of RAT+ equals
  :Def10:
  {} if j = {},
  RED(i,j) if RED(j,i) = 1 otherwise [RED(i,j), RED(j,i)];
  coherence
  proof
A1: RED(i,j) in omega;
    now
      assume j <> {};
      then RED(i,j), RED(j,i) are_relative_prime & RED(j,i) <> {} by Th23,Th24;
      hence RED(j,i) <> 1 implies [RED(i,j), RED(j,i)] in RAT+ by Th39;
    end;
    hence thesis by A1,Lm1,Lm5;
  end;
  consistency by Th31;
end;

notation
  let i,j be natural Ordinal;
  synonym quotient(i,j) for i/j;
end;

theorem Th45:
  (numerator x)/(denominator x) = x
proof
A1: denominator x <> {} by Th41;
  numerator x, denominator x are_relative_prime by Th40;
  then
A2: RED(numerator x, denominator x) = numerator x &
  RED(denominator x, numerator x) = denominator x by Th28;
  per cases;
  suppose
A3: denominator x = 1;
    then x in omega by Th42;
    then numerator x = x by Def8;
    hence thesis by A2,A3,Def10;
  end;
  suppose
A4: denominator x <> 1;
    then not x in omega by Def9;
    then x = [numerator x, denominator x] by Th42;
    hence thesis by A1,A2,A4,Def10;
  end;
end;

theorem Th46:
  {}/b = {} & a/1 = a
proof RED({},b) = {} & (b <> {} implies RED(b,{}) = 1) by Th31;
  hence {}/b = {} by Def10;
  RED(1,a) = 1 & RED(a,1) = a by Th29;
  hence thesis by Def10;
end;

theorem Th47:
  a <> {} implies a/a = 1
proof
  assume a <> {};
  then RED(a,a) = 1 by Th32;
  hence thesis by Def10;
end;

theorem Th48:
  b <> {} implies numerator (a/b) = RED(a,b) & denominator (a/b) = RED(b,a)
proof
  assume
A1: b <> {};
  per cases;
  suppose
A2: RED(b,a) = 1;
    then a/b = RED(a,b) by Def10;
    hence thesis by A2,Def8,Def9;
  end;
  suppose RED(b,a) <> 1;
    then a/b = [RED(a,b), RED(b,a)] & not [RED(a,b), RED(b,a)] in omega
    by A1,Def10,Th38;
    hence thesis by Def8,Def9;
  end;
end;

theorem Th49:
  i,j are_relative_prime & j <> {} implies
  numerator (i/j) = i & denominator (i/j) = j
proof
  assume i,j are_relative_prime;
  then RED(i,j) = i & RED(j,i) = j by Th28;
  hence thesis by Th48;
end;

theorem Th50:
  c <> {} implies (a*^c)/(b*^c) = a/b
proof
  assume
A1: c <> {};
  per cases;
  suppose b = {};
    then a/b = {} & b*^c = {} by Def10,ORDINAL2:52;
    hence thesis by Def10;
  end;
  suppose
A2: b <> {};
    then
A3: b*^c <> {} by A1,ORDINAL3:34;
    then
A4: numerator ((a*^c)/(b*^c)) = RED(a*^c,b*^c) by Th48
      .= RED(a,b) by A1,Th33
      .= numerator (a/b) by A2,Th48;
    denominator ((a*^c)/(b*^c)) = RED(b*^c,a*^c) by A3,Th48
      .= RED(b,a) by A1,Th33
      .= denominator (a/b) by A2,Th48;
    hence (a*^c)/(b*^c) = (numerator (a/b))/denominator (a/b) by A4,Th45
      .= a/b by Th45;
  end;
end;

reserve i,j,k for natural Ordinal;

theorem Th51:
  j <> {} & l <> {} implies (i/j = k/l iff i*^l = j*^k)
proof
  assume
A1: j <> {} & l <> {};
  set x = i/j, y = k/l;
  set nx = numerator x, dx = denominator x;
  set ny = numerator y, dy = denominator y;
A2: nx = RED(i,j) & dx = RED(j,i) by A1,Th48;
A3: ny = RED(k,l) & dy = RED(l,k) by A1,Th48;
  hereby
    assume i/j = k/l;
    then i = ny*^(i hcf j) & l = dx*^(l hcf k) by A2,A3,Th26;
    hence i*^l = ny*^(i hcf j)*^dx*^(l hcf k) by ORDINAL3:58
      .= ny*^((i hcf j)*^dx)*^(l hcf k) by ORDINAL3:58
      .= ny*^j*^(l hcf k) by A2,Th26
      .= j*^(ny*^(l hcf k)) by ORDINAL3:58
      .= j*^k by A3,Th26;
  end;
  assume i*^l = j*^k;
  then nx = RED(j*^k,j*^l) & dx = RED(j*^l,j*^k) by A1,A2,Th33;
  then nx = ny & dx = dy by A1,A3,Th33;
  then x = ny/dy by Th45;
  hence i/j = k/l by Th45;
end;

definition
  let x,y be Element of RAT+;
  func x+y -> Element of RAT+ equals
  ((numerator x)*^(denominator y)+^(numerator y)*^(denominator x))
  / ((denominator x)*^(denominator y));
  coherence;
  commutativity;
  func x*'y -> Element of RAT+ equals
  ((numerator x)*^(numerator y)) / ((denominator x)*^(denominator y));
  coherence;
  commutativity;
end;

theorem Th52:
  j <> {} & l <> {} implies (i/j)+(k/l) = (i*^l+^j*^k)/(j*^l)
proof
  assume
A1: j <> {} & l <> {};
  then numerator (k/l) = RED(k,l) & numerator (i/j) = RED(i,j) &
  denominator (k/l) = RED(l,k) & denominator (i/j) = RED(j,i) by Th48;
  hence (i/j)+(k/l) = (RED(i,j)*^RED(l,k)+^RED(j,i)*^RED(k,l))*^(i hcf j)
  /(RED(j,i)*^RED(l,k)*^(i hcf j)) by A1,Th20,Th50
    .= (RED(i,j)*^RED(l,k)+^RED(j,i)*^RED(k,l))*^(i hcf j)
  /(RED(l,k)*^(RED(j,i)*^(i hcf j))) by ORDINAL3:58
    .= (RED(i,j)*^RED(l,k)+^RED(j,i)*^RED(k,l))*^(i hcf j)/(RED(l,k)*^j)
  by Th26
    .= (RED(i,j)*^RED(l,k)*^(i hcf j)+^RED(j,i)*^RED(k,l)*^(i hcf j))
  /(RED(l,k)*^j) by ORDINAL3:54
    .= (RED(l,k)*^(RED(i,j)*^(i hcf j))+^RED(j,i)*^RED(k,l)*^(i hcf j))
  /(RED(l,k)*^j) by ORDINAL3:58
    .= (RED(l,k)*^i+^RED(j,i)*^RED(k,l)*^(i hcf j))/(RED(l,k)*^j) by Th26
    .= (RED(l,k)*^i+^RED(k,l)*^(RED(j,i)*^(i hcf j)))/(RED(l,k)*^j)
  by ORDINAL3:58
    .= (RED(l,k)*^i+^RED(k,l)*^j)/(RED(l,k)*^j) by Th26
    .= ((RED(l,k)*^i+^RED(k,l)*^j)*^(k hcf l))/(RED(l,k)*^j*^(k hcf l))
  by A1,Th20,Th50
    .= ((RED(l,k)*^i+^RED(k,l)*^j)*^(k hcf l))/(j*^(RED(l,k)*^(k hcf l)))
  by ORDINAL3:58
    .= ((RED(l,k)*^i+^RED(k,l)*^j)*^(k hcf l))/(j*^l) by Th26
    .= (RED(l,k)*^i*^(k hcf l)+^RED(k,l)*^j*^(k hcf l))/(j*^l) by ORDINAL3:54
    .= (i*^(RED(l,k)*^(k hcf l))+^RED(k,l)*^j*^(k hcf l))/(j*^l)
  by ORDINAL3:58
    .= (i*^l+^RED(k,l)*^j*^(k hcf l))/(j*^l) by Th26
    .= (i*^l+^j*^(RED(k,l)*^(k hcf l)))/(j*^l) by ORDINAL3:58
    .= (i*^l+^j*^k)/(j*^l) by Th26;
end;

theorem Th53:
  k <> {} implies (i/k)+(j/k) = (i+^j)/k
proof
  assume
A1: k <> {};
  hence (i/k)+(j/k) = (i*^k+^j*^k)/(k*^k) by Th52
    .= ((i+^j)*^k)/(k*^k) by ORDINAL3:54
    .= (i+^j)/k by A1,Th50;
end;

registration
  cluster empty Element of RAT+;
  existence by Lm1,Lm5;
end;

definition
  redefine func {} -> Element of RAT+;
  coherence by Lm1,Lm5;
  redefine func one -> non empty ordinal Element of RAT+;
  coherence by Lm2,Lm5;
end;

theorem Th54:
  x*'{} = {}
proof
  denominator {} = 1 & numerator {} = {} & (numerator x)*^{} = {} &
  (denominator x)*^1 = denominator x by Def8,Def9,Lm1,ORDINAL2:52,56;
  hence x*'{} = {} by Th46;
end;

theorem Th55:
  (i/j)*'(k/l) = (i*^k)/(j*^l)
proof per cases;
  suppose
A1: j <> {} & l <> {};
    then numerator (k/l) = RED(k,l) & numerator (i/j) = RED(i,j) &
    denominator (k/l) = RED(l,k) & denominator (i/j) = RED(j,i) by Th48;
    hence (i/j)*'(k/l) =
    (RED(i,j)*^RED(k,l)*^(i hcf j))/(RED(j,i)*^RED(l,k)*^(i hcf j))
    by A1,Th20,Th50
      .= (RED(k,l)*^(RED(i,j)*^(i hcf j)))/(RED(j,i)*^RED(l,k)*^(i hcf j))
    by ORDINAL3:58
      .= (RED(k,l)*^i)/(RED(j,i)*^RED(l,k)*^(i hcf j)) by Th26
      .= (RED(k,l)*^i)/(RED(l,k)*^(RED(j,i)*^(i hcf j))) by ORDINAL3:58
      .= (RED(k,l)*^i)/(RED(l,k)*^j) by Th26
      .= (RED(k,l)*^i*^(l hcf k))/(RED(l,k)*^j*^(l hcf k)) by A1,Th20,Th50
      .= (i*^(RED(k,l)*^(l hcf k)))/(RED(l,k)*^j*^(l hcf k)) by ORDINAL3:58
      .= (i*^k)/(RED(l,k)*^j*^(l hcf k)) by Th26
      .= (i*^k)/(j*^(RED(l,k)*^(l hcf k))) by ORDINAL3:58
      .= (i*^k)/(j*^l) by Th26;
  end;
  suppose j = {} or l = {};
    then (i/j = {} or k/l = {}) & j*^l = {} by Def10,ORDINAL2:52;
    then (i/j)*'(k/l) = {} & (i*^k)/(j*^l) = {} by Def10,Th54;
    hence thesis;
  end;
end;

theorem Th56:
  x+{} = x
proof
  denominator {} = 1 & numerator {} = {} & (numerator x)*^1 = numerator x &
  {}*^(denominator x) = {} & (denominator x)*^1 = denominator x &
  (numerator x)+^{} = numerator x by Def8,Def9,Lm1,ORDINAL2:44,52,56;
  hence x+{} = x by Th45;
end;

theorem Th57:
  (x+y)+z = x+(y+z)
proof
  set nx = numerator x, ny = numerator y, nz = numerator z;
  set dx = denominator x, dy = denominator y, dz = denominator z;
A1: dx <> {} & dy <> {} & dz <> {} by Th41;
  then
A2: dx*^dy <> {} & dy*^dz <> {} by ORDINAL3:34;
  thus x+y+z = (nx*^dy+^dx*^ny)/(dx*^dy)+nz/dz by Th45
    .= ((nx*^dy+^dx*^ny)*^dz+^(dx*^dy)*^nz)/(dx*^dy*^dz) by A1,A2,Th52
    .= (nx*^dy*^dz+^dx*^ny*^dz+^dx*^dy*^nz)/(dx*^dy*^dz) by ORDINAL3:54
    .= (nx*^(dy*^dz)+^dx*^ny*^dz+^dx*^dy*^nz)/(dx*^dy*^dz) by ORDINAL3:58
    .= (nx*^(dy*^dz)+^dx*^(ny*^dz)+^dx*^dy*^nz)/(dx*^dy*^dz) by ORDINAL3:58
    .= (nx*^(dy*^dz)+^dx*^(ny*^dz)+^dx*^(dy*^nz))/(dx*^dy*^dz) by ORDINAL3:58
    .= (nx*^(dy*^dz)+^(dx*^(ny*^dz)+^dx*^(dy*^nz)))/(dx*^dy*^dz)
  by ORDINAL3:33
    .= (nx*^(dy*^dz)+^dx*^(ny*^dz+^dy*^nz))/(dx*^dy*^dz) by ORDINAL3:54
    .= (nx*^(dy*^dz)+^dx*^(ny*^dz+^dy*^nz))/(dx*^(dy*^dz)) by ORDINAL3:58
    .= (ny*^dz+^dy*^nz)/(dy*^dz)+nx/dx by A1,A2,Th52
    .= x+(y+z) by Th45;
end;

theorem Th58:
  (x*'y)*'z = x*'(y*'z)
proof
  set nx = numerator x, ny = numerator y, nz = numerator z;
  set dx = denominator x, dy = denominator y, dz = denominator z;
A1: z = nz/dz & x = nx/dx by Th45;
  hence (x*'y)*'z = (nx*^ny*^nz)/(dx*^dy*^dz) by Th55
    .= (nx*^(ny*^nz))/(dx*^dy*^dz) by ORDINAL3:58
    .= (nx*^(ny*^nz))/(dx*^(dy*^dz)) by ORDINAL3:58
    .= x*'(y*'z) by A1,Th55;
end;

theorem Th59:
  x*'one = x
proof
  set y = one;
  (numerator x)*^1 = numerator x & (denominator x)*^1 = denominator x &
  numerator y = 1 & denominator y = 1 by Def8,Def9,ORDINAL2:56;
  hence x*'y = x by Th45;
end;

theorem Th60:
  x <> {} implies ex y st x*'y = 1
proof
  set nx = numerator x, dx = denominator x;
  assume x <> {};
  then
A1: nx <> {} & dx <> {} by Th41,Th43;
  take y = dx/nx;
  nx, dx are_relative_prime by Th40;
  then denominator y = nx & numerator y = dx by A1,Th49;
  hence x*'y = 1 by A1,Th47,ORDINAL3:34;
end;

theorem Th61:
  x <> {} implies ex z st y = x*'z
proof
  assume x <> {};
  then consider z such that
A1: x*'z = 1 by Th60;
  reconsider o = one as Element of RAT+;
  take z*'y; thus y = y*'o by Th59
    .= x*'(z*'y) by A1,Th58;
end;

theorem Th62:
  x <> {} & x*'y = x*'z implies y = z
proof
  assume x <> {};
  then consider r being Element of RAT+ such that
A1: x*'r = 1 by Th60;
  r*'(x*'y) = one*'y & r*'(x*'z) = one*'z by A1,Th58;
  then r*'(x*'y) = y & r*'(x*'z) = z by Th59;
  hence thesis;
end;

theorem Th63:
  x*'(y+z) = x*'y+x*'z
proof
  set nx = numerator x, ny = numerator y, nz = numerator z;
  set dx = denominator x, dy = denominator y, dz = denominator z;
A1: x = nx/dx by Th45;
  dx <> {} & dy <> {} & dz <> {} by Th41;
  then
A2: dx*^dz <> {} & dx*^dy <> {} by ORDINAL3:34;
  thus x*'(y+z) = (nx*^(ny*^dz+^dy*^nz))/(dx*^(dy*^dz)) by A1,Th55
    .= (nx*^(ny*^dz)+^nx*^(dy*^nz))/(dx*^(dy*^dz)) by ORDINAL3:54
    .= (nx*^ny*^dz+^nx*^(dy*^nz))/(dx*^(dy*^dz)) by ORDINAL3:58
    .= (nx*^ny*^dz+^dy*^(nx*^nz))/(dx*^(dy*^dz)) by ORDINAL3:58
    .= (nx*^ny*^dz+^dy*^(nx*^nz))/(dy*^(dx*^dz)) by ORDINAL3:58
    .= (dx*^((nx*^ny)*^dz+^(dy*^(nx*^nz))))/(dx*^(dy*^(dx*^dz))) by Th41,Th50
    .= (dx*^((nx*^ny)*^dz)+^dx*^(dy*^(nx*^nz)))/(dx*^(dy*^(dx*^dz)))
  by ORDINAL3:54
    .= (dx*^((nx*^ny)*^dz)+^(dx*^dy)*^(nx*^nz))/(dx*^(dy*^(dx*^dz)))
  by ORDINAL3:58
    .= ((nx*^ny)*^(dx*^dz)+^(dx*^dy)*^(nx*^nz))/(dx*^(dy*^(dx*^dz)))
  by ORDINAL3:58
    .= ((nx*^ny)*^(dx*^dz)+^(dx*^dy)*^(nx*^nz))/((dx*^dy)*^(dx*^dz))
  by ORDINAL3:58
    .= x*'y+x*'z by A2,Th52;
end;

theorem Th64:
  for i,j being ordinal Element of RAT+ holds i+j = i+^j
proof
  let i,j be ordinal Element of RAT+;
  set ni = numerator i, nj = numerator j;
A1: i in omega & j in omega by ORDINAL1:def 13;
  then denominator i = 1 & denominator j = 1 by Def9;
  hence i+j = (ni*^1+^1*^nj)/1 by ORDINAL2:56
    .= (ni+^1*^nj)/1 by ORDINAL2:56
    .= (ni+^nj)/1 by ORDINAL2:56
    .= ni+^nj by Th46
    .= i+^nj by A1,Def8
    .= i+^j by A1,Def8;
end;

theorem
  for i,j being ordinal Element of RAT+ holds i*'j = i*^j
proof
  let i,j be ordinal Element of RAT+;
  set ni = numerator i, nj = numerator j;
A1: i in omega & j in omega by ORDINAL1:def 13;
  then denominator i = 1 & denominator j = 1 by Def9;
  hence i*'j = (ni*^nj)/1 by ORDINAL2:56
    .= ni*^nj by Th46
    .= i*^nj by A1,Def8
    .= i*^j by A1,Def8;
end;

theorem Th66:
  ex y st x = y+y
proof
  set 02 = one+one;
  02 = 1+^1 by Th64;
  then 02 <> {} by ORDINAL3:29;
  then consider z such that
A1: 02*'z = 1 by Th60;
  take y = z*'x;
  thus x = one*'x by Th59
    .= 02*'y by A1,Th58
    .= one*'y+one*'y by Th63
    .= y+one*'y by Th59
    .= y+y by Th59;
end;

definition
  let x,y be Element of RAT+;
  pred x <=' y means
  : Def13:
  ex z being Element of RAT+ st y = x+z;
  connectedness
  proof
    let x,y be Element of RAT+;
    set nx = numerator x, ny = numerator y;
    set dx = denominator x, dy = denominator y;
    dx <> {} & dy <> {} by Th41;
    then
A1: nx*^dy/(dx*^dy) = nx/dx & ny*^dx/(dx*^dy) = ny/dy & dx*^dy <> {}
    by Th50,ORDINAL3:34;
A2: nx/dx = x & ny/dy = y by Th45;
    nx*^dy c= ny*^dx or ny*^dx c= nx*^dy;
    then ny*^dx = nx*^dy+^(ny*^dx -^ nx*^dy) or nx*^dy = ny*^dx+^(nx*^dy -^ ny
    *^dx) by ORDINAL3:def 6;
    then x = y+((nx*^dy -^ ny*^dx)/(dx*^dy)) or y = x+((ny*^dx -^ nx*^dy)/(dx
    *^dy)) by A1,A2,Th53;
    hence thesis;
  end;
end;

notation
  let x,y be Element of RAT+;
  antonym y < x for x <=' y;
end;

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

canceled;

theorem
  not ex y being set st [{},y] in RAT+
proof
  given y being set such that
A1: [{},y] in RAT+;
  consider i,j being Element of omega such that
A2: [{},y] = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 by Th38,Th35,A1;
  i = {} by A2,ZFMISC_1:33;
  hence thesis by A2,Th7;
end;

theorem Th69:
  s + t = r + t implies s = r
proof
  assume
A1: s + t = r + t;
  set s1 = numerator s, s2 = denominator s;
  set t1 = numerator t, t2 = denominator t;
  set r1 = numerator r, r2 = denominator r;
A2: t2 <> {} & s2 <> {} & r2 <> {} by Th41;
  then r2*^t2 <> {} & s2*^t2 <> {} by ORDINAL3:34;
  then (s1*^t2+^s2*^t1)*^(r2*^t2) = (r1*^t2+^r2*^t1)*^(s2*^t2) by A1,Th51
    .= (r1*^t2+^r2*^t1)*^s2*^t2 by ORDINAL3:58;
  then (s1*^t2+^s2*^t1)*^r2*^t2 = (r1*^t2+^r2*^t1)*^s2*^t2 by ORDINAL3:58;
  then (s1*^t2+^s2*^t1)*^r2 = (r1*^t2+^r2*^t1)*^s2 by A2,ORDINAL3:36
    .= r1*^t2*^s2+^r2*^t1*^s2 by ORDINAL3:54;
  then s1*^t2*^r2+^s2*^t1*^r2 = r1*^t2*^s2+^r2*^t1*^s2 by ORDINAL3:54
    .= r1*^t2*^s2+^s2*^t1*^r2 by ORDINAL3:58;
  then s1*^t2*^r2 = r1*^t2*^s2 by ORDINAL3:24
    .= r1*^s2*^t2 by ORDINAL3:58;
  then s1*^r2*^t2 = r1*^s2*^t2 by ORDINAL3:58;
  then s1*^r2 = r1*^s2 by A2,ORDINAL3:36;
  then s1/s2 = r1/r2 by A2,Th51
    .= r by Th45;
  hence thesis by Th45;
end;

theorem Th70:
  r+s = {} implies r = {}
proof
  set nr = numerator r, dr = denominator r;
  set ns = numerator s, ds = denominator s;
A1: dr <> {} & ds <> {} & denominator (r+s) <> {} by Th41;
  then
A2: dr*^ds <> {} by ORDINAL3:34;
A3: denominator {} = 1 & numerator {} = {} by Def8,Def9,Lm1;
  assume r+s = {};
  then (nr*^ds+^ns*^dr)/(dr*^ds) = {}/1 by A3,Th45;
  then (nr*^ds+^ns*^dr)*^1 = (dr*^ds)*^{} by A2,Th51
    .= {} by ORDINAL2:52;
  then nr*^ds+^ns*^dr = {} by ORDINAL3:34;
  then nr*^ds = {} by ORDINAL3:29;
  then nr = {} by A1,ORDINAL3:34;
  hence thesis by Th43;
end;

theorem Th71:
  {} <=' s
proof
  take s; thus thesis by Th56;
end;

theorem
  s <=' {} implies s = {}
proof
  assume ex r st {} = s+r;
  hence thesis by Th70;
end;

theorem Th73:
  r <=' s & s <=' r implies r = s
proof
  given x such that
A1: s = r+x;
  given y such that
A2: r = s+y;
  r+{} = r by Th56
    .= r+(x+y) by A1,A2,Th57;
  then x = {} by Th69,Th70;
  hence thesis by A1,Th56;
end;

theorem Th74:
  r <=' s & s <=' t implies r <=' t
proof
  given x such that
A1: s = r+x;
  given y such that
A2: t = s+y;
  take x+y; thus thesis by A1,A2,Th57;
end;

theorem
  r < s iff r <=' s & r <> s by Th73;

theorem
  r < s & s <=' t or r <=' s & s < t implies r < t by Th74;

theorem
  r < s & s < t implies r < t by Th74;

theorem Th78:
  x in omega & x+y in omega implies y in omega
proof
  assume
A1: x in omega & x+y in omega;
  set nx = numerator x, dx = denominator x;
  set ny = numerator y, dy = denominator y;
A2: x = nx/dx & y = ny/dy & x+y = numerator (x+y)/denominator (x+y) by Th45;
A3: dx = 1 & dy <> {} & denominator (x+y) = 1 by A1,Def9,Th41;
  then
A4: dx*^dy <> {} by ORDINAL3:34;
  (nx*^dy+^ny*^dx)*^1 = nx*^dy+^ny*^dx by ORDINAL2:56;
  then nx*^dy+^ny*^dx = dx*^dy*^numerator (x+y) by A2,A3,A4,Th51
    .= dy*^numerator (x+y) by A3,ORDINAL2:56;
  then nx*^dy+^ny = dy*^numerator (x+y) by A3,ORDINAL2:56;
  then ny = (dy*^numerator (x+y))-^nx*^dy by ORDINAL3:65;
  then ny = dy*^((numerator (x+y))-^nx) by ORDINAL3:76;
  then dy divides ny & dy divides dy &
  for m being natural Ordinal st m divides dy & m divides ny holds m
  divides dy by Def3;
  then dy hcf ny = dy & ny,dy are_relative_prime by Def5,Th40;
  then dy = 1 by Th25;
  then y = ny by A2,Th46;
  hence thesis;
end;

theorem Th79:
  for i being ordinal Element of RAT+ st i < x & x < i+one
  holds not x in omega
proof
  let i be ordinal Element of RAT+;
  assume
A1: i < x & x < i+one & x in omega;
  then consider y such that
A2: x = i+y by Def13;
  consider z such that
A3: i+one = x+z by A1,Def13;
  i+one = i+^1 by Th64;
  then i+one in omega by Th37;
  then reconsider z' = z as Element of omega by A1,A3,Th78;
  i in omega by Th37;
  then reconsider y' = y as Element of omega by A1,A2,Th78;
  i+one = i+(y+z) by A2,A3,Th57;
  then 1 = y+z by Th69
    .= y'+^z' by Th64;
  then y' c= 1 & z' c= 1 by ORDINAL3:27;
  then (y = {} or y = 1) & (z = {} or z = 1) by ORDINAL3:19;
  then i = x or i+one = x by A2,Th56;
  hence contradiction by A1;
end;

theorem Th80:
  t <> {} implies ex r st r < t & not r in omega
proof
  assume
A1: t <> {};
A2: 1+^1 = succ 1 by ORDINAL2:48;
  per cases;
  suppose
A3: one <=' t;
    consider r such that
A4: one = r+r by Th66;
    take r;
A5: r <=' one by A4,Def13;
    r <> 1 by A2,A4,Th64;
    then r < one by A5,Th73;
    hence r < t by A3,Th74;
    assume r in omega;
    then
A6: denominator r = 1 & denominator one = 1 by Def9;
    then (numerator r)*^denominator r = numerator r & 1*^1 = 1 by ORDINAL2:56;
    then
A7: 1 = (numerator r)+^numerator r by A4,A6,Th46;
    then numerator r c= 1 by ORDINAL3:27;
    then numerator r = {} or numerator r = 1 by ORDINAL3:19;
    hence contradiction by A2,A7,ORDINAL2:44;
  end;
  suppose
A8: t < one;
    consider r such that
A9: t = r+r by Th66;
    take r;
A10: r <=' t by A9,Def13;
    now
      assume r = t;
      then t+{} = t+t by A9,Th56;
      hence contradiction by A1,Th69;
    end;
    hence r < t by A10,Th73;
A11: r < one by A8,A10,Th74;
    r <> {} & {} <=' r by A1,A9,Th56,Th71;
    then {} < r & 1 = {}+one by Th56,Th73;
    hence thesis by A11,Th79;
  end;
end;

theorem
  {s: s < t} in RAT+ iff t = {}
proof
  hereby
    assume
A1: {s: s < t} in RAT+ & t <> {};
    then consider r such that
A2: r < t & not r in omega by Th80;
A3: r in {s: s < t} by A2;
     {s: s < t} in omega implies r is Ordinal by A3;
    then consider i,j being Element of omega such that
A4: {s: s < t} = [i,j] & i,j are_relative_prime & j <> {} & j <> 1
    by A1,A2,Th35,Th37;
    {} <=' t by Th71;
    then {} < t by A1,Th73;
    then {} in {s: s < t};
    hence contradiction by A4,TARSKI:def 2;
  end;
  assume
A5: t = {};
  {s: s < t} c= {}
  proof
    let a be set;
    assume a in {s: s < t};
    then ex s st a = s & s < t;
    hence a in {} by A5,Th71;
  end;
  then {s: s < t} = {};
  hence thesis;
end;

theorem
  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
proof
  let A be Subset of RAT+;
  given t such that
A1: t in A & t <> {};
  assume
A2: for r,s st r in A & s <=' r holds s in A;
  consider x such that
A3: t = x+x by Th66;
  take {}, x, t;
  {} <=' t & x <=' t by A3,Def13,Th71;
  hence {} in A & x in A & t in A by A1,A2;
  thus {} <> x by A1,A3,Th56;
  hereby
    assume x = t;
    then t+{} = t+t by A3,Th56;
    hence contradiction by A1,Th69;
  end;
  thus thesis by A1;
end;

theorem Th83:
  s + t <=' r + t iff s <=' r
proof
  thus s + t <=' r + t implies s <=' r
  proof
    given z such that
A1: r+t = s+t+z;
    take z;
    r+t = s+z+t by A1,Th57;
    hence r = s+z by Th69;
  end;
  given z such that
A2: r = s+z;
  take z; thus thesis by A2,Th57;
end;

canceled;

theorem
  s <=' s + t
proof
  take t; thus thesis;
end;

theorem
  r*'s = {} implies r = {} or s = {}
proof
  set nr = numerator r, dr = denominator r;
  set ns = numerator s, ds = denominator s;
  dr <> {} & ds <> {} & denominator (r*'s) <> {} by Th41;
  then
A1: dr*^ds <> {} by ORDINAL3:34;
A2: denominator {} = 1 & numerator {} = {} by Def8,Def9,Lm1;
  assume r*'s = {};
  then (nr*^ns)/(dr*^ds) = {}/1 by A2,Th45;
  then (nr*^ns)*^1 = (dr*^ds)*^{} by A1,Th51
    .= {} by ORDINAL2:52;
  then nr*^ns = {} by ORDINAL3:34;
  then nr = {} or ns = {} by ORDINAL3:34;
  hence thesis by Th43;
end;

theorem Th87:
  r <=' s *' t implies ex t0 being Element of RAT+ st r = s *' t0 & t0 <=' t
proof
  given x such that
A1: s*'t = r+x;
  per cases;
  suppose s = {};
    then
A2: s*'t = {} by Th54;
    take t; thus thesis by A1,A2,Th70;
  end;
  suppose
A3: s <> {};
    then consider t0 being Element of RAT+ such that
A4: r = s*'t0 by Th61;
    consider t1 being Element of RAT+ such that
A5: x = s*'t1 by A3,Th61;
    take t0; thus r = s*'t0 by A4;
    take t1;
    s*'t = s*'(t0+t1) by A1,A4,A5,Th63;
    hence t = t0+t1 by A3,Th62;
  end;
end;

theorem
  t <> {} & s *' t <=' r *' t implies s <=' r
proof
  assume
A1: t <> {} & s *' t <=' r *' t;
  then consider x such that
A2: s*'t = t*'x & x <=' r by Th87;
  thus s <=' r by A1,A2,Th62;
end;

theorem
  for r1,r2,s1,s2 being Element of RAT+ st r1+r2 = s1+s2
  holds r1 <=' s1 or r2 <=' s2
proof
  let r1,r2,s1,s2 be Element of RAT+ such that
A1: r1+r2 = s1+s2;
  assume s1 < r1 & s2 < r2;
  then s1+s2 < r1+s2 & r1+s2 <=' r1+r2 by Th83;
  hence thesis by A1;
end;

theorem Th90:
  s <=' r implies s *' t <=' r *' t
proof
  given x such that
A1: r = s+x;
  take y = x*'t;
  thus r*'t = s*'t+y by A1,Th63;
end;

theorem
  for r1,r2,s1,s2 being Element of RAT+ st r1*'r2 = s1*'s2
  holds r1 <=' s1 or r2 <=' s2
proof
  let r1,r2,s1,s2 be Element of RAT+ such that
A1: r1*'r2 = s1*'s2;
  assume
A2: s1 < r1 & s2 < r2;
  then
A3: s1 <=' r1 & s1 <> r1 & s2 <=' r2 & s2 <> r2;
  {} <=' s1 & {} <=' s2 by Th71;
  then s1*'s2 <=' r1*'s2 & s1*'s2 <> r1*'s2 by A1,A2,A3,Th62,Th90;
  then s1*'s2 < r1*'s2 & r1*'s2 <=' r1*'r2 by A2,Th73,Th90;
  hence thesis by A1;
end;

theorem
  r = {} iff r + s = s
proof s+{} = s by Th56;
  hence thesis by Th69;
end;

theorem
  for s1,t1,s2,t2 being Element of RAT+ st s1 + t1 = s2 + t2 & s1 <=' s2
  holds t2 <=' t1
proof
  let s1,t1,s2,t2 be Element of RAT+ such that
A1: s1 + t1 = s2 + t2;
  given x such that
A2: s2 = s1+x;
  take x;
  s1+t1 = s1+(x+t2) by A1,A2,Th57;
  hence thesis by Th69;
end;

theorem Th94:
  r <=' s & s <=' r + t implies
  ex t0 being Element of RAT+ st s = r + t0 & t0 <=' t
proof
  given t0 being Element of RAT+ such that
A1: s = r+t0;
  assume s <=' r+t;
  then t0 <=' t by A1,Th83;
  hence thesis by A1;
end;

theorem
  r <=' s + t implies
  ex s0,t0 being Element of RAT+ st r = s0 + t0 & s0 <=' s & t0 <=' t
proof
  assume
A1: r <=' s + t;
  per cases;
  suppose s <=' r;
    then s <=' s & ex t0 being Element of RAT+ st r = s + t0 & t0 <=' t by A1,
    Th94;
    hence thesis;
  end;
  suppose r <=' s;
    then r = r+{} & r <=' s & {} <=' t by Th56,Th71;
    hence thesis;
  end;
end;

theorem
  r < s & r < t implies
  ex t0 being Element of RAT+ st t0 <=' s & t0 <=' t & r < t0
proof s <=' t & s <=' s or t <=' s & t <=' t;
  hence thesis;
end;

theorem
  r <=' s & s <=' t & s <> t implies r <> t by Th73;

theorem
  s < r + t & t <> {} implies ex r0,t0 being Element of RAT+ st s = r0 + t0 &
  r0 <=' r & t0 <=' t & t0 <> t
proof
  assume
A1: s < r + t & t <> {};
  per cases;
  suppose r <=' s;
    then consider t0 being Element of RAT+ such that
A2: s = r + t0 & t0 <=' t by A1,Th94;
    take r,t0; thus thesis by A1,A2;
  end;
  suppose
A3: s <=' r;
    s = s+{} & {} <=' t by Th56,Th71;
    hence thesis by A1,A3;
  end;
end;

theorem
  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
proof
  let A be non empty Subset of RAT+;
  assume
A1: A in RAT+;
  now
    given i,j being Element of omega such that
A2: A = [i,j] & i,j are_relative_prime & j <> {} & j <> 1;
A3: {i} in A by A2,TARSKI:def 2;
    now
      assume {i} in omega;
      then {i} is Ordinal;
      then {} in {i} by ORDINAL3:10;
      then {} = i by TARSKI:def 1;
      hence contradiction by A2,Th7;
    end;
    then consider i1,j1 being Element of omega such that
A4: {i} = [i1,j1] & i1,j1 are_relative_prime & j1 <> {} & j1 <> 1 by A3,Th35;
    {i1} in {i} & {i1,j1} in {i} by A4,TARSKI:def 2;
    then i = {i1} & i = {i1,j1} by TARSKI:def 1;
    then j1 in {i1} by TARSKI:def 2;
    then j1 = i1 & j1 = j1*^1 by ORDINAL2:56,TARSKI:def 1;
    hence contradiction by A4,Def2;
  end;
  then reconsider B = A as Element of omega by A1,Th35;
A5: {} in B by ORDINAL3:10;
  now
    assume B is_limit_ordinal;
    then omega c= B by A5,ORDINAL1:def 12;
    hence contradiction by ORDINAL1:7;
  end;
  then consider C such that
A6: B = succ C by ORDINAL1:42;
  C in B by A6,ORDINAL1:10;
  then reconsider C as ordinal Element of RAT+;
  take C; thus C in A by A6,ORDINAL1:10;
  let r;
  assume
A7: r in A;
  then r in B;
  then reconsider r as ordinal Element of RAT+;
  C-^r in omega by ORDINAL1:def 13;
  then reconsider x = C-^r as ordinal Element of RAT+ by Lm5;
  r c= C by A6,A7,ORDINAL1:34;
  then C = r+^x by ORDINAL3:def 6
    .= r+x by Th64;
  hence thesis by Def13;
end;

theorem
  ex t st r + t = s or s + t = r
proof r <=' s or s <=' r;
  hence thesis by Def13;
end;

theorem
  r < s implies ex t st r < t & t < s
proof
  assume
A1: r < s;
  then consider x such that
A2: s = r+x by Def13;
  consider y such that
A3: x = y+y by Th66;
  take t = r+y;
A4: s = t+y by A2,A3,Th57;
A5: r <> s & t+{} = t & r+{} = r & {}+{} = {} by A1,Th56;
  r <=' t & r <> t by A1,A4,Def13;
  hence r < t by Th73;
  t <=' s & s <> t by A4,A5,Def13,Th69;
  hence t < s by Th73;
end;

theorem
  ex s st r < s
proof
  take s = r+one;
  s+{} = s by Th56;
  then r <=' s & r <> s by Def13,Th69;
  hence thesis by Th73;
end;

theorem
  t <> {} implies ex s st s in omega & r <=' s *' t
proof
  assume t <> {};
  then
A1: numerator t <> {} by Th43;
  (denominator t)*^(numerator r) in omega by ORDINAL1:def 13;
  then reconsider s = (denominator t)*^(numerator r)
  as ordinal Element of RAT+ by Lm5;
  take s; thus s in omega by ORDINAL1:def 13;
  set y=((numerator r)*^(((numerator t)*^denominator r)-^1))/denominator r;
  take y;
A2: denominator r <> {} & denominator t <> {} by Th41;
  then {} in (numerator t)*^denominator r by A1,ORDINAL3:10,34;
  then one c= (numerator t)*^denominator r by Lm3,ORDINAL1:33;
  then (numerator t)*^denominator r = 1+^(((numerator t)*^denominator r)-^ 1)
  by ORDINAL3:def 6;
  then s*^((numerator t)*^denominator r) = (denominator t)*^
  ((numerator r)*^(1+^(((numerator t)*^denominator r)-^1))) by ORDINAL3:58
    .= (denominator t)*^((numerator r)*^1+^
  (numerator r)*^(((numerator t)*^denominator r)-^1)) by ORDINAL3:54;
  then s*^(numerator t)*^denominator r = (denominator t)*^((numerator r)*^1+^
  (numerator r)*^(((numerator t)*^denominator r)-^1)) by ORDINAL3:58;
  then (s*^(numerator t))/denominator t = ((numerator r)*^1+^
  (numerator r)*^(((numerator t)*^denominator r)-^1))/denominator r by A2,Th51
    .= (((numerator r)*^1)/denominator r)+y by Th41,Th53
    .= ((numerator r)/denominator r)+y by ORDINAL2:56
    .= r+y by Th45;
  then r+y = (s*^(numerator t))/(1*^denominator t) by ORDINAL2:56
    .= (s/1)*'((numerator t)/denominator t) by Th55
    .= s*'((numerator t)/denominator t) by Th46;
  hence thesis by Th45;
end;

scheme DisNat { n0,n1,n2() -> Element of RAT+, P[set] }:
  ex s st s in omega & P[s] & not P[s + n1()]
provided
A1: n1() = 1
and
A2: n0() = {}
and
A3: n2() in omega
and
A4: P[n0()]
and
A5: not P[n2()]
proof
  defpred P1[Ordinal] means not P[$1] & $1 in omega;
A6: ex A st P1[A] by A3,A5;
  consider A such that
A7: P1[A] and
A8: for B st P1[B] holds A c= B from ORDINAL1:sch 1(A6);
A9: {} in A by A2,A4,A7,ORDINAL3:10;
  now
    assume A is_limit_ordinal;
    then omega c= A by A9,ORDINAL1:def 12;
    then A in A by A7;
    hence contradiction;
  end;
  then consider B being Ordinal such that
A10: A = succ B by ORDINAL1:42;
  B in A by A10,ORDINAL1:13;
  then
A11: B in omega & not A c= B by A7,ORDINAL1:7,19;
  then reconsider s = B as ordinal Element of RAT+ by Lm5;
  take s; thus s in omega & P[s] by A8,A11;
  A = B+^1 by A10,ORDINAL2:48;
  hence thesis by A1,A7,Th64;
end;