nat_d.miz



    begin

    reserve a,b,p,k,l,m,n,s,h,i,j,t,i1,i2 for natural Number;

     Lm1:

    now

      let k, l;

      reconsider k1 = k, l1 = l as Nat by TARSKI: 1;

      (k1 div l1) in NAT by INT_1: 3, INT_1: 55;

      hence (k div l) is Nat;

    end;

     Lm2:

    now

      let k, l;

      (k mod l) in NAT by INT_1: 3, INT_1: 57;

      hence (k mod l) is Nat;

    end;

    definition

      let k,l be natural Number;

      :: original: div

      redefine

      :: NAT_D:def1

      func k div l -> Nat means

      : Def1: (ex t be Nat st k = ((l * it ) + t) & t < l) or it = 0 & l = 0 ;

      compatibility

      proof

        let r be Nat;

        per cases ;

          suppose l = 0 ;

          hence thesis by INT_1: 48;

        end;

          suppose

           A1: l > 0 ;

          then

           A2: k = ((l * (k div l)) + (k mod l)) by INT_1: 59;

          

           A3: (k mod l) is Nat by Lm2;

          hence r = (k div l) implies (ex t be Nat st k = ((l * r) + t) & t < l) or r = 0 & l = 0 by A1, A2, INT_1: 58;

          assume

           A4: (ex t be Nat st k = ((l * r) + t) & t < l) or r = 0 & l = 0 ;

          

           A5: (k mod l) < l by A1, INT_1: 58;

          (k div l) is Nat by Lm1;

          hence thesis by A2, A3, A4, A5, NAT_1: 18;

        end;

      end;

      coherence by Lm1;

    end

    definition

      let k,l be natural Number;

      :: original: mod

      redefine

      :: NAT_D:def2

      func k mod l -> Nat means

      : Def2: (ex t be Nat st k = ((l * t) + it ) & it < l) or it = 0 & l = 0 ;

      compatibility

      proof

        let r be Nat;

        per cases ;

          suppose l = 0 ;

          hence thesis by INT_1:def 10;

        end;

          suppose

           A1: l > 0 ;

          then

           A2: k = ((l * (k div l)) + (k mod l)) by INT_1: 59;

          hence r = (k mod l) implies (ex t be Nat st k = ((l * t) + r) & r < l) or r = 0 & l = 0 by A1, INT_1: 58;

          assume

           A3: (ex t be Nat st k = ((l * t) + r) & r < l) or r = 0 & l = 0 ;

          

           A4: (k mod l) < l by A1, INT_1: 58;

          (k mod l) is Nat by Lm2;

          hence thesis by A2, A3, A4, NAT_1: 18;

        end;

      end;

      coherence by Lm2;

    end

    definition

      let k,l be Nat;

      :: original: div

      redefine

      func k div l -> Element of NAT ;

      coherence

      proof

        (k div l) is Nat;

        hence thesis by ORDINAL1:def 12;

      end;

      :: original: mod

      redefine

      func k mod l -> Element of NAT ;

      coherence

      proof

        (k mod l) is Nat;

        hence thesis by ORDINAL1:def 12;

      end;

    end

    theorem :: NAT_D:1

    

     Th1: 0 < i implies (j mod i) < i by INT_1: 58;

    theorem :: NAT_D:2

     0 < i implies j = ((i * (j div i)) + (j mod i)) by INT_1: 59;

    definition

      let k,l be natural Number;

      :: original: divides

      redefine

      :: NAT_D:def3

      pred k divides l means ex t be Nat st l = (k * t);

      compatibility

      proof

        hereby

          assume

           A1: k divides l;

          thus ex t be Nat st l = (k * t)

          proof

            consider t be Integer such that

             A2: l = (k * t) by A1, INT_1:def 3;

            per cases ;

              suppose 0 < l;

              then 0 <= t by A2;

              then

              reconsider t as Element of NAT by INT_1: 3;

              take t;

              thus l = (k * t) by A2;

            end;

              suppose

               A3: l = 0 ;

              take 0 ;

              thus l = (k * 0 ) by A3;

            end;

          end;

        end;

        thus thesis by INT_1:def 3;

      end;

      reflexivity

      proof

        let i;

        i = (i * 1);

        hence thesis;

      end;

    end

    theorem :: NAT_D:3

    

     Th3: j divides i iff i = (j * (i div j))

    proof

      thus j divides i implies i = (j * (i div j))

      proof

        assume j divides i;

        then

        consider k be Nat such that

         A1: i = (j * k);

        

         A2: i = ((j * k) + 0 ) by A1;

        now

          assume

           A3: j <> 0 ;

          then

           A4: i = ((j * (i div j)) + (i mod j)) by INT_1: 59;

          (i mod j) < j by A3, Th1;

          hence thesis by A2, A4, NAT_1: 18;

        end;

        hence thesis by A1;

      end;

      thus thesis;

    end;

    theorem :: NAT_D:4

    i divides j & j divides h implies i divides h by INT_2: 9;

    theorem :: NAT_D:5

    

     Th5: i divides j & j divides i implies i = j

    proof

      assume that

       A1: i divides j and

       A2: j divides i;

      

       A3: j = (i * (j div i)) by A1, Th3;

      i = (j * (i div j)) by A2, Th3;

      

      then

       A4: (i * 1) = ((i * (j div i)) * (i div j)) by A3

      .= (i * ((j div i) * (i div j)));

      

       A5: i = 0 implies i = j by A3;

      ((j div i) * (i div j)) = 1 implies i = j

      proof

        assume ((j div i) * (i div j)) = 1;

        then (j div i) = 1 by NAT_1: 15;

        hence thesis by A3;

      end;

      hence thesis by A4, A5, XCMPLX_1: 5;

    end;

    theorem :: NAT_D:6

    

     Th6: i divides 0 & 1 divides i by INT_2: 12;

    theorem :: NAT_D:7

     0 < j & i divides j implies i <= j by INT_2: 27;

    theorem :: NAT_D:8

    

     Th8: i divides j & i divides h implies i divides (j + h)

    proof

      assume that

       A1: i divides j and

       A2: i divides h;

      

       A3: j = (i * (j div i)) by A1, Th3;

      h = (i * (h div i)) by A2, Th3;

      then (j + h) = (i * ((j div i) + (h div i))) by A3;

      hence thesis;

    end;

    theorem :: NAT_D:9

    

     Th9: i divides j implies i divides (j * h) by INT_2: 2;

    theorem :: NAT_D:10

    

     Th10: i divides j & i divides (j + h) implies i divides h

    proof

      assume that

       A1: i divides j and

       A2: i divides (j + h);

      consider t be Nat such that

       A3: (j + h) = (i * t) by A2;

      consider u be Nat such that

       A4: j = (i * u) by A1;

      now

        assume

         A5: i <> 0 ;

        then

         A6: h = ((i * (h div i)) + (h mod i)) by INT_1: 59;

        

         A7: (j + ((i * (h div i)) + (h mod i))) = ((i * (u + (h div i))) + (h mod i)) by A4;

        

         A8: (h mod i) < i by A5, Th1;

        (j + h) = ((i * t) + 0 ) by A3;

        then (h mod i) = 0 by A6, A7, A8, NAT_1: 18;

        hence thesis by A6;

      end;

      hence thesis by A3;

    end;

    theorem :: NAT_D:11

    

     Th11: i divides j & i divides h implies i divides (j mod h)

    proof

      assume that

       A1: i divides j and

       A2: i divides h;

       A3:

      now

        assume h = 0 ;

        then (j mod h) = 0 by Def2;

        hence thesis by Th6;

      end;

      now

        assume h <> 0 ;

        then

         A4: j = ((h * (j div h)) + (j mod h)) by INT_1: 59;

        i divides (h * (j div h)) by A2, Th9;

        hence thesis by A1, A4, Th10;

      end;

      hence thesis by A3;

    end;

    definition

      let k,n be natural Number;

      :: original: lcm

      redefine

      :: NAT_D:def4

      func k lcm n means

      : Def4: k divides it & n divides it & for m be Nat st k divides m & n divides m holds it divides m;

      compatibility

      proof

        let IT be Nat;

        thus IT = (k lcm n) implies k divides IT & n divides IT & for m be Nat st k divides m & n divides m holds IT divides m by INT_2:def 1;

        assume that

         A1: k divides IT and

         A2: n divides IT and

         A3: for m be Nat st k divides m & n divides m holds IT divides m;

        for m be Integer st k divides m & n divides m holds IT divides m

        proof

          let m be Integer;

          m in INT by INT_1:def 2;

          then

          consider i be Nat such that

           A4: m = i or m = ( - i) by INT_1:def 1;

          assume that

           A5: k divides m and

           A6: n divides m;

          

           A7: k divides i by A4, A5, INT_2: 10;

          n divides i by A4, A6, INT_2: 10;

          then IT divides i by A3, A7;

          hence thesis by A4, INT_2: 10;

        end;

        hence thesis by A1, A2, INT_2:def 1;

      end;

    end

    definition

      let k,n be Nat;

      :: original: lcm

      redefine

      func k lcm n -> Element of NAT ;

      coherence by ORDINAL1:def 12;

    end

    definition

      let k,n be natural Number;

      :: original: gcd

      redefine

      :: NAT_D:def5

      func k gcd n means

      : Def5: it divides k & it divides n & for m be Nat st m divides k & m divides n holds m divides it ;

      compatibility

      proof

        let IT be Nat;

        thus IT = (k gcd n) implies IT divides k & IT divides n & for m be Nat st m divides k & m divides n holds m divides IT by INT_2:def 2;

        assume that

         A1: IT divides k and

         A2: IT divides n and

         A3: for m be Nat st m divides k & m divides n holds m divides IT;

        for m be Integer st m divides k & m divides n holds m divides IT

        proof

          let m be Integer;

          m in INT by INT_1:def 2;

          then

          consider i be Nat such that

           A4: m = i or m = ( - i) by INT_1:def 1;

          assume that

           A5: m divides k and

           A6: m divides n;

          

           A7: i divides k by A4, A5, INT_2: 10;

          i divides n by A4, A6, INT_2: 10;

          then i divides IT by A3, A7;

          hence thesis by A4, INT_2: 10;

        end;

        hence thesis by A1, A2, INT_2:def 2;

      end;

    end

    definition

      let k,n be Nat;

      :: original: gcd

      redefine

      func k gcd n -> Element of NAT ;

      coherence by ORDINAL1:def 12;

    end

    ::$Notion-Name

    ::$Notion-Name

    scheme :: NAT_D:sch1

    Euklides { Q( Nat) -> Nat , a,b() -> Nat } :

