The Mizar article:

The Divisibility of Integers and Integer Relatively Primes

by
Rafal Kwiatek, and
Grzegorz Zwara

Received July 10, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: INT_2
[ MML identifier index ]


environ

 vocabulary ARYTM_3, INT_1, ARYTM_1, ABSVALUE, FILTER_0, INT_2;
 notation SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, INT_1, NAT_1, GROUP_1;
 constructors REAL_1, NAT_1, GROUP_1, XBOOLE_0;
 clusters INT_1, ZFMISC_1, XBOOLE_0;
 requirements REAL, NUMERALS, SUBSET, ARITHM;
 theorems AXIOMS, INT_1, REAL_1, ABSVALUE, NAT_1, XCMPLX_0, XCMPLX_1;
 schemes REAL_1;

begin

  ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
  ::     SOME PROPERTIES ON FUNCTIONS: HCF & LCM FOR NATURAL NUMBERS        ::
  ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

 reserve a,b,c,d,e,f,g,h,z for Nat;

canceled 2;

  theorem
  Th3: 0 divides a iff a = 0
   proof
      0 divides a implies a = 0
     proof
      assume 0 divides a;
      then ex b st a = 0*b by NAT_1:def 3;
      hence thesis;
     end;
    hence thesis;
   end;

  theorem
  Th4: a = 0 or b = 0 iff a lcm b = 0
   proof
    A1: a = 0 implies a lcm b = 0
     proof
      assume a = 0;
      then 0 divides (a lcm b) by NAT_1:def 4;
      hence thesis by Th3;
     end;
    A2: b = 0 implies (a lcm b) = 0
     proof
      assume b = 0;
      then 0 divides (a lcm b) by NAT_1:def 4;
      hence thesis by Th3;
     end;
      (a lcm b) = 0 implies a = 0 or b = 0
     proof
      assume A3: (a lcm b) = 0;
A4:   a divides a implies a divides a*b by NAT_1:56;
        b divides b implies b divides b*a by NAT_1:56;
      then 0 divides a*b by A3,A4,NAT_1:def 4;
      then a*b = 0 by Th3;
      hence thesis by XCMPLX_1:6;
     end;
    hence thesis by A1,A2;
   end;

  theorem
     a = 0 & b = 0 iff a hcf b = 0
   proof
      (a hcf b) = 0 implies a = 0 & b = 0
     proof
      assume (a hcf b) = 0;
      then 0 divides a & 0 divides b by NAT_1:def 5;
      hence thesis by Th3;
     end;
    hence thesis;
   end;

  theorem
     a*b = (a lcm b)*(a hcf b)
   proof
    A1: a<>0 & b<>0 implies a*b = (a lcm b)*(a hcf b)
     proof
      assume A2: a<>0 & b<>0;
A3:   a divides a implies a divides a*b by NAT_1:56;
        b divides b implies b divides b*a by NAT_1:56;
      then (a lcm b) divides a*b by A3,NAT_1:def 4;
      then consider c such that A4: a*b = (a lcm b)*c by NAT_1:def 3;
      A5: a divides (a lcm b) & b divides (a lcm b) by NAT_1:def 4;
      then consider d such that A6: (a lcm b) = a*d by NAT_1:def 3;
      consider e such that A7: (a lcm b) = b*e by A5,NAT_1:def 3;
        a*b = a*(c*d) by A4,A6,XCMPLX_1:4;
      then A8: b = c*d by A2,XCMPLX_1:5;
        a*b = b*(c*e) by A4,A7,XCMPLX_1:4;
      then a = c*e by A2,XCMPLX_1:5;
      then A9:c divides a & c divides b by A8,NAT_1:def 3;
        f divides a & f divides b implies f divides c
       proof
        assume A10: f divides a & f divides b;
        then consider g such that A11: a = f*g by NAT_1:def 3;
        consider h such that A12: b = f*h by A10,NAT_1:def 3;
        A13: b*g = g*h*f by A12,XCMPLX_1:4;
          a*h = g*h*f by A11,XCMPLX_1:4;
        then a divides g*h*f & b divides g*h*f by A13,NAT_1:def 3;
        then (a lcm b) divides g*h*f by NAT_1:def 4;
        then consider z such that A14: g*h*f = (a lcm b)*z by NAT_1:def 3;
        A15: c*(a lcm b) = (g*(h*f))*f by A4,A11,A12,XCMPLX_1:4
                      .= (a lcm b)*z*f by A14,XCMPLX_1:4
                      .= (z*f)*(a lcm b) by XCMPLX_1:4;
          (a lcm b) <> 0 by A2,Th4;
        then c = f*z by A15,XCMPLX_1:5;
        hence thesis by NAT_1:def 3;
       end;
      hence thesis by A4,A9,NAT_1:def 5;
     end;
      a = 0 or b = 0 implies a*b = (a lcm b)*(a hcf b)
     proof
      assume A16: a = 0 or b = 0;
      then a*b = 0*(a hcf b)
      .= (a lcm b)*(a hcf b) by A16,Th4;
      hence thesis;
     end;
    hence thesis by A1;
   end;

 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
 ::                 SOME PROPERTIES OF INTEGER NUMBERS                   ::
 ::                              LCM,HCF                                 ::
 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

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

