The Mizar article:

Arithmetic of Non-Negative Rational Numbers

by
Grzegorz Bancerek

Received March 7, 1998

Copyright (c) 1998 Association of Mizar Users

MML identifier: ARYTM_3
[ 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;
 definitions TARSKI, ORDINAL2;
 theorems TARSKI, XBOOLE_0, ZFMISC_1, ORDINAL1, ORDINAL2, ORDINAL3, SUBSET_1,
      XBOOLE_1;
 schemes ORDINAL1, ORDINAL2;

begin :: Natural ordinals

reserve A,B,C for Ordinal;

Lm1: one in omega by ORDINAL1:41,ORDINAL2:19,def 4;

definition
 let A be Ordinal;
 cluster -> ordinal Element of A;
 coherence
   proof
    let x be Element of A;
      A is empty or A is non empty;
    hence thesis by ORDINAL1:23,SUBSET_1:def 2;
   end;
end;

definition
 cluster empty -> natural Ordinal;
 coherence by ORDINAL2:19,def 21;
 cluster one -> natural non empty;
 coherence by Lm1,ORDINAL2:def 21;
 cluster -> natural Element of omega;
 coherence by ORDINAL2:def 21;
end;

definition
 cluster non empty natural Ordinal;
 existence proof take one; thus thesis; end;
end;

definition let a be natural Ordinal;
 cluster succ a -> natural;
 coherence
  proof
      a in omega by ORDINAL2:def 21;
   hence succ a in omega by ORDINAL1:41,ORDINAL2:19;
  end;
end;

scheme Omega_Ind {P[set]}:
 for a being natural Ordinal holds P[a]
provided
A1:   P[{}]
and
A2:   for a being natural Ordinal st P[a] holds P[succ a]
  proof
     defpred _P[Ordinal] means $1 is natural implies P[$1];
A3:  _P[{}] by A1;
A4:  now let A; assume
A5:   _P[A];
      now assume succ A is natural;
       then succ A in omega & A in succ A by ORDINAL1:10,ORDINAL2:def 21;
       then A is Element of omega by ORDINAL1:19;
       hence P[succ A] by A2,A5;
      end; hence _P[succ A];
    end;
A6:  now let A;
A7:   {} c= A by XBOOLE_1:2;
     assume A <> {};
     then {} c< A by A7,XBOOLE_0:def 8;
then A8:   {} in A by ORDINAL1:21;
     assume A is_limit_ordinal;
      then omega c= A & not A in A by A8,ORDINAL2:def 5;
      then not A in omega;
     hence (for B st B in A holds _P[B]) implies _P[A] by ORDINAL2:def 21;
    end;
      for A holds _P[A] from Ordinal_Ind(A3,A4,A6);
   hence thesis;
  end;

definition
 let a, b be natural Ordinal;
 cluster a +^ b -> natural;
 coherence
  proof defpred _P[natural Ordinal] means a+^$1 is natural;
A1:  _P[{}] by ORDINAL2:44;
A2:  now let b be natural Ordinal; assume _P[b]; then
     reconsider c = a+^b as natural Ordinal; a+^succ b = succ c by ORDINAL2:45;
     hence _P[succ b];
    end;
      for b being natural Ordinal holds _P[b] from Omega_Ind(A1,A2);
   hence thesis;
  end;
end;

theorem Th1:
 for a,b being Ordinal st a+^b is natural holds a in omega & b in omega
  proof let x,y be Ordinal such that
A1:  x+^y in omega;
      x c= x+^y & y c= x+^y by ORDINAL3:27;
   hence x in omega & y in omega by A1,ORDINAL1:22;
  end;

definition
 let a, b be natural Ordinal;
 cluster a -^ b -> natural;
 coherence
  proof not b c= a or b c= a;
    then a -^ b = {} or a = b+^(a-^b) by ORDINAL3:def 6;
   hence a-^b in omega by Th1,ORDINAL2:def 5;
  end;
 cluster a *^ b -> natural;
 coherence
  proof defpred _P[natural Ordinal] means $1*^b is natural;
A1:  _P[{}] by ORDINAL2:52;
A2:  now let a be natural Ordinal; assume _P[a]; then
     reconsider c = a*^b as natural Ordinal; (succ a)*^b = c+^b by ORDINAL2:53;
     hence _P[succ a];
    end;
      for a being natural Ordinal holds _P[a] from Omega_Ind(A1,A2);
   hence thesis;
  end;
end;

theorem Th2:
 for a,b being Ordinal st a*^b is natural non empty
  holds a in omega & b in omega
  proof let x,y be Ordinal such that
A1:  x*^y in omega;
   assume x*^y is non empty;
    then x <> {} & y <> {} by ORDINAL2:52,55;
    then x c= x*^y & y c= x*^y by ORDINAL3:39;
   hence x in omega & y in omega by A1,ORDINAL1:22;
  end;

theorem Th3:
 for a,b being natural Ordinal holds a+^b = b+^a
  proof let a be natural Ordinal;
     defpred _R[natural Ordinal] means a+^$1 = $1+^a;
    a+^{} = a by ORDINAL2:44 .= {}+^a by ORDINAL2:47; then
A1: _R[{}];
A2:  now let b be natural Ordinal; assume
A3:    _R[b];
      defpred _P[natural Ordinal] means (succ b)+^$1 = succ (b+^$1);
   (succ b)+^{} = succ b by ORDINAL2:44 .= succ (b+^{}) by ORDINAL2:44;then
A4:  _P[{}];
A5:   now let a be natural Ordinal; assume
A6:    _P[a];
        (succ b)+^succ a
          = succ ((succ b)+^a) by ORDINAL2:45
         .= succ (b+^succ a) by A6,ORDINAL2:45;
       hence _P[succ a];
      end;
A7:  for a being natural Ordinal holds _P[a] from Omega_Ind(A4,A5);
      a+^succ b = succ (b+^a) by A3,ORDINAL2:45 .= (succ b)+^a by A7;
     hence _R[succ b];
    end;
    for b being natural Ordinal holds _R[b] from Omega_Ind(A1,A2);
   hence thesis;
  end;

theorem Th4:
 for a,b being natural Ordinal holds a*^b = b*^a
  proof let a be natural Ordinal;
     defpred _R[natural Ordinal] means a*^$1 = $1*^a;
     a*^{} = {} by ORDINAL2:55 .= {}*^a by ORDINAL2:52; then
A1: _R[{}];
A2:  now let b be natural Ordinal;
      defpred _P[natural Ordinal] means $1*^succ b = $1*^b+^$1;
     assume
A3:   _R[b];
     {}*^succ b = {} by ORDINAL2:52 .= {}+^{} by ORDINAL2:44
               .= {}*^b+^{} by ORDINAL2:52; then
A4:  _P[{}];
A5:   now let a be natural Ordinal; assume
A6:    _P[a];
        (succ a)*^succ b
          = a*^(succ b)+^succ b by ORDINAL2:53
         .= a*^b+^(a+^succ b) by A6,ORDINAL3:33
         .= a*^b+^succ (a+^b) by ORDINAL2:45
         .= succ (a*^b+^(a+^b)) by ORDINAL2:45
         .= succ (a*^b+^(b+^a)) by Th3
         .= succ (a*^b+^b+^a) by ORDINAL3:33
         .= succ ((succ a)*^b+^a) by ORDINAL2:53
         .= (succ a)*^b+^succ a by ORDINAL2:45;
       hence _P[succ a];
      end;
        for a being natural Ordinal holds _P[a] from Omega_Ind(A4,A5);
     then a*^succ b = b*^a+^a by A3 .= (succ b)*^a by ORDINAL2:53;
     hence _R[succ b];
    end;
    for b being natural Ordinal holds _R[b] from Omega_Ind(A1,A2);
   hence thesis;
  end;

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

begin :: Relative prime numbers and divisibility

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

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

theorem Th6:
 one,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 = one
  proof assume
A1:  {},A are_relative_prime & A <> one;
    then A in one or one in A by ORDINAL1:24;
    then one in A & {} = A*^{} & A = A*^one by A1,Th5,ORDINAL2:55,56,ORDINAL3:
17;
   hence contradiction by A1,Def1;
  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,ORDINAL2:def 21,XBOOLE_1:3;
      thus not ex c,d1,d2 being natural Ordinal st
        d1,d2 are_relative_prime & A = c *^ d1 & B = c *^ d2 by A2;
      suppose
A5:    b c= a;
      take A = a, B = b;
      thus B c= A & A in omega & A <> {} by A1,A5,ORDINAL2:def 21,XBOOLE_1:3;
      thus not ex c,d1,d2 being natural Ordinal st
        d1,d2 are_relative_prime & A = c *^ d1 & B = c *^ d2 by A2;
    end;
   consider A such that
A6:  PP[A] and
A7:  for C st PP[C] holds A c= C from Ordinal_Min(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 = one *^ A & B = one *^ 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 <> one by Def1;
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;
      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;
then A13:  A c= d1 by A7,A10,A11;
      one in c or c in one by A9,ORDINAL1:24;
    then one*^d1 in A by A9,A10,ORDINAL3:17,22;
    then d1 in A by ORDINAL2:56;
   hence contradiction by A13,ORDINAL1:7;
  end;

reserve l,m,n for natural Ordinal;

definition let m,n;
 cluster m div^ n -> natural;
 coherence
  proof A1: n in one or one c= n by ORDINAL1:26;
      n = {} implies m div^ n = {} & {}*^one = {}
 by ORDINAL2:52,ORDINAL3:def 7;
    then (m div^ n)*^one c= (m div^ n)*^n by A1,ORDINAL3:17,23,XBOOLE_1:2;
    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 ORDINAL2:def 21,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 ORDINAL2:def 21,ORDINAL3:27;
   hence m mod^ n in omega by ORDINAL1:22;
  end;
end;

definition
 let k,n be Ordinal;
 pred k divides n means: Def2: ex a being Ordinal st n = k*^a;
 reflexivity
  proof let n be Ordinal; take one;
   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;
     suppose b <> {};
       then c is Element of omega by A1,Th2;
      hence ex c st b = a*^c by A1;
    end;
   thus thesis by Def2;
  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,Def2,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 *^ one = 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) = one implies n = m
      proof assume (m div^ n) *^ (n div^ m) = one;
        then m div^ n = one by ORDINAL3:41;
       hence n = m by A1,ORDINAL2:56;
      end;
    hence n = m by A2,A3,ORDINAL3:36;
   end;

theorem Th14:
 n divides {} & one divides n
  proof
      {} = n *^ {} by ORDINAL2:52;
   hence n divides {} by Def2;
      n = one *^ n by ORDINAL2:56;
   hence thesis by Def2;
  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,Def2;
  end;

definition let k,n be natural Ordinal;
 func k lcm n -> Element of omega means:
Def3:  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 ORDINAL2:def 21;
     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;
    suppose
A2:    k <> {} & n <> {};
A3:    k divides k *^ n & n divides k *^ n by Def2;
      defpred _P[Ordinal] means
        ex m st $1 = m & k divides m & n divides m & k c= m;
        {} c= n by XBOOLE_1:2;
      then {} c< n by A2,XBOOLE_0:def 8;
      then {} in n by ORDINAL1:21;
      then one c= n by ORDINAL1:33,ORDINAL2:def 4;
      then k*^one = k & k *^ one 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 Ordinal_Min(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 ORDINAL2:def 21;
     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 by XBOOLE_1:2;
        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 Def2;
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 by XBOOLE_1:2;
          then {} c< m mod^ l by A12,XBOOLE_0:def 8;
          then {} in m mod^ l by ORDINAL1:21;
          then k c= m mod^ l by A11,Th15;
          then l c= m mod^ l by A6,A7,A11;
          then not m mod^ l in l by ORDINAL1:7;
         hence contradiction by A7,A9,Th10;
        end;
        then m = l*^(m div^ l) by A10,ORDINAL2:44;
       hence l divides m by Th11;
      end;
     hence l divides m;
   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 Def2;
   hence thesis by Def3;
  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 Def3,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:
Def4:  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 ORDINAL2:def 21;
     take m;
     thus m divides k & m divides n by A1,Th14;
     thus thesis by A1;
    suppose
A2:    k <> {} & n <> {};
     reconsider l = (k*^n) div^ (k lcm n) as Element of omega
       by ORDINAL2:def 21;
     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,Def2;
then A4:    k lcm n divides
 m*^(k div^ m)*^(n div^ m) & mm = m*^(k div^ m)*^(n div^ m)
       by Def3,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 mm <> {} by A7,ORDINAL3:34;
      then k lcm n <> {} by A5,ORDINAL2:52;
      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 Def2;
   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 ORDINAL2:def 21;
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,Def3,Def4;
  end;

theorem Th20:
 a hcf b = {} implies a = {}
  proof a hcf b divides a by Def4;
    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 ORDINAL2:def 21;
      c divides a & for b st b divides a & b divides a holds b divides c;
   hence a hcf a = a by Def4;
      a divides c & for b st a divides b & a divides b holds c divides b;
   hence thesis by Def3;
  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;
   suppose
A1:  c <> {} & a <> {};
   reconsider d = (a hcf b)*^c as Element of omega by ORDINAL2:def 21;
   set e = ((a*^c) hcf (b*^c)) div^ d;
      a hcf b divides a & a hcf b divides b by Def4;
    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 Def2;
    then d divides (a*^c) hcf (b*^c) by Def4;
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 Def4;
    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 Def2;
    then (a hcf b)*^e divides a hcf b by Def4;
    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)*^one by ORDINAL2:56;
    then a hcf b = {} or e*^((a hcf b) div^ ((a hcf b)*^e)) = one
     by ORDINAL3:36;
    then e = one by A1,Th20,ORDINAL3:41;
   hence thesis by A2,ORDINAL2:56;
   suppose a = {};
    then a hcf b = b & a*^c = {} by Th19,ORDINAL2:52;
   hence thesis by Th19;
  end;

theorem Th23:
 b <> {} implies a hcf b <> {} & b div^ (a hcf b) <> {}
  proof
      a hcf b divides b by Def4;
    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:  one*^a = a & one*^b = b by ORDINAL2:56;
   set ab = a hcf b;
   per cases;
   suppose a = {} or b = {};
    then ab = b & b div^ b = one or
    ab = a & a div^ a = one by A1,A2,Th19,ORDINAL3:81;
   hence thesis by Th6;
   suppose
A3:  a <> {} & b <> {};
      ab divides a & ab divides b by Def4;
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,Th2;
      a = ab*^c*^d1 & b = ab*^c*^d2 by A4,A5,ORDINAL3:58;
    then ab*^c divides a & ab*^c divides b by Def2;
    then ab*^c divides ab by Def4;
    then ab = (ab*^c)*^(ab div^ (ab*^c)) by Th11;
    then ab = ab*^(c*^(ab div^ (ab*^c))) by ORDINAL3:58;
    then ab*^one = ab*^(c*^(ab div^ (ab*^c))) & ab <> {} by A3,A4,ORDINAL2:52,
56;
    then one = c*^(ab div^ (ab*^c)) by ORDINAL3:36;
   hence thesis by ORDINAL3:41;
  end;

theorem Th25:
 a,b are_relative_prime iff a hcf b = one
  proof
      a hcf b divides a & a hcf b divides b by Def4;
    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 = one by Def1;
   assume
A1:  a hcf b = one;
   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,Th2;
      c divides a & c divides b by A2,Def2;
    then c divides one by A1,Def4;
    then ex d st one = 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:
Def5:
  a div^ (a hcf b);
 coherence by ORDINAL2:def 21;
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 Def4,Def5;
   hence thesis by Th11;
  end;

theorem Th27:
 a <> {} or b <> {} implies RED(a,b), RED(b,a) are_relative_prime
  proof assume a <> {} or b <> {};
then A1:  a div^ (a hcf b), b div^ (a hcf b) are_relative_prime by Th24;
      RED(a,b) = a div^ (a hcf b) by Def5;
   hence thesis by A1,Def5;
  end;

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

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

theorem Th30:
 b <> {} implies RED(b,a) <> {}
  proof RED(b,a) = b div^ (b hcf a) by Def5;
   hence thesis by Th23;
  end;

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

theorem Th32:
 a <> {} implies RED(a,a) = one
  proof assume
A1:  a <> {};
   thus RED(a,a) = a div^ (a hcf a) by Def5 .= a div^ a by Th21
     .= a*^one div^ a by ORDINAL2:56
     .= one 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 Def4;
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 Th31,ORDINAL2:52,ORDINAL3:83;
A5:  a div^ (a hcf b) = RED(a,b) by Def5;
   thus RED(a*^c, b*^c)
      = (a*^c)div^((a*^c) hcf (b*^c)) by Def5
     .= (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 A5,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 <> {}};

reconsider 01 = one as Element of omega by ORDINAL2:def 21;
  01 <> {} & 01,01 are_relative_prime by Th6;
then [01,01] in RATplus;
then reconsider RATplus as non empty set;

Lm2: [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:
Def6:
  ({[i,j]: i,j are_relative_prime & j <> {}} \ {[k,one]: not contradiction})
  \/ omega;
 correctness;
end;

theorem Th34:
 omega c= RAT+ by Def6,XBOOLE_1:7;

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

definition
 cluster RAT+ -> non empty;
 coherence by Th34,ORDINAL2:19;
end;

definition
 cluster non empty ordinal Element of RAT+;
 existence by Lm1,Th34;
end;

theorem Th35:
 x in
 omega or ex i,j st x = [i,j] & i,j are_relative_prime & j <> {} & j <> one
  proof assume not x in omega;
    then x in RATplus \ {[k,one]: not contradiction} by Def6,XBOOLE_0:def 2;
then A1:  x in RATplus & not x in {[k,one]: 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,one] in {[k,one]: 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;
A2:  [i,j] = {{i},{i,j}} by TARSKI:def 5;
    {} in [i,j] by A1,ORDINAL3:10;
   hence thesis by A2,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 <> one by
Th35;
   hence thesis by Th36;
  end;

definition
 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 <> one by Th35;
A2:  x = {{i},{i,j}} by A1,TARSKI:def 5;
    then {} in x by ORDINAL3:10;
   hence thesis by A2,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;
A2:  [i,j] = {{i},{i,j}} by TARSKI:def 5;
   reconsider a = [i,j] as Element of omega by A1;
   {} in a by ORDINAL3:10;
   hence thesis by A2,TARSKI:def 2;
  end;

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

definition
 let x be Element of RAT+;
 func numerator x -> Element of omega means:
Def7:
  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,one]: not contradiction} by Def6,XBOOLE_0:def 2;
     then x in RATplus by XBOOLE_0:def 4;
    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:
Def8:
  it = one 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 = one by Lm1;
   assume not x in omega;
     then x in RATplus \ {[k,one]: not contradiction} by Def6,XBOOLE_0:def 2;
     then x in RATplus 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 <> {};
    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 = one by Def8;
   hence thesis by Th6;
   suppose
A1:  not x in omega;
   then consider i,j such that
A2:  x = [i,j] & i,j are_relative_prime & j <> {} & j <> one by Th35;
      i = numerator x by A1,A2,Def7;
   hence thesis by A1,A2,Def8;
  end;

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

theorem Th42:
 not x in omega implies x = [numerator x, denominator x] & denominator x <> one
  proof assume
A1:  not x in omega;
   then consider i,j such that
A2:  x = [i,j] & i,j are_relative_prime & j <> {} & j <> one by Th35;
      i = numerator x & j = denominator x by A1,A2,Def7,Def8;
   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 Def7;
    then consider i,j such that
A3:   x = [i,j] & i,j are_relative_prime & j <> {} & j <> one by Th35;
       i = {} by A1,A2,A3,Def7;
    hence contradiction by A3,Th7;
   end;
      {} in omega by ORDINAL2:def 5;
   hence thesis by Def7;
  end;

theorem
  x in omega iff denominator x = one by Def8,Th42;

definition
 let i,j be natural Ordinal;
 func i/j -> Element of RAT+ equals:
Def9:
  {} if j = {},
  RED(i,j) if RED(j,i) = one 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 Th27,Th30
;
     hence RED(j,i) <> one implies [RED(i,j), RED(j,i)] in RAT+ by Th39;
    end;
   hence thesis by A1,Th34,ORDINAL2:19;
  end;
 consistency by Th31;
 synonym quotient(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 = one;
    then x in omega by Th42;
    then numerator x = x by Def7;
   hence thesis by A2,A3,Def9;
   suppose
A4:  denominator x <> one;
    then not x in omega by Def8;
    then x = [numerator x, denominator x] by Th42;
   hence thesis by A1,A2,A4,Def9;
  end;

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

theorem Th47:
 a <> {} implies a/a = one
  proof assume a <> {};
    then RED(a,a) = one by Th32;
   hence thesis by Def9;
  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) = one;
    then a/b = RED(a,b) by Def9;
   hence thesis by A2,Def7,Def8;
   suppose
    RED(b,a) <> one;
    then a/b = [RED(a,b), RED(b,a)] & not [RED(a,b), RED(b,a)] in omega
     by A1,Def9,Th38;
   hence thesis by Def7,Def8;
  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 Def9,ORDINAL2:52;
   hence thesis by Def9;
   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;

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:
Def10:
  ((numerator x)*^(denominator y)+^(numerator y)*^(denominator x))
   / ((denominator x)*^(denominator y));
 coherence;
 commutativity;
 func x*'y -> Element of RAT+ equals:
Def11:
  ((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 A2:  i hcf j <> {} & k hcf l <> {} by Th20;
      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 A1,Th48;
   hence (i/j)+(k/l)
       = (RED(i,j)*^RED(l,k)+^RED(j,i)*^RED(k,l))/(RED(j,i)*^RED(l,k))
         by Def10
      .= (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 A2,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 A2,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;

definition
 cluster empty Element of RAT+;
 existence by Th34,ORDINAL2:19;
end;

definition
 redefine
 func {} -> empty Element of RAT+;
 coherence by Th34,ORDINAL2:19;
 func one -> non empty ordinal Element of RAT+;
 coherence by Lm1,Th34;
end;

theorem Th54:
 x*'{} = {}
  proof
      denominator {} = one & numerator {} = {} & (numerator x)*^{} = {} &
    (denominator x)*^one = denominator x by Def7,Def8,ORDINAL2:19,52,56;
   hence x*'{} = {}/denominator x by Def11 .= {} by Th46;
  end;

theorem Th55:
 (i/j)*'(k/l) = (i*^k)/(j*^l)
  proof per cases;
   suppose
A1:  j <> {} & l <> {};
then A2:  i hcf j <> {} & k hcf l <> {} by Th20;
      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 A1,Th48;
   hence (i/j)*'(k/l) = (RED(i,j)*^RED(k,l))/(RED(j,i)*^RED(l,k)) by Def11
      .= (RED(i,j)*^RED(k,l)*^(i hcf j))/(RED(j,i)*^RED(l,k)*^(i hcf j))
         by A2,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 A2,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;
   suppose j = {} or l = {};
    then (i/j = {} or k/l = {}) & j*^l = {} by Def9,ORDINAL2:52;
    then (i/j)*'(k/l) = {} & (i*^k)/(j*^l) = {} by Def9,Th54;
   hence thesis;
  end;

theorem Th56:
 x+{} = x
  proof
      denominator {} = one & numerator {} = {}
 & (numerator x)*^one = numerator x &
    {}*^(denominator x) = {} & (denominator x)*^one = denominator x &
    (numerator x)+^{} = numerator x
     by Def7,Def8,ORDINAL2:19,44,52,56;
   hence
      x+{} = (numerator x) / denominator x by Def10 .= 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)+z by Def10
     .= (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
     .= (ny*^dz+^dy*^nz)/(dy*^dz)+x by Th45
     .= x+(y+z) by Def10;
  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;
      x*'y = (nx*^ny)/(dx*^dy) by Def11;
   hence (x*'y)*'z = (nx*^ny*^nz)/(dx*^dy*^dz) by A1,Th55
     .= (nx*^(ny*^nz))/(dx*^dy*^dz) by ORDINAL3:58
     .= (nx*^(ny*^nz))/(dx*^(dy*^dz)) by ORDINAL3:58
     .= x*'(((ny*^nz))/(dy*^dz)) by A1,Th55
     .= x*'(y*'z) by Def11;
  end;

theorem Th59:
 x*'one = x
  proof
   set y = one;
      (numerator x)*^one = numerator x & (denominator x)*^one = denominator x &
    numerator y = one & denominator y = one by Def7,Def8,Lm1,ORDINAL2:56;
   hence x*'y = (numerator x)/denominator x by Def11 .= x by Th45;
  end;

theorem Th60:
 x <> {} implies ex y st x*'y = one
  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 A2:  denominator y = nx & numerator y = dx by A1,Th49;
A3:  nx*^dx <> {} by A1,ORDINAL3:34;
   thus x*'y = (nx*^dx)/(dx*^nx) by A2,Def11 .= one by A3,Th47;
  end;

theorem Th61:
 x <> {} implies ex z st y = x*'z
  proof assume x <> {};
   then consider z such that
A1:  x*'z = one 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 = one 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;
A2:  dx <> {} & dy <> {} & dz <> {} by Th41;
then A3:  dx*^dz <> {} & dx*^dy <> {} by ORDINAL3:34;
   thus x*'(y+z) = x*'((ny*^dz+^dy*^nz)/(dy*^dz)) by Def10
     .= (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 A2,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
     .= ((nx*^ny)/(dx*^dy))+((nx*^nz)/(dx*^dz)) by A3,Th52
     .= ((nx*^ny)/(dx*^dy))+x*'z by Def11
     .= x*'y+x*'z by Def11;
  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 ORDINAL2:def 21;
    then denominator i = one & denominator j = one by Def8;
   hence i+j = (ni*^one+^one*^nj)/(one*^one) by Def10
      .= (ni*^one+^one*^nj)/one by ORDINAL2:56
      .= (ni+^one*^nj)/one by ORDINAL2:56
      .= (ni+^nj)/one by ORDINAL2:56
      .= ni+^nj by Th46
      .= i+^nj by A1,Def7
      .= i+^j by A1,Def7;
  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 ORDINAL2:def 21;
    then denominator i = one & denominator j = one by Def8;
   hence i*'j = (ni*^nj)/(one*^one) by Def11
      .= (ni*^nj)/one by ORDINAL2:56
      .= ni*^nj by Th46
      .= i*^nj by A1,Def7
      .= i*^j by A1,Def7;
  end;

theorem Th66:
 ex y st x = y+y
  proof set 02 = one+one;
      02 = one+^one by Th64;
    then 02 <> {} by ORDINAL3:29;
   then consider z such that
A1:  02*'z = one 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:
Def12:
  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;
 antonym y < x;
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+;
      not [{},y] in omega by Th38;
   then consider i,j being Element of omega such that
A2:  [{},y] = [i,j] & i,j are_relative_prime & j <> {} & j <> one by A1,Th35;
      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 A3:  r2*^t2 <> {} & s2*^t2 <> {} by ORDINAL3:34;
      s+t = (s1*^t2+^s2*^t1)/(s2*^t2) & r+t = (r1*^t2+^r2*^t1)/(r2*^t2)
     by Def10;
    then (s1*^t2+^s2*^t1)*^(r2*^t2) = (r1*^t2+^r2*^t1)*^(s2*^t2) by A1,A3,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 {} = one & numerator {} = {} by Def7,Def8,ORDINAL2:19;
   assume r+s = {};
    then (nr*^ds+^ns*^dr)/(dr*^ds) = {} by Def10 .= {}/one by A3,Th45;
    then (nr*^ds+^ns*^dr)*^one = (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+y by Th69;
    then x = {} by 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:  x+y = (nx*^dy+^ny*^dx)/(dx*^dy) by Def10;
A4:  dx = one & dy <> {} & denominator (x+y) = one by A1,Def8,Th41;
then A5:  dx*^dy <> {} by ORDINAL3:34;
      (nx*^dy+^ny*^dx)*^one = nx*^dy+^ny*^dx by ORDINAL2:56;
    then nx*^dy+^ny*^dx = dx*^dy*^numerator (x+y) by A2,A3,A4,A5,Th51
                  .= dy*^numerator (x+y) by A4,ORDINAL2:56;
    then nx*^dy+^ny = dy*^numerator (x+y) by A4,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 Def2;
    then dy hcf ny = dy & ny,dy are_relative_prime by Def4,Th40;
    then dy = one 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;
A2:  i in omega by Th37;
   consider y such that
A3:  x = i+y by A1,Def12;
   consider z such that
A4:  i+one = x+z by A1,Def12;
      i+one = i+^one by Th64;
    then i+one in omega by Th37;
   then reconsider y' = y, z' = z as Element of omega by A1,A2,A3,A4,Th78;
      i+one = i+(y+z) by A3,A4,Th57;
then one = y+z by Th69 .= y'+^z' by Th64;
    then y' c= one & z' c= one by ORDINAL3:27;
    then (y = {} or y = one) & (z = {} or z = one) by ORDINAL3:19;
    then i = x or i+one = x by A3,Th56;
   hence contradiction by A1;
  end;

theorem Th80:
 t <> {} implies ex r st r < t & not r in omega
  proof assume
A1:  t <> {};
    A2: one+^one = succ one by ORDINAL2:48;
then A3:  one+^one <> one by ORDINAL1:14;
   per cases;
   suppose
A4:   one <=' t;
    consider r such that
A5:   one = r+r by Th66;
    take r;
A6:   r <=' one by A5,Def12;
       r <> one by A3,A5,Th64;
     then r < one by A6,Th73;
    hence r < t by A4,Th74;
    assume r in omega;
then A7:   denominator r = one & denominator one = one by Def8,Lm1;
     then (numerator r)*^denominator r = numerator r & one*^one = one
      by ORDINAL2:56;
then A8:   one = ((numerator r)+^numerator r)/one by A5,A7,Def10
        .= (numerator r)+^numerator r by Th46;
     then numerator r c= one by ORDINAL3:27;
     then numerator r = {} or numerator r = one by ORDINAL3:19;
    hence contradiction by A2,A8,ORDINAL1:14,ORDINAL2:44;
   suppose
A9:   t < one;
    consider r such that
A10:   t = r+r by Th66;
    take r;
A11:   r <=' t by A10,Def12;
       now assume r = t;
       then t+{} = t+t by A10,Th56;
      hence contradiction by A1,Th69;
     end;
    hence r < t by A11,Th73;
A12:   r < one by A9,A11,Th74;
       r <> {} & {} <=' r by A1,A10,Th56,Th71;
     then {} < r & one = {}+one by Th56,Th73;
    hence thesis by A12,Th79;
  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;
       now assume {s: s < t} in omega;
       then {s: s < t} is Ordinal by ORDINAL1:23;
      hence r is Ordinal by A3,ORDINAL1:23;
     end;
    then consider i,j being Element of omega such that
A4:   {s: s < t} = [i,j] & i,j are_relative_prime & j <> {} & j <> one
      by A1,A2,Th35,Th37;
       {} <=' t by Th71;
     then {} < t by A1,Th73;
     then {} in {s: s < t};
     then {} in {{i},{i,j}} by A4,TARSKI:def 5;
    hence contradiction by 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} = {} by XBOOLE_1:3;
   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,Def12,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 Th86:
 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 {} = one & numerator {} = {} by Def7,Def8,ORDINAL2:19;
   assume r*'s = {};
    then (nr*^ns)/(dr*^ds) = {} by Def11 .= {}/one by A2,Th45;
    then (nr*^ns)*^one = (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;
   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;

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 r1*'r2 <> {} by A2,Th86;
    then s1 <> {} & s2 <> {} by A1,Th54;
    then s1*'s2 <=' r1*'s2 & s1*'s2 <> r1*'s2 by 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;
   suppose r <=' s;
     then r = r+{} & r <=' s & {} <=' t by Th56,Th71;
    hence thesis;
  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;
   suppose
A3:   s <=' r;
       s = s+{} & {} <=' t by Th56,Th71;
    hence thesis by A1,A3;
  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 <> one;
        A = {{i},{i,j}} by A2,TARSKI:def 5;
      then A3: {i} in A by TARSKI:def 2;
        now assume {i} in omega;
        then {i} is Ordinal by ORDINAL1:23;
        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 <> one by A3,
Th35;
        {i} = {{i1},{i1,j1}} by A4,TARSKI:def 5;
      then {i1} in {i} & {i1,j1} in {i} by 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*^one by ORDINAL2:56,TARSKI:def 1;
     hence contradiction by A4,Def1;
    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,ORDINAL2:def 5;
     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+ by ORDINAL1:23;
      C-^r in omega by ORDINAL2:def 21;
   then reconsider x = C-^r as ordinal Element of RAT+ by Th34;
      r c= C by A6,A7,ORDINAL1:34;
    then C = r+^x by ORDINAL3:def 6 .= r+x by Th64;
   hence thesis by Def12;
  end;

theorem
   ex t st r + t = s or s + t = r
  proof r <=' s or s <=' r;
   hence thesis by Def12;
  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 Def12;
   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,Def12;
   hence r < t by Th73;
      t <=' s & s <> t by A4,A5,Def12,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 Def12,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 ORDINAL2:def 21;
   then reconsider s = (denominator t)*^(numerator r)
    as ordinal Element of RAT+ by Th34;
   take s; thus s in omega by ORDINAL2:def 21;
   set y=((numerator r)*^(((numerator t)*^denominator r)-^one))/denominator r;
   take y;
A2:  denominator r <> {} & denominator t <> {} by Th41;
    then (numerator t)*^denominator r <> {} by A1,ORDINAL3:34;
    then {} in (numerator t)*^denominator r by ORDINAL3:10;
    then one c= (numerator t)*^denominator r by ORDINAL1:33,ORDINAL2:def 4;
    then (numerator t)*^denominator r = one+^(((numerator t)*^denominator r)-^
one)
      by ORDINAL3:def 6;
    then s*^((numerator t)*^denominator r) = (denominator t)*^
        ((numerator r)*^(one+^(((numerator t)*^denominator r)-^one)))
      by ORDINAL3:58
      .= (denominator t)*^((numerator r)*^one+^
         (numerator r)*^(((numerator t)*^denominator r)-^one))
      by ORDINAL3:54;
    then s*^(numerator t)*^denominator r
      = (denominator t)*^((numerator r)*^one+^
         (numerator r)*^(((numerator t)*^denominator r)-^one))
      by ORDINAL3:58;
    then (s*^(numerator t))/denominator t
      = ((numerator r)*^one+^
         (numerator r)*^(((numerator t)*^denominator r)-^one))/denominator r
      by A2,Th51
      .= (((numerator r)*^one)/denominator r)+y by A2,Th53
      .= ((numerator r)/denominator r)+y by ORDINAL2:56
      .= r+y by Th45;
    then r+y = (s*^(numerator t))/(one*^denominator t) by ORDINAL2:56
       .= (s/one)*'((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() = one and
A2: n0() = {} and
A3: n2() in omega and
A4: P[n0()] and
A5: not P[n2()]
  proof
      defpred _P[Ordinal] means not P[$1] & $1 in omega;
      n2() is Ordinal by A3,ORDINAL1:23;
then A6:  ex A st _P[A] by A3,A5;
   consider A such that
A7:  _P[A] and
A8:  for B st _P[B] holds A c= B from Ordinal_Min(A6);
A9:  {} in A by A2,A4,A7,ORDINAL3:10;
      now assume A is_limit_ordinal;
      then omega c= A by A9,ORDINAL2:def 5;
      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 Th34;
   take s; thus s in omega & P[s] by A8,A11;
      A = B+^one by A10,ORDINAL2:48;
   hence thesis by A1,A7,Th64;
  end;


Back to top