ex n be Nat st Q(n) = (a() gcd b()) & Q(+) = 0

      provided

       A1: 0 < b() & b() < a()

       and

       A2: Q(0) = a() & Q() = b()

       and

       A3: for n be Nat holds Q(+) = (Q(n) mod Q(+));

      defpred P[ Nat] means ex n be Element of NAT st $1 = Q(n);

      

       A4: ex k be Nat st P[k] by A2;

      

       A5: for k be Nat st k <> 0 & P[k] holds ex n be Nat st n < k & P[n]

      proof

        let k be Nat;

        assume that

         A6: k <> 0 and

         A7: ex n be Element of NAT st k = Q(n);

        consider n be Element of NAT such that

         A8: k = Q(n) by A7;

        reconsider Q = Q(+) as Element of NAT by ORDINAL1:def 12;

        

         A9: n = 0 implies Q < k by A1, A2, A8;

        now

          given m be Nat such that

           A10: n = (m + 1);

          reconsider m1 = m as Element of NAT by ORDINAL1:def 12;

          Q(+) = (Q(m1) mod Q(+)) by A3;

          hence Q(+) < k by A6, A8, A10, Th1;

          take m = (n + 1);

          thus Q(+) = Q(m);

        end;

        hence thesis by A9, NAT_1: 6;

      end;

      

       A11: P[ 0 ] from NAT_1:sch 7( A4, A5);

      defpred Q[ Nat] means 0 = Q($1);

      

       A12: ex n be Nat st Q[n] by A11;

      consider k be Nat such that

       A13: Q[k] & for n be Nat st Q[n] holds k <= n from NAT_1:sch 5( A12);

      consider n be Nat such that

       A14: k = (n + 1) by A1, A2, A13, NAT_1: 6;

      reconsider n as Element of NAT by ORDINAL1:def 12;

      take n;

      defpred PP[ Nat] means Q(n) divides Q($1) & Q(n) divides Q(+);

       PP[n] by A13, A14, Th6;

      then

       A15: ex k be Nat st PP[k];

      

       A16: for k be Nat st k <> 0 & PP[k] holds ex m be Nat st m < k & PP[m]

      proof

        let l be Nat;

        assume that

         A17: l <> 0 and

         A18: Q(n) divides Q(l) and

         A19: Q(n) divides Q(+);

        consider m be Nat such that

         A20: l = (m + 1) by A17, NAT_1: 6;

        reconsider m as Element of NAT by ORDINAL1:def 12;

        take m;

        

         A21: m <= (m + 1) by NAT_1: 11;

        m <> (m + 1);

        hence m < l by A20, A21, XXREAL_0: 1;

         A22:

        now

          assume

           A23: Q(+) = 0 ;

          now

            assume

             A24: (m + 1) <> k;

            k <= (m + 1) by A13, A23;

            then k < (m + 1) by A24, XXREAL_0: 1;

            then

             A25: k <= m by NAT_1: 13;

            defpred Q[ Nat] means k <= $1 implies Q($1) = 0 ;

            

             A26: Q[ 0 ] by A13;

            

             A27: for m be Nat st Q[m] holds Q[(m + 1)]

            proof

              let m be Nat such that

               A28: k <= m implies Q(m) = 0 and

               A29: k <= (m + 1);

              now

                assume k <> (m + 1);

                then

                 A30: k < (m + 1) by A29, XXREAL_0: 1;

                then

                consider l be Nat such that

                 A31: m = (l + 1) by A1, A2, A28, NAT_1: 6, NAT_1: 13;

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

                Q(+) = (Q(l) mod Q(+)) by A3;

                hence thesis by A28, A30, A31, Def2, NAT_1: 13;

              end;

              hence thesis by A13;

            end;

            for m be Nat holds Q[m] from NAT_1:sch 2( A26, A27);

            then Q(m) = 0 by A25;

            hence Q(n) divides Q(m) by Th6;

          end;

          hence Q(n) divides Q(m) by A14;

        end;

        now

          assume

           A32: Q(+) <> 0 ;

          Q(+) = (Q(m) mod Q(+)) by A3;

          then

           A33: Q(m) = ((Q(+) * (Q(m) div Q(+))) + Q(+)) by A32, INT_1: 59;

          Q(n) divides (Q(+) * (Q(m) div Q(+))) by A18, A20, Th9;

          hence Q(n) divides Q(m) by A19, A20, A33, Th8;

        end;

        hence Q(n) divides Q(m) by A22;

        thus Q(n) divides Q(+) by A18, A20;

      end;

      now

         PP[ 0 ] from NAT_1:sch 7( A15, A16);

        hence Q(n) divides a() & Q(n) divides b() by A2;

        let m be Nat;

        defpred P1[ Nat] means m divides Q($1) & m divides Q(+);

        assume that

         A34: m divides a() and

         A35: m divides b();

        

         A36: P1[ 0 ] by A2, A34, A35;

        

         A37: for k be Nat st P1[k] holds P1[(k + 1)]

        proof

          let k be Nat;

          assume that

           A38: m divides Q(k) and

           A39: m divides Q(+);

          thus m divides Q(+) by A39;

          Q(+) = (Q(k) mod Q(+)) by A3;

          hence m divides Q(+) by A38, A39, Th11;

        end;

        for k be Nat holds P1[k] from NAT_1:sch 2( A36, A37);

        hence m divides Q(n);

      end;

      hence Q(n) = (a() gcd b()) by Def5;

      thus thesis by A13, A14;

    end;

    theorem :: NAT_D:12

    (n mod 2) = 0 or (n mod 2) = 1

    proof

      assume

       A1: (n mod 2) <> 0 ;

      

       A2: 2 = (1 + 1);

      (n mod 2) < 2 by Th1;

      then

       A3: (n mod 2) <= 1 by A2, NAT_1: 13;

      (n mod 2) >= 1 by A1, NAT_1: 14;

      hence thesis by A3, XXREAL_0: 1;

    end;

    theorem :: NAT_D:13

    ((k * n) mod k) = 0

    proof

      

       A0: k is Nat & n is Nat by TARSKI: 1;

      per cases ;

        suppose k = 0 ;

        hence thesis by Def2;

      end;

        suppose

         A1: k <> 0 ;

        (k * n) = ((k * n) + 0 );

        hence thesis by A0, A1, Def2;

      end;

    end;

    theorem :: NAT_D:14

    k > 1 implies (1 mod k) = 1

    proof

      assume

       A1: k > 1;

      1 = ((k * 0 ) + 1);

      hence thesis by A1, Def2;

    end;

    theorem :: NAT_D:15

    (k mod n) = 0 & l = (k - (m * n)) implies (l mod n) = 0

    proof

      assume that

       A1: (k mod n) = 0 and

       A2: l = (k - (m * n));

      per cases ;

        suppose n = 0 ;

        hence thesis by A1, A2;

      end;

        suppose n <> 0 ;

        then

        consider t be Nat such that

         A3: k = ((n * t) + 0 ) and

         A4: 0 < n by A1, Def2;

        

         A5: l = ((n * (t - m)) + 0 ) by A2, A3;

        now

          assume t < (m + 0 );

          then (t - m) < 0 by XREAL_1: 19;

          then l < (n * 0 ) by A4, A5, XREAL_1: 68;

          hence contradiction;

        end;

        then (t - m) is Element of NAT by NAT_1: 21;

        hence thesis by A4, A5, Def2;

      end;

    end;

    theorem :: NAT_D:16

    n <> 0 & (k mod n) = 0 & l < n implies ((k + l) mod n) = l

    proof

      

       A0: k is Nat & n is Nat & l is Nat by TARSKI: 1;

      assume that

       A1: n <> 0 and

       A2: (k mod n) = 0 and

       A3: l < n;

      ex t be Nat st k = ((n * t) + 0 ) & 0 < n by A1, A2, Def2;

      hence thesis by A0, A3, Def2;

    end;

    theorem :: NAT_D:17

    (k mod n) = 0 implies ((k + l) mod n) = (l mod n)

    proof

      assume that

       A1: (k mod n) = 0 ;

      per cases ;

        suppose

         A2: n = 0 ;

        

        hence ((k + l) mod n) = 0 by Def2

        .= (l mod n) by A2, Def2;

      end;

        suppose

         A3: n <> 0 ;

        then

        consider m be Nat such that

         A4: k = ((n * m) + 0 ) and 0 < n by A1, Def2;

        consider t be Nat such that

         A5: l = ((n * t) + (l mod n)) and

         A6: (l mod n) < n by A3, Def2;

        (k + l) = ((n * (m + t)) + (l mod n)) by A4, A5;

        hence thesis by A6, Def2;

      end;

    end;

    theorem :: NAT_D:18

    k <> 0 implies ((k * n) div k) = n

    proof

      

       A0: k is Nat & n is Nat by TARSKI: 1;

      assume

       A1: k <> 0 ;

      (k * n) = ((k * n) + 0 );

      hence thesis by A0, A1, Def1;

    end;

    theorem :: NAT_D:19

    (k mod n) = 0 implies ((k + l) div n) = ((k div n) + (l div n))

    proof

      assume

       A1: (k mod n) = 0 ;

      per cases ;

        suppose

         A2: n <> 0 ;

        then

         A3: k = ((n * (k div n)) + 0 ) by A1, INT_1: 59;

        

         A4: ex t be Nat st l = ((n * t) + (l mod n)) & (l mod n) < n by A2, Def2;

        l = ((n * (l div n)) + (l mod n)) by A2, INT_1: 59;

        then (k + l) = ((n * ((k div n) + (l div n))) + (l mod n)) by A3;

        hence thesis by A4, Def1;

      end;

        suppose

         A5: n = 0 ;

        then

         A6: ((k + l) div n) = 0 by Def1;

        (k div n) = 0 by A5, Def1;

        hence thesis by A5, A6, Def1;

      end;

    end;

    begin

    ::$Canceled

    theorem :: NAT_D:21

    

     Th21: (m mod n) = (((n * k) + m) mod n)

    proof

      per cases ;

        suppose

         A1: n > 0 ;

        (m mod n) = t implies (((n * k) + m) mod n) = t

        proof

          assume (m mod n) = t;

          then

          consider q be Nat such that

           A2: m = ((n * q) + t) and

           A3: t < n by A1, Def2;

          

           A0: k is Nat & m is Nat & n is Nat & t is Nat by TARSKI: 1;

          ex p be Nat st ((n * k) + m) = ((n * p) + t) & t < n

          proof

            reconsider p = (k + q) as Element of NAT by ORDINAL1:def 12;

            take p;

            thus thesis by A2, A3;

          end;

          hence thesis by A0, Def2;

        end;

        hence thesis;

      end;

        suppose n = 0 ;

        hence thesis;

      end;

    end;

    theorem :: NAT_D:22

    

     Th22: ((p + s) mod n) = (((p mod n) + s) mod n)

    proof

      per cases ;

        suppose n > 0 ;

        

        then ((p + s) mod n) = ((((n * (p div n)) + (p mod n)) + s) mod n) by INT_1: 59

        .= (((n * (p div n)) + ((p mod n) + s)) mod n)

        .= (((p mod n) + s) mod n) by Th21;

        hence thesis;

      end;

        suppose

         A1: n = 0 ;

        

        hence ((p + s) mod n) = 0 by Def2

        .= (((p mod n) + s) mod n) by A1, Def2;

      end;

    end;

    theorem :: NAT_D:23

    ((p + s) mod n) = ((p + (s mod n)) mod n) by Th22;

    theorem :: NAT_D:24

    

     Th24: k < n implies (k mod n) = k

    proof

      k = ((n * 0 ) + k);

      hence thesis by Def2;

    end;

    theorem :: NAT_D:25

    

     Th25: (n mod n) = 0

    proof

      per cases ;

        suppose

         A1: n > 0 ;

        n = ((n * 1) + 0 );

        hence thesis by A1, Def2;

      end;

        suppose n = 0 ;

        hence thesis by Def2;

      end;

    end;

    theorem :: NAT_D:26

    

     Th26: 0 = ( 0 mod n)

    proof

      n = 0 or n > 0 ;

      hence thesis by Def2, Th24;

    end;

    theorem :: NAT_D:27

    

     Th27: i < j implies (i div j) = 0

    proof

      assume

       A1: i < j;

      per cases by Def1;

        suppose ex j1 be Nat st i = ((j * (i div j)) + j1) & j1 < j;

        then

        consider j1 be Nat such that

         A2: i = ((j * (i div j)) + j1) and j1 < j;

        assume (i div j) <> 0 ;

        then

        consider k be Nat such that

         A3: (i div j) = (k + 1) by NAT_1: 6;

        i = (j + ((j * k) + j1)) by A2, A3;

        hence contradiction by A1, NAT_1: 11;

      end;

        suppose (i div j) = 0 & j = 0 ;

        hence thesis;

      end;

    end;

    theorem :: NAT_D:28

    

     Th28: m > 0 implies (n gcd m) = (m gcd (n mod m))

    proof

      set r = (n mod m), x = (n gcd m), y = (m gcd r);

      assume m > 0 ;

      then

      consider t be Nat such that

       A1: n = ((m * t) + r) and r < m by Def2;

      reconsider t as Element of NAT by ORDINAL1:def 12;

      

       A2: x divides n by Def5;

      

       A3: x divides m by Def5;

      then x divides r by A2, Th11;

      then

       A4: x divides y by A3, Def5;

      

       A5: y divides m by Def5;

      

       A6: y divides r by Def5;

      y divides (m * t) by A5, Th9;

      then y divides n by A1, A6, Th8;

      then y divides x by A5, Def5;

      hence thesis by A4, Th5;

    end;

    scheme :: NAT_D:sch2

    INDI { k,n() -> Element of NAT , P[ set] } :

