arytm_3.miz

    begin

    reserve A,B,C for Ordinal;



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



     Lm2: 1 in omega ;

    definition

      :: ARYTM_3:def1

      func one -> set equals 1;

      correctness ;

    end

    begin

    definition

      let a,b be Ordinal;

      :: ARYTM_3:def2

      pred a,b are_coprime means for c,d1,d2 be Ordinal st a = (c *^ d1) & b = (c *^ d2) holds c = 1;

      symmetry ;

    end

    theorem :: ARYTM_3:1

     not ( {} , {} ) are_coprime

    proof

      take {} , {} , {} ;

      thus thesis by ORDINAL2: 35;

    end;

    theorem :: ARYTM_3:2



     Th2: (1,A) are_coprime by ORDINAL3: 37;

    theorem :: ARYTM_3:3



     Th3: ( {} ,A) are_coprime implies A = 1

    proof



       A1: {} = (A *^ {} ) & A = (A *^ 1) by ORDINAL2: 38, ORDINAL2: 39;

      assume ( {} ,A) are_coprime & A <> 1;

      hence contradiction by A1;

    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 be natural Ordinal st (d1,d2) are_coprime & $1 = (c *^ d1) & B = (c *^ d2);

    theorem :: ARYTM_3:4

    a <> {} or b <> {} implies ex c,d1,d2 be natural Ordinal st (d1,d2) are_coprime & a = (c *^ d1) & b = (c *^ d2)

    proof

      assume that

       A1: a <> {} or b <> {} and

       A2: not ex c,d1,d2 be natural Ordinal st (d1,d2) are_coprime & 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 12;

          thus thesis 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 12;

          thus thesis 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 and

       A9: A in omega and

       A10: A <> {} and

       A11: not ex c,d1,d2 be natural Ordinal st (d1,d2) are_coprime & A = (c *^ d1) & B = (c *^ d2) by A6;

      reconsider A, B as Element of omega by A8, A9, ORDINAL1: 12;

      A = (1 *^ A) & B = (1 *^ B) by ORDINAL2: 39;

      then not (A,B) are_coprime by A11;

      then

      consider c,d1,d2 be Ordinal such that

       A12: A = (c *^ d1) and

       A13: B = (c *^ d2) and

       A14: c <> 1;



       A15: c <> {} by A10, A12, ORDINAL2: 35;

      then

       A16: d1 c= A & d2 c= B by A12, A13, ORDINAL3: 36;



       A17: d1 <> {} by A10, A12, ORDINAL2: 38;

      then c c= A by A12, ORDINAL3: 36;

      then

      reconsider c, d1, d2 as Element of omega by A16, ORDINAL1: 12;

      1 in c or c in 1 by A14, ORDINAL1: 14;

      then (1 *^ d1) in A by A12, A17, A15, ORDINAL3: 14, ORDINAL3: 19;

      then

       A18: d1 in A by ORDINAL2: 39;

       A19:

      now

        let c9,d19,d29 be natural Ordinal;

        assume that

         A20: (d19,d29) are_coprime and

         A21: d1 = (c9 *^ d19) & d2 = (c9 *^ d29);

        A = ((c *^ c9) *^ d19) & B = ((c *^ c9) *^ d29) by A12, A13, A21, ORDINAL3: 50;

        hence contradiction by A11, A20;

      end;

      A = (d1 *^ c) & B = (d2 *^ c) by A12, A13;

      then d2 c= d1 by A8, A15, ORDINAL3: 35;

      hence contradiction by A7, A17, A19, A18, ORDINAL1: 5;

    end;

    reserve l,m,n for natural Ordinal;

    registration

      let m, n;

      cluster (m div^ n) -> natural;

      coherence

      proof



         A1: n = {} implies (m div^ n) = {} & ( {} *^ 1) = {} by ORDINAL2: 35, ORDINAL3:def 6;

        n in 1 or 1 c= n by ORDINAL1: 16;

        then ((m div^ n) *^ 1) c= ((m div^ n) *^ n) by A1, ORDINAL3: 14, ORDINAL3: 20;

        then

         A2: (m div^ n) c= ((m div^ n) *^ n) by ORDINAL2: 39;

        ((m div^ n) *^ n) c= m & m in omega by ORDINAL1:def 12, ORDINAL3: 64;

        hence (m div^ n) in omega by A2, ORDINAL1: 12, XBOOLE_1: 1;

      end;

      cluster (m mod^ n) -> natural;

      coherence

      proof

        (((m div^ n) *^ n) +^ (m mod^ n)) = m by ORDINAL3: 65;

        then

         A3: (m mod^ n) c= m by ORDINAL3: 24;

        m in omega by ORDINAL1:def 12;

        hence (m mod^ n) in omega by A3, ORDINAL1: 12;

      end;

    end

    definition

      let k,n be Ordinal;

      :: ARYTM_3:def3

      pred k divides n means ex a be Ordinal st n = (k *^ a);

      reflexivity

      proof

        let n be Ordinal;

        take 1;

        thus thesis by ORDINAL2: 39;

      end;

    end

    theorem :: ARYTM_3:5



     Th5: 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 be Ordinal such that

         A1: b = (a *^ c);

        per cases ;

          suppose b = {} ;

          then b = (a *^ {} ) by ORDINAL2: 38;

          hence thesis;

        end;

          suppose b <> {} ;

          then c is Element of omega by A1, ORDINAL3: 75;

          hence thesis by A1;

        end;

      end;

      thus thesis;

    end;

    theorem :: ARYTM_3:6



     Th6: for m, n st {} in m holds (n mod^ m) in m

    proof

      let m, n;

      assume {} in m;

      then

       A1: ex C st n = (((n div^ m) *^ m) +^ C) & C in m by ORDINAL3:def 6;

      (n mod^ m) = (n -^ ((n div^ m) *^ m)) by ORDINAL3:def 7;

      hence thesis by A1, ORDINAL3: 52;

    end;

    theorem :: ARYTM_3:7



     Th7: 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 Th5;

      ( {} *^ a) = {} by ORDINAL2: 35;

      then {} <> m by A1, A2, ORDINAL2: 35;

      then

       A3: {} in m by ORDINAL3: 8;

      n = ((a *^ m) +^ {} ) by A2, ORDINAL2: 27;

      hence thesis by A1, A2, A3, ORDINAL3:def 6;

    end;

    theorem :: ARYTM_3:8



     Th8: for n, m st n divides m & m divides n holds n = m

    proof

      let n, m;

      assume that

       A1: n divides m and

       A2: m divides n;



       A3: m = (n *^ (m div^ n)) by A1, Th7;



       A4: ((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: 37;

        hence thesis by A3, ORDINAL2: 39;

      end;

      n = (m *^ (n div^ m)) by A2, Th7;

      then

       A5: (n *^ 1) = n & n = (n *^ ((m div^ n) *^ (n div^ m))) by A3, ORDINAL2: 39, ORDINAL3: 50;

      n = {} implies n = m by A3, ORDINAL2: 35;

      hence thesis by A5, A4, ORDINAL3: 33;

    end;

    theorem :: ARYTM_3:9



     Th9: n divides {} & 1 divides n

    proof

       {} = (n *^ {} ) by ORDINAL2: 35;

      hence n divides {} ;

      n = (1 *^ n) by ORDINAL2: 39;

      hence thesis;

    end;

    theorem :: ARYTM_3:10



     Th10: for n, m st {} in m & n divides m holds n c= m

    proof

      let n, m such that

       A1: {} in m;

      given a be Ordinal such that

       A2: m = (n *^ a);

      a <> {} by A1, A2, ORDINAL2: 38;

      hence thesis by A2, ORDINAL3: 36;

    end;

    theorem :: ARYTM_3:11



     Th11: 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 Th5;

      assume n divides (m +^ l);

      then

      consider b such that

       A2: (m +^ l) = (n *^ b) by Th5;

      assume

       A3: not n divides l;

      l = ((n *^ b) -^ (n *^ a)) by A1, A2, ORDINAL3: 52

      .= ((b -^ a) *^ n) by ORDINAL3: 63;

      hence thesis by A3;

    end;



     Lm3: 1 = ( succ 0 );

    definition

      let k,n be natural Ordinal;

      :: ARYTM_3:def4

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

          take w;

          thus k divides w & n divides w by Th9;

          let m;

          assume k divides m & n divides m;

          hence thesis by A1;

        end;

          suppose

           A2: k <> {} & n <> {} ;

           {} c= k;

          then {} c< k by A2, XBOOLE_0:def 8;

          then

           A3: {} in k by ORDINAL1: 11;

           {} c= n;

          then {} c< n by A2, XBOOLE_0:def 8;

          then {} in n by ORDINAL1: 11;

          then

           A4: 1 c= n by Lm3, ORDINAL1: 21;

          defpred P[ Ordinal] means ex m st $1 = m & k divides m & n divides m & k c= m;



           A5: (k *^ 1) = k by ORDINAL2: 39;

          k divides (k *^ n) & n divides (k *^ n);

          then

           A6: ex A st P[A] by A4, A5, ORDINAL2: 41;

          consider A such that

           A7: P[A] and

           A8: for B st P[B] holds A c= B from ORDINAL1:sch 1( A6);

          consider l such that

           A9: A = l and

           A10: k divides l and

           A11: n divides l and

           A12: k c= l by A7;

          reconsider l as Element of omega by ORDINAL1:def 12;

          take l;

          thus k divides l & n divides l by A10, A11;

          let m such that

           A13: k divides m and

           A14: n divides m;



           A15: m = ((l *^ (m div^ l)) +^ (m mod^ l)) by ORDINAL3: 65;

          l = (k *^ (l div^ k)) by A10, Th7;

          then (l *^ (m div^ l)) = (k *^ ((l div^ k) *^ (m div^ l))) by ORDINAL3: 50;

          then k divides (l *^ (m div^ l));

          then

           A16: k divides (m mod^ l) by A13, A15, Th11;

          l = (n *^ (l div^ n)) by A11, Th7;

          then (l *^ (m div^ l)) = (n *^ ((l div^ n) *^ (m div^ l))) by ORDINAL3: 50;

          then n divides (l *^ (m div^ l));

          then

           A17: n divides (m mod^ l) by A14, A15, Th11;

          now



             A18: {} c= (m mod^ l);

            assume (m mod^ l) <> {} ;

            then {} c< (m mod^ l) by A18, XBOOLE_0:def 8;

            then k c= (m mod^ l) by A16, Th10, ORDINAL1: 11;

            then l c= (m mod^ l) by A8, A9, A16, A17;

            hence contradiction by A12, A3, Th6, ORDINAL1: 5;

          end;

          then m = (l *^ (m div^ l)) by A15, ORDINAL2: 27;

          hence thesis;

        end;

      end;

      uniqueness

      proof

        let m1,m2 be Element of omega ;

        assume k divides m1 & n divides m1 & (for m st k divides m & n divides m holds m1 divides m) & k divides m2 & (n divides m2 & for m st k divides m & n divides m holds m2 divides m);

        then m1 divides m2 & m2 divides m1;

        hence thesis by Th8;

      end;

      commutativity ;

    end

    theorem :: ARYTM_3:12



     Th12: (m lcm n) divides (m *^ n)

    proof

      m divides (m *^ n) & n divides (m *^ n);

      hence thesis by Def4;

    end;

    theorem :: ARYTM_3:13



     Th13: n <> {} implies ((m *^ n) div^ (m lcm n)) divides m

    proof

      assume

       A1: n <> {} ;

      take ((m lcm n) div^ n);

      n divides (m lcm n) by Def4;

      then

       A2: (m lcm n) = (n *^ ((m lcm n) div^ n)) by Th7;

      (m lcm n) divides (m *^ n) by Th12;

      then (m *^ n) = ((m lcm n) *^ ((m *^ n) div^ (m lcm n))) by Th7;

      then (n *^ m) = (n *^ (((m lcm n) div^ n) *^ ((m *^ n) div^ (m lcm n)))) by A2, ORDINAL3: 50;

      hence m = (((m *^ n) div^ (m lcm n)) *^ ((m lcm n) div^ n)) by A1, ORDINAL3: 33;

    end;

    definition

      let k,n be natural Ordinal;

      :: ARYTM_3:def5

      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 m1 = (k \/ n) as Element of omega by ORDINAL1:def 12;

          take m1;

          thus m1 divides k & m1 divides n by A1, Th9;

          thus thesis by A1;

        end;

          suppose

           A2: k <> {} & n <> {} ;

          reconsider l = ((k *^ n) div^ (k lcm n)) as Element of omega by ORDINAL1:def 12;

          take l;

          thus l divides k & l divides n by A2, Th13;

          let m;

          assume that

           A3: m divides k and

           A4: m divides n;



           A5: n = (m *^ (n div^ m)) by A4, Th7;

          then

           A6: (n div^ m) <> {} by A2, ORDINAL2: 35;

          ((m *^ (k div^ m)) *^ (n div^ m)) = (n *^ (k div^ m)) by A5, ORDINAL3: 50;

          then

           A7: n divides ((m *^ (k div^ m)) *^ (n div^ m));

          set mm = (m *^ ((k div^ m) *^ (n div^ m)));



           A8: mm = ((m *^ (k div^ m)) *^ (n div^ m)) by ORDINAL3: 50;



           A9: k = (m *^ (k div^ m)) by A3, Th7;

          then (k div^ m) <> {} by A2, ORDINAL2: 35;

          then

           A10: ((k div^ m) *^ (n div^ m)) <> {} by A6, ORDINAL3: 31;

          k divides ((m *^ (k div^ m)) *^ (n div^ m)) by A9;

          then (k lcm n) divides ((m *^ (k div^ m)) *^ (n div^ m)) by A7, Def4;

          then

           A11: mm = ((k lcm n) *^ (mm div^ (k lcm n))) by A8, Th7;

          m <> {} by A2, A9, ORDINAL2: 35;

          then (k lcm n) <> {} by A11, A10, ORDINAL2: 35, ORDINAL3: 31;

          then

           A12: (k *^ n) = ((k *^ n) +^ {} ) & {} in (k lcm n) by ORDINAL2: 27, ORDINAL3: 8;

          (mm *^ m) = ((k lcm n) *^ (m *^ (mm div^ (k lcm n)))) by A11, ORDINAL3: 50;

          then (k *^ n) = ((k lcm n) *^ (m *^ (mm div^ (k lcm n)))) by A9, A5, A8, ORDINAL3: 50;

          then l = (m *^ (mm div^ (k lcm n))) by A12, ORDINAL3: 66;

          hence thesis;

        end;

      end;

      uniqueness

      proof

        let m1,m2 be Element of omega ;

        assume m1 divides k & m1 divides n & (for m st m divides k & m divides n holds m divides m1) & m2 divides k & (m2 divides n & for m st m divides k & m divides n holds m divides m2);

        then m1 divides m2 & m2 divides m1;

        hence thesis by Th8;

      end;

      commutativity ;

    end

    theorem :: ARYTM_3:14



     Th14: (a hcf {} ) = a & (a lcm {} ) = {}

    proof

      reconsider e = a, c = {} as Element of omega by ORDINAL1:def 12;



       A1: for b st a divides b & {} divides b holds c divides b;

      (for n st n divides a & n divides {} holds n divides e) & a divides c by Th9;

      hence thesis by A1, Def4, Def5;

    end;

    theorem :: ARYTM_3:15



     Th15: (a hcf b) = {} implies a = {}

    proof

      (a hcf b) divides a by Def5;

      then a = ((a hcf b) *^ (a div^ (a hcf b))) by Th7;

      hence thesis by ORDINAL2: 35;

    end;

    theorem :: ARYTM_3:16



     Th16: (a hcf a) = a & (a lcm a) = a

    proof

      reconsider c = a as Element of omega by ORDINAL1:def 12;

      for b st b divides a & b divides a holds b divides c;

      hence (a hcf a) = a by Def5;

      for b st a divides b & a divides b holds c divides b;

      hence thesis by Def4;

    end;

    theorem :: ARYTM_3:17



     Th17: ((a *^ c) hcf (b *^ c)) = ((a hcf b) *^ c)

    proof

      per cases ;

        suppose

         A1: c = {} ;

        then

         A2: ((a hcf b) *^ c) = {} by ORDINAL2: 35;

        (a *^ c) = {} & (b *^ c) = {} by A1, ORDINAL2: 35;

        hence thesis by A2, Th16;

      end;

        suppose

         A3: c <> {} & a <> {} ;

        reconsider d = ((a hcf b) *^ c) as Element of omega by ORDINAL1:def 12;

        set e = (((a *^ c) hcf (b *^ c)) div^ d);

        (a hcf b) divides b by Def5;

        then b = ((a hcf b) *^ (b div^ (a hcf b))) by Th7;

        then (b *^ c) = (d *^ (b div^ (a hcf b))) by ORDINAL3: 50;

        then

         A4: d divides (b *^ c);

        (a hcf b) divides a by Def5;

        then a = ((a hcf b) *^ (a div^ (a hcf b))) by Th7;

        then (a *^ c) = (d *^ (a div^ (a hcf b))) by ORDINAL3: 50;

        then d divides (a *^ c);

        then d divides ((a *^ c) hcf (b *^ c)) by A4, Def5;



        then

         A5: ((a *^ c) hcf (b *^ c)) = (d *^ e) by Th7

        .= (((a hcf b) *^ e) *^ c) by ORDINAL3: 50;

        then (((a hcf b) *^ e) *^ c) divides (b *^ c) by Def5;

        then ((((a hcf b) *^ e) *^ c) *^ ((b *^ c) div^ (((a hcf b) *^ e) *^ c))) = (b *^ c) by Th7;

        then ((((a hcf b) *^ e) *^ ((b *^ c) div^ (((a hcf b) *^ e) *^ c))) *^ c) = (b *^ c) by ORDINAL3: 50;

        then (((a hcf b) *^ e) *^ ((b *^ c) div^ (((a hcf b) *^ e) *^ c))) = b by A3, ORDINAL3: 33;

        then

         A6: ((a hcf b) *^ e) divides b;

        (((a hcf b) *^ e) *^ c) divides (a *^ c) by A5, Def5;

        then ((((a hcf b) *^ e) *^ c) *^ ((a *^ c) div^ (((a hcf b) *^ e) *^ c))) = (a *^ c) by Th7;

        then ((((a hcf b) *^ e) *^ ((a *^ c) div^ (((a hcf b) *^ e) *^ c))) *^ c) = (a *^ c) by ORDINAL3: 50;

        then (((a hcf b) *^ e) *^ ((a *^ c) div^ (((a hcf b) *^ e) *^ c))) = a by A3, ORDINAL3: 33;

        then ((a hcf b) *^ e) divides a;

        then ((a hcf b) *^ e) divides (a hcf b) by A6, Def5;

        then (((a hcf b) *^ e) *^ ((a hcf b) div^ ((a hcf b) *^ e))) = (a hcf b) by Th7;



        then ((a hcf b) *^ (e *^ ((a hcf b) div^ ((a hcf b) *^ e)))) = (a hcf b) by ORDINAL3: 50

        .= ((a hcf b) *^ 1) by ORDINAL2: 39;

        then (a hcf b) = {} or (e *^ ((a hcf b) div^ ((a hcf b) *^ e))) = 1 by ORDINAL3: 33;

        then e = 1 by A3, Th15, ORDINAL3: 37;

        hence thesis by A5, ORDINAL2: 39;

      end;

        suppose a = {} ;

        then (a hcf b) = b & (a *^ c) = {} by Th14, ORDINAL2: 35;

        hence thesis by Th14;

      end;

    end;

    theorem :: ARYTM_3:18



     Th18: 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 Th7;

      hence thesis by ORDINAL2: 35;

    end;

    theorem :: ARYTM_3:19



     Th19: a <> {} or b <> {} implies ((a div^ (a hcf b)),(b div^ (a hcf b))) are_coprime

    proof

      assume

       A1: a <> {} or b <> {} ;

      set ab = (a hcf b);



       A2: (1 *^ a) = a & (1 *^ b) = b by ORDINAL2: 39;

      per cases ;

        suppose a = {} or b = {} ;

        then ab = b & (b div^ b) = 1 or ab = a & (a div^ a) = 1 by A1, A2, Th14, ORDINAL3: 68;

        hence thesis by Th2;

      end;

        suppose

         A3: a <> {} & b <> {} ;

        ab divides b by Def5;

        then

         A4: b = (ab *^ (b div^ ab)) by Th7;

        then

         A5: (b div^ ab) <> {} by A3, ORDINAL2: 35;

        let c,d1,d2 be Ordinal such that

         A6: (a div^ (a hcf b)) = (c *^ d1) and

         A7: (b div^ (a hcf b)) = (c *^ d2);

        ab divides a by Def5;

        then

         A8: a = (ab *^ (a div^ ab)) by Th7;

        then (a div^ ab) <> {} by A3, ORDINAL2: 35;

        then

        reconsider c, d1, d2 as Element of omega by A6, A7, A5, ORDINAL3: 75;

        b = ((ab *^ c) *^ d2) by A4, A7, ORDINAL3: 50;

        then

         A9: (ab *^ c) divides b;

        a = ((ab *^ c) *^ d1) by A8, A6, ORDINAL3: 50;

        then (ab *^ c) divides a;

        then (ab *^ c) divides ab by A9, Def5;

        then ab = ((ab *^ c) *^ (ab div^ (ab *^ c))) by Th7;

        then ab = (ab *^ (c *^ (ab div^ (ab *^ c)))) by ORDINAL3: 50;

        then

         A10: (ab *^ 1) = (ab *^ (c *^ (ab div^ (ab *^ c)))) by ORDINAL2: 39;

        ab <> {} by A3, A8, ORDINAL2: 35;

        then 1 = (c *^ (ab div^ (ab *^ c))) by A10, ORDINAL3: 33;

        hence thesis by ORDINAL3: 37;

      end;

    end;



     Lm4: 0 = {} ;

    theorem :: ARYTM_3:20



     Th20: (a,b) are_coprime iff (a hcf b) = 1

    proof

      (a hcf b) divides b by Def5;

      then

       A1: b = ((a hcf b) *^ (b div^ (a hcf b))) by Th7;

      (a hcf b) divides a by Def5;

      then a = ((a hcf b) *^ (a div^ (a hcf b))) by Th7;

      hence (a,b) are_coprime implies (a hcf b) = 1 by A1;

      assume

       A2: (a hcf b) = 1;

      let c,d1,d2 be Ordinal such that

       A3: a = (c *^ d1) & b = (c *^ d2);

      a <> {} or b <> {} by A2, Th14, Lm4;

      then

      reconsider c as Element of omega by A3, ORDINAL3: 75;

      c divides a & c divides b by A3;

      then c divides 1 by A2, Def5;

      then ex d st 1 = (c *^ d) by Th5;

      hence thesis by ORDINAL3: 37;

    end;

    definition

      let a,b be natural Ordinal;

      :: ARYTM_3:def6

      func RED (a,b) -> Element of omega equals (a div^ (a hcf b));

      coherence by ORDINAL1:def 12;

    end

    theorem :: ARYTM_3:21



     Th21: (( RED (a,b)) *^ (a hcf b)) = a

    proof

      (a hcf b) divides a by Def5;

      hence thesis by Th7;

    end;

    theorem :: ARYTM_3:22

    a <> {} or b <> {} implies (( RED (a,b)),( RED (b,a))) are_coprime by Th19;

    theorem :: ARYTM_3:23



     Th23: (a,b) are_coprime implies ( RED (a,b)) = a

    proof

      assume (a,b) are_coprime ;

      then (a hcf b) = 1 by Th20;

      hence thesis by ORDINAL3: 71;

    end;

    theorem :: ARYTM_3:24



     Th24: ( RED (a,1)) = a & ( RED (1,a)) = 1

    proof

      (a,1) are_coprime by Th2;

      then (a hcf 1) = 1 by Th20;

      hence thesis by ORDINAL3: 71;

    end;

    theorem :: ARYTM_3:25

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

    theorem :: ARYTM_3:26



     Th26: ( RED ( {} ,a)) = {} & (a <> {} implies ( RED (a, {} )) = 1)

    proof

      thus ( RED ( {} ,a)) = {} by ORDINAL3: 70;

      assume

       A1: a <> {} ;



      thus ( RED (a, {} )) = (a div^ a) by Th14

      .= ((a *^ 1) div^ a) by ORDINAL2: 39

      .= 1 by A1, ORDINAL3: 68;

    end;

    theorem :: ARYTM_3:27



     Th27: a <> {} implies ( RED (a,a)) = 1

    proof

      assume

       A1: a <> {} ;



      thus ( RED (a,a)) = (a div^ a) by Th16

      .= ((a *^ 1) div^ a) by ORDINAL2: 39

      .= 1 by A1, ORDINAL3: 68;

    end;

    theorem :: ARYTM_3:28



     Th28: c <> {} implies ( RED ((a *^ c),(b *^ c))) = ( RED (a,b))

    proof

      assume

       A1: c <> {} ;

      a <> {} implies (a hcf b) <> {} by Th18;

      then

       A2: a <> {} implies ((a hcf b) *^ c) <> {} by A1, ORDINAL3: 31;



       A3: ( RED ( {} ,b)) = {} & ( {} *^ ((a hcf b) *^ c)) = {} by ORDINAL2: 35, ORDINAL3: 70;



       A4: (a hcf b) divides a by Def5;



      thus ( RED ((a *^ c),(b *^ c))) = ((a *^ c) div^ ((a hcf b) *^ c)) by Th17

      .= ((((a div^ (a hcf b)) *^ (a hcf b)) *^ c) div^ ((a hcf b) *^ c)) by A4, Th7

      .= ((( RED (a,b)) *^ ((a hcf b) *^ c)) div^ ((a hcf b) *^ c)) by ORDINAL3: 50

      .= ( RED (a,b)) by A2, A3, ORDINAL3: 68, ORDINAL3: 70;

    end;

    set RATplus = { [a, b] where a,b be Element of omega : (a,b) are_coprime & b <> {} };



     Lm5: [a, b] in RATplus implies (a,b) are_coprime & b <> {}

    proof

      assume [a, b] in RATplus;

      then

      consider c,d be Element of omega such that

       A1: [a, b] = [c, d] and

       A2: (c,d) are_coprime & d <> {} ;

      a = c by A1, XTUPLE_0: 1;

      hence thesis by A1, A2, XTUPLE_0: 1;

    end;

    begin

    reserve i,j,k for Element of omega ;

    definition

      :: ARYTM_3:def7

      func RAT+ -> set equals (({ [i, j] : (i,j) are_coprime & j <> {} } \ the set of all [k, 1]) \/ omega );

      correctness ;

    end



     Lm6: 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 for Element of RAT+ ;

      existence by Lm2, Lm6, Lm4;

    end

    theorem :: ARYTM_3:29



     Th29: x in omega or ex i, j st x = [i, j] & (i,j) are_coprime & j <> {} & j <> 1

    proof

      assume not x in omega ;

      then

       A1: x in (RATplus \ the set of all [k, 1]) by XBOOLE_0:def 3;

      then

       A2: not x in the set of all [k, 1] by XBOOLE_0:def 5;

      x in RATplus by A1;

      then

      consider a,b be Element of omega such that

       A3: x = [a, b] & (a,b) are_coprime & b <> {} ;

       [a, 1] in the set of all [k, 1];

      hence thesis by A2, A3;

    end;

    theorem :: ARYTM_3:30



     Th30: not ex i,j be set st [i, j] is Ordinal

    proof

      given i,j be set such that

       A1: [i, j] is Ordinal;

       {} in { {i}, {i, j}} by A1, ORDINAL3: 8;

      hence thesis by TARSKI:def 2;

    end;

    theorem :: ARYTM_3:31



     Th31: 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_coprime & j <> {} & j <> 1 by Th29;

      hence thesis by Th30;

    end;

    registration

      cluster -> natural for ordinal Element of RAT+ ;

      coherence

      proof

        let x be ordinal Element of RAT+ ;

        assume not x in omega ;

        then

         A1: ex i, j st x = [i, j] & (i,j) are_coprime & j <> {} & j <> 1 by Th29;

        then {} in x by ORDINAL3: 8;

        hence thesis by A1, TARSKI:def 2;

      end;

    end

    theorem :: ARYTM_3:32



     Th32: not ex i,j be object st [i, j] in omega

    proof

      given i,j be object such that

       A1: [i, j] in omega ;

      reconsider a = [i, j] as Element of omega by A1;

       {} in a by ORDINAL3: 8;

      hence thesis by TARSKI:def 2;

    end;

    theorem :: ARYTM_3:33



     Th33: [i, j] in RAT+ iff (i,j) are_coprime & j <> {} & j <> 1

    proof



       A1: not [i, j] in omega by Th32;

      hereby

        assume [i, j] in RAT+ ;

        then

         A2: [i, j] in (RATplus \ the set of all [k, 1]) by A1, XBOOLE_0:def 3;

        hence (i,j) are_coprime & j <> {} by Lm5;

         not [i, j] in the set of all [k, 1] by A2, XBOOLE_0:def 5;

        hence j <> 1;

      end;

      assume (i,j) are_coprime & j <> {} ;

      then

       A3: [i, j] in RATplus;

      assume j <> 1;

      then not ex k st [i, j] = [k, 1] by XTUPLE_0: 1;

      then not [i, j] in the set of all [k, 1];

      then [i, j] in (RATplus \ the set of all [k, 1]) by A3, XBOOLE_0:def 5;

      hence thesis by XBOOLE_0:def 3;

    end;

    definition

      let x be Element of RAT+ ;

      :: ARYTM_3:def8

      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 be Element of omega st a = x;

        assume not x in omega ;

        then x in (RATplus \ the set of all [k, 1]) by XBOOLE_0:def 3;

        then x in RATplus;

        then

        consider a,b be Element of omega such that

         A1: x = [a, b] and (a,b) are_coprime and b <> {} ;

        take a, b;

        thus thesis by A1;

      end;

      correctness by XTUPLE_0: 1;

      :: ARYTM_3:def9

      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 be Element of omega st a = 1;

        assume not x in omega ;

        then x in (RATplus \ the set of all [k, 1]) by XBOOLE_0:def 3;

        then x in RATplus;

        then

        consider a,b be Element of omega such that

         A2: x = [a, b] and (a,b) are_coprime and b <> {} ;

        take b, a;

        thus thesis by A2;

      end;

      correctness by XTUPLE_0: 1;

    end

    theorem :: ARYTM_3:34



     Th34: (( numerator x),( denominator x)) are_coprime

    proof

      per cases ;

        suppose x in omega ;

        then ( denominator x) = 1 by Def9;

        hence thesis by Th2;

      end;

        suppose

         A1: not x in omega ;

        then

        consider i, j such that

         A2: x = [i, j] and

         A3: (i,j) are_coprime and j <> {} and j <> 1 by Th29;

        i = ( numerator x) by A1, A2, Def8;

        hence thesis by A1, A2, A3, Def9;

      end;

    end;

    theorem :: ARYTM_3:35



     Th35: ( denominator x) <> {}

    proof

      per cases ;

        suppose x in omega ;

        hence thesis by Def9, Lm4;

      end;

        suppose

         A1: not x in omega ;

        then ex i, j st x = [i, j] & (i,j) are_coprime & j <> {} & j <> 1 by Th29;

        hence thesis by A1, Def9;

      end;

    end;

    theorem :: ARYTM_3:36



     Th36: 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] and (i,j) are_coprime and j <> {} and

       A3: j <> 1 by Th29;

      i = ( numerator x) by A1, A2, Def8;

      hence thesis by A1, A2, A3, Def9;

    end;

    theorem :: ARYTM_3:37



     Th37: x <> {} iff ( numerator x) <> {}

    proof

      hereby

        assume that

         A1: x <> {} and

         A2: ( numerator x) = {} ;



         A3: not x in omega by A1, A2, Def8;

        then

        consider i, j such that

         A4: x = [i, j] and

         A5: (i,j) are_coprime and j <> {} and

         A6: j <> 1 by Th29;

        i = {} by A2, A3, A4, Def8;

        hence contradiction by A5, A6, Th3;

      end;

       {} in omega by ORDINAL1:def 11;

      hence thesis by Def8;

    end;

    theorem :: ARYTM_3:38

    x in omega iff ( denominator x) = 1 by Def9, Th36;

    definition

      let i,j be natural Ordinal;

      :: ARYTM_3:def10

      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:

        now

          assume j <> {} ;

          then (( RED (i,j)),( RED (j,i))) are_coprime & ( RED (j,i)) <> {} by Th18, Th19;

          hence ( RED (j,i)) <> 1 implies [( RED (i,j)), ( RED (j,i))] in RAT+ by Th33;

        end;

        thus thesis by A1, Lm1, Lm6;

      end;

      consistency by Th26, Lm4;

    end

    notation

      let i,j be natural Ordinal;

      synonym quotient (i,j) for i / j;

    end

    theorem :: ARYTM_3:39



     Th39: (( numerator x) / ( denominator x)) = x

    proof



       A1: ( denominator x) <> {} by Th35;



       A2: ( RED (( numerator x),( denominator x))) = ( numerator x) by Th23, Th34;

      (( numerator x),( denominator x)) are_coprime by Th34;

      then

       A3: ( RED (( denominator x),( numerator x))) = ( denominator x) by Th23;

      per cases ;

        suppose

         A4: ( denominator x) = 1;

        then x in omega by Th36;

        then ( numerator x) = x by Def8;

        hence thesis by A2, A3, A4, Def10;

      end;

        suppose

         A5: ( denominator x) <> 1;

        then not x in omega by Def9;

        then x = [( numerator x), ( denominator x)] by Th36;

        hence thesis by A1, A2, A3, A5, Def10;

      end;

    end;

    theorem :: ARYTM_3:40



     Th40: ( {} / b) = {} & (a / 1) = a

    proof



       A1: b <> {} implies ( RED (b, {} )) = 1 by Th26;

      ( RED ( {} ,b)) = {} by Th26;

      hence ( {} / b) = {} by A1, Def10;

      ( RED (1,a)) = 1 & ( RED (a,1)) = a by Th24;

      hence thesis by Def10;

    end;

    theorem :: ARYTM_3:41



     Th41: a <> {} implies (a / a) = 1

    proof

      assume a <> {} ;

      then ( RED (a,a)) = 1 by Th27;

      hence thesis by Def10;

    end;

    theorem :: ARYTM_3:42



     Th42: 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

         A3: ( RED (b,a)) <> 1;



         A4: not [( RED (a,b)), ( RED (b,a))] in omega by Th32;

        (a / b) = [( RED (a,b)), ( RED (b,a))] by A1, A3, Def10;

        hence thesis by A4, Def8, Def9;

      end;

    end;

    theorem :: ARYTM_3:43



     Th43: (i,j) are_coprime & j <> {} implies ( numerator (i / j)) = i & ( denominator (i / j)) = j

    proof

      assume (i,j) are_coprime ;

      then ( RED (i,j)) = i & ( RED (j,i)) = j by Th23;

      hence thesis by Th42;

    end;

    theorem :: ARYTM_3:44



     Th44: c <> {} implies ((a *^ c) / (b *^ c)) = (a / b)

    proof

      assume

       A1: c <> {} ;

      per cases ;

        suppose b = {} ;

        then (a / b) = {} & (b *^ c) = {} by Def10, ORDINAL2: 35;

        hence thesis by Def10;

      end;

        suppose

         A2: b <> {} ;

        then

         A3: (b *^ c) <> {} by A1, ORDINAL3: 31;



        then

         A4: ( denominator ((a *^ c) / (b *^ c))) = ( RED ((b *^ c),(a *^ c))) by Th42

        .= ( RED (b,a)) by A1, Th28

        .= ( denominator (a / b)) by A2, Th42;

        ( numerator ((a *^ c) / (b *^ c))) = ( RED ((a *^ c),(b *^ c))) by A3, Th42

        .= ( RED (a,b)) by A1, Th28

        .= ( numerator (a / b)) by A2, Th42;



        hence ((a *^ c) / (b *^ c)) = (( numerator (a / b)) / ( denominator (a / b))) by A4, Th39

        .= (a / b) by Th39;

      end;

    end;

    reserve i,j,k for natural Ordinal;

    theorem :: ARYTM_3:45



     Th45: j <> {} & l <> {} implies ((i / j) = (k / l) iff (i *^ l) = (j *^ k))

    proof

      assume that

       A1: j <> {} and

       A2: l <> {} ;

      set x = (i / j), y = (k / l);

      set ny = ( numerator y), dy = ( denominator y);



       A3: ny = ( RED (k,l)) by A2, Th42;

      set nx = ( numerator x), dx = ( denominator x);



       A4: dx = ( RED (j,i)) by A1, Th42;



       A5: dy = ( RED (l,k)) by A2, Th42;



       A6: nx = ( RED (i,j)) by A1, Th42;

      hereby

        assume (i / j) = (k / l);

        then i = (ny *^ (i hcf j)) & l = (dx *^ (l hcf k)) by A6, A5, Th21;



        hence (i *^ l) = (((ny *^ (i hcf j)) *^ dx) *^ (l hcf k)) by ORDINAL3: 50

        .= ((ny *^ ((i hcf j) *^ dx)) *^ (l hcf k)) by ORDINAL3: 50

        .= ((ny *^ j) *^ (l hcf k)) by A4, Th21

        .= (j *^ (ny *^ (l hcf k))) by ORDINAL3: 50

        .= (j *^ k) by A3, Th21;

      end;

      assume

       A7: (i *^ l) = (j *^ k);

      then dx = ( RED ((j *^ l),(j *^ k))) by A2, A4, Th28;

      then

       A8: dx = dy by A1, A5, Th28;

      nx = ( RED ((j *^ k),(j *^ l))) by A2, A6, A7, Th28;

      then nx = ny by A1, A3, Th28;

      then x = (ny / dy) by A8, Th39;

      hence thesis by Th39;

    end;

    definition

      let x,y be Element of RAT+ ;

      :: ARYTM_3:def11

      func x + y -> Element of RAT+ equals (((( numerator x) *^ ( denominator y)) +^ (( numerator y) *^ ( denominator x))) / (( denominator x) *^ ( denominator y)));

      coherence ;

      commutativity ;

      :: ARYTM_3:def12

      func x *' y -> Element of RAT+ equals ((( numerator x) *^ ( numerator y)) / (( denominator x) *^ ( denominator y)));

      coherence ;

      commutativity ;

    end

    theorem :: ARYTM_3:46



     Th46: j <> {} & l <> {} implies ((i / j) + (k / l)) = (((i *^ l) +^ (j *^ k)) / (j *^ l))

    proof

      assume that

       A1: j <> {} and

       A2: l <> {} ;



       A3: ( denominator (k / l)) = ( RED (l,k)) & ( denominator (i / j)) = ( RED (j,i)) by A1, A2, Th42;

      ( numerator (k / l)) = ( RED (k,l)) & ( numerator (i / j)) = ( RED (i,j)) by A1, A2, Th42;



      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, A3, Th15, Th44

      .= ((((( 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: 50

      .= ((((( RED (i,j)) *^ ( RED (l,k))) +^ (( RED (j,i)) *^ ( RED (k,l)))) *^ (i hcf j)) / (( RED (l,k)) *^ j)) by Th21

      .= ((((( RED (i,j)) *^ ( RED (l,k))) *^ (i hcf j)) +^ ((( RED (j,i)) *^ ( RED (k,l))) *^ (i hcf j))) / (( RED (l,k)) *^ j)) by ORDINAL3: 46

      .= (((( RED (l,k)) *^ (( RED (i,j)) *^ (i hcf j))) +^ ((( RED (j,i)) *^ ( RED (k,l))) *^ (i hcf j))) / (( RED (l,k)) *^ j)) by ORDINAL3: 50

      .= (((( RED (l,k)) *^ i) +^ ((( RED (j,i)) *^ ( RED (k,l))) *^ (i hcf j))) / (( RED (l,k)) *^ j)) by Th21

      .= (((( RED (l,k)) *^ i) +^ (( RED (k,l)) *^ (( RED (j,i)) *^ (i hcf j)))) / (( RED (l,k)) *^ j)) by ORDINAL3: 50

      .= (((( RED (l,k)) *^ i) +^ (( RED (k,l)) *^ j)) / (( RED (l,k)) *^ j)) by Th21

      .= ((((( RED (l,k)) *^ i) +^ (( RED (k,l)) *^ j)) *^ (k hcf l)) / ((( RED (l,k)) *^ j) *^ (k hcf l))) by A2, Th15, Th44

      .= ((((( RED (l,k)) *^ i) +^ (( RED (k,l)) *^ j)) *^ (k hcf l)) / (j *^ (( RED (l,k)) *^ (k hcf l)))) by ORDINAL3: 50

      .= ((((( RED (l,k)) *^ i) +^ (( RED (k,l)) *^ j)) *^ (k hcf l)) / (j *^ l)) by Th21

      .= ((((( RED (l,k)) *^ i) *^ (k hcf l)) +^ ((( RED (k,l)) *^ j) *^ (k hcf l))) / (j *^ l)) by ORDINAL3: 46

      .= (((i *^ (( RED (l,k)) *^ (k hcf l))) +^ ((( RED (k,l)) *^ j) *^ (k hcf l))) / (j *^ l)) by ORDINAL3: 50

      .= (((i *^ l) +^ ((( RED (k,l)) *^ j) *^ (k hcf l))) / (j *^ l)) by Th21

      .= (((i *^ l) +^ (j *^ (( RED (k,l)) *^ (k hcf l)))) / (j *^ l)) by ORDINAL3: 50

      .= (((i *^ l) +^ (j *^ k)) / (j *^ l)) by Th21;

    end;

    theorem :: ARYTM_3:47



     Th47: 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 Th46

      .= (((i +^ j) *^ k) / (k *^ k)) by ORDINAL3: 46

      .= ((i +^ j) / k) by A1, Th44;

    end;

    registration

      cluster empty for Element of RAT+ ;

      existence by Lm1, Lm6;

    end

    definition

      :: original: {}

      redefine

      func {} -> Element of RAT+ ;

      coherence by Lm1, Lm6;

      :: original: one

      redefine

      func one -> non empty ordinal Element of RAT+ ;

      coherence by Lm6, Lm4;

    end

    theorem :: ARYTM_3:48



     Th48: (x *' {} ) = {}

    proof

      ( numerator {} ) = {} & (( numerator x) *^ {} ) = {} by Def8, Lm1, ORDINAL2: 35;

      hence thesis by Th40;

    end;

    theorem :: ARYTM_3:49



     Th49: ((i / j) *' (k / l)) = ((i *^ k) / (j *^ l))

    proof

      per cases ;

        suppose

         A1: j <> {} & l <> {} ;

        then

         A2: ( denominator (k / l)) = ( RED (l,k)) & ( denominator (i / j)) = ( RED (j,i)) by Th42;

        ( numerator (k / l)) = ( RED (k,l)) & ( numerator (i / j)) = ( RED (i,j)) by A1, Th42;



        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, A2, Th15, Th44

        .= ((( RED (k,l)) *^ (( RED (i,j)) *^ (i hcf j))) / ((( RED (j,i)) *^ ( RED (l,k))) *^ (i hcf j))) by ORDINAL3: 50

        .= ((( RED (k,l)) *^ i) / ((( RED (j,i)) *^ ( RED (l,k))) *^ (i hcf j))) by Th21

        .= ((( RED (k,l)) *^ i) / (( RED (l,k)) *^ (( RED (j,i)) *^ (i hcf j)))) by ORDINAL3: 50

        .= ((( RED (k,l)) *^ i) / (( RED (l,k)) *^ j)) by Th21

        .= (((( RED (k,l)) *^ i) *^ (l hcf k)) / ((( RED (l,k)) *^ j) *^ (l hcf k))) by A1, Th15, Th44

        .= ((i *^ (( RED (k,l)) *^ (l hcf k))) / ((( RED (l,k)) *^ j) *^ (l hcf k))) by ORDINAL3: 50

        .= ((i *^ k) / ((( RED (l,k)) *^ j) *^ (l hcf k))) by Th21

        .= ((i *^ k) / (j *^ (( RED (l,k)) *^ (l hcf k)))) by ORDINAL3: 50

        .= ((i *^ k) / (j *^ l)) by Th21;

      end;

        suppose

         A3: j = {} or l = {} ;

        then (i / j) = {} or (k / l) = {} by Def10;

        then

         A4: ((i / j) *' (k / l)) = {} by Th48;

        (j *^ l) = {} by A3, ORDINAL2: 35;

        hence thesis by A4, Def10;

      end;

    end;

    theorem :: ARYTM_3:50



     Th50: (x + {} ) = x

    proof



       A1: (( numerator x) *^ 1) = ( numerator x) & ( {} *^ ( denominator x)) = {} by ORDINAL2: 35, ORDINAL2: 39;



       A2: (( denominator x) *^ 1) = ( denominator x) & (( numerator x) +^ {} ) = ( numerator x) by ORDINAL2: 27, ORDINAL2: 39;

      ( denominator {} ) = 1 & ( numerator {} ) = {} by Def8, Def9, Lm1;

      hence thesis by A1, A2, Th39;

    end;

    theorem :: ARYTM_3:51



     Th51: ((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: dy <> {} by Th35;



       A2: dz <> {} by Th35;

      then

       A3: (dy *^ dz) <> {} by A1, ORDINAL3: 31;



       A4: dx <> {} by Th35;

      then

       A5: (dx *^ dy) <> {} by A1, ORDINAL3: 31;



      thus ((x + y) + z) = ((((nx *^ dy) +^ (dx *^ ny)) / (dx *^ dy)) + (nz / dz)) by Th39

      .= (((((nx *^ dy) +^ (dx *^ ny)) *^ dz) +^ ((dx *^ dy) *^ nz)) / ((dx *^ dy) *^ dz)) by A2, A5, Th46

      .= (((((nx *^ dy) *^ dz) +^ ((dx *^ ny) *^ dz)) +^ ((dx *^ dy) *^ nz)) / ((dx *^ dy) *^ dz)) by ORDINAL3: 46

      .= ((((nx *^ (dy *^ dz)) +^ ((dx *^ ny) *^ dz)) +^ ((dx *^ dy) *^ nz)) / ((dx *^ dy) *^ dz)) by ORDINAL3: 50

      .= ((((nx *^ (dy *^ dz)) +^ (dx *^ (ny *^ dz))) +^ ((dx *^ dy) *^ nz)) / ((dx *^ dy) *^ dz)) by ORDINAL3: 50

      .= ((((nx *^ (dy *^ dz)) +^ (dx *^ (ny *^ dz))) +^ (dx *^ (dy *^ nz))) / ((dx *^ dy) *^ dz)) by ORDINAL3: 50

      .= (((nx *^ (dy *^ dz)) +^ ((dx *^ (ny *^ dz)) +^ (dx *^ (dy *^ nz)))) / ((dx *^ dy) *^ dz)) by ORDINAL3: 30

      .= (((nx *^ (dy *^ dz)) +^ (dx *^ ((ny *^ dz) +^ (dy *^ nz)))) / ((dx *^ dy) *^ dz)) by ORDINAL3: 46

      .= (((nx *^ (dy *^ dz)) +^ (dx *^ ((ny *^ dz) +^ (dy *^ nz)))) / (dx *^ (dy *^ dz))) by ORDINAL3: 50

      .= ((((ny *^ dz) +^ (dy *^ nz)) / (dy *^ dz)) + (nx / dx)) by A4, A3, Th46

      .= (x + (y + z)) by Th39;

    end;

    theorem :: ARYTM_3:52



     Th52: ((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: x = (nx / dx) by Th39;

      z = (nz / dz) by Th39;



      hence ((x *' y) *' z) = (((nx *^ ny) *^ nz) / ((dx *^ dy) *^ dz)) by Th49

      .= ((nx *^ (ny *^ nz)) / ((dx *^ dy) *^ dz)) by ORDINAL3: 50

      .= ((nx *^ (ny *^ nz)) / (dx *^ (dy *^ dz))) by ORDINAL3: 50

      .= (x *' (y *' z)) by A1, Th49;

    end;

    theorem :: ARYTM_3:53



     Th53: (x *' one ) = x

    proof

      set y = one ;



       A1: (( numerator x) *^ 1) = ( numerator x) & (( denominator x) *^ 1) = ( denominator x) by ORDINAL2: 39;

      ( numerator y) = 1 & ( denominator y) = 1 by Def8, Def9;

      hence thesis by A1, Th39;

    end;

    theorem :: ARYTM_3:54



     Th54: x <> {} implies ex y st (x *' y) = 1

    proof

      set nx = ( numerator x), dx = ( denominator x);



       A1: dx <> {} by Th35;

      assume x <> {} ;

      then

       A2: nx <> {} by Th37;

      take y = (dx / nx);

      (nx,dx) are_coprime by Th34;

      then ( denominator y) = nx & ( numerator y) = dx by A2, Th43;

      hence thesis by A2, A1, Th41, ORDINAL3: 31;

    end;

    theorem :: ARYTM_3:55



     Th55: x <> {} implies ex z st y = (x *' z)

    proof

      reconsider o = one as Element of RAT+ ;

      assume x <> {} ;

      then

      consider z such that

       A1: (x *' z) = 1 by Th54;

      take (z *' y);



      thus y = (y *' o) by Th53

      .= (x *' (z *' y)) by A1, Th52;

    end;

    theorem :: ARYTM_3:56



     Th56: x <> {} & (x *' y) = (x *' z) implies y = z

    proof

      assume x <> {} ;

      then

      consider r be Element of RAT+ such that

       A1: (x *' r) = 1 by Th54;

      (r *' (x *' y)) = ( one *' y) by A1, Th52;

      then

       A2: (r *' (x *' y)) = y by Th53;

      (r *' (x *' z)) = ( one *' z) by A1, Th52;

      hence thesis by A2, Th53;

    end;

    theorem :: ARYTM_3:57



     Th57: (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: dx <> {} by Th35;

      dz <> {} by Th35;

      then

       A2: (dx *^ dz) <> {} by A1, ORDINAL3: 31;

      dy <> {} by Th35;

      then

       A3: (dx *^ dy) <> {} by A1, ORDINAL3: 31;

      x = (nx / dx) by Th39;



      hence (x *' (y + z)) = ((nx *^ ((ny *^ dz) +^ (dy *^ nz))) / (dx *^ (dy *^ dz))) by Th49

      .= (((nx *^ (ny *^ dz)) +^ (nx *^ (dy *^ nz))) / (dx *^ (dy *^ dz))) by ORDINAL3: 46

      .= ((((nx *^ ny) *^ dz) +^ (nx *^ (dy *^ nz))) / (dx *^ (dy *^ dz))) by ORDINAL3: 50

      .= ((((nx *^ ny) *^ dz) +^ (dy *^ (nx *^ nz))) / (dx *^ (dy *^ dz))) by ORDINAL3: 50

      .= ((((nx *^ ny) *^ dz) +^ (dy *^ (nx *^ nz))) / (dy *^ (dx *^ dz))) by ORDINAL3: 50

      .= ((dx *^ (((nx *^ ny) *^ dz) +^ (dy *^ (nx *^ nz)))) / (dx *^ (dy *^ (dx *^ dz)))) by Th35, Th44

      .= (((dx *^ ((nx *^ ny) *^ dz)) +^ (dx *^ (dy *^ (nx *^ nz)))) / (dx *^ (dy *^ (dx *^ dz)))) by ORDINAL3: 46

      .= (((dx *^ ((nx *^ ny) *^ dz)) +^ ((dx *^ dy) *^ (nx *^ nz))) / (dx *^ (dy *^ (dx *^ dz)))) by ORDINAL3: 50

      .= ((((nx *^ ny) *^ (dx *^ dz)) +^ ((dx *^ dy) *^ (nx *^ nz))) / (dx *^ (dy *^ (dx *^ dz)))) by ORDINAL3: 50

      .= ((((nx *^ ny) *^ (dx *^ dz)) +^ ((dx *^ dy) *^ (nx *^ nz))) / ((dx *^ dy) *^ (dx *^ dz))) by ORDINAL3: 50

      .= ((x *' y) + (x *' z)) by A2, A3, Th46;

    end;

    theorem :: ARYTM_3:58



     Th58: for i,j be 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: j in omega by ORDINAL1:def 12;

      then

       A2: ( denominator j) = 1 by Def9;



       A3: i in omega by ORDINAL1:def 12;

      then ( denominator i) = 1 by Def9;



      hence (i + j) = (((ni *^ 1) +^ (1 *^ nj)) / 1) by A2, ORDINAL2: 39

      .= ((ni +^ (1 *^ nj)) / 1) by ORDINAL2: 39

      .= ((ni +^ nj) / 1) by ORDINAL2: 39

      .= (ni +^ nj) by Th40

      .= (i +^ nj) by A3, Def8

      .= (i +^ j) by A1, Def8;

    end;

    theorem :: ARYTM_3:59

    for i,j be 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: j in omega by ORDINAL1:def 12;

      then

       A2: ( denominator j) = 1 by Def9;



       A3: i in omega by ORDINAL1:def 12;

      then ( denominator i) = 1 by Def9;



      hence (i *' j) = ((ni *^ nj) / 1) by A2, ORDINAL2: 39

      .= (ni *^ nj) by Th40

      .= (i *^ nj) by A3, Def8

      .= (i *^ j) by A1, Def8;

    end;

    theorem :: ARYTM_3:60



     Th60: ex y st x = (y + y)

    proof

      set O2 = ( one + one );

      O2 = (1 +^ 1) by Th58;

      then O2 <> {} by ORDINAL3: 26;

      then

      consider z such that

       A1: (O2 *' z) = 1 by Th54;

      take y = (z *' x);



      thus x = ( one *' x) by Th53

      .= (O2 *' y) by A1, Th52

      .= (( one *' y) + ( one *' y)) by Th57

      .= (y + ( one *' y)) by Th53

      .= (y + y) by Th53;

    end;

    definition

      let x,y be Element of RAT+ ;

      :: ARYTM_3:def13

      pred x <=' y means

      : Def13: ex z be 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);



         A1: dx <> {} & dy <> {} by Th35;



         A2: (nx / dx) = x & (ny / dy) = y by Th39;

        (nx *^ dy) c= (ny *^ dx) or (ny *^ dx) c= (nx *^ dy);

        then

         A3: (ny *^ dx) = ((nx *^ dy) +^ ((ny *^ dx) -^ (nx *^ dy))) or (nx *^ dy) = ((ny *^ dx) +^ ((nx *^ dy) -^ (ny *^ dx))) by ORDINAL3:def 5;

        ((nx *^ dy) / (dx *^ dy)) = (nx / dx) & ((ny *^ dx) / (dx *^ dy)) = (ny / dy) by Th35, Th44;

        then x = (y + (((nx *^ dy) -^ (ny *^ dx)) / (dx *^ dy))) or y = (x + (((ny *^ dx) -^ (nx *^ dy)) / (dx *^ dy))) by A1, A2, A3, Th47, ORDINAL3: 31;

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

    theorem :: ARYTM_3:61

     not ex y be object st [ {} , y] in RAT+

    proof

      given y be object such that

       A1: [ {} , y] in RAT+ ;

      consider i,j be Element of omega such that

       A2: [ {} , y] = [i, j] and

       A3: (i,j) are_coprime and j <> {} and

       A4: j <> 1 by A1, Th29, Th32;

      i = {} by A2, XTUPLE_0: 1;

      hence thesis by A3, A4, Th3;

    end;

    theorem :: ARYTM_3:62



     Th62: (s + t) = (r + t) implies s = r

    proof

      assume

       A1: (s + t) = (r + t);

      set r1 = ( numerator r), r2 = ( denominator r);

      set t1 = ( numerator t), t2 = ( denominator t);

      set s1 = ( numerator s), s2 = ( denominator s);



       A2: t2 <> {} by Th35;



       A3: s2 <> {} by Th35;

      then

       A4: (s2 *^ t2) <> {} by A2, ORDINAL3: 31;



       A5: r2 <> {} by Th35;

      then (r2 *^ t2) <> {} by A2, ORDINAL3: 31;



      then (((s1 *^ t2) +^ (s2 *^ t1)) *^ (r2 *^ t2)) = (((r1 *^ t2) +^ (r2 *^ t1)) *^ (s2 *^ t2)) by A1, A4, Th45

      .= ((((r1 *^ t2) +^ (r2 *^ t1)) *^ s2) *^ t2) by ORDINAL3: 50;

      then ((((s1 *^ t2) +^ (s2 *^ t1)) *^ r2) *^ t2) = ((((r1 *^ t2) +^ (r2 *^ t1)) *^ s2) *^ t2) by ORDINAL3: 50;



      then (((s1 *^ t2) +^ (s2 *^ t1)) *^ r2) = (((r1 *^ t2) +^ (r2 *^ t1)) *^ s2) by A2, ORDINAL3: 33

      .= (((r1 *^ t2) *^ s2) +^ ((r2 *^ t1) *^ s2)) by ORDINAL3: 46;



      then (((s1 *^ t2) *^ r2) +^ ((s2 *^ t1) *^ r2)) = (((r1 *^ t2) *^ s2) +^ ((r2 *^ t1) *^ s2)) by ORDINAL3: 46

      .= (((r1 *^ t2) *^ s2) +^ ((s2 *^ t1) *^ r2)) by ORDINAL3: 50;



      then ((s1 *^ t2) *^ r2) = ((r1 *^ t2) *^ s2) by ORDINAL3: 21

      .= ((r1 *^ s2) *^ t2) by ORDINAL3: 50;

      then ((s1 *^ r2) *^ t2) = ((r1 *^ s2) *^ t2) by ORDINAL3: 50;

      then (s1 *^ r2) = (r1 *^ s2) by A2, ORDINAL3: 33;



      then (s1 / s2) = (r1 / r2) by A3, A5, Th45

      .= r by Th39;

      hence thesis by Th39;

    end;

    theorem :: ARYTM_3:63



     Th63: (r + s) = {} implies r = {}

    proof

      set nr = ( numerator r), dr = ( denominator r);

      set ns = ( numerator s), ds = ( denominator s);

      assume

       A1: (r + s) = {} ;

      ( denominator {} ) = 1 & ( numerator {} ) = {} by Def8, Def9, Lm1;

      then

       A2: (((nr *^ ds) +^ (ns *^ dr)) / (dr *^ ds)) = ( {} / 1) by A1, Th39;



       A3: ds <> {} by Th35;

      dr <> {} by Th35;

      then (dr *^ ds) <> {} by A3, ORDINAL3: 31;



      then (((nr *^ ds) +^ (ns *^ dr)) *^ 1) = ((dr *^ ds) *^ {} ) by A2, Th45, Lm4

      .= {} by ORDINAL2: 35;

      then ((nr *^ ds) +^ (ns *^ dr)) = {} by ORDINAL3: 31, Lm4;

      then (nr *^ ds) = {} by ORDINAL3: 26;

      then nr = {} by A3, ORDINAL3: 31;

      hence thesis by Th37;

    end;

    theorem :: ARYTM_3:64



     Th64: {} <=' s

    proof

      take s;

      thus thesis by Th50;

    end;

    theorem :: ARYTM_3:65

    s <=' {} implies s = {} by Th63;

    theorem :: ARYTM_3:66



     Th66: 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 Th50

      .= (r + (x + y)) by A1, A2, Th51;

      then x = {} by Th62, Th63;

      hence thesis by A1, Th50;

    end;

    theorem :: ARYTM_3:67



     Th67: 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, Th51;

    end;

    theorem :: ARYTM_3:68

    r < s iff r <=' s & r <> s by Th66;

    theorem :: ARYTM_3:69

    r < s & s <=' t or r <=' s & s < t implies r < t by Th67;

    theorem :: ARYTM_3:70

    r < s & s < t implies r < t by Th67;

    theorem :: ARYTM_3:71



     Th71: x in omega & (x + y) in omega implies y in omega

    proof

      assume that

       A1: x in omega and

       A2: (x + y) in omega ;



       A3: ( denominator (x + y)) = 1 by A2, Def9;

      set nx = ( numerator x), dx = ( denominator x);



       A4: dx = 1 by A1, Def9;

      set ny = ( numerator y), dy = ( denominator y);



       A5: (x + y) = (( numerator (x + y)) / ( denominator (x + y))) & (((nx *^ dy) +^ (ny *^ dx)) *^ 1) = ((nx *^ dy) +^ (ny *^ dx)) by Th39, ORDINAL2: 39;

      dy <> {} by Th35;

      then (dx *^ dy) <> {} by A4, ORDINAL3: 31, Lm4;



      then ((nx *^ dy) +^ (ny *^ dx)) = ((dx *^ dy) *^ ( numerator (x + y))) by A3, A5, Th45, Lm4

      .= (dy *^ ( numerator (x + y))) by A4, ORDINAL2: 39;

      then ((nx *^ dy) +^ ny) = (dy *^ ( numerator (x + y))) by A4, ORDINAL2: 39;

      then ny = ((dy *^ ( numerator (x + y))) -^ (nx *^ dy)) by ORDINAL3: 52;

      then ny = (dy *^ (( numerator (x + y)) -^ nx)) by ORDINAL3: 63;

      then

       A6: dy divides ny;



       A7: (ny,dy) are_coprime by Th34;

      for m be natural Ordinal st m divides dy & m divides ny holds m divides dy;

      then (dy hcf ny) = dy by A6, Def5;

      then

       A8: dy = 1 by A7, Th20;

      y = (ny / dy) by Th39;

      then y = ny by A8, Th40;

      hence thesis;

    end;

    theorem :: ARYTM_3:72



     Th72: for i be ordinal Element of RAT+ st i < x & x < (i + one ) holds not x in omega

    proof

      let i be ordinal Element of RAT+ ;

      assume that

       A1: i < x and

       A2: x < (i + one ) and

       A3: x in omega ;

      consider z such that

       A4: (i + one ) = (x + z) by A2, Def13;

      (i + one ) = (i +^ 1) by Th58;

      then (i + one ) in omega by Th31;

      then

      reconsider z9 = z as Element of omega by A3, A4, Th71;

      consider y such that

       A5: x = (i + y) by A1, Def13;

      i in omega by Th31;

      then

      reconsider y9 = y as Element of omega by A3, A5, Th71;

      (i + one ) = (i + (y + z)) by A5, A4, Th51;



      then 1 = (y + z) by Th62

      .= (y9 +^ z9) by Th58;

      then y9 c= 1 by ORDINAL3: 24;

      then y = {} or y = 1 by ORDINAL3: 16;

      then i = x or (i + one ) = x by A5, Th50;

      hence contradiction by A1, A2;

    end;

    theorem :: ARYTM_3:73



     Th73: t <> {} implies ex r st r < t & not r in omega

    proof

      assume

       A1: t <> {} ;



       A2: (1 +^ 1) = ( succ 1) by ORDINAL2: 31;

      per cases ;

        suppose

         A3: one <=' t;

        consider r such that

         A4: one = (r + r) by Th60;

        take r;

        r <=' one & r <> 1 by A2, A4, Th58;

        then r < one by Th66;

        hence r < t by A3, Th67;



         A5: (1 *^ 1) = 1 by ORDINAL2: 39;

        assume r in omega ;

        then

         A6: ( denominator r) = 1 by Def9;

        then (( numerator r) *^ ( denominator r)) = ( numerator r) by ORDINAL2: 39;

        then

         A7: 1 = (( numerator r) +^ ( numerator r)) by A4, A6, A5, Th40;

        then ( numerator r) c= 1 by ORDINAL3: 24;

        then ( numerator r) = {} or ( numerator r) = 1 by ORDINAL3: 16;

        hence contradiction by A2, A7, ORDINAL2: 27;

      end;

        suppose

         A8: t < one ;

        consider r such that

         A9: t = (r + r) by Th60;



         A10: {} <=' r by Th64;

        r <> {} by A1, A9, Th50;

        then

         A11: {} < r by A10, Th66;

        take r;



         A12: 1 = ( {} + one ) by Th50;



         A13: r <=' t by A9;

        now

          assume r = t;

          then (t + {} ) = (t + t) by A9, Th50;

          hence contradiction by A1, Th62;

        end;

        hence r < t by A13, Th66;

        r < one by A8, A13, Th67;

        hence thesis by A11, A12, Th72;

      end;

    end;

    theorem :: ARYTM_3:74

    { 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 and

         A3: not r in omega by Th73;

         {} <=' t by Th64;

        then {} < t by A1, Th66;

        then

         A4: {} in { s : s < t };

        r in { s : s < t } by A2;

        then { s : s < t } in omega implies r is Ordinal;

        then ex i,j be Element of omega st { s : s < t } = [i, j] & (i,j) are_coprime & j <> {} & j <> 1 by A1, A3, Th29, Th31;

        hence contradiction by A4, TARSKI:def 2;

      end;

      assume

       A5: t = {} ;

      { s : s < t } c= {}

      proof

        let a be object;

        assume a in { s : s < t };

        then ex s st a = s & s < t;

        hence thesis by A5, Th64;

      end;

      then { s : s < t } = {} ;

      hence thesis;

    end;

    theorem :: ARYTM_3:75

    for A be Subset of RAT+ st (ex t st t in A & t <> {} ) & for r, s st r in A & s <=' r holds s in A holds ex r1,r2,r3 be 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 and

       A2: t <> {} ;

      assume

       A3: for r, s st r in A & s <=' r holds s in A;

      consider x such that

       A4: t = (x + x) by Th60;

      take {} , x, t;

      x <=' t by A4;

      hence {} in A & x in A & t in A by A1, A3, Th64;

      thus {} <> x by A2, A4, Th50;

      hereby

        assume x = t;

        then (t + {} ) = (t + t) by A4, Th50;

        hence contradiction by A2, Th62;

      end;

      thus thesis by A2;

    end;

    theorem :: ARYTM_3:76



     Th76: (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, Th51;

        hence thesis by Th62;

      end;

      given z such that

       A2: r = (s + z);

      take z;

      thus thesis by A2, Th51;

    end;

    theorem :: ARYTM_3:77

    s <=' (s + t);

    theorem :: ARYTM_3:78

    (r *' s) = {} implies r = {} or s = {}

    proof

      set nr = ( numerator r), dr = ( denominator r);

      set ns = ( numerator s), ds = ( denominator s);

      assume

       A1: (r *' s) = {} ;

      dr <> {} & ds <> {} by Th35;

      then

       A2: (dr *^ ds) <> {} by ORDINAL3: 31;

      ( denominator {} ) = 1 & ( numerator {} ) = {} by Def8, Def9, Lm1;

      then ((nr *^ ns) / (dr *^ ds)) = ( {} / 1) by A1, Th39;



      then ((nr *^ ns) *^ 1) = ((dr *^ ds) *^ {} ) by A2, Th45, Lm4

      .= {} by ORDINAL2: 35;

      then (nr *^ ns) = {} by ORDINAL3: 31, Lm4;

      then nr = {} or ns = {} by ORDINAL3: 31;

      hence thesis by Th37;

    end;

    theorem :: ARYTM_3:79



     Th79: r <=' (s *' t) implies ex t0 be Element of RAT+ st r = (s *' t0) & t0 <=' t

    proof

      given x such that

       A1: (s *' t) = (r + x);

      per cases ;

        suppose

         A2: s = {} ;

        take t;

        (s *' t) = {} by A2, Th48;

        hence thesis by A1, Th63;

      end;

        suppose

         A3: s <> {} ;

        then

        consider t1 be Element of RAT+ such that

         A4: x = (s *' t1) by Th55;

        consider t0 be Element of RAT+ such that

         A5: r = (s *' t0) by A3, Th55;

        take t0;

        thus r = (s *' t0) by A5;

        take t1;

        (s *' t) = (s *' (t0 + t1)) by A1, A5, A4, Th57;

        hence thesis by A3, Th56;

      end;

    end;

    theorem :: ARYTM_3:80

    t <> {} & (s *' t) <=' (r *' t) implies s <=' r

    proof

      assume that

       A1: t <> {} and

       A2: (s *' t) <=' (r *' t);

      ex x st (s *' t) = (t *' x) & x <=' r by A2, Th79;

      hence thesis by A1, Th56;

    end;

    theorem :: ARYTM_3:81

    for r1,r2,s1,s2 be 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 that

       A2: s1 < r1 and

       A3: s2 < r2;

      (s1 + s2) < (r1 + s2) by A2, Th76;

      hence thesis by A1, A3, Th76;

    end;

    theorem :: ARYTM_3:82



     Th82: s <=' r implies (s *' t) <=' (r *' t)

    proof

      given x such that

       A1: r = (s + x);

      take (x *' t);

      thus thesis by A1, Th57;

    end;

    theorem :: ARYTM_3:83

    for r1,r2,s1,s2 be 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);



       A2: {} <=' s1 by Th64;

      assume that

       A3: s1 < r1 and

       A4: s2 < r2;

      s2 <> r2 & (s1 *' s2) <=' (r1 *' s2) by A3, A4, Th82;

      then (s1 *' s2) < (r1 *' s2) by A1, A3, A2, Th56, Th66;

      hence thesis by A1, A4, Th82;

    end;

    theorem :: ARYTM_3:84

    r = {} iff (r + s) = s

    proof

      (s + {} ) = s by Th50;

      hence thesis by Th62;

    end;

    theorem :: ARYTM_3:85

    for s1,t1,s2,t2 be 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, Th51;

      hence thesis by Th62;

    end;

    theorem :: ARYTM_3:86



     Th86: r <=' s & s <=' (r + t) implies ex t0 be Element of RAT+ st s = (r + t0) & t0 <=' t by Th76;

    theorem :: ARYTM_3:87

    r <=' (s + t) implies ex s0,t0 be 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 be Element of RAT+ st r = (s + t0) & t0 <=' t by A1, Th86;

        hence thesis;

      end;

        suppose

         A2: r <=' s;

        r = (r + {} ) & {} <=' t by Th50, Th64;

        hence thesis by A2;

      end;

    end;

    theorem :: ARYTM_3:88

    r < s & r < t implies ex t0 be Element of RAT+ st t0 <=' s & t0 <=' t & r < t0

    proof

      s <=' t & s <=' s or t <=' s & t <=' t;

      hence thesis;

    end;

    theorem :: ARYTM_3:89

    r <=' s & s <=' t & s <> t implies r <> t by Th66;

    theorem :: ARYTM_3:90

    s < (r + t) & t <> {} implies ex r0,t0 be Element of RAT+ st s = (r0 + t0) & r0 <=' r & t0 <=' t & t0 <> t

    proof

      assume that

       A1: s < (r + t) and

       A2: t <> {} ;

      per cases ;

        suppose r <=' s;

        then

        consider t0 be Element of RAT+ such that

         A3: s = (r + t0) & t0 <=' t by A1, Th86;

        take r, t0;

        thus thesis by A1, A3;

      end;

        suppose

         A4: s <=' r;

        s = (s + {} ) & {} <=' t by Th50, Th64;

        hence thesis by A2, A4;

      end;

    end;

    theorem :: ARYTM_3:91

    for A be non empty Subset of RAT+ st A in RAT+ holds ex s st s in A & for r st r in A holds r <=' s

    proof

      let A be non empty Subset of RAT+ ;

       A1:

      now

        given i,j be Element of omega such that

         A2: A = [i, j] and

         A3: (i,j) are_coprime and j <> {} and

         A4: j <> 1;

         A5:

        now

          assume {i} in omega ;

          then {} in {i} by ORDINAL3: 8;

          then {} = i by TARSKI:def 1;

          hence contradiction by A3, A4, Th3;

        end;

         {i} in A by A2, TARSKI:def 2;

        then

        consider i1,j1 be Element of omega such that

         A6: {i} = [i1, j1] and

         A7: (i1,j1) are_coprime and j1 <> {} and

         A8: j1 <> 1 by A5, Th29;

         {i1, j1} in {i} by A6, TARSKI:def 2;

        then

         A9: i = {i1, j1} by TARSKI:def 1;

         {i1} in {i} by A6, TARSKI:def 2;

        then i = {i1} by TARSKI:def 1;

        then j1 in {i1} by A9, TARSKI:def 2;

        then

         A10: j1 = i1 by TARSKI:def 1;

        j1 = (j1 *^ 1) by ORDINAL2: 39;

        hence contradiction by A7, A8, A10;

      end;

      assume A in RAT+ ;

      then

      reconsider B = A as Element of omega by A1, Th29;



       A11: {} in B by ORDINAL3: 8;

      now

        assume B is limit_ordinal;

        then omega c= B by A11, ORDINAL1:def 11;

        hence contradiction by ORDINAL1: 5;

      end;

      then

      consider C such that

       A12: B = ( succ C) by ORDINAL1: 29;

      C in B by A12, ORDINAL1: 6;

      then

      reconsider C as ordinal Element of RAT+ ;

      take C;

      thus C in A by A12, ORDINAL1: 6;

      let r;

      assume

       A13: r in A;

      then r in B;

      then

      reconsider r as ordinal Element of RAT+ ;

      (C -^ r) in omega by ORDINAL1:def 12;

      then

      reconsider x = (C -^ r) as ordinal Element of RAT+ by Lm6;

      r c= C by A12, A13, ORDINAL1: 22;



      then C = (r +^ x) by ORDINAL3:def 5

      .= (r + x) by Th58;

      hence thesis;

    end;

    theorem :: ARYTM_3:92

    ex t st (r + t) = s or (s + t) = r

    proof

      r <=' s or s <=' r;

      hence thesis;

    end;

    theorem :: ARYTM_3:93

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

      take t = (r + y);



       A4: s = (t + y) by A2, A3, Th51;

      then

       A5: t <=' s;

      r <=' t;

      hence r < t by A1, A4, Th66;

      r <> s by A1;

      then s <> t by A4, Th62;

      hence thesis by A5, Th66;

    end;

    theorem :: ARYTM_3:94

    ex s st r < s

    proof

      take s = (r + one );

      (s + {} ) = s by Th50;

      then

       A1: r <> s by Th62;

      r <=' s;

      hence thesis by A1, Th66;

    end;

    theorem :: ARYTM_3:95

    t <> {} implies ex s st s in omega & r <=' (s *' t)

    proof

      set y = ((( numerator r) *^ ((( numerator t) *^ ( denominator r)) -^ 1)) / ( denominator r));



       A1: ( denominator r) <> {} by Th35;

      (( denominator t) *^ ( numerator r)) in omega by ORDINAL1:def 12;

      then

      reconsider s = (( denominator t) *^ ( numerator r)) as ordinal Element of RAT+ by Lm6;

      assume t <> {} ;

      then ( numerator t) <> {} by Th37;

      then {} in (( numerator t) *^ ( denominator r)) by A1, ORDINAL3: 8, ORDINAL3: 31;

      then one c= (( numerator t) *^ ( denominator r)) by Lm3, ORDINAL1: 21;

      then (( numerator t) *^ ( denominator r)) = (1 +^ ((( numerator t) *^ ( denominator r)) -^ 1)) by ORDINAL3:def 5;



      then (s *^ (( numerator t) *^ ( denominator r))) = (( denominator t) *^ (( numerator r) *^ (1 +^ ((( numerator t) *^ ( denominator r)) -^ 1)))) by ORDINAL3: 50

      .= (( denominator t) *^ ((( numerator r) *^ 1) +^ (( numerator r) *^ ((( numerator t) *^ ( denominator r)) -^ 1)))) by ORDINAL3: 46;

      then

       A2: ((s *^ ( numerator t)) *^ ( denominator r)) = (( denominator t) *^ ((( numerator r) *^ 1) +^ (( numerator r) *^ ((( numerator t) *^ ( denominator r)) -^ 1)))) by ORDINAL3: 50;

      take s;

      thus s in omega by ORDINAL1:def 12;

      take y;

      ( denominator t) <> {} by Th35;



      then ((s *^ ( numerator t)) / ( denominator t)) = (((( numerator r) *^ 1) +^ (( numerator r) *^ ((( numerator t) *^ ( denominator r)) -^ 1))) / ( denominator r)) by A1, A2, Th45

      .= (((( numerator r) *^ 1) / ( denominator r)) + y) by Th35, Th47

      .= ((( numerator r) / ( denominator r)) + y) by ORDINAL2: 39

      .= (r + y) by Th39;



      then (r + y) = ((s *^ ( numerator t)) / (1 *^ ( denominator t))) by ORDINAL2: 39

      .= ((s / 1) *' (( numerator t) / ( denominator t))) by Th49

      .= (s *' (( numerator t) / ( denominator t))) by Th40;

      hence thesis by Th39;

    end;

    scheme :: ARYTM_3:sch1

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

      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: 8;

      now

        assume A is limit_ordinal;

        then omega c= A by A9, ORDINAL1:def 11;

        then A in A by A7;

        hence contradiction;

      end;

      then

      consider B be Ordinal such that

       A10: A = ( succ B) by ORDINAL1: 29;



       A11: B in A by A10, ORDINAL1: 8;

      then

       A12: B in omega by A7, ORDINAL1: 10;

      then

      reconsider s = B as ordinal Element of RAT+ by Lm6;

      take s;

      thus s in omega & P[s] by A8, A11, A12, ORDINAL1: 5;

      A = (B +^ 1) by A10, ORDINAL2: 31;

      hence thesis by A1, A7, Th58;

    end;