int_2.miz



    begin

    definition

      let a be Integer;

      :: original: |.

      redefine

      func |.a.| -> Element of NAT ;

      coherence

      proof

        per cases ;

          suppose

           A1: a >= 0 ;

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

          hence thesis by A1, INT_1: 3;

        end;

          suppose a < 0 ;

          then |.a.| = ( - a) & ( - a) > 0 by ABSVALUE:def 1, XREAL_1: 58;

          hence thesis by INT_1: 3;

        end;

      end;

    end

    reserve a,b,c for Integer;

    theorem :: INT_2:1

    

     Th1: a divides b & a divides (b + c) implies a divides c

    proof

      given u be Integer such that

       A1: b = (a * u);

      given t be Integer such that

       A2: (b + c) = (a * t);

      c = (a * (t - u)) by A1, A2;

      hence thesis;

    end;

    theorem :: INT_2:2

    

     Th2: a divides b implies a divides (b * c)

    proof

      assume a divides b;

      then

      consider l be Integer such that

       A1: b = (a * l);

      ((a * l) * c) = (a * (l * c));

      hence thesis by A1;

    end;

    theorem :: INT_2:3

     0 divides a iff a = 0 ;

    

     Lm1: a divides ( - a) & ( - a) divides a

    proof

      ( - a) = (a * ( - 1));

      hence a divides ( - a);

      a = (( - a) * ( - 1));

      hence thesis;

    end;

    

     Lm2: a divides b & b divides c implies a divides c

    proof

      assume that

       A1: a divides b and

       A2: b divides c;

      consider k be Integer such that

       A3: b = (a * k) by A1;

      consider l be Integer such that

       A4: c = (b * l) by A2;

      c = (a * (k * l)) by A3, A4;

      hence thesis;

    end;

    

     Lm3: a divides b iff a divides ( - b)

    proof

      thus a divides b implies a divides ( - b)

      proof

        assume

         A1: a divides b;

        b divides ( - b) by Lm1;

        hence thesis by A1, Lm2;

      end;

      assume

       A2: a divides ( - b);

      ( - b) divides b by Lm1;

      hence thesis by A2, Lm2;

    end;

    

     Lm4: a divides b iff ( - a) divides b

    proof

      thus a divides b implies ( - a) divides b

      proof

        assume

         A1: a divides b;

        ( - a) divides a by Lm1;

        hence thesis by A1, Lm2;

      end;

      assume

       A2: ( - a) divides b;

      a divides ( - a) by Lm1;

      hence thesis by A2, Lm2;

    end;

    

     Lm5: a divides 0 & 1 divides a & ( - 1) divides a

    proof

       0 = (a * 0 );

      hence a divides 0 ;

      a = (1 * a);

      hence 1 divides a;

      a = (( - 1) * ( - a));

      hence thesis;

    end;

    

     Lm6: a divides b & a divides c implies a divides (b mod c)

    proof

      assume that

       A1: a divides b and

       A2: a divides c;

       A3:

      now

        assume c <> 0 ;

        then

         A4: b = ((c * (b div c)) + (b mod c)) by INT_1: 59;

        a divides (c * (b div c)) by A2, Th2;

        hence thesis by A1, A4, Th1;

      end;

      now

        assume c = 0 ;

        then (b mod c) = 0 by INT_1:def 10;

        hence thesis by Lm5;

      end;

      hence thesis by A3;

    end;

    reserve i,j,k,l for Nat;

    

     Lm7: k divides l iff ex t be Nat st l = (k * t)

    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;

          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;

      assume ex t be Nat st l = (k * t);

      hence thesis;

    end;

    

     Lm8: i divides j & j divides i implies i = j

    proof

      assume i divides j;

      then

      consider a such that

       A1: j = (i * a);

      assume j divides i;

      then

      consider b such that

       A2: i = (j * b);

      i <> 0 implies i = j

      proof

        

         A3: i >= 0 ;

        assume

         A4: i <> 0 ;

        (1 * i) = (i * (a * b)) by A1, A2;

        then (a * b) = 1 by A4, XCMPLX_1: 5;

        then i = (j * 1) or i = (j * ( - 1)) by A2, INT_1: 9;

        hence thesis by A4, A3;

      end;

      hence thesis by A1;

    end;

    definition

      let a,b be Integer;

      :: INT_2:def1

      func a lcm b -> Nat means

      : Def1: a divides it & b divides it & for m be Integer st a divides m & b divides m holds it divides m;

      existence

      proof

        per cases ;

          suppose

           A1: a = 0 or b = 0 ;

          take 0 ;

          thus a divides 0 & b divides 0 by Lm5;

          thus thesis by A1;

        end;

          suppose

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

          defpred P[ Nat] means a divides $1 & b divides $1 & $1 <> 0 ;

          (a * b) in INT by INT_1:def 2;

          then

          consider k be Nat such that

           A3: (a * b) = k or (a * b) = ( - k) by INT_1:def 1;

          b divides (a * b);

          then

           A4: b divides k by A3, Lm3;

          a divides (a * b);

          then

           A5: a divides k by A3, Lm3;

          k <> 0 by A2, A3, XCMPLX_1: 6;

          then

           A6: ex k be Nat st P[k] by A5, A4;

          consider k be Nat such that

           A7: P[k] and

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

          take k;

          thus a divides k & b divides k by A7;

          let m be Integer;

          m in INT by INT_1:def 2;

          then

          consider n be Nat such that

           A9: m = n or m = ( - n) by INT_1:def 1;

          assume that

           A10: a divides m and

           A11: b divides m;

          b divides n by A9, A11, Lm3;

          then

           A12: b divides (n mod k) by A7, Lm6;

          

           A13: k > 0 by A7;

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

          then

          reconsider i = (n mod k) as Nat;

          assume

           A14: not k divides m;

           A15:

          now

            assume i = 0 ;

            then (n - ((n div k) * k)) = 0 by A7, INT_1:def 10;

            then k divides n;

            hence contradiction by A9, A14, Lm3;

          end;

          a divides n by A9, A10, Lm3;

          then a divides (n mod k) by A7, Lm6;

          then k divides n by A8, A13, A12, A15, INT_1: 58;

          hence contradiction by A9, A14, Lm3;

        end;

      end;

      uniqueness

      proof

        let IT1,IT2 be Nat;

        assume a divides IT1 & b divides IT1 & (for m be Integer st a divides m & b divides m holds IT1 divides m) & a divides IT2 & (b divides IT2 & for m be Integer st a divides m & b divides m holds IT2 divides m);

        then IT1 divides IT2 & IT2 divides IT1;

        hence thesis by Lm8;

      end;

      commutativity ;

    end

    theorem :: INT_2:4

    

     Th4: a = 0 or b = 0 iff (a lcm b) = 0

    proof

      

       A1: b = 0 implies (a lcm b) = 0

      proof

        assume b = 0 ;

        then 0 divides (a lcm b) by Def1;

        hence thesis;

      end;

      

       A2: (a lcm b) = 0 implies a = 0 or b = 0

      proof

        

         A3: b divides b implies b divides (b * a);

        assume

         A4: (a lcm b) = 0 ;

        a divides a implies a divides (a * b);

        then 0 divides (a * b) by A4, A3, Def1;

        then (a * b) = 0 ;

        hence thesis by XCMPLX_1: 6;

      end;

      a = 0 implies (a lcm b) = 0

      proof

        assume a = 0 ;

        then 0 divides (a lcm b) by Def1;

        hence thesis;

      end;

      hence thesis by A1, A2;

    end;

    

     Lm9: 0 < j & i divides j implies i <= j

    proof

      assume that

       A1: 0 < j and

       A2: i divides j;

      consider l such that

       A3: j = (i * l) by A2, Lm7;

      l <> 0 by A1, A3;

      then

      consider k such that

       A4: l = (k + 1) by NAT_1: 6;

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

      hence thesis by A3, A4, NAT_1: 11;

    end;

    definition

      let a,b be Integer;

      :: INT_2:def2

      func a gcd b -> Nat means

      : Def2: it divides a & it divides b & for m be Integer st m divides a & m divides b holds m divides it ;

      existence

      proof

        per cases ;

          suppose

           A1: a = 0 ;

          b in INT by INT_1:def 2;

          then

          consider k be Nat such that

           A2: b = k or b = ( - k) by INT_1:def 1;

          take k;

          thus k divides a & k divides b by A1, A2, Lm4, Lm5;

          let m be Integer;

          assume that m divides a and

           A3: m divides b;

          thus thesis by A2, A3, Lm3;

        end;

          suppose

           A4: b = 0 ;

          a in INT by INT_1:def 2;

          then

          consider k be Nat such that

           A5: a = k or a = ( - k) by INT_1:def 1;

          take k;

          thus k divides a & k divides b by A4, A5, Lm4, Lm5;

          let m be Integer;

          assume that

           A6: m divides a and m divides b;

          thus thesis by A5, A6, Lm3;

        end;

          suppose

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

          defpred P[ Nat] means $1 divides a & $1 divides b & $1 <> 0 ;

          

           A8: a divides (a * b);

          (a * b) in INT by INT_1:def 2;

          then

          consider k be Nat such that

           A9: (a * b) = k or (a * b) = ( - k) by INT_1:def 1;

          k <> 0 by A7, A9, XCMPLX_1: 6;

          then

           A10: k > 0 ;

          

           A11: for i be Nat st P[i] holds i <= k

          proof

            let i be Nat;

            assume P[i];

            then i divides (a * b) by A8, Lm2;

            then i divides k by A9, Lm3;

            hence thesis by A10, Lm9;

          end;

          1 divides a & 1 divides b by Lm5;

          then

           A12: ex k be Nat st P[k];

          consider k be Nat such that

           A13: P[k] and

           A14: for n be Nat st P[n] holds n <= k from NAT_1:sch 6( A11, A12);

          take k;

          thus k divides a & k divides b by A13;

          let m be Integer;

          assume that

           A15: m divides a and

           A16: m divides b;

          m in INT by INT_1:def 2;

          then

          consider n be Nat such that

           A17: m = n or m = ( - n) by INT_1:def 1;

          set i = (n lcm k);

          

           A18: k divides i by Def1;

          now

            assume i = 0 ;

            then n = 0 or k = 0 by Th4;

            hence contradiction by A7, A13, A17, A15;

          end;

          then 0 < i;

          then

           A19: k <= i by A18, Lm9;

          n divides b by A17, A16, Lm4;

          then

           A20: (n lcm k) divides b by A13, Def1;

          n divides a by A17, A15, Lm4;

          then (n lcm k) divides a by A13, Def1;

          then k >= (n lcm k) by A14, A20;

          then k = i by A19, XXREAL_0: 1;

          then

           A21: n divides k by Def1;

          assume not m divides k;

          hence contradiction by A17, A21, Lm4;

        end;

      end;

      uniqueness

      proof

        let IT1,IT2 be Nat;

        assume IT1 divides a & IT1 divides b & (for m be Integer st m divides a & m divides b holds m divides IT1) & IT2 divides a & (IT2 divides b & for m be Integer st m divides a & m divides b holds m divides IT2);

        then IT1 divides IT2 & IT2 divides IT1;

        hence thesis by Lm8;

      end;

      commutativity ;

    end

    theorem :: INT_2:5

    

     Th5: a = 0 & b = 0 iff (a gcd b) = 0

    proof

       0 divides ( 0 gcd 0 ) by Def2;

      hence a = 0 & b = 0 implies (a gcd b) = 0 ;

      assume (a gcd b) = 0 ;

      then 0 divides a & 0 divides b by Def2;

      hence thesis;

    end;

    reserve n for Nat;

    reserve a,b,c,d,a1,b1,a2,b2,k,l for Integer;

    theorem :: INT_2:6

    

     Th6: ( - n) is Element of NAT iff n = 0

    proof

      thus ( - n) is Element of NAT implies n = 0

      proof

        assume ( - n) is Element of NAT ;

        then ( - n) >= 0 & (n + ( - n)) >= ( 0 + n);

        hence thesis;

      end;

      thus thesis;

    end;

    registration

      let n be non zero Nat;

      cluster ( - n) -> non natural;

      coherence

      proof

         not ( - n) is Element of NAT by Th6;

        hence thesis by ORDINAL1:def 12;

      end;

    end

    theorem :: INT_2:7

     not ( - 1) is Element of NAT ;

    theorem :: INT_2:8

    a divides ( - a) & ( - a) divides a by Lm1;

    theorem :: INT_2:9

    a divides b & b divides c implies a divides c by Lm2;

    theorem :: INT_2:10

    

     Th10: (a divides b iff a divides ( - b)) & (a divides b iff ( - a) divides b) & (a divides b iff ( - a) divides ( - b)) & (a divides ( - b) iff ( - a) divides b)

    proof

      

       A1: a divides b implies a divides ( - b)

      proof

        assume

         A2: a divides b;

        b divides ( - b) by Lm1;

        hence thesis by A2, Lm2;

      end;

      

       A3: a divides ( - b) implies a divides b

      proof

        assume

         A4: a divides ( - b);

        ( - b) divides b by Lm1;

        hence thesis by A4, Lm2;

      end;

      hence a divides b iff a divides ( - b) by A1;

      

       A5: ( - a) divides b implies a divides b

      proof

        assume

         A6: ( - a) divides b;

        a divides ( - a) by Lm1;

        hence thesis by A6, Lm2;

      end;

      

       A7: ( - a) divides ( - b) implies a divides b

      proof

        assume

         A8: ( - a) divides ( - b);

        ( - b) divides b by Lm1;

        hence thesis by A5, A8, Lm2;

      end;

      

       A9: a divides b implies ( - a) divides b

      proof

        assume

         A10: a divides b;

        ( - a) divides a by Lm1;

        hence thesis by A10, Lm2;

      end;

      hence a divides b iff ( - a) divides b by A5;

      a divides b implies ( - a) divides ( - b)

      proof

        assume

         A11: a divides b;

        ( - a) divides a by Lm1;

        hence thesis by A1, A11, Lm2;

      end;

      hence a divides b iff ( - a) divides ( - b) by A7;

      thus thesis by A1, A3, A9, A5;

    end;

    theorem :: INT_2:11

    a divides b & b divides a implies a = b or a = ( - b)

    proof

      assume that

       A1: a divides b and

       A2: b divides a;

      consider a1 such that

       A3: b = (a * a1) by A1;

      consider b1 such that

       A4: a = (b * b1) by A2;

      a <> 0 implies a = b or a = ( - b)

      proof

        assume

         A5: a <> 0 ;

        (1 * a) = (a * (a1 * b1)) by A3, A4;

        then (a1 * b1) = 1 by A5, XCMPLX_1: 5;

        then a = (b * 1) or a = (b * ( - 1)) by A4, INT_1: 9;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: INT_2:12

    a divides 0 & 1 divides a & ( - 1) divides a by Lm5;

    theorem :: INT_2:13

    

     Th13: a divides 1 or a divides ( - 1) implies a = 1 or a = ( - 1) by INT_1: 9, INT_1: 10;

    theorem :: INT_2:14

    a = 1 or a = ( - 1) implies a divides 1 & a divides ( - 1) by Lm5;

    theorem :: INT_2:15

    (a,b) are_congruent_mod c iff c divides (a - b);

    theorem :: INT_2:16

    a divides b iff |.a.| divides |.b.|

    proof

      thus a divides b implies |.a.| divides |.b.|

      proof

        assume a divides b;

        then

        consider c such that

         A1: b = (a * c);

         |.b.| = ( |.a.| * |.c.|) by A1, COMPLEX1: 65;

        hence thesis;

      end;

      assume |.a.| divides |.b.|;

      then

      consider m be Integer such that

       A2: |.b.| = ( |.a.| * m);

      

       A3: a >= 0 implies a divides b

      proof

        assume a >= 0 ;

        then

         A4: |.b.| = (a * m) by A2, ABSVALUE:def 1;

        per cases ;

          suppose b < 0 ;

          then ( - b) = (a * m) by A4, ABSVALUE:def 1;

          then b = (a * ( - m));

          hence thesis;

        end;

          suppose b >= 0 ;

          then b = (a * m) by A4, ABSVALUE:def 1;

          hence thesis;

        end;

      end;

      a < 0 implies a divides b

      proof

        assume a < 0 ;

        then

         A5: |.b.| = (( - a) * m) by A2, ABSVALUE:def 1;

        per cases ;

          suppose b < 0 ;

          then ( - b) = ( - (a * m)) by A5, ABSVALUE:def 1;

          hence thesis;

        end;

          suppose b >= 0 ;

          then b = (a * ( - m)) by A5, ABSVALUE:def 1;

          hence thesis;

        end;

      end;

      hence thesis by A3;

    end;

    theorem :: INT_2:17

    (a lcm b) is Element of NAT by ORDINAL1:def 12;

    theorem :: INT_2:18

    a divides (a lcm b) by Def1;

    theorem :: INT_2:19

    for c st a divides c & b divides c holds (a lcm b) divides c by Def1;

    theorem :: INT_2:20

    (a gcd b) is Element of NAT by ORDINAL1:def 12;

    theorem :: INT_2:21

    

     Th21: (a gcd b) divides a by Def2;

    theorem :: INT_2:22

    for c st c divides a & c divides b holds c divides (a gcd b) by Def2;

    definition

      let a,b be Integer;

      :: INT_2:def3

      pred a,b are_coprime means (a gcd b) = 1;

      symmetry ;

    end

    theorem :: INT_2:23

    a <> 0 or b <> 0 implies ex a1, b1 st a = ((a gcd b) * a1) & b = ((a gcd b) * b1) & (a1,b1) are_coprime

    proof

      assume a <> 0 or b <> 0 ;

      then

       A1: (a gcd b) <> 0 by Th5;

      (a gcd b) divides a by Def2;

      then

      consider a1 such that

       A2: a = ((a gcd b) * a1);

      (a gcd b) divides b by Def2;

      then

      consider b1 such that

       A3: b = ((a gcd b) * b1);

      (a1 gcd b1) divides b1 by Def2;

      then

      consider b2 such that

       A4: b1 = ((a1 gcd b1) * b2);

      b = (((a gcd b) * (a1 gcd b1)) * b2) by A3, A4;

      then

       A5: ((a gcd b) * (a1 gcd b1)) divides b;

      (a1 gcd b1) divides a1 by Def2;

      then

      consider a2 such that

       A6: a1 = ((a1 gcd b1) * a2);

      a = (((a gcd b) * (a1 gcd b1)) * a2) by A2, A6;

      then ((a gcd b) * (a1 gcd b1)) divides a;

      then ((a gcd b) * (a1 gcd b1)) divides (a gcd b) by A5, Def2;

      then

      consider c such that

       A7: (a gcd b) = (((a gcd b) * (a1 gcd b1)) * c);

      ((a gcd b) * 1) = ((a gcd b) * ((a1 gcd b1) * c)) by A7;

      then 1 = ((a1 gcd b1) * c) by A1, XCMPLX_1: 5;

      then (a1 gcd b1) = 1 or (a1 gcd b1) = ( - 1) by INT_1: 9;

      then (a1,b1) are_coprime ;

      hence thesis by A2, A3;

    end;

    theorem :: INT_2:24

    

     Th24: (a,b) are_coprime implies ((c * a) gcd (c * b)) = |.c.| & ((c * a) gcd (b * c)) = |.c.| & ((a * c) gcd (c * b)) = |.c.| & ((a * c) gcd (b * c)) = |.c.|

    proof

      assume (a,b) are_coprime ;

      then

       A1: (a gcd b) = 1;

      thus

       A2: ((c * a) gcd (c * b)) = |.c.|

      proof

        ((c * a) gcd (c * b)) divides (c * b) by Def2;

        then

        consider l such that

         A3: (c * b) = (((c * a) gcd (c * b)) * l);

        ((c * a) gcd (c * b)) divides (c * a) by Def2;

        then

        consider k such that

         A4: (c * a) = (((c * a) gcd (c * b)) * k);

        c divides (c * a) & c divides (c * b);

        then c divides ((c * a) gcd (c * b)) by Def2;

        then

        consider d such that

         A5: ((c * a) gcd (c * b)) = (c * d);

        

         A6: (c * b) = (c * (d * l)) by A5, A3;

        

         A7: (c * a) = (c * (d * k)) by A5, A4;

        

         A8: c <> 0 implies ((c * a) gcd (c * b)) = |.c.|

        proof

          assume

           A9: c <> 0 ;

          then b = (d * l) by A6, XCMPLX_1: 5;

          then

           A10: d divides b;

          a = (d * k) by A7, A9, XCMPLX_1: 5;

          then d divides a;

          then d divides 1 by A1, A10, Def2;

          then ((c * a) gcd (c * b)) = (c * 1) or ((c * a) gcd (c * b)) = (c * ( - 1)) by A5, Th13;

          then ((c * a) gcd (c * b)) = (c * 1) or ((c * a) gcd (c * b)) = (( - c) * 1);

          then

           A11: |.((c * a) gcd (c * b)).| = |.c.| by COMPLEX1: 52;

          thus thesis by A11, ABSVALUE:def 1;

        end;

        (( 0 * a) gcd ( 0 * b)) = 0 by Th5

        .= |. 0 .| by ABSVALUE: 2;

        hence thesis by A8;

      end;

      hence ((c * a) gcd (b * c)) = |.c.|;

      thus thesis by A2;

    end;

    theorem :: INT_2:25

    

     Th25: c divides (a * b) & (a,c) are_coprime implies c divides b

    proof

      assume that

       A1: c divides (a * b) and

       A2: (a,c) are_coprime ;

      c divides (c * b);

      then

       A3: c divides ((a * b) gcd (c * b)) by A1, Def2;

      

       A4: ((a * b) gcd (c * b)) = |.b.| by A2, Th24;

      b < 0 implies c divides b

      proof

        assume b < 0 ;

        then c divides ( - b) by A4, A3, ABSVALUE:def 1;

        hence thesis by Th10;

      end;

      hence thesis by A4, A3, ABSVALUE:def 1;

    end;

    theorem :: INT_2:26

    (a,c) are_coprime & (b,c) are_coprime implies ((a * b),c) are_coprime

    proof

      assume that

       A1: (a,c) are_coprime and

       A2: (b,c) are_coprime ;

      

       A3: (a gcd c) = 1 by A1;

      

       A4: (((a * b) gcd c) gcd a) divides a by Def2;

      

       A5: ((a * b) gcd c) divides c by Def2;

      (((a * b) gcd c) gcd a) divides ((a * b) gcd c) by Def2;

      then (((a * b) gcd c) gcd a) divides c by A5, Lm2;

      then (((a * b) gcd c) gcd a) divides 1 by A3, A4, Def2;

      then (((a * b) gcd c) gcd a) = 1 or (((a * b) gcd c) gcd a) = ( - 1) by Th13;

      then (a,((a * b) gcd c)) are_coprime ;

      then

       A6: ((a * b) gcd c) divides b by Th21, Th25;

      (b gcd c) = 1 by A2;

      then ((a * b) gcd c) divides 1 by A5, A6, Def2;

      then ((a * b) gcd c) = 1 or ((a * b) gcd c) = ( - 1) by Th13;

      hence thesis;

    end;

    reserve p,p1,q,l for Nat;

    definition

      let p be integer Number;

      :: INT_2:def4

      attr p is prime means p > 1 & for n be Nat st n divides p holds n = 1 or n = p;

    end

    registration

      cluster prime -> natural for integer Number;

      coherence

      proof

        let p be integer Number;

        assume p is prime;

        then p in NAT by INT_1: 3;

        hence thesis;

      end;

    end

    theorem :: INT_2:27

    

     Th27: 0 < b & a divides b implies a <= b

    proof

      assume

       A1: 0 < b;

      assume a divides b;

      then

      consider c such that

       A2: b = (a * c);

      per cases ;

        suppose a <= 0 ;

        hence thesis by A1;

      end;

        suppose

         A3: a > 0 ;

        then c > 0 by A1, A2;

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

        hence thesis by A2, A3, XREAL_1: 151;

      end;

    end;

    theorem :: INT_2:28

    

     Th28: 2 is prime

    proof

      thus 2 > 1;

      let n be Nat;

      assume

       A1: n divides 2;

      then n <= 2 by Th27;

      then n = 0 or ... or n = 2;

      hence thesis by A1;

    end;

    theorem :: INT_2:29

    

     Th29: not 4 is prime

    proof

      ex n st n divides 4 & n <> 1 & n <> 4

      proof

        take 2;

        4 = (2 * 2);

        hence thesis;

      end;

      hence thesis;

    end;

    registration

      cluster prime for Nat;

      existence by Th28;

      cluster non zero non prime for Nat;

      existence by Th29;

    end

    theorem :: INT_2:30

    p is prime & q is prime implies (p,q) are_coprime or p = q

    proof

      assume that

       A1: p is prime and

       A2: q is prime;

      

       A3: (p gcd q) divides q by Def2;

      assume not (p,q) are_coprime ;

      then

       A4: (p gcd q) <> 1;

      (p gcd q) divides p by Def2;

      then (p gcd q) = p by A1, A4;

      hence thesis by A2, A4, A3;

    end;

    theorem :: INT_2:31

    l >= 2 implies ex p be Element of NAT st p is prime & p divides l

    proof

      defpred P[ Nat] means ex p st p is prime & p divides $1;

      

       A1: for k be Nat st k >= 2 holds (for n be Nat st n >= 2 holds n < k implies P[n]) implies P[k]

      proof

        let k be Nat;

        assume

         A2: k >= 2;

        assume

         A3: for n be Nat st n >= 2 holds n < k implies ex p st p is prime & p divides n;

        

         A4: ((k + 1) - 1) > ((1 + 1) - 1) by A2, NAT_1: 13;

         not k is prime implies ex p be Element of NAT st p is prime & p divides k

        proof

          assume not k is prime;

          then

          consider m be Nat such that

           A5: m divides k and

           A6: m <> 1 and

           A7: m <> k by A4;

          m <> 0 by A5, A7;

          then m > 0 ;

          then m >= ( 0 + 1) by NAT_1: 13;

          then m > 1 by A6, XXREAL_0: 1;

          then

           A8: m >= (1 + 1) by NAT_1: 13;

          k > 0 by A2;

          then m <= k by A5, Th27;

          then m < k by A7, XXREAL_0: 1;

          then

          consider p1 such that

           A9: p1 is prime & p1 divides m by A3, A8;

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

          take p1;

          thus thesis by A5, A9, Lm2;

        end;

        hence thesis;

      end;

      

       A10: for k be Nat st k >= 2 holds P[k] from NAT_1:sch 9( A1);

      assume l >= 2;

      then

      consider p such that

       A11: p is prime & p divides l by A10;

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

      take p;

      thus thesis by A11;

    end;

    begin

    theorem :: INT_2:32

    for i,j be Integer st i >= 0 & j >= 0 holds ( |.i.| mod |.j.|) = (i mod j) & ( |.i.| div |.j.|) = (i div j)

    proof

      let i,j be Integer;

      assume that

       A1: i >= 0 and

       A2: j >= 0 ;

      per cases by A2;

        suppose

         A3: j > 0 ;

        i = |.i.| by A1, ABSVALUE:def 1;

        hence thesis by A3, ABSVALUE:def 1;

      end;

        suppose

         A4: j = 0 ;

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

        then ( |.i.| mod |. 0 .|) = 0 & ( |.i.| div |. 0 .|) = 0 by INT_1: 48, INT_1:def 10;

        hence thesis by A4, INT_1: 48, INT_1:def 10;

      end;

    end;

    theorem :: INT_2:33

    (a lcm b) = ( |.a.| lcm |.b.|)

    proof

      

       A1: |.b.| = b or |.b.| = ( - b) by ABSVALUE: 1;

      

       A2: |.a.| = a or |.a.| = ( - a) by ABSVALUE: 1;

       A3:

      now

        let m be Integer;

        assume |.a.| divides m & |.b.| divides m;

        then a divides m & b divides m by A2, A1, Th10;

        hence (a lcm b) divides m by Def1;

      end;

      b divides (a lcm b) by Def1;

      then

       A4: |.b.| divides (a lcm b) by A1, Th10;

      a divides (a lcm b) by Def1;

      then |.a.| divides (a lcm b) by A2, Th10;

      hence thesis by A4, A3, Def1;

    end;

    theorem :: INT_2:34

    (a gcd b) = ( |.a.| gcd |.b.|)

    proof

      

       A1: |.b.| = b or |.b.| = ( - b) by ABSVALUE: 1;

      

       A2: |.a.| = a or |.a.| = ( - a) by ABSVALUE: 1;

       A3:

      now

        let m be Integer;

        assume m divides |.a.| & m divides |.b.|;

        then m divides a & m divides b by A2, A1, Th10;

        hence m divides (a gcd b) by Def2;

      end;

      (a gcd b) divides b by Def2;

      then

       A4: (a gcd b) divides |.b.| by A1, Th10;

      (a gcd b) divides a by Def2;

      then (a gcd b) divides |.a.| by A2, Th10;

      hence thesis by A4, A3, Def2;

    end;