P[n()]

      provided

       A1: P[ 0 ]

       and

       A2: k() > 0

       and

       A3: for i,j be Nat st P[(k() * i)] & j <> 0 & j <= k() holds P[((k() * i) + j)];

      defpred R[ Nat] means P[(k() * $1)];

      

       A4: R[ 0 ] by A1;

       A5:

      now

        let i be Nat;

        assume

         A6: R[i];

        (k() * (i + 1)) = ((k() * i) + k());

        hence R[(i + 1)] by A2, A3, A6;

      end;

      

       A7: for i be Nat holds R[i] from NAT_1:sch 2( A4, A5);

      per cases ;

        suppose (n() mod k()) = 0 ;

        then n() = ((k() * (n() div k())) + 0 ) by A2, INT_1: 59;

        hence thesis by A7;

      end;

        suppose

         A8: (n() mod k()) <> 0 ;

        

         A9: n() = ((k() * (n() div k())) + (n() mod k())) by A2, INT_1: 59;

        (n() mod k()) <= k() by A2, Th1;

        hence thesis by A3, A7, A8, A9;

      end;

    end;

    theorem :: NAT_D:29

    (i * j) = ((i lcm j) * (i gcd j))

    proof

      

       A0: i is Nat & j is Nat by TARSKI: 1;

      

       A1: i <> 0 & j <> 0 implies (i * j) = ((i lcm j) * (i gcd j))

      proof

        assume that

         A2: i <> 0 and

         A3: j <> 0 ;

        

         A4: i divides i implies i divides (i * j) by A0;

        j divides j implies j divides (j * i) by A0;

        then (i lcm j) divides (i * j) by A4, Def4;

        then

        consider c be Nat such that

         A5: (i * j) = ((i lcm j) * c);

        

         A6: i divides (i lcm j) by Def4;

        

         A7: j divides (i lcm j) by Def4;

        consider d be Nat such that

         A8: (i lcm j) = (i * d) by A6;

        consider e be Nat such that

         A9: (i lcm j) = (j * e) by A7;

        (i * j) = (i * (c * d)) by A5, A8;

        then

         A10: j = (c * d) by A2, XCMPLX_1: 5;

        (i * j) = (j * (c * e)) by A5, A9;

        then i = (c * e) by A3, XCMPLX_1: 5;

        then

         A11: c divides i;

        

         A12: c divides j by A10;

        for f be Nat holds f divides i & f divides j implies f divides c

        proof

          let f be Nat;

          assume that

           A13: f divides i and

           A14: f divides j;

          consider g be Nat such that

           A15: i = (f * g) by A13;

          consider h be Nat such that

           A16: j = (f * h) by A14;

          

           A17: (j * g) = ((g * h) * f) by A16;

          (i * h) = ((g * h) * f) by A15;

          then

           A18: i divides ((g * h) * f);

          j divides ((g * h) * f) by A17;

          then (i lcm j) divides ((g * h) * f) by A18, Def4;

          then

          consider z be Nat such that

           A19: ((g * h) * f) = ((i lcm j) * z);

          

           A20: (c * (i lcm j)) = ((g * (h * f)) * f) by A5, A15, A16

          .= (((i lcm j) * z) * f) by A19

          .= ((z * f) * (i lcm j));

          (i lcm j) <> 0 by A2, A3, INT_2: 4;

          then c = (f * z) by A20, XCMPLX_1: 5;

          hence thesis;

        end;

        hence thesis by A5, A11, A12, Def5;

      end;

      i = 0 or j = 0 implies (i * j) = ((i lcm j) * (i gcd j))

      proof

        assume

         A21: i = 0 or j = 0 ;

        

        then (i * j) = ( 0 * (i gcd j))

        .= ((i lcm j) * (i gcd j)) by A21, INT_2: 4;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: NAT_D:30

    for i,j be Integer st i >= 0 & j > 0 holds (i gcd j) = (j gcd (i mod j))

    proof

      let i,j be Integer;

      assume that

       A1: i >= 0 and

       A2: j > 0 ;

      

       A3: |.j.| > 0 by A2, ABSVALUE:def 1;

      

      thus (i gcd j) = ( |.i.| gcd |.j.|) by INT_2: 34

      .= ( |.j.| gcd ( |.i.| mod |.j.|)) by A3, Th28

      .= ( |.j.| gcd |.( |.i.| mod |.j.|).|) by ABSVALUE:def 1

      .= (j gcd ( |.i.| mod |.j.|)) by INT_2: 34

      .= (j gcd (i mod j)) by A1, A2, INT_2: 32;

    end;

    theorem :: NAT_D:31

    (i lcm i) = i

    proof

      

       A0: i is Nat by TARSKI: 1;

      for m be Nat st i divides m & i divides m holds i divides m;

      hence thesis by A0, Def4;

    end;

    theorem :: NAT_D:32

    (i gcd i) = i

    proof

      

       A0: i is Nat by TARSKI: 1;

      for m be Nat st m divides i & m divides i holds m divides i;

      hence thesis by A0, Def5;

    end;

    theorem :: NAT_D:33

    i < j & i <> 0 implies not (i / j) is integer

    proof

      assume that

       A1: i < j and

       A2: i <> 0 ;

      assume (i / j) is integer;

      then

      reconsider r = (i / j) as Integer;

      r = [\r/] by INT_1: 25

      .= (i qua Integer div j) by INT_1:def 9;

      hence thesis by A1, A2, Th27, XCMPLX_1: 50;

    end;

    definition

      let i,j be Nat;

      :: original: -'

      redefine

      func i -' j -> Element of NAT ;

      coherence

      proof

        (i -' j) = (i - j) & 0 <= (i -' j) or (i -' j) = 0 by XREAL_0:def 2;

        hence thesis by INT_1: 3;

      end;

    end

    theorem :: NAT_D:34

    

     Th34: ((i + j) -' j) = i

    proof

      ((i + j) - j) >= 0 ;

      hence thesis by XREAL_0:def 2;

    end;

    theorem :: NAT_D:35

    

     Th35: (a -' b) <= a

    proof

      (a - b) <= (a - 0 ) by XREAL_1: 230;

      hence thesis by XREAL_0:def 2;

    end;

    theorem :: NAT_D:36

    

     Th36: (n -' i) = 0 implies n <= i

    proof

      assume

       A1: (n -' i) = 0 ;

      assume i < n;

      then (i + 1) <= n by NAT_1: 13;

      then ((i + 1) - i) <= (n - i) by XREAL_1: 9;

      hence contradiction by A1, XREAL_0:def 2;

    end;

    theorem :: NAT_D:37

    i <= j implies ((j + k) -' i) = ((j + k) - i) by NAT_1: 12, XREAL_1: 233;

    theorem :: NAT_D:38

    i <= j implies ((j + k) -' i) = ((j -' i) + k)

    proof

      assume

       A1: i <= j;

      

      hence ((j + k) -' i) = ((j + k) - i) by NAT_1: 12, XREAL_1: 233

      .= ((j - i) + k)

      .= ((j -' i) + k) by A1, XREAL_1: 233;

    end;

    theorem :: NAT_D:39

    

     Th39: (i -' i1) >= 1 or (i - i1) >= 1 implies (i -' i1) = (i - i1)

    proof

      assume

       A1: (i -' i1) >= 1 or (i - i1) >= 1;

      per cases by A1;

        suppose (i -' i1) >= 1;

        hence thesis by XREAL_0:def 2;

      end;

        suppose (i - i1) >= 1;

        hence thesis by XREAL_0:def 2;

      end;

    end;

    theorem :: NAT_D:40

    (n -' 0 ) = n

    proof

      (n -' 0 ) = (n - 0 ) by XREAL_0:def 2

      .= n;

      hence thesis;

    end;

    theorem :: NAT_D:41

    i1 <= i2 implies (n -' i2) <= (n -' i1)

    proof

      assume

       A1: i1 <= i2;

      per cases ;

        suppose

         A2: i2 <= n;

        then

         A3: (n -' i1) = (n - i1) by A1, XREAL_1: 233, XXREAL_0: 2;

        (n -' i2) = (n - i2) by A2, XREAL_1: 233;

        hence thesis by A1, A3, XREAL_1: 10;

      end;

        suppose i2 > n;

        then (n - i2) < 0 by XREAL_1: 49;

        hence thesis by XREAL_0:def 2;

      end;

    end;

    theorem :: NAT_D:42

    

     Th42: i1 <= i2 implies (i1 -' n) <= (i2 -' n)

    proof

      assume

       A1: i1 <= i2;

      per cases ;

        suppose (i1 - n) >= 0 ;

        then

         A2: (i1 -' n) = (i1 - n) by XREAL_0:def 2;

        (i1 - n) <= (i2 - n) by A1, XREAL_1: 9;

        hence thesis by A2, XREAL_0:def 2;

      end;

        suppose (i1 - n) < 0 ;

        hence thesis by XREAL_0:def 2;

      end;

    end;

    theorem :: NAT_D:43

    

     Th43: (i -' i1) >= 1 or (i - i1) >= 1 implies ((i -' i1) + i1) = i

    proof

      assume (i -' i1) >= 1 or (i - i1) >= 1;

      

      then ((i -' i1) + i1) = ((i - i1) + i1) by Th39

      .= i;

      hence thesis;

    end;

    theorem :: NAT_D:44

    i1 <= i2 implies (i1 -' 1) <= i2

    proof

      assume

       A1: i1 <= i2;

      reconsider i1, i2 as Nat by TARSKI: 1;

      per cases ;

        suppose (i1 - 1) >= 0 ;

        then (i1 -' 1) = (i1 - 1) by XREAL_0:def 2;

        then (i1 -' 1) <= ((i1 - 1) + 1) by NAT_1: 12;

        hence thesis by A1, XXREAL_0: 2;

      end;

        suppose (i1 - 1) < 0 ;

        hence thesis by XREAL_0:def 2;

      end;

    end;

    theorem :: NAT_D:45

    

     Th45: (i -' 2) = ((i -' 1) -' 1)

    proof

      per cases ;

        suppose

         A1: i >= 2;

        then 1 <= i by XXREAL_0: 2;

        then (i - 1) >= 0 by XREAL_1: 48;

        then

         A2: (i -' 1) = (i - 1) by XREAL_0:def 2;

        (i - 1) >= ((1 + 1) - 1) by A1, XREAL_1: 9;

        then ((i - 1) - 1) >= (1 - 1) by XREAL_1: 9;

        then ((i -' 1) -' 1) = (i - 2) by A2, XREAL_0:def 2;

        hence thesis by XREAL_0:def 2;

      end;

        suppose

         A3: i < 2;

        then (i - 2) < (2 - 2) by XREAL_1: 9;

        then

         A4: (i -' 2) = 0 by XREAL_0:def 2;

        

         A5: ((i + 1) - 1) <= ((1 + 1) - 1) by A3, NAT_1: 13;

        now

          per cases ;

            case 1 <= i;

            then i = 1 by A5, XXREAL_0: 1;

            then ((i -' 1) -' 1) = ( 0 -' 1) by XREAL_1: 232;

            hence thesis by A4, Th35;

          end;

            case i < 1;

            then (i - 1) < (1 - 1) by XREAL_1: 9;

            then ((i -' 1) -' 1) = ( 0 -' 1) by XREAL_0:def 2;

            hence thesis by A4, Th35;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: NAT_D:46

    

     Th46: (i1 + 1) <= i2 implies (i1 -' 1) < i2 & (i1 -' 2) < i2 & i1 <= i2

    proof

      assume

       A1: (i1 + 1) <= i2;

      then

       A2: i1 < i2 by NAT_1: 13;

      (i1 -' 1) <= i1 by Th35;

      hence

       A3: (i1 -' 1) < i2 by A2, XXREAL_0: 2;

      

       A4: ((i1 -' 1) -' 1) = (i1 -' 2) by Th45;

      reconsider i1 as Nat by TARSKI: 1;

      ((i1 -' 1) -' 1) <= (i1 -' 1) by Th35;

      hence thesis by A1, A3, A4, XXREAL_0: 2, NAT_1: 13;

    end;

    theorem :: NAT_D:47

    (i1 + 2) <= i2 or ((i1 + 1) + 1) <= i2 implies (i1 + 1) < i2 & ((i1 + 1) -' 1) < i2 & ((i1 + 1) -' 2) < i2 & (i1 + 1) <= i2 & ((i1 -' 1) + 1) < i2 & (((i1 -' 1) + 1) -' 1) < i2 & i1 < i2 & (i1 -' 1) < i2 & (i1 -' 2) < i2 & i1 <= i2

    proof

      assume (i1 + 2) <= i2 or ((i1 + 1) + 1) <= i2;

      then ((i1 + 1) + 1) <= i2;

      hence

       A1: (i1 + 1) < i2 & ((i1 + 1) -' 1) < i2 & ((i1 + 1) -' 2) < i2 & (i1 + 1) <= i2 by Th46, NAT_1: 13;

      (i1 -' 1) <= i1 by Th35;

      then ((i1 -' 1) + 1) <= (i1 + 1) by XREAL_1: 6;

      then

       A2: ((i1 -' 1) + 1) < i2 by A1, XXREAL_0: 2;

      reconsider i1 as Nat by TARSKI: 1;

      (((i1 -' 1) + 1) -' 1) <= ((i1 -' 1) + 1) by Th35;

      hence thesis by A1, Th46, A2, XXREAL_0: 2, NAT_1: 13;

    end;

    theorem :: NAT_D:48

    i1 <= i2 or i1 <= (i2 -' 1) implies i1 < (i2 + 1) & i1 <= (i2 + 1) & i1 < ((i2 + 1) + 1) & i1 <= ((i2 + 1) + 1) & i1 < (i2 + 2) & i1 <= (i2 + 2)

    proof

      assume

       A1: i1 <= i2 or i1 <= (i2 -' 1);

       A2:

      now

        assume i1 <= i2;

        then

         A3: i1 < (i2 + 1) by NAT_1: 13;

        ((i2 + 1) + 1) = (i2 + (1 + 1));

        hence thesis by A3, NAT_1: 13;

      end;

      now

        assume

         A4: i1 <= (i2 -' 1);

        (i2 -' 1) <= i2 by Th35;

        hence thesis by A2, A4, XXREAL_0: 2;

      end;

      hence thesis by A1, A2;

    end;

    theorem :: NAT_D:49

    i1 < i2 or (i1 + 1) <= i2 implies i1 <= (i2 -' 1)

    proof

      assume

       A1: i1 < i2 or (i1 + 1) <= i2;

      per cases by A1;

        suppose

         A2: i1 < i2;

        then (i1 + 1) <= i2 by NAT_1: 13;

        then

         A3: ((i1 + 1) - 1) <= (i2 - 1) by XREAL_1: 9;

        ( 0 + 1) <= i2 by A2, NAT_1: 13;

        hence thesis by A3, XREAL_1: 233;

      end;

        suppose

         A4: (i1 + 1) <= i2;

        then

         A5: ((i1 + 1) - 1) <= (i2 - 1) by XREAL_1: 9;

        ( 0 + 1) <= i2 by A4, NAT_1: 13;

        hence thesis by A5, XREAL_1: 233;

      end;

    end;

    theorem :: NAT_D:50

    

     Th50: i >= i1 implies i >= (i1 -' i2)

    proof

      assume

       A1: i >= i1;

      i1 >= (i1 -' i2) by Th35;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: NAT_D:51

    1 <= i & 1 <= (i1 -' i) implies (i1 -' i) < i1

    proof

      assume that

       A1: 1 <= i and

       A2: 1 <= (i1 -' i);

      (i1 - i) = (((i1 -' i) + i) - i) by A2, Th43

      .= (i1 -' i);

      hence thesis by A1, XREAL_1: 231;

    end;

    theorem :: NAT_D:52

    

     Th52: (i -' k) <= j implies i <= (j + k)

    proof

      assume

       A1: (i -' k) <= j;

      per cases ;

        suppose

         A2: i >= k;

        ((i -' k) + k) <= (j + k) by A1, XREAL_1: 6;

        hence thesis by A2, XREAL_1: 235;

      end;

        suppose

         A3: i <= k;

        k <= (j + k) by NAT_1: 11;

        hence thesis by A3, XXREAL_0: 2;

      end;

    end;

    theorem :: NAT_D:53

    i <= (j + k) implies (i -' k) <= j

    proof

      assume i <= (j + k);

      then (i -' k) <= ((j + k) -' k) by Th42;

      hence thesis by Th34;

    end;

    theorem :: NAT_D:54

    i <= (j -' k) & k <= j implies (i + k) <= j

    proof

      assume that

       A1: i <= (j -' k) and

       A2: j >= k;

      (i + k) <= ((j -' k) + k) by A1, XREAL_1: 6;

      hence thesis by A2, XREAL_1: 235;

    end;

    theorem :: NAT_D:55

    (j + k) <= i implies k <= (i -' j)

    proof

      assume

       A1: (j + k) <= i;

      per cases by A1, XXREAL_0: 1;

        suppose (j + k) = i;

        hence thesis by Th34;

      end;

        suppose (j + k) < i;

        hence thesis by Th52;

      end;

    end;

    theorem :: NAT_D:56

    k <= i & i < j implies (i -' k) < (j -' k)

    proof

      assume that

       A1: k <= i and

       A2: i < j;

      ((i -' k) + k) = i by A1, XREAL_1: 235;

      then ((i -' k) + k) < ((j -' k) + k) by A1, A2, XREAL_1: 235, XXREAL_0: 2;

      hence thesis by XREAL_1: 6;

    end;

    theorem :: NAT_D:57

    i < j & k < j implies (i -' k) < (j -' k)

    proof

      assume that

       A1: i < j and

       A2: k < j;

      per cases ;

        suppose k <= i;

        then

         A3: (i -' k) = (i - k) by XREAL_1: 233;

        (j -' k) = (j - k) by A2, XREAL_1: 233;

        hence thesis by A1, A3, XREAL_1: 9;

      end;

        suppose k > i;

        then (i - k) < 0 by XREAL_1: 49;

        then

         A4: (i -' k) = 0 by XREAL_0:def 2;

        (j -' k) <> 0 by A2, Th36;

        hence thesis by A4;

      end;

    end;

    theorem :: NAT_D:58

    i <= j implies (j -' (j -' i)) = i

    proof

      assume

       A1: i <= j;

      ((j -' (j -' i)) + (j -' i)) = j by Th50, XREAL_1: 235

      .= (i + (j -' i)) by A1, XREAL_1: 235;

      hence thesis;

    end;

    theorem :: NAT_D:59

    n < k implies ((k -' (n + 1)) + 1) = (k -' n)

    proof

      assume

       A1: n < k;

      

       A2: (k -' n) = (k - n) by A1, XREAL_1: 233;

      (n + 1) <= k by A1, NAT_1: 13;

      then (k -' (n + 1)) = (k - (n + 1)) by XREAL_1: 233;

      hence thesis by A2;

    end;

    theorem :: NAT_D:60

    for A be finite set holds A is trivial iff ( card A) < 2

    proof

      let A be finite set;

      hereby

        assume

         A1: A is trivial;

        per cases ;

          suppose A is empty;

          hence ( card A) < 2;

        end;

          suppose A is non empty;

          then ex x be object st A = {x} by A1, ZFMISC_1: 131;

          then ( card A) = 1 by CARD_1: 30;

          hence ( card A) < 2;

        end;

      end;

      assume

       A2: ( card A) < 2;

      per cases by A2, NAT_1: 23;

        suppose ( card A) = 0 ;

        hence thesis;

      end;

        suppose ( card A) = 1;

        then A is 1 -element by CARD_1:def 7;

        hence thesis;

      end;

    end;

    theorem :: NAT_D:61

    

     Th61: for n,a,k be Integer holds (n <> 0 implies ((a + (n * k)) div n) = ((a div n) + k)) & ((a + (n * k)) mod n) = (a mod n)

    proof

      let n,a,k be Integer;

      now

        assume

         A2: n <> 0 ;

        

        thus ((a + (n * k)) div n) = [\((a + (n * k)) / n)/] by INT_1:def 9

        .= [\((a + (n * k)) * (n " ))/] by XCMPLX_0:def 9

        .= [\((a * (n " )) + ((n * (n " )) * k))/]

        .= [\((a * (n " )) + (1 * k))/] by A2, XCMPLX_0:def 7

        .= ( [\(a * (n " ))/] + k) by INT_1: 28

        .= ( [\(a / n)/] + k) by XCMPLX_0:def 9

        .= ((a div n) + k) by INT_1:def 9;

      end;

      per cases ;

        suppose

         A3: n <> 0 ;

        

        hence ((a + (n * k)) mod n) = ((a + (n * k)) - (((a div n) + k) * n)) by A1, INT_1:def 10

        .= (a - ((a div n) * n))

        .= (a mod n) by A3, INT_1:def 10;

      end;

        suppose n = 0 ;

        hence thesis;

      end;

    end;

    theorem :: NAT_D:62

    

     Th62: for n be natural Number st n > 0 holds for a be Integer holds (a mod n) >= 0 & (a mod n) < n

    proof

      let n be natural Number;

      assume

       A1: n > 0 ;

      let a be Integer;

      now

        (a div n) = [\(a / n)/] by INT_1:def 9;

        then (a div n) <= (a / n) by INT_1:def 6;

        then ((a div n) * n) <= ((a / n) * n) by XREAL_1: 64;

        then ((a div n) * n) <= ((a * (n " )) * n) by XCMPLX_0:def 9;

        then ((a div n) * n) <= (a * ((n " ) * n));

        then ((a div n) * n) <= (a * 1) by A1, XCMPLX_0:def 7;

        then (((a div n) * n) - ((a div n) * n)) <= (a - ((a div n) * n)) by XREAL_1: 9;

        hence 0 <= (a mod n) by INT_1:def 10;

        assume (a mod n) >= n;

        then (a - ((a div n) * n)) >= n by A1, INT_1:def 10;

        then ((a + ( - ((a div n) * n))) + ((a div n) * n)) >= (n + ((a div n) * n)) by XREAL_1: 6;

        then (a - n) >= ((n + ((a div n) * n)) - n) by XREAL_1: 9;

        then ((a - n) * (n " )) >= (((a div n) * n) * (n " )) by XREAL_1: 64;

        then ((a - n) * (n " )) >= ((a div n) * (n * (n " )));

        then ((a * (n " )) - (n * (n " ))) >= ((a div n) * 1) by A1, XCMPLX_0:def 7;

        then ((a * (n " )) - 1) >= (a div n) by A1, XCMPLX_0:def 7;

        then

         A2: ((a / n) - 1) >= (a div n) by XCMPLX_0:def 9;

        (a div n) = [\(a / n)/] by INT_1:def 9;

        hence contradiction by A2, INT_1:def 6;

      end;

      hence thesis;

    end;

    theorem :: NAT_D:63

    

     Th63: for n,a be Integer holds ( 0 <= a & a < n implies (a mod n) = a) & ( 0 > a & a >= ( - n) implies (a mod n) = (n + a))

    proof

      let n,a be Integer;

      per cases ;

        suppose n = 0 ;

        hence thesis;

      end;

        suppose

         A1: n <> 0 ;

        hereby

          assume that

           A2: 0 <= a and

           A3: a < n;

          reconsider aa = a as Element of NAT by A2, INT_1: 3;

          reconsider nn = n as Element of NAT by A2, A3, INT_1: 3;

          consider t be Nat such that

           A4: aa = ((nn * t) + (aa mod nn)) and (aa mod nn) < nn by A1, Def2;

          t = 0

          proof

            assume t <> 0 ;

            then t >= (1 + 0 ) by INT_1: 7;

            then

             A5: (t * n) >= (1 * n) by A2, A3, XREAL_1: 64;

            ((nn * t) + (aa mod nn)) >= (nn * t) by NAT_1: 11;

            hence thesis by A3, A4, A5, XXREAL_0: 2;

          end;

          hence (a mod n) = a by A4;

        end;

        assume that

         A6: 0 > a and

         A7: a >= ( - n);

        

         A8: n >= 0 by A6, A7;

        

         A9: ((a / n) - 1) < ( - 1)

        proof

          assume ((a / n) - 1) >= ( - 1);

          then (((a / n) - 1) + 1) >= (( - 1) + 1) by XREAL_1: 6;

          then (a * (n " )) >= 0 by XCMPLX_0:def 9;

          then ((a * (n " )) * n) >= ( 0 * n) by A8;

          then (a * ((n " ) * n)) >= 0 ;

          then (a * 1) >= 0 by A1, XCMPLX_0:def 7;

          hence thesis by A6;

        end;

        (a * (n " )) >= (( - n) * (n " )) by A7, A8, XREAL_1: 64;

        then (a / n) >= ( - (n * (n " ))) by XCMPLX_0:def 9;

        then ( - 1) <= (a / n) by A1, XCMPLX_0:def 7;

        then [\(a / n)/] = ( - 1) by A9, INT_1:def 6;

        then

         A10: (a div n) = ( - 1) by INT_1:def 9;

        (a mod n) = (a - ((a div n) * n)) by A1, INT_1:def 10;

        hence thesis by A10;

      end;

    end;

    theorem :: NAT_D:64

    

     Th64: for n,a,b be Integer holds (n <> 0 & (a mod n) = (b mod n) implies (a,b) are_congruent_mod n) & ((a,b) are_congruent_mod n implies (a mod n) = (b mod n))

    proof

      let n,a,b be Integer;

      hereby

        assume

         A1: n <> 0 ;

        assume (a mod n) = (b mod n);

        then (a - ((a div n) * n)) = (b mod n) by A1, INT_1:def 10;

        then (a - ((a div n) * n)) = (b - ((b div n) * n)) by A1, INT_1:def 10;

        then (a - b) = ((( - (b div n)) + (a div n)) * n);

        then n divides (a - b) by INT_1:def 3;

        hence (a,b) are_congruent_mod n by INT_2: 15;

      end;

      assume (a,b) are_congruent_mod n;

      then n divides (a - b) by INT_2: 15;

      then

      consider k be Integer such that

       A2: (n * k) = (a - b) by INT_1:def 3;

      a = ((n * k) + b) by A2;

      hence thesis by Th61;

    end;

    theorem :: NAT_D:65

    for n be natural Number, a be Integer holds ((a mod n) mod n) = (a mod n)

    proof

      let n be natural Number;

      let a be Integer;

      per cases ;

        suppose

         A1: n = 0 ;

        

        hence ((a mod n) mod n) = 0 by INT_1:def 10

        .= (a mod n) by A1, INT_1:def 10;

      end;

        suppose n <> 0 ;

        then (a mod n) >= 0 & (a mod n) < n by Th62;

        hence thesis by Th63;

      end;

    end;

    theorem :: NAT_D:66

    for n,a,b be Integer holds ((a + b) mod n) = (((a mod n) + (b mod n)) mod n)

    proof

      let n,a,b be Integer;

      per cases ;

        suppose

         A1: n = 0 ;

        

        hence ((a + b) mod n) = 0 by INT_1:def 10

        .= (((a mod n) + (b mod n)) mod n) by A1, INT_1:def 10;

      end;

        suppose n <> 0 ;

        then ((a mod n) + ((a div n) * n)) = ((a - ((a div n) * n)) + ((a div n) * n)) & ((b mod n) + ((b div n) * n)) = ((b - ((b div n) * n)) + ((b div n) * n)) by INT_1:def 10;

        then ((a + b) - ((a mod n) + (b mod n))) = (((a div n) + (b div n)) * n);

        then n divides ((a + b) - ((a mod n) + (b mod n))) by INT_1:def 3;

        then ((a + b),((a mod n) + (b mod n))) are_congruent_mod n by INT_2: 15;

        hence thesis by Th64;

      end;

    end;

    theorem :: NAT_D:67

    

     Th67: for n,a,b be Integer holds ((a * b) mod n) = (((a mod n) * (b mod n)) mod n)

    proof

      let n,a,b be Integer;

      per cases ;

        suppose

         A1: n = 0 ;

        

        hence ((a * b) mod n) = 0 by INT_1:def 10

        .= (((a mod n) * (b mod n)) mod n) by A1, INT_1:def 10;

      end;

        suppose n <> 0 ;

        then ((a mod n) + ((a div n) * n)) = ((a - ((a div n) * n)) + ((a div n) * n)) & ((b mod n) + ((b div n) * n)) = ((b - ((b div n) * n)) + ((b div n) * n)) by INT_1:def 10;

        then ((a * b) - ((a mod n) * (b mod n))) = ((((a mod n) * (b div n)) + (((a div n) * (b mod n)) + (((a div n) * n) * (b div n)))) * n);

        then n divides ((a * b) - ((a mod n) * (b mod n))) by INT_1:def 3;

        then ((a * b),((a mod n) * (b mod n))) are_congruent_mod n by INT_2: 15;

        hence thesis by Th64;

      end;

    end;

    ::$Notion-Name

    ::$Notion-Name

    theorem :: NAT_D:68

    for a,b be Integer holds ex s,t be Integer st (a gcd b) = ((s * a) + (t * b))

    proof

      let a,b be Integer;

      

       A1: for a,b be Integer st a > 0 & b > 0 holds ex s,t be Integer st (a gcd b) = ((s * a) + (t * b))

      proof

        let a,b be Integer;

        assume that

         A2: a > 0 and

         A3: b > 0 ;

        reconsider a, b as Element of NAT by A2, A3, INT_1: 3;

        set M = { z where z be Element of NAT : ex s,t be Integer st z = ((s * a) + (t * b)) };

        defpred P[ Nat] means ($1 in M & $1 <> 0 );

        a = ((1 * a) + ( 0 * b));

        then

         A4: a in M;

        then

         A5: ex k be Nat st P[k] by A2;

        consider g be Nat such that

         A6: P[g] & for n be Nat st P[n] holds g <= n from NAT_1:sch 5( A5);

        set G = { zz where zz be Element of NAT : ex s be Element of NAT st zz = (s * g) };

        ex z be Element of NAT st z = g & ex s,t be Integer st z = ((s * a) + (t * b)) by A6;

        then

        consider s,t be Integer such that

         A7: g = ((s * a) + (t * b));

        

         A8: for x be object holds x in M implies x in G

        proof

          let x be object;

          assume x in M;

          then

          consider x9 be Element of NAT such that

           A9: x9 = x and

           A10: ex u,v be Integer st x9 = ((u * a) + (v * b));

          consider u,v be Integer such that

           A11: x = ((u * a) + (v * b)) by A9, A10;

          consider r be Nat such that

           A12: x9 = ((g * (x9 div g)) + r) and

           A13: r < g by A6, Def1;

          

           A14: r in NAT by ORDINAL1:def 12;

          r = (x9 - (g * (x9 div g))) by A12

          .= ((a * (u + ( - (s * (x9 div g))))) + (b * (v + ( - (t * (x9 div g)))))) by A7, A9, A11;

          then r in M by A14;

          then r = 0 by A6, A13;

          hence thesis by A9, A12;

        end;

        for x be object holds x in G implies x in M

        proof

          let x be object;

          assume x in G;

          then

           A15: ex x9 be Element of NAT st x9 = x & ex u be Element of NAT st x9 = (u * g);

          then

          consider u be Integer such that

           A16: x = (u * g);

          x = (((u * s) * a) + ((u * t) * b)) by A7, A16;

          hence thesis by A15;

        end;

        then

         A17: G = M by A8, TARSKI: 2;

        

         A18: |.b.| = b by ABSVALUE:def 1;

        

         A19: |.a.| = a by ABSVALUE:def 1;

        

         A20: for m be Nat st m divides |.a.| & m divides |.b.| holds m divides g

        proof

          ex g9 be Element of NAT st g9 = g & ex s,t be Integer st g9 = ((s * a) + (t * b)) by A6;

          then

          consider s,t be Integer such that

           A21: g = ((s * a) + (t * b));

          let m be Nat;

          assume that

           A22: m divides |.a.| and

           A23: m divides |.b.|;

          consider u be Nat such that

           A24: a = (m * u) by A19, A22;

          consider v be Nat such that

           A25: b = (m * v) by A18, A23;

          

           A26: g = (m * ((s * u) + (t * v))) by A24, A25, A21;

          then ((s * u) + (t * v)) >= 0 by A6;

          then ((s * u) + (t * v)) is Element of NAT by INT_1: 3;

          hence thesis by A26;

        end;

        b = (( 0 * a) + (1 * b));

        then b in M;

        then ex b9 be Element of NAT st b9 = b & ex t be Element of NAT st b9 = (t * g) by A17;

        then

         A27: g divides |.b.| by A18;

        ex a9 be Element of NAT st a9 = a & ex s be Element of NAT st a9 = (s * g) by A4, A17;

        then g divides |.a.| by A19;

        

        then g = ( |.a.| gcd |.b.|) by A27, A20, Def5

        .= (a gcd b) by INT_2: 34;

        hence thesis by A7;

      end;

      now

        per cases ;

          case

           A28: a = 0 or b = 0 ;

          

           A29: for a,b be Integer holds a = 0 implies (a gcd b) = |.b.|

          proof

            let a,b be Integer;

            assume a = 0 ;

            then |.a.| = 0 by ABSVALUE:def 1;

            then

             A30: |.b.| divides |.a.| by Th6;

            (a gcd b) = ( |.a.| gcd |.b.|) & for m be Nat st m divides |.a.| & m divides |.b.| holds m divides |.b.| by INT_2: 34;

            hence thesis by A30, Def5;

          end;

          now

            per cases by A28;

              case a = 0 ;

              then

               A31: (a gcd b) = |.b.| by A29;

              now

                per cases ;

                  case b >= 0 ;

                  hence (a gcd b) = (( 0 * a) + (1 * b)) by A31, ABSVALUE:def 1;

                end;

                  case b < 0 ;

                  

                  hence (a gcd b) = ( - (b * 1)) by A31, ABSVALUE:def 1

                  .= (( 0 * a) + (( - 1) * b));

                end;

              end;

              hence thesis;

            end;

              case b = 0 ;

              then

               A32: (a gcd b) = |.a.| by A29;

              now

                per cases ;

                  case a >= 0 ;

                  hence (a gcd b) = ((1 * a) + ( 0 * b)) by A32, ABSVALUE:def 1;

                end;

                  case a < 0 ;

                  

                  hence (a gcd b) = ( - (a * 1)) by A32, ABSVALUE:def 1

                  .= (( 0 * b) + (( - 1) * a));

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

          case

           A33: a <> 0 & b <> 0 ;

          now

            per cases ;

              case a >= 0 & b >= 0 ;

              hence thesis by A1, A33;

            end;

              case

               A34: a < 0 & b >= 0 ;

              then ( - a) > 0 by XREAL_1: 58;

              then

              consider s,t be Integer such that

               A35: (( - a) gcd b) = ((s * ( - a)) + (t * b)) by A1, A33, A34;

              

               A36: (a gcd b) = ( |.a.| gcd |.b.|) by INT_2: 34

              .= ( |.( - a).| gcd |.b.|) by COMPLEX1: 52

              .= (( - a) gcd b) by INT_2: 34;

              ((s * ( - a)) + (t * b)) = ((( - s) * a) + (t * b));

              hence thesis by A35, A36;

            end;

              case

               A37: a >= 0 & b < 0 ;

              then ( - b) > 0 by XREAL_1: 58;

              then

              consider s,t be Integer such that

               A38: (a gcd ( - b)) = ((s * a) + (t * ( - b))) by A1, A33, A37;

              

               A39: (a gcd b) = ( |.a.| gcd |.b.|) by INT_2: 34

              .= ( |.a.| gcd |.( - b).|) by COMPLEX1: 52

              .= (a gcd ( - b)) by INT_2: 34;

              ((s * a) + (t * ( - b))) = ((s * a) + (( - t) * b));

              hence thesis by A38, A39;

            end;

              case a < 0 & b < 0 ;

              then ( - a) > 0 & ( - b) > 0 by XREAL_1: 58;

              then

              consider s,t be Integer such that

               A40: (( - a) gcd ( - b)) = ((s * ( - a)) + (t * ( - b))) by A1;

              

               A41: (a gcd b) = ( |.a.| gcd |.b.|) by INT_2: 34

              .= ( |.a.| gcd |.( - b).|) by COMPLEX1: 52

              .= ( |.( - a).| gcd |.( - b).|) by COMPLEX1: 52

              .= (( - a) gcd ( - b)) by INT_2: 34;

              ((s * ( - a)) + (t * ( - b))) = ((( - s) * a) + (( - t) * b));

              hence thesis by A40, A41;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: NAT_D:69

    (n mod k) = (k - 1) implies ((n + 1) mod k) = 0

    proof

      per cases ;

        suppose k <> 0 ;

        then k >= 1 by NAT_1: 14;

        then

        reconsider K = (k - 1) as Element of NAT by INT_1: 3, XREAL_1: 48;

        

         A1: (K + 1) = (k - 0 );

        assume (n mod k) = (k - 1);

        then ((n + 1) mod k) = (k mod k) by A1, Th22;

        hence thesis by Th25;

      end;

        suppose k = 0 ;

        hence thesis;

      end;

    end;

    theorem :: NAT_D:70

    (n mod k) < (k - 1) implies ((n + 1) mod k) = ((n mod k) + 1)

    proof

      assume (n mod k) < (k - 1);

      then

       A1: ((n mod k) + 1) < k by XREAL_1: 20;

      ((n + 1) mod k) = (((n mod k) + 1) mod k) by Th22;

      hence thesis by A1, Th24;

    end;

    theorem :: NAT_D:71

    for i be Integer, n be Nat holds ((i * n) mod n) = 0

    proof

      let i be Integer, n be Nat;

      ((i * n) mod n) = (((i mod n) * (n mod n)) mod n) by Th67

      .= (((i mod n) * 0 ) mod n) by Th25

      .= ( 0 mod n);

      hence thesis by Th26;

    end;

    theorem :: NAT_D:72

    (m - n) >= 0 implies ((m -' n) + n) = m

    proof

      assume (m - n) >= 0 ;

      then (m -' n) = (m - n) by XREAL_0:def 2;

      hence thesis;

    end;