canceled;

  theorem
  Th8: -n is Nat iff n = 0
   proof
    thus -n is Nat implies n = 0
     proof
      assume -n is Nat;
      then A1: -n>=0 & n>=0 by NAT_1:18;
      then n+(-n)>=0+n by AXIOMS:24;
      then n-n>=0+n by XCMPLX_0:def 8;
      then 0>=n by XCMPLX_1:14;
      hence thesis by A1,AXIOMS:21;
     end;
    thus n = 0 implies -n is Nat;
    thus thesis;
   end;

  theorem
  Th9: not -1 is Nat by Th8;

  theorem
  Th10: 0 divides a iff a = 0
   proof
      0 divides a implies a = 0
     proof
      assume 0 divides a;
      then consider a1 such that A1: a = 0*a1 by INT_1:def 9;
      thus thesis by A1;
     end;
    hence thesis;
   end;

  theorem
  Th11: a divides -a & -a divides a
   proof
    thus a divides -a
     proof
        -a = -(a*1) .= a*(-1) by XCMPLX_1:175;
      hence thesis by INT_1:def 9;
     end;
    thus thesis
     proof
        a = -(-(a*1)).= (-a)*(-1) by XCMPLX_1:176;
      hence thesis by INT_1:def 9;
     end;
   end;

  theorem
  Th12: a divides b implies a divides b*c
   proof
    assume a divides b;
    then consider d such that A1: b = a*d by INT_1:def 9;
      b*c = a*(d*c) by A1,XCMPLX_1:4;
    hence thesis by INT_1:def 9;
   end;

  theorem
  Th13: a divides b & b divides c implies a divides c
   proof
    assume that A1: a divides b and A2: b divides c;
    consider k such that A3: b = a*k by A1,INT_1:def 9;
    consider l such that A4: c = b*l by A2,INT_1:def 9;
      c = a*(k*l) by A3,A4,XCMPLX_1:4;
    hence thesis by INT_1:def 9;
   end;

  theorem
  Th14: (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
    thus A1: a divides b iff a divides -b
     proof
      A2: a divides b implies a divides -b
       proof
        assume A3: a divides b;
          b divides -b by Th11;
        hence thesis by A3,Th13;
       end;
        a divides -b implies a divides b
       proof
        assume A4: a divides -b;
          -b divides b by Th11;
        hence thesis by A4,Th13;
       end;
      hence thesis by A2;
     end;
    thus A5: a divides b iff -a divides b
     proof
      A6: a divides b implies -a divides b
       proof
        assume A7: a divides b;
          -a divides a by Th11;
        hence thesis by A7,Th13;
       end;
        -a divides b implies a divides b
       proof
        assume A8: -a divides b;
          a divides -a by Th11;
        hence thesis by A8,Th13;
       end;
      hence thesis by A6;
     end;
    thus a divides b iff -a divides -b
     proof
      A9: a divides b implies -a divides -b
       proof
        assume A10: a divides b;
          -a divides a by Th11;
        hence thesis by A1,A10,Th13;
       end;
        -a divides -b implies a divides b
       proof
        assume A11: -a divides -b;
          -b divides b by Th11;
        hence thesis by A5,A11,Th13;
       end;
      hence thesis by A9;
     end;
    thus thesis by A1,A5;
   end;

  theorem
     a divides b & b divides a implies a = b or a = -b
   proof
    assume A1: a divides b & b divides a;
    then consider a1 such that A2: b = a*a1 by INT_1:def 9;
    consider b1 such that A3: a = b*b1 by A1,INT_1:def 9;
      a<>0 implies a = b or a = -b
     proof
      assume A4: a<>0;
        1*a = a*(a1*b1) by A2,A3,XCMPLX_1:4;
      then a1*b1 = 1 by A4,XCMPLX_1:5;
      then a = b*1 or a = b*(-1) by A3,INT_1:22;
      then a = b*1 or a = (-b)*1 by XCMPLX_1:175;
      hence thesis;
     end;
    hence thesis by A1,Th10;
   end;

  theorem
  Th16: a divides 0 & 1 divides a & -1 divides a
   proof
    thus a divides 0
     proof
        0 = a*0;
      hence thesis by INT_1:def 9;
     end;
    thus 1 divides a
     proof
        a = 1*a;
      hence thesis by INT_1:def 9;
     end;
    thus thesis
     proof
        a = -(1*(-a))
       .= (-1)*(-a) by XCMPLX_1:175;
      hence thesis by INT_1:def 9;
     end;
   end;

  theorem
  Th17: a divides 1 or a divides -1 implies a = 1 or a = -1
   proof
    assume A1: a divides 1 or a divides -1;
    A2: a divides 1 implies a = 1 or a = -1
     proof
      assume a divides 1;
      then consider b such that A3: 1 = a*b by INT_1:def 9;
      thus thesis by A3,INT_1:22;
     end;
      a divides -1 implies a = 1 or a = -1
     proof
      assume a divides -1;
      then ex b st -1 = a*b by INT_1:def 9;
      hence thesis by INT_1:23;
     end;
    hence thesis by A1,A2;
   end;

  theorem
     a = 1 or a = -1 implies a divides 1 & a divides -1 by Th16;

  theorem
     a,b are_congruent_mod c iff c divides (a-b)
   proof
    A1: a,b are_congruent_mod c implies c divides (a-b)
     proof
      assume a,b are_congruent_mod c;
      then ex d st (a-b) = c*d by INT_1:def 3;
      hence thesis by INT_1:def 9;
     end;
      c divides (a-b) implies a,b are_congruent_mod c
     proof
      assume c divides (a-b);
      then ex d st (a-b) = c*d by INT_1:def 9;
      hence thesis by INT_1:def 3;
     end;
    hence thesis by A1;
   end;

theorem
    abs(a) is Nat;

  theorem
  Th21: a divides b iff (abs(a)) divides (abs(b))
   proof
    A1: a divides b implies (abs(a)) divides (abs(b))
     proof
      assume a divides b;
      then consider c such that A2: b = a*c by INT_1:def 9;
        abs(b) = abs(a)*abs(c) by A2,ABSVALUE:10;
      hence thesis by NAT_1:def 3;
     end;
      (abs(a)) divides (abs(b)) implies a divides b
     proof
      assume (abs(a)) divides (abs(b));
      then consider m such that A3: abs(b) = abs(a)*m by NAT_1:def 3;
      A4: a>=0 implies a divides b
       proof
        assume a>=0;
        then A5: abs(b) = a*m by A3,ABSVALUE:def 1;
        A6: b>=0 implies a divides b
         proof
          assume b>=0;
          then b = a*m by A5,ABSVALUE:def 1;
          hence thesis by INT_1:def 9;
         end;
          b<0 implies a divides b
         proof
          assume b<0;
          then -b = a*m by A5,ABSVALUE:def 1;
          then b = -(a*m) .= a*(-m) by XCMPLX_1:175;
          hence thesis by INT_1:def 9;
         end;
        hence thesis by A6;
       end;
        a<0 implies a divides b
       proof
        assume a<0;
        then A7: abs(b) = (-a)*m by A3,ABSVALUE:def 1;
        A8: b>=0 implies a divides b
         proof
          assume b>=0;
          then b = (-a)*m by A7,ABSVALUE:def 1 .= a*(-m) by XCMPLX_1:176;
          hence thesis by INT_1:def 9;
         end;
          b<0 implies a divides b
         proof
          assume b<0;
          then -b = (-a)*m by A7,ABSVALUE:def 1 .= -(a*m) by XCMPLX_1:175;
          then -(-b) = a*m;
          hence thesis by INT_1:def 9;
         end;
        hence thesis by A8;
       end;
      hence thesis by A4;
     end;
    hence thesis by A1;
   end;

                         ::::::::::::::::::
                         ::     LCM      ::
                         ::::::::::::::::::

  definition let a,b;
 canceled;

   func a lcm' b -> Integer equals :Def2:  abs(a) lcm abs(b);
   coherence;
   commutativity;
  end;

canceled;

  theorem
     a lcm' b is Nat
   proof
      a lcm' b = abs(a) lcm abs(b) by Def2;
    hence thesis;
   end;

canceled;

  theorem
  Th25: a divides (a lcm' b)
   proof
      abs(a) divides (abs(a) lcm abs(b)) by NAT_1:def 4;
    then consider m such that A1: (abs(a) lcm abs(b)) = abs(a)*m by NAT_1:def 3
;
    A2: a>=0 implies a divides (a lcm' b)
     proof
      assume A3: a>=0;
      reconsider c = (abs(a) lcm abs(b)) as Integer;
      reconsider a1 = m as Integer;
        c = a*a1 by A1,A3,ABSVALUE:def 1;
      then a divides c by INT_1:def 9;
      hence thesis by Def2;
     end;
      a<0 implies a divides (a lcm' b)
     proof
      assume A4: a<0;
      reconsider c = abs(a) lcm abs(b) as Integer;
      reconsider b1 = m as Integer;
        c = (-a)*b1 by A1,A4,ABSVALUE:def 1 .= a*(-b1) by XCMPLX_1:176;
      then a divides c by INT_1:def 9;
      hence thesis by Def2;
     end;
    hence thesis by A2;
   end;

  theorem
    b divides (a lcm' b) by Th25;

  theorem
  Th27: for c st a divides c & b divides c holds (a lcm' b) divides c
   proof
    let c; assume A1: a divides c & b divides c;
    then A2: (abs(a)) divides (abs(c)) by Th21;
       (abs(b)) divides (abs(c)) by A1,Th21;
    then (abs(a) lcm abs(b)) divides (abs(c)) by A2,NAT_1:def 4;
    then consider m such that
A3: abs(c) = (abs(a) lcm abs(b))*m by NAT_1:def 3;
    A4: c>=0 implies (a lcm' b) divides c
     proof
      assume c>=0;
      then abs(c) = c by ABSVALUE:def 1;
      then c = (a lcm' b)*m by A3,Def2;
      hence thesis by INT_1:def 9;
     end;
      c <0 implies (a lcm' b) divides c
     proof
      assume c <0;
      then abs(c) = -c by ABSVALUE:def 1;
      then -c = (a lcm' b)*m by A3,Def2;
      then c = -((a lcm' b)*m) .= (a lcm' b)*(-m) by XCMPLX_1:175;
      hence thesis by INT_1:def 9;
     end;
    hence thesis by A4;
   end;

                          ::::::::::::::::::
                          ::      GCD     ::
                          ::::::::::::::::::

  definition let a,b;
   func a gcd b -> Integer equals :Def3:  abs(a) hcf abs(b);
   coherence;
   commutativity;
  end;

canceled;

  theorem
  Th29: a gcd b is Nat
   proof
      a gcd b = abs(a) hcf abs(b) by Def3;
    hence thesis;
   end;

canceled;

  theorem
  Th31: (a gcd b) divides a
   proof
      (abs(a) hcf abs(b)) divides (abs(a)) by NAT_1:def 5;
    then consider m such that
A1: abs(a) = (abs(a) hcf abs(b))*m by NAT_1:def 3;
    A2: a>=0 implies (a gcd b) divides a
     proof
      assume A3: a>=0;
      reconsider c = abs(a) hcf abs(b) as Integer;
      reconsider a1 = m as Integer;
        a = c*a1 by A1,A3,ABSVALUE:def 1;
      then c divides a by INT_1:def 9;
      hence thesis by Def3;
     end;
      a<0 implies (a gcd b) divides a
     proof
      assume A4: a<0;
      reconsider c = abs(a) hcf abs(b) as Integer;
      reconsider b1 = m as Integer;
        -(-a) = -(c*b1) by A1,A4,ABSVALUE:def 1 .= c*(-b1) by XCMPLX_1:175;
      then c divides a by INT_1:def 9;
      hence thesis by Def3;
     end;
    hence thesis by A2;
   end;

  theorem
    (a gcd b) divides b by Th31;

  theorem
  Th33: for c st c divides a & c divides b holds c divides (a gcd b)
   proof
    let c; assume A1: c divides a & c divides b;
    then A2: (abs(c)) divides (abs(a)) by Th21;
       (abs(c)) divides (abs(b)) by A1,Th21;
    then (abs(c)) divides (abs(a) hcf abs(b)) by A2,NAT_1:def 5;
    then consider m such that
A3: abs(a) hcf abs(b) = (abs(c))*m by NAT_1:def 3;
    A4: c>=0 implies c divides (a gcd b)
     proof
      assume c>=0;
      then abs(c) = c by ABSVALUE:def 1;
      then a gcd b = c*m by A3,Def3;
      hence thesis by INT_1:def 9;
     end;
      c <0 implies c divides (a gcd b)
     proof
      assume c <0;
      then abs(c) = -c by ABSVALUE:def 1;
      then a gcd b = (-c)*m by A3,Def3;
      then a gcd b = c*(-m) by XCMPLX_1:176;
      hence thesis by INT_1:def 9;
     end;
    hence thesis by A4;
   end;

  theorem
     a = 0 or b = 0 iff a lcm' b = 0
   proof
    A1: a = 0 implies a lcm' b = 0
     proof
      assume a = 0;
      then 0 divides (a lcm' b) by Th25;
      hence thesis by Th10;
     end;
    A2: b = 0 implies a lcm' b = 0
     proof
      assume b = 0;
      then 0 divides (a lcm' b) by Th25;
      hence thesis by Th10;
     end;
      a lcm' b = 0 implies a = 0 or b = 0
     proof
      assume A3: a lcm' b = 0;
A4:      a divides a implies a divides a*b by Th12;
        b divides b implies b divides b*a by Th12;
      then 0 divides a*b by A3,A4,Th27;
      then a*b = 0 by Th10;
      hence thesis by XCMPLX_1:6;
     end;
    hence thesis by A1,A2;
   end;

  theorem
  Th35: a = 0 & b = 0 iff a gcd b = 0
   proof
    A1: a = 0 & b = 0 implies a gcd b = 0
     proof
      assume a = 0 & b = 0;
      then 0 divides (a gcd b) by Th33;
      hence thesis by Th10;
     end;
      a gcd b = 0 implies a = 0 & b = 0
     proof
      assume a gcd b = 0;
      then 0 divides a & 0 divides b by Th31;
      hence thesis by Th10;
     end;
    hence thesis by A1;
   end;

  ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
  ::                      RELATIVE PRIME NUMBERS                            ::
  ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

  definition let a,b;
  pred a,b are_relative_prime means :Def4: a gcd b = 1;
   symmetry;
  end;

canceled 2;

  theorem
     a<>0 or b<>0 implies ex a1,b1 st
       a = (a gcd b)*a1 & b = (a gcd b)*b1 & a1,b1 are_relative_prime
   proof
    assume A1: a<>0 or b<>0;
      (a gcd b) divides a by Th31;
    then consider a1 such that A2: a = (a gcd b)*a1 by INT_1:def 9;
      (a gcd b) divides b by Th31;
    then consider b1 such that A3: b = (a gcd b)*b1 by INT_1:def 9;
      (a1 gcd b1) divides a1 by Th31;
    then consider a2 such that A4: a1 = (a1 gcd b1)*a2 by INT_1:def 9;
      (a1 gcd b1) divides b1 by Th31;
    then consider b2 such that A5: b1 = (a1 gcd b1)*b2 by INT_1:def 9;
    A6: a = ((a gcd b)*(a1 gcd b1))*a2 by A2,A4,XCMPLX_1:4;
      b = ((a gcd b)*(a1 gcd b1))*b2 by A3,A5,XCMPLX_1:4;
    then (a gcd b)*(a1 gcd b1) divides a & (a gcd b)*(a1 gcd b1) divides
b by A6,INT_1:def 9;
    then (a gcd b)*(a1 gcd b1) divides (a gcd b) by Th33;
    then consider c such that A7: a gcd b = ((a gcd b)*(a1 gcd b1))*c
     by INT_1:def 9;
    A8: (a gcd b)*1 = (a gcd b)*((a1 gcd b1)*c) by A7,XCMPLX_1:4;
      a gcd b <>0 by A1,Th35;
    then 1 = (a1 gcd b1)*c by A8,XCMPLX_1:5;
    then a1 gcd b1 = 1 or a1 gcd b1 = -1 by INT_1:22;
    then a1,b1 are_relative_prime by Def4,Th9,Th29;
    hence thesis by A2,A3;
   end;

  theorem
  Th39: a,b are_relative_prime implies (c*a gcd c*b) = abs(c)
  & c*a gcd b*c = abs(c) & a*c gcd c*b = abs(c) & a*c gcd b*c = abs(c)
   proof
    assume a,b are_relative_prime;
    then A1: a gcd b = 1 by Def4;
    thus A2: c*a gcd c*b = abs(c)
     proof
        c divides c*a & c divides c*b by Th12;
      then c divides (c*a gcd c*b) by Th33;
      then consider d such that A3: c*a gcd c*b = c*d by INT_1:def 9;
        (c*a gcd c*b) divides c*a by Th31;
      then consider k such that A4: c*a = (c*a gcd c*b)*k by INT_1:def 9;
        (c*a gcd c*b) divides c*b by Th31;
      then consider l such that A5: c*b = (c*a gcd c*b)*l by INT_1:def 9;
      A6: c*a = c*(d*k) by A3,A4,XCMPLX_1:4;
      A7: c*b = c*(d*l) by A3,A5,XCMPLX_1:4;
      A8: c <>0 implies c*a gcd c*b = abs(c)
       proof
        assume A9: c <>0;
        then a = d*k by A6,XCMPLX_1:5;
        then A10: d divides a by INT_1:def 9;
          b = d*l by A7,A9,XCMPLX_1:5;
        then d divides b by INT_1:def 9;
        then d divides 1 by A1,A10,Th33;
        then c*a gcd c*b = c*1 or c*a gcd c*b = c*(-1) by A3,Th17;
        then c*a gcd c*b = c*1 or c*a gcd c*b = (-c)*1 by XCMPLX_1:175;
        then A11: abs((c*a gcd c*b)) = abs(c) by ABSVALUE:17;
          c*a gcd c*b is Nat by Th29;
        then c*a gcd c*b >=0 by NAT_1:18;
        hence thesis by A11,ABSVALUE:def 1;
       end;
        c = 0 implies c*a gcd c*b = abs(c)
       proof
        assume A12: c = 0;
        then c*a gcd c*b = 0 by Th35 .= abs(0) by ABSVALUE:def 1;
        hence thesis by A12;
       end;
      hence thesis by A8;
     end;
    hence c*a gcd b*c = abs(c);
    thus thesis by A2;
   end;

  theorem
  Th40: c divides a*b & a,c are_relative_prime implies c divides b
   proof
    assume A1: c divides a*b & a,c are_relative_prime;
    then A2: a*b gcd c*b = abs(b) by Th39;
      c divides c*b by Th12;
    then A3: c divides (a*b gcd c*b) by A1,Th33;
      b<0 implies c divides b
     proof
      assume b<0;
      then c divides (-b) by A2,A3,ABSVALUE:def 1;
      hence thesis by Th14;
     end;
    hence thesis by A2,A3,ABSVALUE:def 1;
   end;

  theorem
     a,c are_relative_prime & b,c are_relative_prime implies
       a*b,c are_relative_prime
   proof
    assume a,c are_relative_prime & b,c are_relative_prime;
    then A1: (a gcd c) = 1 & (b gcd c) = 1 by Def4;
    A2: (a*b gcd c) divides a*b & (a*b gcd c) divides c by Th31;
    A3: ((a*b gcd c) gcd a) divides (a*b gcd c) & ((a*b gcd c) gcd a) divides
a by Th31;
    then ((a*b gcd c) gcd a) divides c by A2,Th13;
    then ((a*b gcd c) gcd a) divides 1 by A1,A3,Th33;
    then (a*b gcd c) gcd a = 1 or (a*b gcd c) gcd a = -1 by Th17;
    then a,(a*b gcd c) are_relative_prime by Def4,Th9,Th29;
    then (a*b gcd c) divides b by A2,Th40;
    then (a*b gcd c) divides 1 by A1,A2,Th33;
    then a*b gcd c = 1 or a*b gcd c = -1 by Th17;
    hence thesis by Def4,Th9,Th29;
   end;

::***************************************************************************::
::                           PRIME NUMBERS                                   ::
::***************************************************************************::

  reserve p,p1,q,k,l for Nat;
  reserve x for Real;
  reserve X for Subset of REAL;

  definition let p;
   attr p is prime means :Def5: p>1 &
    for n holds n divides p implies n = 1 or n = p;
  end;

  definition let m,n;
   pred m,n are_relative_prime means :Def6: m hcf n = 1;
  end;

canceled 2;

  theorem
     2 is prime
   proof
    thus 2>1 & for n holds n divides 2 implies n = 1 or n = 2
     proof
      thus 2>1;
        let n;
        assume A1: n divides 2;
        then n<>0 by Th3;
        then n>0 by NAT_1:19;
        then A2: n>=0+1 by NAT_1:38;
        then n+(-1+1)>=1;
        then (n+-1)+1>=1 by XCMPLX_1:1;
        then A3: (n-1)+1>=1 by XCMPLX_0:def 8;
          n-1>=1-1 by A2,REAL_1:49;
        then reconsider m = n-1 as Nat by INT_1:16;
          m+1 = 1 or m>=1 by A3,NAT_1:26;
        then (n-1)+1 = 1 or (n-1)+1>=1+1 by AXIOMS:24;
        then n+-1+1 = 1 or (n+-1)+1>=1+1 by XCMPLX_0:def 8;
        then A4: n+(-1+1) = 1 or n+(-1+1)>=2 by XCMPLX_1:1;
          n<=2 by A1,NAT_1:54;
        hence thesis by A4,AXIOMS:21;
     end;
   end;

canceled;

  theorem
    ex p st not p is prime
   proof
    take 4;
      ex n st n divides 4 & n<>1 & n<>4
     proof
      take 2;
        4 = 2*2;
      hence thesis by NAT_1:def 3;
     end;
    hence thesis by Def5;
   end;

  theorem
     p is prime & q is prime implies p,q are_relative_prime or p = q
   proof
    assume A1: p is prime & q is prime;
    assume not p,q are_relative_prime;
    then A2: (p hcf q)<>1 by Def6;
      (p hcf q) divides p & (p hcf q) divides q by NAT_1:def 5;
    then (p hcf q) = p & (p hcf q) = q by A1,A2,Def5;
    hence thesis;
   end;

  scheme Ind1 { a() -> Nat,P[Nat] } : for k st k>=a() holds P[k] provided
   A1: P[a()] and
   A2: for k st k>=a() & P[k] holds P[k+1]
   proof
    let k;
    assume k>=a();
    then k-a()>=a()-a() by REAL_1:49;
    then k-a()>=0 by XCMPLX_1:14;
    then reconsider m = k-a() as Nat by INT_1:16;
      k-(a()-a()) = m+a() by XCMPLX_1:37;
    then A3: k-0 = m+a() by XCMPLX_1:14;
    defpred P1[Real] means ex m st P[m+a()] & m = $1;
    consider X such that A4: x in X iff P1[x]
     from SepReal;
      P[0+a()] by A1;
    then A5: 0 in X by A4;
       for x st x in X holds x+1 in X
     proof
      let x;
      assume x in X;
      then consider m such that A6: P[m+a()] & m = x by A4;
        m+a()>=a() & P[m+a()] implies P[m+a()+1] by A2;
      then A7: m+a()>=a() & P[m+a()] implies P[m+1+a()] by XCMPLX_1:1;
        m>=0 by NAT_1:18;
      then m+a()>=0+a() by AXIOMS:24;
      hence thesis by A4,A6,A7;
     end;
    then m in X by A5,NAT_1:2;
    then ex n st P[n+a()] & n = m by A4;
    hence P[k] by A3;
   end;

  scheme Comp_Ind1 { a() -> Nat,P[Nat] } : for k st k>=a() holds P[k] provided
   A1: for k st k>=a() & (for n st n>=a() & n<k holds P[n]) holds P[k]
   proof
     defpred P1[Nat] means for n st (n>=a() & n<$1) holds P[n];
    A2: P1[a()];
    A3: for k st k>=a() holds P1[k] implies P1[k+1]
     proof
      let k;
      assume k>=a();
      assume A4: for n st n>=a() & n<k holds P[n];
      let n;
      assume A5: n>=a() & n<k+1;
      then n<=k by NAT_1:38;
      then n<k or n = k by REAL_1:def 5;
      hence thesis by A1,A4,A5;
     end;
    let k;
    A6: for k st k>=a() holds P1[k]
      from Ind1(A2,A3);
    assume A7: k>=a();
    then for n st (n>=a() & n<k) holds P[n] by A6;
    hence P[k] by A1,A7;
   end;

  theorem
     l>=2 implies ex p st p is prime & p divides l
   proof
    assume A1: l>=2;
    defpred P[Nat] means (ex p st p is prime & p divides $1);
    A2: for k st k>=2 holds (for n st n>=2 holds n<k implies P[n])
    implies P[k]
     proof
      let k; assume k>=2;
      then k+1>1+1 by NAT_1:38;
      then k+1-1>1+1-1 by REAL_1:54;
      then A3: k+(1-1)>1+1-1 by XCMPLX_1:29;
      assume A4: for n st n>=2 holds n<k implies (ex p st p is prime & p
 divides n);
        not k is prime implies ex p st p is prime & p divides k
       proof
        assume not k is prime;
        then consider m such that A5: m divides k & m<>1 & m<>k by A3,Def5;
          m>=2 & m<k
         proof
          thus m>=2
           proof
              m<>0 by A5,Th3;
            then m>0 by NAT_1:19;
            then m>=0+1 by NAT_1:38;
            then m>1 by A5,REAL_1:def 5;
            then m>=1+1 by NAT_1:38;
            hence thesis;
           end;
              k>0 by A3,AXIOMS:22;
            then m<=k by A5,NAT_1:54;
            hence thesis by A5,REAL_1:def 5;
         end;
        then consider p1 such that A6: p1 is prime & p1 divides m by A4;
        take p1;
        thus thesis by A5,A6,NAT_1:51;
       end;
      hence thesis;
     end;
      for k st k>=2 holds P[k] from Comp_Ind1 (A2);
    hence thesis by A1;
   end;

Back to top