int_4.miz

    begin

    reserve a,b,m,x,y,i1,i2,i3,i for Integer,

k,p,q,n for Nat,

c,c1,c2 for Element of NAT ,

z for set;

    theorem :: INT_4:1



     Th1: for X be real-membered set, a be Real holds (X,(a ++ X)) are_equipotent

    proof

      let X be real-membered set, a be Real;

      deffunc F( Real) = (a + $1);

      consider f be Function such that

       A1: ( dom f) = X & for x be Element of REAL st x in X holds (f . x) = F(x) from CLASSES1:sch 2;



       A2: ( rng f) = (a ++ X)

      proof

        thus ( rng f) c= (a ++ X)

        proof

          let z be object;

          assume z in ( rng f);

          then

          consider x be object such that

           A3: x in ( dom f) and

           A4: z = (f . x) by FUNCT_1:def 3;

          reconsider x as Real by A1, A3;

          reconsider x as Element of REAL by XREAL_0:def 1;

          (a + x) in REAL by XREAL_0:def 1;

          then

          reconsider z9 = z as Element of REAL by A1, A3, A4;

          z9 = (a + x) by A1, A3, A4;

          hence thesis by A1, A3, MEMBER_1: 141;

        end;

        let z be object;

        assume

         A5: z in (a ++ X);

        then

        reconsider z as Element of REAL ;

        consider x be Complex such that

         A6: z = (a + x) and

         A7: x in X by A5, MEMBER_1: 143;

        X c= REAL by MEMBERED: 3;

        then

        reconsider x as Element of REAL by A7;

        (f . x) = z by A1, A7, A6;

        hence thesis by A1, A7, FUNCT_1:def 3;

      end;

      take f;

      f is one-to-one

      proof

        let x,y be object;

        assume that

         A8: x in ( dom f) and

         A9: y in ( dom f) and

         A10: (f . x) = (f . y);

        reconsider x, y as Element of REAL by A1, A8, A9, XREAL_0:def 1;

        (f . x) = (a + x) by A1, A8;

        then (a + x) = (a + y) by A1, A9, A10;

        hence thesis;

      end;

      hence thesis by A1, A2;

    end;

    registration

      let X be finite real-membered set, a be Real;

      cluster (a ++ X) -> finite;

      coherence by Th1, CARD_1: 38;

    end

    theorem :: INT_4:2



     Th2: for X be real-membered set, a be Real holds ( card X) = ( card (a ++ X)) by Th1, CARD_1: 5;



     Lm1: for a be Integer, X be Subset of INT holds (a ++ X) c= INT

    proof

      let a be Integer, X be Subset of INT ;

      let x be object;

      assume

       A1: x in (a ++ X);

      then

      reconsider x9 = x as Real;

      consider y be Complex such that

       A2: x9 = (a + y) and

       A3: y in X by A1, MEMBER_1: 143;

      reconsider y9 = y as Integer by A3;

      x9 = (a + y9) by A2;

      hence thesis by INT_1:def 2;

    end;



     Lm2: for a be Integer, X be Subset of INT holds (a ** X) c= INT

    proof

      let a be Integer, X be Subset of INT ;

      let x be object;

      assume

       A1: x in (a ** X);

      then

      reconsider x9 = x as Real;

      consider y be Complex such that

       A2: x9 = (a * y) and

       A3: y in X by A1, MEMBER_1: 195;

      reconsider y9 = y as Integer by A3;

      x9 = (a * y9) by A2;

      hence thesis by INT_1:def 2;

    end;



     Lm3: for X be Subset of INT , a be Integer holds x in (a ** X) iff ex y be Integer st y in X & x = (a * y)

    proof

      let X be Subset of INT , a be Integer;

      hereby

        assume x in (a ** X);

        then

        consider z be Complex such that

         A1: x = (a * z) and

         A2: z in X by MEMBER_1: 195;

        reconsider z as Integer by A2;

        take z;

        thus z in X & x = (a * z) by A2, A1;

      end;

      given y be Integer such that

       A3: y in X & x = (a * y);

      reconsider x9 = x as Real;

      reconsider y as Real;

      ex z be Real st z in X & x9 = (a * z) by A3;

      hence thesis by MEMBER_1: 193;

    end;

    theorem :: INT_4:3



     Th3: for X be real-membered set, a be Real st a <> 0 holds (X,(a ** X)) are_equipotent

    proof

      let X be real-membered set, a be Real;

      deffunc F( Real) = (a * $1);

      consider f be Function such that

       A1: ( dom f) = X & for x be Element of REAL st x in X holds (f . x) = F(x) from CLASSES1:sch 2;

      assume

       A2: a <> 0 ;



       A3: f is one-to-one

      proof

        let x,y be object;

        assume that

         A4: x in ( dom f) & y in ( dom f) and

         A5: (f . x) = (f . y);

        reconsider x, y as Element of REAL by A1, A4, XREAL_0:def 1;

        (f . x) = (a * x) & (f . y) = (a * y) by A1, A4;

        hence thesis by A2, A5, XCMPLX_1: 5;

      end;

      take f;

      ( rng f) = (a ** X)

      proof

        thus ( rng f) c= (a ** X)

        proof

          let z be object;

          assume z in ( rng f);

          then

          consider x be object such that

           A6: x in ( dom f) and

           A7: z = (f . x) by FUNCT_1:def 3;

          reconsider x9 = x as Element of REAL by A1, A6, XREAL_0:def 1;

          z = (a * x9) by A1, A6, A7;

          hence thesis by A1, A6, MEMBER_1: 193;

        end;

        let z be object;

        assume

         A8: z in (a ** X);

        then

        reconsider z as Element of REAL ;

        consider x be Complex such that

         A9: z = (a * x) and

         A10: x in X by A8, MEMBER_1: 195;

        reconsider x as Element of REAL by A10, XREAL_0:def 1;

        (f . x) = z by A1, A10, A9;

        hence thesis by A1, A10, FUNCT_1:def 3;

      end;

      hence thesis by A1, A3;

    end;

    theorem :: INT_4:4



     Th4: for X be real-membered set, a be Real holds (a = 0 & X is non empty implies (a ** X) = { 0 }) & ((a ** X) = { 0 } implies a = 0 or X = { 0 })

    proof

      let X be real-membered set, a be Real;

      thus a = 0 & X is non empty implies (a ** X) = { 0 }

      proof

        assume that

         A1: a = 0 and

         A2: X is non empty;

        thus (a ** X) c= { 0 }

        proof

          let i be object;

          assume

           A3: i in (a ** X);

          then

          reconsider i as Real;

          ex x be Complex st i = (a * x) & x in X by A3, MEMBER_1: 195;

          hence thesis by A1, TARSKI:def 1;

        end;

        then (a ** X) = {} or (a ** X) = { 0 } by ZFMISC_1: 33;

        hence thesis by A2, INTEGRA2: 7;

      end;

      assume that

       A4: (a ** X) = { 0 } and

       A5: a <> 0 ;

      (X,(a ** X)) are_equipotent by A5, Th3;

      then

      consider x be object such that

       A6: X = {x} by A4, CARD_1: 28;



       A7: x in X by A6, TARSKI:def 1;

      then

      reconsider x as Real;

      (a * x) in (a ** X) by A7, MEMBER_1: 193;

      then (a * x) = 0 by A4, TARSKI:def 1;

      hence thesis by A5, A6, XCMPLX_1: 6;

    end;

    registration

      let X be finite real-membered set, a be Real;

      cluster (a ** X) -> finite;

      coherence

      proof

        per cases ;

          suppose a <> 0 ;

          hence thesis by Th3, CARD_1: 38;

        end;

          suppose

           A1: a = 0 ;

          per cases ;

            suppose X is empty;

            hence thesis by INTEGRA2: 7;

          end;

            suppose X is non empty;

            hence thesis by A1, Th4;

          end;

        end;

      end;

    end

    theorem :: INT_4:5



     Th5: for X be real-membered set, a be Real st a <> 0 holds ( card X) = ( card (a ** X)) by Th3, CARD_1: 5;

    begin



     Lm4: i1 divides i2 & i1 divides i3 implies i1 divides (i2 - i3)

    proof

      assume that

       A1: i1 divides i2 and

       A2: i1 divides i3;

      consider i4 be Integer such that

       A3: i2 = (i1 * i4) by A1;

      consider i5 be Integer such that

       A4: i3 = (i1 * i5) by A2;

      (i2 - i3) = (i1 * (i4 - i5)) by A3, A4;

      hence thesis;

    end;



     Lm5: i divides a & i divides (a - b) implies i divides b

    proof

      assume that

       A1: i divides a and

       A2: i divides (a - b);



       A3: b = (( - (a - b)) + a);

      i divides ( - (a - b)) by A2, INT_2: 10;

      hence thesis by A1, A3, WSIERP_1: 4;

    end;



     Lm6: p is prime & (p,n) are_coprime implies not p divides n

    proof

      assume that

       A1: p is prime and

       A2: (p,n) are_coprime ;

      assume p divides n;

      then (n gcd p) = p by NEWTON: 49;

      then (n gcd p) > 1 by A1, INT_2:def 4;

      hence contradiction by A2, INT_2:def 3;

    end;



     Lm7: p > 0 implies p >= (1 + 0 ) by NAT_1: 13;

    theorem :: INT_4:6



     Th6: i divides i1 & i1 <> 0 implies |.i.| <= |.i1.|

    proof

      assume i divides i1 & i1 <> 0 ;

      then |.i1.| <> 0 & |.i.| divides |.i1.| by ABSVALUE: 2, INT_2: 16;

      hence thesis by NAT_D: 7;

    end;

    theorem :: INT_4:7



     Th7: for i3 st i3 <> 0 holds i1 divides i2 iff (i1 * i3) divides (i2 * i3)

    proof

      let i3;

      assume

       A1: i3 <> 0 ;

      thus i1 divides i2 implies (i1 * i3) divides (i2 * i3)

      proof

        assume i1 divides i2;

        then

        consider i4 be Integer such that

         A2: i2 = (i1 * i4);

        (i2 * i3) = ((i1 * i3) * i4) by A2;

        hence thesis;

      end;

      assume (i1 * i3) divides (i2 * i3);

      then

      consider i5 be Integer such that

       A3: (i2 * i3) = ((i1 * i3) * i5);

      (i2 * i3) = ((i1 * i5) * i3) by A3;

      then i2 = (i1 * i5) by A1, XCMPLX_1: 5;

      hence thesis;

    end;

    theorem :: INT_4:8

    for a,b,m be Nat holds for n be Element of NAT st (a mod m) = (b mod m) holds ((a |^ n) mod m) = ((b |^ n) mod m)

    proof

      let a,b,m be Nat;

      let n be Element of NAT ;

      defpred P[ Nat] means ((a |^ $1) mod m) = ((b |^ $1) mod m);

      assume

       A1: (a mod m) = (b mod m);



       A2: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A3: P[k];

        reconsider l1 = (a |^ k), l2 = (b |^ k), a, b, m as Element of NAT by ORDINAL1:def 12;

        ((a |^ (k + 1)) mod m) = (((a |^ k) * a) mod m) by NEWTON: 6

        .= (((l1 mod m) * (a mod m)) mod m) by EULER_2: 9

        .= ((l2 * b) mod m) by A1, A3, EULER_2: 9

        .= ((b |^ (k + 1)) mod m) by NEWTON: 6;

        hence thesis;

      end;

      (a |^ 0 ) = 1 by NEWTON: 4;

      then

       A4: P[ 0 ] by NEWTON: 4;

      for k be Nat holds P[k] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: INT_4:9



     Th9: ((i1 * i),(i2 * i)) are_congruent_mod i3 & (i,i3) are_coprime implies (i1,i2) are_congruent_mod i3

    proof

      assume that

       A1: ((i1 * i),(i2 * i)) are_congruent_mod i3 and

       A2: (i,i3) are_coprime ;

      i3 divides ((i1 * i) - (i2 * i)) by A1;

      then i3 divides ((i1 - i2) * i);

      then i3 divides (i1 - i2) by A2, INT_2: 25;

      hence thesis;

    end;

    theorem :: INT_4:10



     Th10: (i1,i2) are_congruent_mod i3 implies ((i1 * k),(i2 * k)) are_congruent_mod (i3 * k)

    proof

      assume (i1,i2) are_congruent_mod i3;

      then

      consider i4 be Integer such that

       A1: (i3 * i4) = (i1 - i2);

      ((i3 * k) * i4) = ((i3 * i4) * k)

      .= ((i1 + ( - i2)) * k) by A1

      .= ((i1 * k) - (i2 * k));

      hence thesis;

    end;

    theorem :: INT_4:11



     Th11: (i1,i2) are_congruent_mod i implies ((i1 * i3),(i2 * i3)) are_congruent_mod i

    proof

      assume (i1,i2) are_congruent_mod i;

      then i divides (i1 - i2);

      then i divides ((i1 - i2) * i3) by INT_2: 2;

      then i divides ((i1 * i3) - (i2 * i3));

      hence thesis;

    end;

    ::$Canceled



     Th12: for i be Integer holds 0 = ( 0 mod i) by INT_1: 73;

    theorem :: INT_4:13



     Th13: for b st b > 0 holds for a holds ex q,r be Integer st a = ((b * q) + r) & r >= 0 & r < b

    proof

      let b;

      assume

       A1: b > 0 ;

      let a be Integer;

      per cases ;

        suppose

         A2: a >= 0 ;



         A3: b in NAT by A1, INT_1: 3;

        a in NAT by A2, INT_1: 3;

        then

        consider k,t be Nat such that

         A4: a = ((b * k) + t) & t < b by A1, A3, NAT_1: 17;

        take k, t;

        thus thesis by A4;

      end;

        suppose

         A5: a < 0 ;



         A6: b in NAT by A1, INT_1: 3;

        ( - a) in NAT by A5, INT_1: 3;

        then

        consider k,t be Nat such that

         A7: ( - a) = ((b * k) + t) and

         A8: t < b by A1, A6, NAT_1: 17;

        per cases ;

          suppose

           A9: t = 0 ;

          take q = ( - k), r = 0 ;

          a = (b * ( - k)) by A7, A9;

          hence a = ((b * q) + r);

          thus thesis by A1;

        end;

          suppose

           A10: t <> 0 ;

          take q = (( - k) - 1), r = (b - t);

          a = ((b * (( - k) - 1)) + (b - t)) by A7;

          hence a = ((b * q) + r);

          thus thesis by A8, A10, XREAL_1: 44, XREAL_1: 50;

        end;

      end;

    end;

    ::$Canceled

    theorem :: INT_4:15



     Th15: (a,m) are_coprime implies ex x be Integer st (((a * x) - b) mod m) = 0

    proof

      assume (a,m) are_coprime ;

      then (a gcd m) = 1 by INT_2:def 3;

      then

      consider s,t be Integer such that

       A1: 1 = ((s * a) + (t * m)) by NAT_D: 68;

      take (b * s);

      ((((a * b) * s) - b) mod m) = ((((a * s) - 1) * b) mod m)

      .= ((( - (m * t)) * b) mod m) by A1

      .= (( 0 + (m * (( - t) * b))) mod m)

      .= ( 0 mod m) by NAT_D: 61

      .= 0 by Th12;

      hence thesis;

    end;

    theorem :: INT_4:16



     Th16: m > 0 & (a,m) are_coprime implies ex n be Nat st (((a * n) - b) mod m) = 0

    proof

      assume that

       A1: m > 0 and

       A2: (a,m) are_coprime ;

      consider x be Integer such that

       A3: (((a * x) - b) mod m) = 0 by A2, Th15;

      consider q,n be Integer such that

       A4: x = ((m * q) + n) and

       A5: n >= 0 and n < m by A1, Th13;



       A6: (((a * x) - b) mod m) = ((((a * q) * m) + ((a * n) - b)) mod m) by A4

      .= (((a * n) - b) mod m) by EULER_1: 12;

      n in NAT by A5, INT_1: 3;

      then

      reconsider n as Nat;

      take n;

      thus thesis by A3, A6;

    end;

    theorem :: INT_4:17

    m <> 0 & not (a gcd m) divides b implies not ex x be Integer st (((a * x) - b) mod m) = 0

    proof

      assume that

       A1: m <> 0 and

       A2: not (a gcd m) divides b;

      given y such that

       A3: (((a * y) - b) mod m) = 0 ;

      (a gcd m) divides m by INT_2: 21;

      then

       A4: ex i be Integer st m = ((a gcd m) * i);

      (((a * y) - b) mod m) = ( 0 mod m) by A3, Th12;

      then (((a * y) - b), 0 ) are_congruent_mod m by A1, NAT_D: 64;

      then (((a * y) - b), 0 ) are_congruent_mod (a gcd m) by A4, INT_1: 20;

      then

       A5: (a gcd m) divides (((a * y) - b) - 0 );

      (a gcd m) divides (a * y) by INT_2: 2, INT_2: 21;

      hence contradiction by A2, A5, Lm5;

    end;

    theorem :: INT_4:18

    m <> 0 & (a gcd m) divides b implies ex x be Integer st (((a * x) - b) mod m) = 0

    proof

      assume that

       A1: m <> 0 and

       A2: (a gcd m) divides b;

      consider a1,m1 be Integer such that

       A3: a = ((a gcd m) * a1) and

       A4: m = ((a gcd m) * m1) and

       A5: (a1,m1) are_coprime by A1, INT_2: 23;

      consider b1 be Integer such that

       A6: b = ((a gcd m) * b1) by A2;



       A7: m1 <> 0 by A1, A4;

      consider y be Integer such that

       A8: (((a1 * y) - b1) mod m1) = 0 by A5, Th15;

      take y;

      (((a1 * y) - b1) mod m1) = ( 0 mod m1) by A8, Th12;

      then (((a1 * y) - b1), 0 ) are_congruent_mod m1 by A7, NAT_D: 64;

      then ((((a1 * y) - b1) * (a gcd m)),((a gcd m) * 0 qua Nat)) are_congruent_mod (m1 * (a gcd m)) by Th10;

      then (((a * y) - b) mod m) = ( 0 mod m) by A3, A4, A6, NAT_D: 64;

      hence thesis by Th12;

    end;

    begin

    theorem :: INT_4:19



     Th19: n > 0 & p > 0 implies ((p * q) mod (p |^ n)) = (p * (q mod (p |^ (n -' 1))))

    proof

      assume that

       A1: n > 0 and

       A2: p > 0 ;



       A3: n >= ( 0 + 1) by A1, NAT_1: 13;

      (p * (q mod (p |^ (n -' 1)))) = (p * (q - ((q div (p |^ (n -' 1))) * (p |^ (n -' 1))))) by A2, NEWTON: 63

      .= ((p * q) - ((q div (p |^ (n -' 1))) * (p * (p |^ (n -' 1)))))

      .= ((p * q) - ((q div (p |^ (n -' 1))) * (p |^ ((n -' 1) + 1)))) by NEWTON: 6

      .= ((p * q) - ((q div (p |^ (n -' 1))) * (p |^ n))) by A3, XREAL_1: 235;

      then

       A4: (p * q) = (((q div (p |^ (n -' 1))) * (p |^ n)) + (p * (q mod (p |^ (n -' 1)))));

      (p * (q mod (p |^ (n -' 1)))) < (p * (p |^ (n -' 1))) by A2, NAT_D: 1, XREAL_1: 68;

      then (p * (q mod (p |^ (n -' 1)))) < (p |^ ((n -' 1) + 1)) by NEWTON: 6;

      then (p * (q mod (p |^ (n -' 1)))) < (p |^ n) by A3, XREAL_1: 235;

      hence thesis by A4, NAT_D:def 2;

    end;

    theorem :: INT_4:20

    ((p * q) mod (p * n)) = (p * (q mod n))

    proof

      per cases ;

        suppose

         A1: n = 0 ;

        then (q mod n) = 0 by NAT_D:def 2;

        hence thesis by A1, NAT_D:def 2;

      end;

        suppose

         A2: n > 0 ;



        then

         A3: (p * q) = (p * ((n * (q div n)) + (q mod n))) by NAT_D: 2

        .= (((p * n) * (q div n)) + (p * (q mod n)));

        per cases ;

          suppose p = 0 ;

          hence thesis by NAT_D:def 2;

        end;

          suppose p > 0 ;

          then (p * (q mod n)) < (p * n) by A2, NAT_D: 1, XREAL_1: 68;

          hence thesis by A3, NAT_D:def 2;

        end;

      end;

    end;

    theorem :: INT_4:21



     Th21: n > 0 & p is prime & (p,q) are_coprime implies not p divides (q mod (p |^ n))

    proof

      assume that

       A1: n > 0 and

       A2: p is prime and

       A3: (p,q) are_coprime ;

      n >= ( 0 + 1) by A1, NAT_1: 13;

      then (p |^ 1) divides (p |^ n) by NEWTON: 89;

      then p divides (p |^ n);

      then

       A4: p divides ((p |^ n) * (q div (p |^ n))) by NAT_D: 9;

      q = (((p |^ n) * (q div (p |^ n))) + (q mod (p |^ n))) by A2, NAT_D: 2;

      hence thesis by A2, A3, A4, Lm6, NAT_D: 8;

    end;

    theorem :: INT_4:22



     Th22: for p,q,n be Nat st n > 0 holds ((p - q) mod n) = 0 iff (p mod n) = (q mod n)

    proof

      let p,q,n be Nat;

      assume

       A1: n > 0 ;

      thus ((p - q) mod n) = 0 implies (p mod n) = (q mod n)

      proof

        assume ((p - q) mod n) = 0 ;

        then n divides (p - q) by A1, INT_1: 62;

        then

        consider s be Integer such that

         A2: (n * s) = (p - q);

        per cases by XXREAL_0: 1;

          suppose p > q;

          then s > 0 by A2, XREAL_1: 50;

          then s in NAT by INT_1: 3;

          then

          reconsider s9 = s as Nat;

          (p mod n) = (((n * s9) + q) mod n) by A2

          .= (q mod n) by NAT_D: 21;

          hence thesis;

        end;

          suppose p = q;

          hence thesis;

        end;

          suppose

           A3: p < q;



           A4: (q - p) = (n * ( - s)) by A2;

          then ( - s) > 0 by A3, XREAL_1: 50;

          then ( - s) in NAT by INT_1: 3;

          then

          reconsider s9 = ( - s) as Nat;

          (q - p) = (n * s9) by A4;



          then (q mod n) = (((n * s9) + p) mod n)

          .= (p mod n) by NAT_D: 21;

          hence thesis;

        end;

      end;

      assume

       A5: (p mod n) = (q mod n);

      p = ((n * (p div n)) + (p mod n)) by A1, NAT_D: 2

      .= ((n * (p div n)) + (q - (n * (q div n)))) by A1, A5, NEWTON: 63

      .= (q + (n * ((p div n) - (q div n))));

      then n divides (p - q);

      hence thesis by A1, INT_1: 62;

    end;

    theorem :: INT_4:23

    for a,b,m be Nat st m > 0 holds (a mod m) = (b mod m) iff m divides (a - b)

    proof

      let a,b,m be Nat;

      assume

       A1: m > 0 ;

      thus (a mod m) = (b mod m) implies m divides (a - b)

      proof

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

        then ((a - b) mod m) = 0 by A1, Th22;

        hence thesis by A1, INT_1: 62;

      end;

      assume m divides (a - b);

      then ((a - b) mod m) = 0 by A1, INT_1: 62;

      hence thesis by A1, Th22;

    end;

    theorem :: INT_4:24

    n > 0 & p is prime & (p,q) are_coprime implies not ex x be Integer st (((p * (x ^2 )) - q) mod (p |^ n)) = 0

    proof

      assume that

       A1: n > 0 and

       A2: p is prime and

       A3: (p,q) are_coprime ;

      given x such that

       A4: (((p * (x ^2 )) - q) mod (p |^ n)) = 0 ;

      ((p * (x ^2 )) mod (p |^ n)) = (q mod (p |^ n)) by A2, A4, Th22;

      then (p * ((x ^2 ) mod (p |^ (n -' 1)))) = (q mod (p |^ n)) by A1, A2, Th19;

      then p divides (q mod (p |^ n));

      hence contradiction by A1, A2, A3, Th21;

    end;

    theorem :: INT_4:25

    n > 0 & p is prime & (p,q) are_coprime implies not ex x be Integer st (((p * x) - q) mod (p |^ n)) = 0

    proof

      assume that

       A1: n > 0 and

       A2: p is prime and

       A3: (p,q) are_coprime ;



       A4: p > 1 by A2, INT_2:def 4;

      given x be Integer such that

       A5: (((p * x) - q) mod (p |^ n)) = 0 ;

      per cases ;

        suppose x >= 0 ;

        then x in NAT by INT_1: 3;

        then

        reconsider x as Nat;

        ((p * x) mod (p |^ n)) = (q mod (p |^ n)) by A2, A5, Th22;

        then (p * (x mod (p |^ (n -' 1)))) = (q mod (p |^ n)) by A1, A2, Th19;

        then p divides (q mod (p |^ n));

        hence contradiction by A1, A2, A3, Th21;

      end;

        suppose x < 0 ;

        then ( - x) in NAT by INT_1: 3;

        then

        reconsider l = ( - x) as Nat;



         A6: p divides (p * l);

        (p |^ n) divides ((p * x) - q) by A2, A5, INT_1: 62;

        then (p |^ n) divides (( - 1) * ((p * x) - q)) by INT_2: 2;

        then

        consider k be Integer such that

         A7: ((p * l) + q) = ((p |^ n) * k);

        k >= 0 by A2, A7, XREAL_1: 132;

        then k in NAT by INT_1: 3;

        then

        reconsider k as Nat;

        ((p * l) + q) = ((p |^ n) * k) by A7;

        then

         A8: (p |^ n) divides ((p * l) + q);

        p divides (p |^ n) by A1, NAT_3: 3;

        then

         A9: p divides ((p * l) + q) by A8, NAT_D: 4;

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

        (p gcd q) > 1 by A4, A9, A6, NAT_D: 10, NEWTON: 49;

        hence contradiction by A3, INT_2:def 3;

      end;

    end;

    begin

    definition

      let m be Integer;

      :: INT_4:def1

      func Cong (m) -> Relation of INT means

      : Def1: [x, y] in it iff (x,y) are_congruent_mod m;

      existence

      proof

        defpred Z[ Element of INT , Element of INT ] means ($1,$2) are_congruent_mod m;

        consider R be Relation of INT , INT such that

         A1: for x be Element of INT , y be Element of INT holds [x, y] in R iff Z[x, y] from RELSET_1:sch 2;

        take R;

        let x, y;

        for x,y be Integer holds [x, y] in R iff (x,y) are_congruent_mod m

        proof

          let x,y be Integer;

          reconsider x, y as Element of INT by INT_1:def 2;

           [x, y] in R iff Z[x, y] by A1;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let P1,P2 be Relation of INT such that

         A2: [x, y] in P1 iff (x,y) are_congruent_mod m and

         A3: [x, y] in P2 iff (x,y) are_congruent_mod m;



         A4: for x, y holds [x, y] in P1 iff [x, y] in P2 by A2, A3;

        thus P1 c= P2

        proof

          let a be object;

          assume

           A5: a in P1;

          then

          consider x,y be object such that

           A6: a = [x, y] and

           A7: x in INT & y in INT by RELSET_1: 2;

          reconsider x, y as Integer by A7;

           [x, y] in P2 by A4, A5, A6;

          hence thesis by A6;

        end;

        let a be object;

        assume

         A8: a in P2;

        then

        consider x,y be object such that

         A9: a = [x, y] and

         A10: x in INT & y in INT by RELSET_1: 2;

        reconsider x, y as Integer by A10;

         [x, y] in P1 by A4, A8, A9;

        hence thesis by A9;

      end;

    end

    registration

      let m be Integer;

      cluster ( Cong m) -> total;

      coherence

      proof

        thus ( dom ( Cong m)) c= INT ;

        thus INT c= ( dom ( Cong m))

        proof

          let x be object;

          assume x in INT ;

          then

          reconsider x as Integer;

          (x,x) are_congruent_mod m by INT_1: 11;

          then [x, x] in ( Cong m) by Def1;

          hence thesis by XTUPLE_0:def 12;

        end;

      end;

    end



     Lm8: ( Cong m) is Equivalence_Relation of INT

    proof



       A1: ( Cong m) is_symmetric_in INT

      proof

        let x,y be object;

        assume that

         A2: x in INT and

         A3: y in INT and

         A4: [x, y] in ( Cong m);

        reconsider y as Integer by A3;

        reconsider x as Integer by A2;

        (x,y) are_congruent_mod m by A4, Def1;

        then (y,x) are_congruent_mod m by INT_1: 14;

        hence thesis by Def1;

      end;



       A5: ( Cong m) is_transitive_in INT

      proof

        let x,y,z be object;

        assume that

         A6: x in INT & y in INT & z in INT and

         A7: [x, y] in ( Cong m) & [y, z] in ( Cong m);

        reconsider x, y, z as Integer by A6;

        (x,y) are_congruent_mod m & (y,z) are_congruent_mod m by A7, Def1;

        then (x,z) are_congruent_mod m by INT_1: 15;

        hence thesis by Def1;

      end;

      ( field ( Cong m)) = INT by ORDERS_1: 12;

      hence thesis by A1, A5, RELAT_2:def 11, RELAT_2:def 16;

    end;

    registration

      let m be Integer;

      cluster ( Cong m) -> reflexive symmetric transitive;

      coherence by Lm8;

    end

    theorem :: INT_4:26



     Th26: m <> 0 & (((a * x) - b) mod m) = 0 implies for y be Integer holds ((a,m) are_coprime & (((a * y) - b) mod m) = 0 implies y in ( Class (( Cong m),x))) & (y in ( Class (( Cong m),x)) implies (((a * y) - b) mod m) = 0 )

    proof

      assume that

       A1: m <> 0 and

       A2: (((a * x) - b) mod m) = 0 ;

      let y be Integer;

      hereby

        assume that

         A3: (a,m) are_coprime and

         A4: (((a * y) - b) mod m) = 0 ;

        (((a * x) - b),((a * y) - b)) are_congruent_mod m by A1, A2, A4, NAT_D: 64;

        then ((((a * x) - b) + b),(a * y)) are_congruent_mod m;

        then (x,y) are_congruent_mod m by A3, Th9;

        then [x, y] in ( Cong m) by Def1;

        hence y in ( Class (( Cong m),x)) by EQREL_1: 18;

      end;

      assume y in ( Class (( Cong m),x));

      then [x, y] in ( Cong m) by EQREL_1: 18;

      then (x,y) are_congruent_mod m by Def1;

      then

       A5: ((x * a),(y * a)) are_congruent_mod m by Th11;

      (((a * x) - b) mod m) = ( 0 mod m) by A2, Th12;

      then ( 0 ,((a * x) - b)) are_congruent_mod m by A1, NAT_D: 64;

      then (( 0 + b),(a * x)) are_congruent_mod m;

      then (( 0 + b),(a * y)) are_congruent_mod m by A5, INT_1: 15;

      then ( 0 ,((a * y) - b)) are_congruent_mod m;

      then (((a * y) - b) mod m) = ( 0 mod m) by NAT_D: 64;

      hence thesis by Th12;

    end;

    theorem :: INT_4:27

    for a,b,m,x be Integer holds m <> 0 & (a,m) are_coprime & (((a * x) - b) mod m) = 0 implies ex s be Integer st [x, (b * s)] in ( Cong m)

    proof

      let a, b, m, x;

      assume that

       A1: m <> 0 and

       A2: (a,m) are_coprime and

       A3: (((a * x) - b) mod m) = 0 ;

      (a gcd m) = 1 by A2, INT_2:def 3;

      then

      consider r,t be Integer such that

       A4: 1 = ((r * a) + (t * m)) by NAT_D: 68;

      (((a * x) - b) mod m) = ( 0 mod m) by A3, Th12;

      then (((a * x) - b), 0 ) are_congruent_mod m by A1, NAT_D: 64;

      then ((((a * x) - b) * r),( 0 * r)) are_congruent_mod m by Th11;

      then (((x * (a * r)) - (b * r)), 0 ) are_congruent_mod m;

      then

       A5: (((x * (1 - (t * m))) - (b * r)), 0 ) are_congruent_mod m by A4;

      take s = r;

      (((x - ((x * t) * m)) - (b * r)) mod m) = (((x - (b * r)) + ((( - x) * t) * m)) mod m)

      .= ((x - (b * r)) mod m) by NAT_D: 61;

      then ((x - (b * r)) mod m) = ( 0 mod m) by A5, NAT_D: 64;

      then ( 0 ,(x - (b * r))) are_congruent_mod m by A1, NAT_D: 64;

      then (( 0 + (b * r)),x) are_congruent_mod m;

      then (x,(b * s)) are_congruent_mod m by INT_1: 14;

      hence thesis by Def1;

    end;

    theorem :: INT_4:28

    for a,m be Element of NAT st a <> 0 & m > 1 & (a,m) are_coprime holds for b,x be Integer holds (((a * x) - b) mod m) = 0 implies [x, (b * (a |^ (( Euler m) -' 1)))] in ( Cong m)

    proof

      let a,m be Element of NAT ;

      assume that

       A1: a <> 0 and

       A2: m > 1 and

       A3: (a,m) are_coprime ;

      let b,x be Integer;

      ((a |^ ( Euler m)) mod m) = 1 by A1, A2, A3, EULER_2: 18;

      then (a |^ ( Euler m)) = ((m * ((a |^ ( Euler m)) div m)) + 1) by A2, NAT_D: 2;

      then m divides ((a |^ ( Euler m)) - 1);

      then ((a |^ ( Euler m)),1) are_congruent_mod m;

      then

       A4: (((a |^ ( Euler m)) * x),(1 * x)) are_congruent_mod m by Th11;

      ( Euler m) <> 0

      proof

        set X = { k where k be Element of NAT : (m,k) are_coprime & k >= 1 & k <= m };

        (1 gcd m) = 1 by NEWTON: 51;

        then (m,1) are_coprime by INT_2:def 3;

        then

         A5: 1 in X by A2;

        assume ( Euler m) = 0 ;

        hence contradiction by A5;

      end;



      then

       A6: ((( Euler m) -' 1) + 1) = ((( Euler m) - 1) + 1) by NAT_1: 14, XREAL_1: 233

      .= ( Euler m);

      assume (((a * x) - b) mod m) = 0 ;

      then m divides (((a * x) - b) - 0 ) by A2, INT_1: 62;

      then (((a * x) - b), 0 ) are_congruent_mod m;

      then ( 0 ,((a * x) - b)) are_congruent_mod m by INT_1: 14;

      then (((a |^ (( Euler m) -' 1)) * 0 qua Nat),((a |^ (( Euler m) -' 1)) * ((a * x) - b))) are_congruent_mod m by Th11;

      then ( 0 ,((((a |^ (( Euler m) -' 1)) * a) * x) - ((a |^ (( Euler m) -' 1)) * b))) are_congruent_mod m;

      then ( 0 ,(((a |^ ((( Euler m) -' 1) + 1)) * x) - ((a |^ (( Euler m) -' 1)) * b))) are_congruent_mod m by NEWTON: 6;

      then (( 0 + ((a |^ (( Euler m) -' 1)) * b)),((a |^ ( Euler m)) * x)) are_congruent_mod m by A6;

      then (((a |^ (( Euler m) -' 1)) * b),x) are_congruent_mod m by A4, INT_1: 15;

      then (x,(b * (a |^ (( Euler m) -' 1)))) are_congruent_mod m by INT_1: 14;

      hence thesis by Def1;

    end;

    theorem :: INT_4:29

    m <> 0 & (a gcd m) divides b implies ex fp be FinSequence of INT st ( len fp) = (a gcd m) & (for c st c in ( dom fp) holds (((a * (fp . c)) - b) mod m) = 0 ) & for c1, c2 st c1 in ( dom fp) & c2 in ( dom fp) & c1 <> c2 holds not ((fp . c1),(fp . c2)) are_congruent_mod m

    proof

      assume that

       A1: m <> 0 and

       A2: (a gcd m) divides b;

      set l = (a gcd m);

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

      consider a1,m1 be Integer such that

       A3: a = (l * a1) and

       A4: m = (l * m1) and

       A5: (a1,m1) are_coprime by A1, INT_2: 23;

      consider b1 be Integer such that

       A6: b = (l * b1) by A2;

      consider x1 be Integer such that

       A7: (((a1 * x1) - b1) mod m1) = 0 by A5, Th15;

      deffunc P( Nat) = (x1 + (($1 - 1) * m1));

      consider fp be FinSequence such that

       A8: ( len fp) = l & for c be Nat st c in ( dom fp) holds (fp . c) = P(c) from FINSEQ_1:sch 2;

      for c be Nat st c in ( dom fp) holds (fp . c) in INT

      proof

        let c be Nat;

        assume c in ( dom fp);

        then (fp . c) = (x1 + ((c - 1) * m1)) by A8;

        hence thesis by INT_1:def 2;

      end;

      then

      reconsider fp as FinSequence of INT by FINSEQ_2: 12;



       A9: m1 <> 0 by A1, A4;



       A10: for c1, c2 st c1 in ( dom fp) & c2 in ( dom fp) & c1 <> c2 holds not ((fp . c1),(fp . c2)) are_congruent_mod m

      proof

        let c1, c2;

        assume that

         A11: c1 in ( dom fp) and

         A12: c2 in ( dom fp) and

         A13: c1 <> c2;

        assume

         A14: ((fp . c1),(fp . c2)) are_congruent_mod m;

        (fp . c1) = (x1 + ((c1 - 1) * m1)) & (fp . c2) = (x1 + ((c2 - 1) * m1)) by A8, A11, A12;

        then m divides ((((c1 - 1) * m1) + x1) - (((c2 - 1) * m1) + x1)) by A14;

        then

        consider w be Integer such that

         A15: ((c1 - c2) * m1) = ((l * m1) * w) by A4;

        ((c1 - c2) * m1) = ((l * w) * m1) by A15;

        then (c1 - c2) = (l * w) by A9, XCMPLX_1: 5;

        then

         A16: l divides (c1 - c2);



         A17: c2 in ( Seg l) by A8, A12, FINSEQ_1:def 3;

        then

         A18: c2 >= 1 by FINSEQ_1: 1;



         A19: c1 in ( Seg l) by A8, A11, FINSEQ_1:def 3;

        then c1 <= l by FINSEQ_1: 1;

        then (c1 - c2) <= (l - 1) by A18, XREAL_1: 13;

        then

         A20: (c1 - c2) < l by XREAL_1: 147;



         A21: c2 <= l by A17, FINSEQ_1: 1;

        c1 >= 1 by A19, FINSEQ_1: 1;

        then (c1 - c2) >= (1 - l) by A21, XREAL_1: 13;

        then (c1 - c2) > ( - l) by XREAL_1: 145;

        then

         A22: |.(c1 - c2).| < l by A20, SEQ_2: 1;

        (c1 - c2) <> 0 by A13;

        then |.l.| <= |.(c1 - c2).| by A16, Th6;

        hence contradiction by A22, ABSVALUE:def 1;

      end;

      take fp;

      (((a1 * x1) - b1) mod m1) = ( 0 mod m1) by A7, Th12;

      then (((a1 * x1) - b1), 0 ) are_congruent_mod m1 by A9, NAT_D: 64;

      then ((((a1 * x1) - b1) * l),( 0 * l)) are_congruent_mod (m1 * l) by Th10;

      then

       A23: (((a * x1) - b) mod m) = ( 0 mod m) by A3, A4, A6, NAT_D: 64;

      for c st c in ( dom fp) holds (((a * (fp . c)) - b) mod m) = 0

      proof

        let c;

        assume c in ( dom fp);



        hence (((a * (fp . c)) - b) mod m) = (((a * (x1 + ((c - 1) * m1))) - b) mod m) by A8

        .= ((((a * x1) - b) + ((a1 * (c - 1)) * m)) mod m) by A3, A4

        .= (((a * x1) - b) mod m) by NAT_D: 61

        .= 0 by A23, Th12;

      end;

      hence thesis by A8, A10;

    end;

    begin

    reserve fp,fp1 for FinSequence of NAT ,

b,c,d,n for Element of NAT ,

a for Nat;

    theorem :: INT_4:30



     Th30: for b, n st b in ( dom fp) & ( len fp) = (n + 1) holds ( Del ((fp ^ <*d*>),b)) = (( Del (fp,b)) ^ <*d*>)

    proof

      let b, n such that

       A1: b in ( dom fp) and

       A2: ( len fp) = (n + 1);



       A3: ( len ( Del (fp,b))) = n by A1, A2, FINSEQ_3: 109;

      then

       A4: ( len (( Del (fp,b)) ^ <*d*>)) = (n + 1) by FINSEQ_2: 16;



       A5: ( len (fp ^ <*d*>)) = ((n + 1) + 1) & b in ( dom (fp ^ <*d*>)) by A1, A2, FINSEQ_2: 16, FINSEQ_3: 22;

      then

       A6: ( len ( Del ((fp ^ <*d*>),b))) = ( len (( Del (fp,b)) ^ <*d*>)) by A4, FINSEQ_3: 109;

      for k be Nat st 1 <= k & k <= ( len ( Del ((fp ^ <*d*>),b))) holds (( Del ((fp ^ <*d*>),b)) . k) = ((( Del (fp,b)) ^ <*d*>) . k)

      proof

        let k be Nat such that

         A7: 1 <= k and

         A8: k <= ( len ( Del ((fp ^ <*d*>),b)));



         A9: k in ( dom fp) by A2, A4, A6, A7, A8, FINSEQ_3: 25;

        per cases ;

          suppose

           A10: k < b;

          b <= (n + 1) by A1, A2, FINSEQ_3: 25;

          then k < (n + 1) by A10, XXREAL_0: 2;

          then k <= n by NAT_1: 13;

          then k in ( dom ( Del (fp,b))) by A3, A7, FINSEQ_3: 25;



          then

           A11: ((( Del (fp,b)) ^ <*d*>) . k) = (( Del (fp,b)) . k) by FINSEQ_1:def 7

          .= (fp . k) by A10, FINSEQ_3: 110;

          set fpd = (fp ^ <*d*>);

          (( Del (fpd,b)) . k) = (fpd . k) by A10, FINSEQ_3: 110

          .= (fp . k) by A9, FINSEQ_1:def 7;

          hence thesis by A11;

        end;

          suppose

           A12: b <= k;

          then

           A13: (( Del ((fp ^ <*d*>),b)) . k) = ((fp ^ <*d*>) . (k + 1)) by A4, A5, A6, A8, FINSEQ_3: 111;

          per cases by A4, A6, A8, NAT_1: 8;

            suppose

             A14: k <= n;

            then k in ( dom ( Del (fp,b))) by A3, A7, FINSEQ_3: 25;



            then

             A15: ((( Del (fp,b)) ^ <*d*>) . k) = (( Del (fp,b)) . k) by FINSEQ_1:def 7

            .= (fp . (k + 1)) by A1, A2, A12, A14, FINSEQ_3: 111;



             A16: (k + 1) >= 1 by NAT_1: 11;

            (k + 1) <= (n + 1) by A14, XREAL_1: 6;

            then (k + 1) in ( dom fp) by A2, A16, FINSEQ_3: 25;

            hence thesis by A13, A15, FINSEQ_1:def 7;

          end;

            suppose

             A17: k = (n + 1);

            then (( Del ((fp ^ <*d*>),b)) . k) = d by A2, A13, FINSEQ_1: 42;

            hence thesis by A3, A17, FINSEQ_1: 42;

          end;

        end;

      end;

      hence thesis by A4, A5, FINSEQ_3: 109;

    end;

    theorem :: INT_4:31



     Th31: ( len fp) >= 2 & (for b, c st b in ( dom fp) & c in ( dom fp) & b <> c holds ((fp . b) gcd (fp . c)) = 1) implies for b st b in ( dom fp) holds (( Product ( Del (fp,b))) gcd (fp . b)) = 1

    proof

      defpred CC[ FinSequence of NAT ] means for b st b in ( dom $1) holds (( Product ( Del ($1,b))) gcd ($1 . b)) = 1;

      defpred RP[ FinSequence of NAT ] means for b, c st b in ( dom $1) & c in ( dom $1) & b <> c holds (($1 . b) gcd ($1 . c)) = 1;

      defpred TH[ set] means ex f be FinSequence of NAT st f = $1 & (( len f) >= 2 & RP[f] implies CC[f]);

       A1:

      now

        let fp, d such that

         A2: TH[fp];

        set k = ( len fp);

        set fp1 = (fp ^ <*d*>);

        now

          assume that

           A3: ( len fp1) >= 2 and

           A4: RP[fp1];



           A5: ( len fp1) = (k + 1) by FINSEQ_2: 16;

          now

            per cases by A3, XXREAL_0: 1;

              suppose

               A6: ( len fp1) = 2;

              then 1 in ( dom fp1) & 2 in ( dom fp1) by FINSEQ_3: 25;

              then

               A7: ((fp1 . 2) gcd (fp1 . 1)) = 1 by A4;



               A8: fp1 = <*(fp1 . 1), (fp1 . 2)*> by A6, FINSEQ_1: 44;

              for b st b in ( dom fp1) holds (( Product ( Del (fp1,b))) gcd (fp1 . b)) = 1

              proof

                let b;

                assume b in ( dom fp1);

                then

                 A9: b in ( Seg ( len fp1)) by FINSEQ_1:def 3;

                per cases by A6, A9, FINSEQ_1: 2, TARSKI:def 2;

                  suppose b = 1;



                  hence (( Product ( Del (fp1,b))) gcd (fp1 . b)) = (( Product <*(fp1 . 2)*>) gcd (fp1 . 1)) by A8, WSIERP_1: 19

                  .= 1 by A7, RVSUM_1: 95;

                end;

                  suppose b = 2;



                  hence (( Product ( Del (fp1,b))) gcd (fp1 . b)) = (( Product <*(fp1 . 1)*>) gcd (fp1 . 2)) by A8, WSIERP_1: 19

                  .= 1 by A7, RVSUM_1: 95;

                end;

              end;

              hence CC[fp1];

            end;

              suppose ( len fp1) > 2;

              then

               A10: (k + 1) > (1 + 1) by FINSEQ_2: 16;

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

              then

              consider n be Nat such that

               A11: k = (n + 1) by NAT_1: 6;



               A12: RP[fp]

              proof



                 A13: ( dom fp) c= ( dom fp1) by FINSEQ_1: 26;

                let b, c such that

                 A14: b in ( dom fp) & c in ( dom fp) and

                 A15: b <> c;

                (fp1 . b) = (fp . b) & (fp1 . c) = (fp . c) by A14, FINSEQ_1:def 7;

                hence thesis by A4, A14, A15, A13;

              end;



               A16: a in ( dom fp) implies ((fp . a) gcd d) = 1

              proof



                 A17: (( len fp) + 1) in ( dom fp1) by A5, FINSEQ_5: 6;



                 A18: ( dom fp) c= ( dom fp1) & (fp1 . (( len fp) + 1)) = d by FINSEQ_1: 26, FINSEQ_1: 42;

                assume

                 A19: a in ( dom fp);

                (( len fp) + 1) > ( len fp) by NAT_1: 13;

                then

                 A20: (( len fp) + 1) <> a by A19, FINSEQ_3: 25;

                (fp1 . a) = (fp . a) by A19, FINSEQ_1:def 7;

                hence thesis by A4, A19, A18, A20, A17;

              end;

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



               A21: k = (n + 1) by A11;

              for b st b in ( dom fp1) holds (( Product ( Del (fp1,b))) gcd (fp1 . b)) = 1

              proof

                let b such that

                 A22: b in ( dom fp1);



                 A23: b >= 1 by A22, FINSEQ_3: 25;



                 A24: b <= (k + 1) by A5, A22, FINSEQ_3: 25;

                per cases by A24, NAT_1: 8;

                  suppose b <= k;

                  then

                   A25: b in ( dom fp) by A23, FINSEQ_3: 25;

                  then (( Product ( Del (fp,b))) gcd (fp . b)) = 1 & ((fp . b) gcd d) = 1 by A2, A10, A12, A16, NAT_1: 13;

                  then ((( Product ( Del (fp,b))) * d) gcd (fp . b)) = 1 by WSIERP_1: 7;

                  then

                   A26: (( Product (( Del (fp,b)) ^ <*d*>)) gcd (fp . b)) = 1 by RVSUM_1: 96;

                  ( Del (fp1,b)) = (( Del (fp,b)) ^ <*d*>) by A21, A25, Th30;

                  hence thesis by A25, A26, FINSEQ_1:def 7;

                end;

                  suppose b = (k + 1);



                  hence (( Product ( Del (fp1,b))) gcd (fp1 . b)) = (( Product ( Del (fp1,(k + 1)))) gcd d) by FINSEQ_1: 42

                  .= (( Product fp) gcd d) by WSIERP_1: 40

                  .= 1 by A16, WSIERP_1: 36;

                end;

              end;

              hence CC[fp1];

            end;

          end;

          hence CC[fp1];

        end;

        hence TH[fp1];

      end;



       A27: TH[( <*> NAT )]

      proof

        take ( <*> NAT );

        thus thesis;

      end;

      for fp holds TH[fp] from FINSEQ_2:sch 2( A27, A1);

      then ex f be FinSequence of NAT st f = fp & (( len f) >= 2 & RP[f] implies CC[f]);

      hence thesis;

    end;

    theorem :: INT_4:32



     Th32: for a st a in ( dom fp) holds (fp . a) divides ( Product fp)

    proof

      let a;

      assume a in ( dom fp);

      then (fp . a) in ( rng fp) by FUNCT_1: 3;

      hence thesis by NAT_3: 7;

    end;

    theorem :: INT_4:33

    a in ( dom fp) & p divides (fp . a) implies p divides ( Product fp)

    proof

      assume that

       A1: a in ( dom fp) and

       A2: p divides (fp . a);

      (fp . a) divides ( Product fp) by A1, Th32;

      hence thesis by A2, NAT_D: 4;

    end;

    theorem :: INT_4:34

    ( len fp) = (n + 1) & a >= 1 & a <= n implies (( Del (fp,a)) . n) = (fp . ( len fp))

    proof

      assume that

       A1: ( len fp) = (n + 1) and

       A2: a >= 1 and

       A3: a <= n;

      n < (n + 1) by XREAL_1: 29;

      then a < (n + 1) by A3, XXREAL_0: 2;

      then a in ( dom fp) by A1, A2, FINSEQ_3: 25;

      hence thesis by A1, A3, WSIERP_1:def 1;

    end;

    theorem :: INT_4:35



     Th35: for a, b st a in ( dom fp) & b in ( dom fp) & a <> b & ( len fp) >= 1 holds (fp . b) divides ( Product ( Del (fp,a)))

    proof

      let a, b;

      assume that

       A1: a in ( dom fp) and

       A2: b in ( dom fp) and

       A3: a <> b and

       A4: ( len fp) >= 1;

      consider n be Nat such that

       A5: ( len fp) = (n + 1) by A4, NAT_1: 6;



       A6: a <= (n + 1) by A1, A5, FINSEQ_3: 25;



       A7: a >= 1 by A1, FINSEQ_3: 25;



       A8: b >= 1 by A2, FINSEQ_3: 25;



       A9: (( len ( Del (fp,a))) + 1) = (n + 1) by A1, A5, WSIERP_1:def 1;



       A10: b <= (n + 1) by A2, A5, FINSEQ_3: 25;

      per cases by A6, NAT_1: 8;

        suppose

         A11: a <= n;

        per cases by A3, XXREAL_0: 1;

          suppose

           A12: b < a;

          then b <= n by A11, XXREAL_0: 2;

          then

           A13: b in ( dom ( Del (fp,a))) by A8, A9, FINSEQ_3: 25;

          (( Del (fp,a)) . b) = (fp . b) by A1, A12, WSIERP_1:def 1;

          hence thesis by A13, Th32;

        end;

          suppose

           A14: a < b;

          then b >= (a + 1) by NAT_1: 13;

          then (b - 1) >= a by XREAL_1: 19;

          then (b -' 1) >= a by A8, XREAL_1: 233;

          then

           A15: (( Del (fp,a)) . (b -' 1)) = (fp . ((b -' 1) + 1)) by A1, WSIERP_1:def 1;

          b > 1 by A7, A14, XXREAL_0: 2;

          then (b - 1) > 0 by XREAL_1: 50;

          then (b -' 1) > 0 by A8, XREAL_1: 233;

          then

           A16: (b -' 1) >= 1 by Lm7;

          (b - 1) <= ((n + 1) - 1) by A10, XREAL_1: 9;

          then (b -' 1) <= n by A8, XREAL_1: 233;

          then (b -' 1) in ( dom ( Del (fp,a))) by A9, A16, FINSEQ_3: 25;

          then (( Del (fp,a)) . (b -' 1)) divides ( Product ( Del (fp,a))) by Th32;

          hence thesis by A8, A15, XREAL_1: 235;

        end;

      end;

        suppose

         A17: a = (n + 1);

        then b < (n + 1) by A3, A10, XXREAL_0: 1;

        then b <= n by NAT_1: 13;

        then

         A18: b in ( dom ( Del (fp,a))) by A8, A9, FINSEQ_3: 25;

        b < a by A3, A10, A17, XXREAL_0: 1;

        then (( Del (fp,a)) . b) = (fp . b) by A1, WSIERP_1:def 1;

        hence thesis by A18, Th32;

      end;

    end;



     Lm9: for i1,i2 be Integer holds for n be Nat st n > 0 & (i1 mod n) = 0 holds ((i1 * i2) mod n) = 0

    proof

      let i1,i2 be Integer, n be Nat;

      assume that

       A1: n > 0 and

       A2: (i1 mod n) = 0 ;

      n divides i1 by A1, A2, INT_1: 62;

      then n divides (i1 * i2) by INT_2: 2;

      hence thesis by A1, INT_1: 62;

    end;

    theorem :: INT_4:36



     Th36: (for b be Nat st b in ( dom fp) holds a divides (fp . b)) implies a divides ( Sum fp)

    proof

      defpred RP[ FinSequence of NAT ] means for b be Nat st b in ( dom $1) holds a divides ($1 . b);

      defpred CC[ FinSequence of NAT ] means a divides ( Sum $1);

      defpred TH[ set] means ex f be FinSequence of NAT st f = $1 & ( RP[f] implies CC[f]);

       A1:

      now

        let fp, d such that

         A2: TH[fp];

        set fp1 = (fp ^ <*d*>);

        now

          assume

           A3: RP[fp1];



           A4: RP[fp]

          proof

            let b be Nat such that

             A5: b in ( dom fp);

            ( dom fp) c= ( dom fp1) & (fp1 . b) = (fp . b) by A5, FINSEQ_1: 26, FINSEQ_1:def 7;

            hence thesis by A3, A5;

          end;

          ( len fp1) in ( dom fp1) by FINSEQ_5: 6;

          then a divides (fp1 . ( len fp1)) by A3;

          then a divides (fp1 . (( len fp) + 1)) by FINSEQ_2: 16;

          then a divides d by FINSEQ_1: 42;

          then a divides (( Sum fp) + d) by A2, A4, NAT_D: 8;

          hence CC[fp1] by RVSUM_1: 74;

        end;

        hence TH[fp1];

      end;



       A6: TH[( <*> NAT )] by NAT_D: 6, RVSUM_1: 72;

      for fp holds TH[fp] from FINSEQ_2:sch 2( A6, A1);

      then ex f be FinSequence of NAT st f = fp & ( RP[f] implies CC[f]);

      hence thesis;

    end;

    theorem :: INT_4:37

    ( len fp) >= 2 & (for b, c st b in ( dom fp) & c in ( dom fp) & b <> c holds ((fp . b) gcd (fp . c)) = 1) & (for b st b in ( dom fp) holds (fp . b) <> 0 ) implies for fp1 holds ex x be Integer st for b st b in ( dom fp) holds ((x - (fp1 . b)) mod (fp . b)) = 0

    proof

      assume that

       A1: ( len fp) >= 2 and

       A2: for b, c st b in ( dom fp) & c in ( dom fp) & b <> c holds ((fp . b) gcd (fp . c)) = 1 and

       A3: for b st b in ( dom fp) holds (fp . b) <> 0 ;

      consider fp2 be FinSequence of NAT , q be Element of NAT such that

       A4: fp = (fp2 ^ <*q*>) by A1, FINSEQ_2: 19;

      deffunc F( Nat) = { l where l be Element of NAT : (((( Product ( Del (fp,$1))) * l) - 1) mod (fp . $1)) = 0 };

      defpred FF[ Nat, Nat] means $2 in F($1);



       A5: for a be Nat st a in ( Seg ( len fp)) holds ex n be Element of NAT st FF[a, n]

      proof

        let a be Nat;

        reconsider l = (fp . a) as Integer;

        assume a in ( Seg ( len fp));

        then

         A6: a in ( dom fp) by FINSEQ_1:def 3;

        then (( Product ( Del (fp,a))) gcd (fp . a)) = 1 by A1, A2, Th31;

        then

         A7: (( Product ( Del (fp,a))),l) are_coprime by INT_2:def 3;

        l <> 0 by A3, A6;

        then

        consider n be Nat such that

         A8: (((( Product ( Del (fp,a))) * n) - 1) mod l) = 0 by A7, Th16;

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

        take n;

        thus thesis by A8;

      end;

      consider s be FinSequence of NAT such that

       A9: ( dom s) = ( Seg ( len fp)) & for a be Nat st a in ( Seg ( len fp)) holds FF[a, (s . a)] from FINSEQ_1:sch 5( A5);

      let fp1;

      set k = ( len fp2);

      deffunc P( Nat) = ((( Product ( Del (fp,$1))) * (s . $1)) * (fp1 . $1));

      consider s1 be FinSequence such that

       A10: ( len s1) = (k + 1) & for a be Nat st a in ( dom s1) holds (s1 . a) = P(a) from FINSEQ_1:sch 2;

      for a be Nat st a in ( dom s1) holds (s1 . a) in NAT

      proof

        let a be Nat;

        assume

         A11: a in ( dom s1);

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

        (s1 . a) = ((( Product ( Del (fp,a))) * (s . a)) * (fp1 . a)) by A10, A11;

        hence thesis by ORDINAL1:def 12;

      end;

      then

      reconsider s1 as FinSequence of NAT by FINSEQ_2: 12;

      set x = ( Sum s1);

      take x;



       A12: ( len fp) = (k + 1) by A4, FINSEQ_2: 16;



       A13: for a, b st a in ( dom fp) & b in ( dom fp) & a <> b holds (fp . b) divides (s1 . a)

      proof

        let a, b;

        assume that

         A14: a in ( dom fp) and

         A15: b in ( dom fp) & a <> b;

        ( len fp) >= 1 by A1, XXREAL_0: 2;

        then (fp . b) divides (( Product ( Del (fp,a))) * ((s . a) * (fp1 . a))) by A14, A15, Th35, NAT_D: 9;

        then

         A16: (fp . b) divides ((( Product ( Del (fp,a))) * (s . a)) * (fp1 . a));

        a in ( dom s1) by A12, A10, A14, FINSEQ_3: 29;

        hence thesis by A10, A16;

      end;



       A17: for b st b in ( dom fp) holds (fp . b) divides ( Sum ( Del (s1,b)))

      proof

        let b;

        assume

         A18: b in ( dom fp);

        then b in ( Seg ( len s1)) by A12, A10, FINSEQ_1:def 3;

        then

         A19: b in ( dom s1) by FINSEQ_1:def 3;

        then

         A20: (( len ( Del (s1,b))) + 1) = (k + 1) by A10, WSIERP_1:def 1;

        for a st a in ( dom ( Del (s1,b))) holds (fp . b) divides (( Del (s1,b)) . a)

        proof

          let a;

          assume

           A21: a in ( dom ( Del (s1,b)));

          then

           A22: a >= 1 & a <= k by A20, FINSEQ_3: 25;

          ( dom ( Del (s1,b))) c= ( dom s1) by WSIERP_1: 39;

          then a in ( dom s1) by A21;

          then a in ( Seg (k + 1)) by A10, FINSEQ_1:def 3;

          then

           A23: a in ( dom fp) by A12, FINSEQ_1:def 3;

          per cases ;

            suppose

             A24: a < b;

            then (( Del (s1,b)) . a) = (s1 . a) by A19, WSIERP_1:def 1;

            hence thesis by A13, A18, A23, A24;

          end;

            suppose

             A25: a >= b;

            (a + 1) <= (k + 1) & (a + 1) > 1 by A22, XREAL_1: 6, XREAL_1: 29;

            then

             A26: (a + 1) in ( dom fp) by A12, FINSEQ_3: 25;

            (( Del (s1,b)) . a) = (s1 . (a + 1)) & (a + 1) > b by A19, A25, WSIERP_1:def 1, XREAL_1: 39;

            hence thesis by A13, A18, A26;

          end;

        end;

        hence thesis by Th36;

      end;

      for b st b in ( dom fp) holds ((x - (fp1 . b)) mod (fp . b)) = 0

      proof

        let b;

        assume

         A27: b in ( dom fp);

        then

         A28: (fp . b) <> 0 by A3;



         A29: (fp . b) divides ( Sum ( Del (s1,b))) by A17, A27;



         A30: ((( Sum ( Del (s1,b))) + ((s1 . b) - (fp1 . b))) mod (fp . b)) = (((s1 . b) - (fp1 . b)) mod (fp . b))

        proof

          reconsider l = ( Sum ( Del (s1,b))) as Integer;



           A31: (l mod (fp . b)) = 0 by A29, A28, INT_1: 62;

          ((( Sum ( Del (s1,b))) + ((s1 . b) - (fp1 . b))) mod (fp . b)) = (((l mod (fp . b)) + (((s1 . b) - (fp1 . b)) mod (fp . b))) mod (fp . b)) by NAT_D: 66

          .= (((s1 . b) - (fp1 . b)) mod (fp . b)) by A31, NAT_D: 65;

          hence thesis;

        end;



         A32: b >= 1 & b <= (k + 1) by A12, A27, FINSEQ_3: 25;

        then

         A33: b in ( Seg (k + 1));

        then b in ( dom s1) by A10, FINSEQ_1:def 3;



        then

         A34: ((s1 . b) - (fp1 . b)) = (((( Product ( Del (fp,b))) * (s . b)) * (fp1 . b)) - (1 * (fp1 . b))) by A10

        .= (((( Product ( Del (fp,b))) * (s . b)) - 1) * (fp1 . b));

        (s . b) in F(b) by A12, A9, A33;

        then

         A35: ex ll be Element of NAT st ll = (s . b) & (((( Product ( Del (fp,b))) * ll) - 1) mod (fp . b)) = 0 ;



         A36: s1 is FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

        b in ( dom s1) by A10, A32, FINSEQ_3: 25;



        then ((x - (fp1 . b)) mod (fp . b)) = (((( Sum ( Del (s1,b))) + (s1 . b)) - (fp1 . b)) mod (fp . b)) by WSIERP_1: 20, A36

        .= 0 by A28, A34, A35, A30, Lm9;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: INT_4:38



     Th38: (for b, c st b in ( dom fp) & c in ( dom fp) & b <> c holds ((fp . b) gcd (fp . c)) = 1) & (for b st b in ( dom fp) holds (fp . b) divides a) implies ( Product fp) divides a

    proof

      defpred RP[ FinSequence of NAT ] means (for b, c st b in ( dom $1) & c in ( dom $1) & b <> c holds (($1 . b) gcd ($1 . c)) = 1) & (for b st b in ( dom $1) holds ($1 . b) divides a);

      defpred CC[ FinSequence of NAT ] means ( Product $1) divides a;

      defpred TH[ set] means ex f be FinSequence of NAT st f = $1 & ( RP[f] implies CC[f]);

       A1:

      now

        let fp, d such that

         A2: TH[fp];

        set fp1 = (fp ^ <*d*>);

        (( len fp) + 1) >= ( 0 + 1) by XREAL_1: 6;

        then

         A3: ( len fp1) >= 1 by FINSEQ_2: 16;

        now

          assume

           A4: RP[fp1];

          for a st a in ( dom fp) holds ((fp . a) gcd d) = 1

          proof

            let a;



             A5: ( len fp1) in ( dom fp1) by A3, FINSEQ_3: 25;

            assume

             A6: a in ( dom fp);

            then a <= ( len fp) by FINSEQ_3: 25;

            then a < (( len fp) + 1) by XREAL_1: 39;

            then

             A7: a < ( len fp1) by FINSEQ_2: 16;

            a in ( dom fp1) by A6, FINSEQ_2: 15;

            then ((fp1 . a) gcd (fp1 . ( len fp1))) = 1 by A4, A7, A5;

            then

             A8: ((fp1 . a) gcd (fp1 . (( len fp) + 1))) = 1 by FINSEQ_2: 16;

            (fp1 . a) = (fp . a) by A6, FINSEQ_1:def 7;

            hence thesis by A8, FINSEQ_1: 42;

          end;

          then (( Product fp) gcd d) = 1 by WSIERP_1: 36;

          then

           A9: (( Product fp),d) are_coprime by INT_2:def 3;



           A10: ( dom fp) c= ( dom fp1) by FINSEQ_1: 26;



           A11: for b, c st b in ( dom fp) & c in ( dom fp) & b <> c holds ((fp . b) gcd (fp . c)) = 1

          proof

            let b, c;

            assume that

             A12: b in ( dom fp) & c in ( dom fp) and

             A13: b <> c;

            (fp1 . b) = (fp . b) & (fp1 . c) = (fp . c) by A12, FINSEQ_1:def 7;

            hence thesis by A4, A10, A12, A13;

          end;



           A14: for b st b in ( dom fp) holds (fp . b) divides a

          proof

            let b;

            assume

             A15: b in ( dom fp);

            then (fp1 . b) = (fp . b) by FINSEQ_1:def 7;

            hence thesis by A4, A10, A15;

          end;

          ( len fp1) in ( dom fp1) by FINSEQ_5: 6;

          then (fp1 . ( len fp1)) divides a by A4;

          then (fp1 . (( len fp) + 1)) divides a by FINSEQ_2: 16;

          then d divides a by FINSEQ_1: 42;

          then (( Product fp) * d) divides a by A2, A11, A14, A9, PEPIN: 4;

          hence CC[fp1] by RVSUM_1: 96;

        end;

        hence TH[fp1];

      end;



       A16: TH[( <*> NAT )]

      proof

        take ( <*> NAT );

        thus thesis by NAT_D: 6, RVSUM_1: 94;

      end;

      for fp holds TH[fp] from FINSEQ_2:sch 2( A16, A1);

      then ex f be FinSequence of NAT st f = fp & ( RP[f] implies CC[f]);

      hence thesis;

    end;

    theorem :: INT_4:39

    (for b, c st b in ( dom fp) & c in ( dom fp) & b <> c holds ((fp . b) gcd (fp . c)) = 1) & (for b st b in ( dom fp) holds (fp . b) > 0 ) implies for fp1 st (for b st b in ( dom fp) holds ((x - (fp1 . b)) mod (fp . b)) = 0 & ((y - (fp1 . b)) mod (fp . b)) = 0 ) holds (x,y) are_congruent_mod ( Product fp)

    proof

      assume that

       A1: for b, c st b in ( dom fp) & c in ( dom fp) & b <> c holds ((fp . b) gcd (fp . c)) = 1 and

       A2: for b st b in ( dom fp) holds (fp . b) > 0 ;

      let fp1 such that

       A3: for b st b in ( dom fp) holds ((x - (fp1 . b)) mod (fp . b)) = 0 & ((y - (fp1 . b)) mod (fp . b)) = 0 ;

      per cases ;

        suppose x >= y;

        then (x - y) in NAT by INT_1: 3, XREAL_1: 48;

        then

        reconsider k = (x - y) as Nat;

        for b st b in ( dom fp) holds (fp . b) divides k

        proof

          let b such that

           A4: b in ( dom fp);



           A5: (fp . b) > 0 by A2, A4;

          ((y - (fp1 . b)) mod (fp . b)) = 0 by A3, A4;

          then

           A6: (fp . b) divides (y - (fp1 . b)) by A5, INT_1: 62;

          ((x - (fp1 . b)) mod (fp . b)) = 0 by A3, A4;

          then (fp . b) divides (x - (fp1 . b)) by A5, INT_1: 62;

          then (fp . b) divides ((x - (fp1 . b)) - (y - (fp1 . b))) by A6, Lm4;

          then

          consider i be Integer such that

           A7: (x - y) = ((fp . b) * i);

          i >= 0

          proof

            assume i < 0 ;

            then k < 0 by A2, A4, A7, XREAL_1: 132;

            hence contradiction;

          end;

          then i in NAT by INT_1: 3;

          then

          reconsider i as Nat;

          thus thesis by A7;

        end;

        then ( Product fp) divides k by A1, Th38;

        hence thesis;

      end;

        suppose x < y;

        then (y - x) > 0 by XREAL_1: 50;

        then (y - x) in NAT by INT_1: 3;

        then

        reconsider k = (y - x) as Nat;

        for b st b in ( dom fp) holds (fp . b) divides k

        proof

          let b such that

           A8: b in ( dom fp);



           A9: (fp . b) > 0 by A2, A8;

          ((y - (fp1 . b)) mod (fp . b)) = 0 by A3, A8;

          then

           A10: (fp . b) divides (y - (fp1 . b)) by A9, INT_1: 62;

          ((x - (fp1 . b)) mod (fp . b)) = 0 by A3, A8;

          then (fp . b) divides (x - (fp1 . b)) by A9, INT_1: 62;

          then (fp . b) divides ((y - (fp1 . b)) - (x - (fp1 . b))) by A10, Lm4;

          then

          consider i be Integer such that

           A11: (y - x) = ((fp . b) * i);

          k = ((fp . b) * i) by A11;

          then i >= 0 by A2, A8, XREAL_1: 132;

          then i in NAT by INT_1: 3;

          then

          reconsider i as Nat;

          thus thesis by A11;

        end;

        then ( Product fp) divides k by A1, Th38;

        then (y,x) are_congruent_mod ( Product fp);

        hence thesis by INT_1: 14;

      end;

    end;

    reserve i,m,m1,m2,m3,r,s,a,b,c,c1,c2,x,y for Integer;



     Lm10: (x divides y implies (y mod x) = 0 ) & (x <> 0 & (y mod x) = 0 implies x divides y)

    proof



       A1: x divides y implies (y mod x) = 0

      proof

        assume x divides y;

        then

        consider i such that

         A2: y = (x * i);

        (y mod x) = (((x * i) + 0 ) mod x) by A2

        .= ( 0 mod x) by EULER_1: 12

        .= 0 by Th12;

        hence thesis;

      end;

      x <> 0 & (y mod x) = 0 implies x divides y

      proof

        assume that

         A3: x <> 0 and

         A4: (y mod x) = 0 ;

        y = (((y div x) * x) + (y mod x)) by A3, INT_1: 59

        .= ((y div x) * x) by A4;

        hence thesis;

      end;

      hence thesis by A1;

    end;



     Lm11: x divides y implies y = ((y div x) * x)

    proof

      assume

       A1: x divides y;

      then

       A2: (y mod x) = 0 by Lm10;

      per cases ;

        suppose x = 0 ;

        hence thesis by A1;

      end;

        suppose x <> 0 ;



        hence y = (((y div x) * x) + (y mod x)) by INT_1: 59

        .= ((y div x) * x) by A2;

      end;

    end;



     Lm12: (x <> 0 or y <> 0 ) implies ((x div (x gcd y)),(y div (x gcd y))) are_coprime

    proof

      assume

       A1: x <> 0 or y <> 0 ;

      then

       A2: (x gcd y) <> 0 by INT_2: 5;



       A3: y = ((y div (x gcd y)) * (x gcd y)) by Lm11, INT_2: 21;

      consider a,b be Integer such that

       A4: x = ((x gcd y) * a) and

       A5: y = ((x gcd y) * b) & (a,b) are_coprime by A1, INT_2: 23;

      x = ((x div (x gcd y)) * (x gcd y)) by Lm11, INT_2: 21;

      then a = (x div (x gcd y)) by A2, A4, XCMPLX_1: 5;

      hence thesis by A2, A3, A5, XCMPLX_1: 5;

    end;



     Lm13: x divides i & y divides i & (x,y) are_coprime implies (x * y) divides i

    proof

      assume that

       A1: x divides i and

       A2: y divides i & (x,y) are_coprime ;

      consider m such that

       A3: i = (x * m) by A1;

      y divides m by A2, A3, INT_2: 25;

      then

      consider r such that

       A4: m = (y * r);

      i = ((x * y) * r) by A3, A4;

      hence thesis;

    end;

    theorem :: INT_4:40



     Th40: m1 <> 0 & m2 <> 0 & (m1,m2) are_coprime implies ex r be Integer st (for x st ((x - c1) mod m1) = 0 & ((x - c2) mod m2) = 0 holds (x,(c1 + (m1 * r))) are_congruent_mod (m1 * m2)) & (((m1 * r) - (c2 - c1)) mod m2) = 0

    proof

      assume that

       A1: m1 <> 0 and

       A2: m2 <> 0 and

       A3: (m1,m2) are_coprime ;

      consider r be Integer such that

       A4: (((m1 * r) - (c2 - c1)) mod m2) = 0 by A3, Th15;

      take r;

      for x st ((x - c1) mod m1) = 0 & ((x - c2) mod m2) = 0 holds (x,(c1 + (m1 * r))) are_congruent_mod (m1 * m2)

      proof

        let x;

        assume that

         A5: ((x - c1) mod m1) = 0 and

         A6: ((x - c2) mod m2) = 0 ;

        set y = ((x - c1) div m1);



         A7: (x - c1) = ((((x - c1) div m1) * m1) + ((x - c1) mod m1)) by A1, INT_1: 59

        .= (((x - c1) div m1) * m1) by A5;

        then ((x - c2) mod m2) = (((m1 * y) - (c2 - c1)) mod m2);

        then y in ( Class (( Cong m2),r)) by A2, A3, A4, A6, Th26;

        then [r, y] in ( Cong m2) by EQREL_1: 18;

        then (r,y) are_congruent_mod m2 by Def1;

        then (y,r) are_congruent_mod m2 by INT_1: 14;

        then m2 divides (y - r);

        then

        consider t be Integer such that

         A8: (y - r) = (m2 * t);

        x = (c1 + (y * m1)) by A7

        .= (c1 + ((r + (m2 * t)) * m1)) by A8

        .= ((c1 + (r * m1)) + ((m1 * m2) * t));

        then (m1 * m2) divides (x - (c1 + (r * m1)));

        hence thesis;

      end;

      hence thesis by A4;

    end;

    theorem :: INT_4:41



     Th41: m1 <> 0 & m2 <> 0 & not (m1 gcd m2) divides (c1 - c2) implies not ex x st ((x - c1) mod m1) = 0 & ((x - c2) mod m2) = 0

    proof

      assume that

       A1: m1 <> 0 and

       A2: m2 <> 0 and

       A3: not (m1 gcd m2) divides (c1 - c2);



       A4: (m1 gcd m2) divides m2 by INT_2: 21;

      given x such that

       A5: ((x - c1) mod m1) = 0 and

       A6: ((x - c2) mod m2) = 0 ;

      m2 divides (x - c2) by A2, A6, Lm10;

      then

       A7: (m1 gcd m2) divides (x - c2) by A4, INT_2: 9;



       A8: (m1 gcd m2) divides m1 by INT_2: 21;

      m1 divides (x - c1) by A1, A5, Lm10;

      then (m1 gcd m2) divides (x - c1) by A8, INT_2: 9;

      then (m1 gcd m2) divides ((x - c2) - (x - c1)) by A7, Lm4;

      hence contradiction by A3;

    end;

    theorem :: INT_4:42



     Th42: m1 <> 0 & m2 <> 0 & (m1 gcd m2) divides (c2 - c1) implies ex r st (for x st ((x - c1) mod m1) = 0 & ((x - c2) mod m2) = 0 holds (x,(c1 + (m1 * r))) are_congruent_mod (m1 lcm m2)) & ((((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2))) = 0

    proof

      assume that

       A1: m1 <> 0 and

       A2: m2 <> 0 and

       A3: (m1 gcd m2) divides (c2 - c1);

      set d = (m1 gcd m2);

      set d1 = (m1 div d);

      set d2 = (m2 div d);

      set d3 = ((c2 - c1) div d);



       A4: (d1,d2) are_coprime by A1, Lm12;

      then

      consider r such that

       A5: (((d1 * r) - d3) mod d2) = 0 by Th15;

      take r;



       A6: m1 = ((m1 div (m1 gcd m2)) * (m1 gcd m2)) by Lm11, INT_2: 21;



       A7: m2 = ((m2 div (m1 gcd m2)) * (m1 gcd m2)) by Lm11, INT_2: 21;



       A8: d <> 0 by A1, INT_2: 5;

      for x st ((x - c1) mod m1) = 0 & ((x - c2) mod m2) = 0 holds (x,(c1 + (m1 * r))) are_congruent_mod (m1 lcm m2)

      proof

        let x;

        assume that

         A9: ((x - c1) mod m1) = 0 and

         A10: ((x - c2) mod m2) = 0 ;

        set y = ((x - c1) div m1);



         A11: (x - c1) = ((((x - c1) div m1) * m1) + ((x - c1) mod m1)) by A1, INT_1: 59

        .= (((x - c1) div m1) * m1) by A9;

        then (x - ((m1 * r) + c1)) = (m1 * (((x - c1) div m1) - r));

        then

         A12: m1 divides (x - ((m1 * r) + c1));

        ((x - c2) mod m2) = (((m1 * y) - (c2 - c1)) mod m2) by A11

        .= ((((d * d1) * y) - (d * d3)) mod (d * d2)) by A3, A6, A7, Lm11;

        then (d2 * d) divides (((d1 * y) - d3) * d) by A2, A7, A10, Lm10;

        then d2 divides ((d1 * y) - d3) by A8, Th7;

        then

         A13: (((d1 * y) - d3) mod d2) = 0 by Lm10;

        d2 <> 0 by A2, A7;

        then r in ( Class (( Cong d2),y)) by A4, A5, A13, Th26;

        then [y, r] in ( Cong d2) by EQREL_1: 18;

        then (y,r) are_congruent_mod d2 by Def1;

        then d2 divides (y - r);

        then

        consider w be Integer such that

         A14: (y - r) = (d2 * w);

        x = (c1 + (y * m1)) by A11

        .= (c1 + (((d2 * w) + r) * m1)) by A14

        .= (((m1 * r) + c1) + ((w * d1) * m2)) by A6, A7;

        then m2 divides (x - ((m1 * r) + c1));

        then (m1 lcm m2) divides (x - ((m1 * r) + c1)) by A12, INT_2: 19;

        hence thesis;

      end;

      hence thesis by A5;

    end;

    theorem :: INT_4:43

    m1 <> 0 & m2 <> 0 & (a gcd m1) divides c1 & (b gcd m2) divides c2 & (m1,m2) are_coprime implies ex w,r,s be Integer st (for x st (((a * x) - c1) mod m1) = 0 & (((b * x) - c2) mod m2) = 0 holds (x,(r + ((m1 div (a gcd m1)) * w))) are_congruent_mod ((m1 div (a gcd m1)) * (m2 div (b gcd m2)))) & ((((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1))) = 0 & ((((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2))) = 0 & ((((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2))) = 0

    proof

      assume that

       A1: m1 <> 0 and

       A2: m2 <> 0 and

       A3: (a gcd m1) divides c1 and

       A4: (b gcd m2) divides c2 and

       A5: (m1,m2) are_coprime ;

      set d2 = (b gcd m2);



       A6: d2 <> 0 by A2, INT_2: 5;

      set d1 = (a gcd m1);



       A7: d1 <> 0 by A1, INT_2: 5;



       A8: ((a div d1),(m1 div d1)) are_coprime by A1, Lm12;

      then

      consider r such that

       A9: ((((a div d1) * r) - (c1 div d1)) mod (m1 div d1)) = 0 by Th15;



       A10: c2 = ((c2 div d2) * d2) by A4, Lm11;



       A11: b = ((b div d2) * d2) by Lm11, INT_2: 21;



       A12: m2 = ((m2 div d2) * d2) by Lm11, INT_2: 21;

      then

       A13: (m2 div d2) divides m2;



       A14: (m2 div d2) <> 0 by A2, A12;



       A15: c1 = ((c1 div d1) * d1) by A3, Lm11;



       A16: a = ((a div d1) * d1) by Lm11, INT_2: 21;



       A17: ((b div d2),(m2 div d2)) are_coprime by A2, Lm12;

      then

      consider s be Integer such that

       A18: ((((b div d2) * s) - (c2 div d2)) mod (m2 div d2)) = 0 by Th15;



       A19: m1 = ((m1 div d1) * d1) by Lm11, INT_2: 21;

      then

       A20: (m1 div d1) divides m1;



       A21: ((m1 div d1),(m2 div d2)) are_coprime

      proof

        reconsider e = ((m1 div d1) gcd (m2 div d2)) as Element of NAT by ORDINAL1:def 12;

        assume not ((m1 div d1),(m2 div d2)) are_coprime ;

        then

         A22: ((m1 div d1) gcd (m2 div d2)) <> 1 by INT_2:def 3;

        e divides (m2 div d2) by INT_2: 21;

        then

         A23: e divides m2 by A13, INT_2: 9;

        e divides (m1 div d1) by INT_2: 21;

        then e divides m1 by A20, INT_2: 9;

        then e divides (m1 gcd m2) by A23, INT_2: 22;

        then e divides 1 by A5, INT_2:def 3;

        hence contradiction by A22, WSIERP_1: 15;

      end;

      then

      consider w be Integer such that

       A24: ((((m1 div d1) * w) - (s - r)) mod (m2 div d2)) = 0 by Th15;

      take w, r, s;



       A25: (m1 div d1) <> 0 by A1, A19;

      for x st (((a * x) - c1) mod m1) = 0 & (((b * x) - c2) mod m2) = 0 holds (x,(r + ((m1 div (a gcd m1)) * w))) are_congruent_mod ((m1 div (a gcd m1)) * (m2 div (b gcd m2)))

      proof

        let x;

        assume that

         A26: (((a * x) - c1) mod m1) = 0 and

         A27: (((b * x) - c2) mod m2) = 0 ;

        ((m1 div d1) * d1) divides ((((a div d1) * x) - (c1 div d1)) * d1) by A1, A19, A15, A16, A26, Lm10;

        then (m1 div d1) divides (((a div d1) * x) - (c1 div d1)) by A7, Th7;

        then ((((a div d1) * x) - (c1 div d1)) mod (m1 div d1)) = 0 by Lm10;

        then r in ( Class (( Cong (m1 div d1)),x)) by A8, A9, A25, Th26;

        then [x, r] in ( Cong (m1 div d1)) by EQREL_1: 18;

        then (x,r) are_congruent_mod (m1 div d1) by Def1;

        then

         A28: (m1 div d1) divides (x - r);

        ((m2 div d2) * d2) divides ((((b div d2) * x) - (c2 div d2)) * d2) by A2, A12, A10, A11, A27, Lm10;

        then (m2 div d2) divides (((b div d2) * x) - (c2 div d2)) by A6, Th7;

        then ((((b div d2) * x) - (c2 div d2)) mod (m2 div d2)) = 0 by Lm10;

        then s in ( Class (( Cong (m2 div d2)),x)) by A17, A18, A14, Th26;

        then [x, s] in ( Cong (m2 div d2)) by EQREL_1: 18;

        then (x,s) are_congruent_mod (m2 div d2) by Def1;

        then

         A29: (m2 div d2) divides (x - s);

        (m2 div d2) divides (((m1 div d1) * w) - (s - r)) by A14, A24, Lm10;

        then

         A30: (m2 div d2) divides ((x - s) - ((((m1 div d1) * w) + r) - s)) by A29, Lm4;

        (m1 div d1) divides ((m1 div d1) * w);

        then (m1 div d1) divides ((x - r) - ((m1 div d1) * w)) by A28, Lm4;

        then ((m1 div d1) * (m2 div d2)) divides (x - (r + ((m1 div d1) * w))) by A21, A30, Lm13;

        hence thesis;

      end;

      hence thesis by A9, A18, A24;

    end;

    theorem :: INT_4:44

    m1 <> 0 & m2 <> 0 & m3 <> 0 & (m1,m2) are_coprime & (m1,m3) are_coprime & (m2,m3) are_coprime implies ex r, s st for x st ((x - a) mod m1) = 0 & ((x - b) mod m2) = 0 & ((x - c) mod m3) = 0 holds (x,((a + (m1 * r)) + ((m1 * m2) * s))) are_congruent_mod ((m1 * m2) * m3) & (((m1 * r) - (b - a)) mod m2) = 0 & ((((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3) = 0

    proof

      assume that

       A1: m1 <> 0 & m2 <> 0 and

       A2: m3 <> 0 and

       A3: (m1,m2) are_coprime and

       A4: (m1,m3) are_coprime & (m2,m3) are_coprime ;

      consider r such that

       A5: for x st ((x - a) mod m1) = 0 & ((x - b) mod m2) = 0 holds (x,(a + (m1 * r))) are_congruent_mod (m1 * m2) and

       A6: (((m1 * r) - (b - a)) mod m2) = 0 by A1, A3, Th40;

      (m1 * m2) <> 0 by A1, XCMPLX_1: 6;

      then

      consider s such that

       A7: (for x st ((x - (a + (m1 * r))) mod (m1 * m2)) = 0 & ((x - c) mod m3) = 0 holds (x,((a + (m1 * r)) + ((m1 * m2) * s))) are_congruent_mod ((m1 * m2) * m3)) & ((((m1 * m2) * s) - (c - (a + (m1 * r)))) mod m3) = 0 by A2, A4, Th40, INT_2: 26;

      take r, s;

      for x st ((x - a) mod m1) = 0 & ((x - b) mod m2) = 0 & ((x - c) mod m3) = 0 holds (x,((a + (m1 * r)) + ((m1 * m2) * s))) are_congruent_mod ((m1 * m2) * m3) & (((m1 * r) - (b - a)) mod m2) = 0 & ((((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3) = 0

      proof

        let x;

        assume that

         A8: ((x - a) mod m1) = 0 & ((x - b) mod m2) = 0 and

         A9: ((x - c) mod m3) = 0 ;

        (x,(a + (m1 * r))) are_congruent_mod (m1 * m2) by A5, A8;

        then (m1 * m2) divides (x - (a + (m1 * r)));

        then ((x - (a + (m1 * r))) mod (m1 * m2)) = 0 by Lm10;

        hence thesis by A6, A7, A9;

      end;

      hence thesis;

    end;

    theorem :: INT_4:45

    m1 <> 0 & m2 <> 0 & m3 <> 0 & ( not (m1 gcd m2) divides (a - b) or not (m1 gcd m3) divides (a - c) or not (m2 gcd m3) divides (b - c)) implies not ex x st ((x - a) mod m1) = 0 & ((x - b) mod m2) = 0 & ((x - c) mod m3) = 0 by Th41;

    theorem :: INT_4:46



     Th46: for n1,n2,n3 be non zero Nat holds ((n1 gcd n3) lcm (n2 gcd n3)) = ((n1 lcm n2) gcd n3)

    proof

      let n1,n2,n3 be non zero Nat;

      set d1 = (n1 gcd n3);

      set d2 = (n2 gcd n3);

      set M = (n1 lcm n2);

      reconsider d = (M gcd n3) as non zero Nat by INT_2: 5;

      reconsider M as non zero Nat by INT_2: 4;

      d1 divides n3 & d2 divides n3 by NAT_D:def 5;

      then

       A1: (d1 lcm d2) divides n3 by NAT_D:def 4;

      d2 divides n2 & n2 divides M by NAT_D:def 4, NAT_D:def 5;

      then

       A2: d2 divides M by NAT_D: 4;



       A3: for p be Nat st p in ( support ( pfexp d)) holds (( ppf d) . p) divides n1 or (( ppf d) . p) divides n2

      proof

        let p be Nat;

        assume that

         A4: p in ( support ( pfexp d)) and

         A5: not (( ppf d) . p) divides n1 and

         A6: not (( ppf d) . p) divides n2;



         A7: not (p |^ (p |-count d)) divides n2 by A4, A6, NAT_3:def 9;



         A8: p is Prime by A4, NAT_3: 34;



         A9: not (p |^ (p |-count d)) divides n1 by A4, A5, NAT_3:def 9;



         A10: (p |-count d) > (p |-count M)

        proof



           A11: (p |-count M) = (( pfexp M) . p) by A8, NAT_3:def 8

          .= (( max (( pfexp n1),( pfexp n2))) . p) by NAT_3: 54;

          per cases ;

            suppose (( pfexp n1) . p) <= (( pfexp n2) . p);



            then (p |-count M) = (( pfexp n2) . p) by A11, NAT_3:def 4

            .= (p |-count n2) by A8, NAT_3:def 8;

            hence thesis by A7, A8, MOEBIUS1: 9;

          end;

            suppose (( pfexp n1) . p) > (( pfexp n2) . p);



            then (p |-count M) = (( pfexp n1) . p) by A11, NAT_3:def 4

            .= (p |-count n1) by A8, NAT_3:def 8;

            hence thesis by A9, A8, MOEBIUS1: 9;

          end;

        end;

        d divides M by NAT_D:def 5;

        hence contradiction by A8, A10, NAT_3: 30;

      end;



       A12: for p be Nat st p in ( support ( pfexp d)) holds (( ppf d) . p) divides (d1 lcm d2)

      proof



         A13: d2 divides (d1 lcm d2) by NAT_D:def 4;

        let p be Nat;



         A14: d1 divides (d1 lcm d2) by NAT_D:def 4;

        assume

         A15: p in ( support ( pfexp d));

        then

         A16: p is Prime by NAT_3: 34;

        d divides n3 by NAT_D:def 5;

        then (p |-count d) <= (p |-count n3) by A16, NAT_3: 30;

        then (p |^ (p |-count d)) divides (p |^ (p |-count n3)) by NEWTON: 89;

        then

         A17: (( ppf d) . p) divides (p |^ (p |-count n3)) by A15, NAT_3:def 9;

        p <> 1 by A16, INT_2:def 4;

        then (p |^ (p |-count n3)) divides n3 by NAT_3:def 7;

        then

         A18: (( ppf d) . p) divides n3 by A17, NAT_D: 4;

        per cases by A3, A15;

          suppose (( ppf d) . p) divides n1;

          then (( ppf d) . p) divides d1 by A18, NAT_D:def 5;

          hence thesis by A14, NAT_D: 4;

        end;

          suppose (( ppf d) . p) divides n2;

          then (( ppf d) . p) divides d2 by A18, NAT_D:def 5;

          hence thesis by A13, NAT_D: 4;

        end;

      end;

      ( Product ( ppf d)) divides (d1 lcm d2)

      proof

        set g = ( ppf d);

        set K = ( canFS ( support g));

        consider f be FinSequence of COMPLEX such that

         A19: ( Product g) = ( Product f) and

         A20: f = (g * K) by NAT_3:def 5;

        ( rng f) c= NAT by A20, VALUED_0:def 6;

        then

        reconsider f as FinSequence of NAT by FINSEQ_1:def 4;



         A21: ( rng K) = ( support g) by FUNCT_2:def 3;

        then ( rng K) c= NAT by XBOOLE_1: 1;

        then

        reconsider K as FinSequence of NAT by FINSEQ_1:def 4;



         A22: for m,n be Element of NAT st m in ( dom f) & n in ( dom f) & m <> n holds ((f . m) gcd (f . n)) = 1

        proof

          let m,n be Element of NAT ;

          assume that

           A23: m in ( dom f) and

           A24: n in ( dom f) and

           A25: m <> n;



           A26: m in ( dom K) by A20, A23, FUNCT_1: 11;

          then (K . m) in ( support g) by A21, FUNCT_1: 3;

          then

           A27: (K . m) in ( support ( pfexp d)) by NAT_3:def 9;

          then

           A28: (K . m) is prime by NAT_3: 34;



           A29: n in ( dom K) by A20, A24, FUNCT_1: 11;

          then (K . n) in ( support g) by A21, FUNCT_1: 3;

          then

           A30: (K . n) in ( support ( pfexp d)) by NAT_3:def 9;

          then

           A31: (K . n) is prime by NAT_3: 34;

          (f . n) = (g . (K . n)) by A20, A24, FUNCT_1: 12;

          then

           A32: (f . n) = ((K . n) |^ ((K . n) |-count d)) by A30, NAT_3:def 9;

          (f . m) = (g . (K . m)) by A20, A23, FUNCT_1: 12;

          then

           A33: (f . m) = ((K . m) |^ ((K . m) |-count d)) by A27, NAT_3:def 9;

          (K . m) <> (K . n) by A25, A26, A29, FUNCT_1:def 4;

          then

           A34: ((K . n),((K . m) |^ ((K . m) |-count d))) are_coprime by A28, A31, EULER_2: 17, INT_2: 30;



           A35: (K . n) > 0 by A30, NAT_3: 34;

          (K . m) > 0 by A27, NAT_3: 34;

          then (((K . n) |^ ((K . n) |-count d)),((K . m) |^ ((K . m) |-count d))) are_coprime by A35, A34, EULER_2: 17;

          hence thesis by A33, A32, INT_2:def 3;

        end;

        for m be Element of NAT st m in ( dom f) holds (f . m) divides (d1 lcm d2)

        proof

          let m be Element of NAT ;

          assume

           A36: m in ( dom f);

          then m in ( dom K) by A20, FUNCT_1: 11;

          then (K . m) in ( support g) by A21, FUNCT_1: 3;

          then (K . m) in ( support ( pfexp d)) by NAT_3:def 9;

          then (g . (K . m)) divides (d1 lcm d2) by A12;

          hence thesis by A20, A36, FUNCT_1: 12;

        end;

        hence thesis by A19, A22, Th38;

      end;

      then

       A37: d divides (d1 lcm d2) by NAT_3: 61;

      d1 divides n1 & n1 divides M by NAT_D:def 4, NAT_D:def 5;

      then d1 divides M by NAT_D: 4;

      then (d1 lcm d2) divides M by A2, NAT_D:def 4;

      then (d1 lcm d2) divides d by A1, NAT_D:def 5;

      hence thesis by A37, NAT_D: 5;

    end;

    theorem :: INT_4:47

    for n1,n2,n3 be non zero Nat st (n1 gcd n2) divides (a - b) holds ex r, s st for x st ((x - a) mod n1) = 0 & ((x - b) mod n2) = 0 & ((x - c) mod n3) = 0 holds (x,((a + (n1 * r)) + ((n1 lcm n2) * s))) are_congruent_mod ((n1 lcm n2) lcm n3) & ((((n1 div (n1 gcd n2)) * r) - ((b - a) div (n1 gcd n2))) mod (n2 div (n1 gcd n2))) = 0 & (((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * s) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3))) = 0

    proof

      let n1,n2,n3 be non zero Nat;

      set d1 = (n1 gcd n2);

      set d2 = (n1 gcd n3);

      set d3 = (n2 gcd n3);

      set dd1 = (n1 gcd n2);

      set K = (n1 lcm n2);



       A1: n2 divides (n1 lcm n2) by NAT_D:def 4;

      assume (n1 gcd n2) divides (a - b);

      then d1 divides ( - (a - b)) by INT_2: 10;

      then

      consider r such that

       A2: for x st ((x - a) mod n1) = 0 & ((x - b) mod n2) = 0 holds (x,(a + (n1 * r))) are_congruent_mod K and

       A3: ((((n1 div dd1) * r) - ((b - a) div dd1)) mod (n2 div dd1)) = 0 by Th42;

      take r;

      set y = (a + (n1 * r));



       A4: ((K div (K gcd n3)),(n3 div (K gcd n3))) are_coprime by Lm12;

      then

      consider s such that

       A5: ((((K div (K gcd n3)) * s) - ((c - y) div (K gcd n3))) mod (n3 div (K gcd n3))) = 0 by Th15;

      take s;



       A6: n1 divides (n1 lcm n2) by NAT_D:def 4;



       A7: for x st ((x - a) mod n1) = 0 & ((x - b) mod n2) = 0 & ((x - c) mod n3) = 0 holds ((n1 lcm n2) gcd n3) divides (y - c)

      proof

        let x;

        assume that

         A8: ((x - a) mod n1) = 0 & ((x - b) mod n2) = 0 and

         A9: ((x - c) mod n3) = 0 ;



         A10: n3 divides (x - c) by A9, Lm10;

        (x,y) are_congruent_mod K by A2, A8;

        then K divides (x - y);

        then

         A11: K divides ( - (x - y)) by INT_2: 10;

        then n1 divides (y - x) by A6, INT_2: 9;

        then

        consider t1 be Integer such that

         A12: (y - x) = (n1 * t1);

        d3 divides n3 by NAT_D:def 5;

        then

         A13: d3 divides (x - c) by A10, INT_2: 9;

        d2 divides n3 by NAT_D:def 5;

        then

         A14: d2 divides (x - c) by A10, INT_2: 9;

        n2 divides (y - x) by A1, A11, INT_2: 9;

        then

        consider t2 be Integer such that

         A15: (y - x) = (n2 * t2);

        d3 divides n2 by NAT_D:def 5;

        then

         A16: d3 divides (n2 * t2) by INT_2: 2;

        (y - c) = ((x - c) + (n2 * t2)) by A15;

        then

         A17: d3 divides (y - c) by A16, A13, WSIERP_1: 4;

        d2 divides n1 by NAT_D:def 5;

        then

         A18: d2 divides (n1 * t1) by INT_2: 2;

        (y - c) = ((x - c) + (n1 * t1)) by A12;

        then d2 divides (y - c) by A18, A14, WSIERP_1: 4;

        then (d2 lcm d3) divides (y - c) by A17, INT_2: 19;

        hence thesis by Th46;

      end;

      for x st ((x - a) mod n1) = 0 & ((x - b) mod n2) = 0 & ((x - c) mod n3) = 0 holds (x,(y + ((n1 lcm n2) * s))) are_congruent_mod ((n1 lcm n2) lcm n3)

      proof



         A19: K <> 0 by INT_2: 4;

        let x;

        assume that

         A20: ((x - a) mod n1) = 0 & ((x - b) mod n2) = 0 and

         A21: ((x - c) mod n3) = 0 ;

        ((n1 lcm n2) gcd n3) divides (y - c) by A7, A20, A21;

        then (K gcd n3) divides ( - (y - c)) by INT_2: 10;

        then

        consider w be Integer such that

         A22: for x st ((x - y) mod K) = 0 & ((x - c) mod n3) = 0 holds (x,(y + (K * w))) are_congruent_mod (K lcm n3) and

         A23: ((((K div (K gcd n3)) * w) - ((c - y) div (K gcd n3))) mod (n3 div (K gcd n3))) = 0 by A19, Th42;



         A24: n3 = ((n3 div (K gcd n3)) * (K gcd n3)) by Lm11, INT_2: 21;

        then (n3 div (K gcd n3)) <> 0 ;

        then w in ( Class (( Cong (n3 div (K gcd n3))),s)) by A4, A5, A23, Th26;

        then [s, w] in ( Cong (n3 div (K gcd n3))) by EQREL_1: 18;

        then (s,w) are_congruent_mod (n3 div (K gcd n3)) by Def1;

        then

         A25: ((K * s),(K * w)) are_congruent_mod (K * (n3 div (K gcd n3))) by Th10;

        (K * (n3 div (K gcd n3))) = (((K div (K gcd n3)) * (K gcd n3)) * (n3 div (K gcd n3))) by Lm11, INT_2: 21

        .= (n3 * (K div (K gcd n3))) by A24;

        then ((K * s),(K * w)) are_congruent_mod n3 by A25, INT_1: 20;

        then

         A26: n3 divides ((K * s) - (K * w));

        K divides (K * (s - w));

        then (K lcm n3) divides (((K * s) + y) - ((K * w) + y)) by A26, INT_2: 19;

        then (((K * s) + y),((K * w) + y)) are_congruent_mod (K lcm n3);

        then

         A27: (((K * w) + y),((K * s) + y)) are_congruent_mod (K lcm n3) by INT_1: 14;

        (x,y) are_congruent_mod K by A2, A20;

        then K divides (x - y);

        then ((x - y) mod K) = 0 by Lm10;

        then (x,((K * w) + y)) are_congruent_mod (K lcm n3) by A21, A22;

        hence thesis by A27, INT_1: 15;

      end;

      hence thesis by A3, A5;

    end;

    begin

    reserve a,b,c,m for Element of NAT ;

    definition

      let m be Nat, X be set;

      :: INT_4:def2

      pred X is_CRS_of m means ex fp be FinSequence of INT st X = ( rng fp) & ( len fp) = m & for b be Nat st b in ( dom fp) holds (fp . b) in ( Class (( Cong m),(b -' 1)));

    end

    theorem :: INT_4:48

    { a where a be Nat : a < m } is_CRS_of m

    proof

      deffunc F( Nat) = ($1 -' 1);

      consider fp be FinSequence such that

       A1: ( len fp) = m & for a be Nat st a in ( dom fp) holds (fp . a) = F(a) from FINSEQ_1:sch 2;

      for a be Nat st a in ( dom fp) holds (fp . a) in INT

      proof

        let a be Nat;

        assume a in ( dom fp);

        then (fp . a) = F(a) by A1;

        hence thesis by INT_1:def 2;

      end;

      then

      reconsider fp as FinSequence of INT by FINSEQ_2: 12;



       A2: { a where a be Nat : a < m } = ( rng fp)

      proof

        set A = { a where a be Nat : a < m };



         A3: ( rng fp) c= A

        proof

          let b be object;

          assume b in ( rng fp);

          then

          consider k be object such that

           A4: k in ( dom fp) and

           A5: b = (fp . k) by FUNCT_1:def 3;

          reconsider k as Element of NAT by A4;



           A6: k in ( Seg m) by A1, A4, FINSEQ_1:def 3;

          then k <= m by FINSEQ_1: 1;

          then

           A7: (k - 1) < m by XREAL_1: 147;

          k >= 1 by A6, FINSEQ_1: 1;

          then

           A8: (k -' 1) < m by A7, XREAL_1: 233;

          reconsider b as Integer by A5;

          b = (k -' 1) by A1, A4, A5;

          hence thesis by A8;

        end;

        A c= ( rng fp)

        proof

          let b be object;

          assume b in A;

          then

          consider k be Nat such that

           A9: k = b and

           A10: k < m;

          (k + 1) >= 1 & (k + 1) <= m by A10, NAT_1: 11, NAT_1: 13;

          then

           A11: (k + 1) in ( dom fp) by A1, FINSEQ_3: 25;



          then (fp . (k + 1)) = ((k + 1) -' 1) by A1

          .= k by NAT_D: 34;

          hence thesis by A9, A11, FUNCT_1:def 3;

        end;

        hence thesis by A3;

      end;

      for a be Nat st a in ( dom fp) holds (fp . a) in ( Class (( Cong m),(a -' 1)))

      proof

        let a be Nat;

        ((a -' 1),(a -' 1)) are_congruent_mod m by INT_1: 11;

        then

         A12: [(a -' 1), (a -' 1)] in ( Cong m) by Def1;

        assume a in ( dom fp);

        then (fp . a) = (a -' 1) by A1;

        hence thesis by A12, EQREL_1: 18;

      end;

      hence thesis by A1, A2;

    end;

    theorem :: INT_4:49



     Th49: for X be finite set st X is_CRS_of m holds ( card X) = m & for x,y be Integer st x in X & y in X & x <> y holds not [x, y] in ( Cong m)

    proof

      let X be finite set;

      assume X is_CRS_of m;

      then

      consider fp be FinSequence of INT such that

       A1: X = ( rng fp) and

       A2: ( len fp) = m and

       A3: for b be Nat st b in ( dom fp) holds (fp . b) in ( Class (( Cong m),(b -' 1)));



       A4: for x,y be Integer st x in X & y in X & x <> y holds not [x, y] in ( Cong m)

      proof

        let x,y be Integer;

        assume that

         A5: x in X and

         A6: y in X and

         A7: x <> y;

        consider a be object such that

         A8: a in ( dom fp) and

         A9: x = (fp . a) by A1, A5, FUNCT_1:def 3;

        reconsider a as Element of NAT by A8;

        x in ( Class (( Cong m),(a -' 1))) by A3, A8, A9;

        then [(a -' 1), x] in ( Cong m) by EQREL_1: 18;

        then

         A10: ((a -' 1),x) are_congruent_mod m by Def1;

        consider b be object such that

         A11: b in ( dom fp) and

         A12: y = (fp . b) by A1, A6, FUNCT_1:def 3;

        reconsider b as Element of NAT by A11;



         A13: b in ( Seg m) by A2, A11, FINSEQ_1:def 3;

        then

         A14: b >= 1 by FINSEQ_1: 1;

        y in ( Class (( Cong m),(b -' 1))) by A3, A11, A12;

        then [(b -' 1), y] in ( Cong m) by EQREL_1: 18;

        then ((b -' 1),y) are_congruent_mod m by Def1;

        then

         A15: (y,(b -' 1)) are_congruent_mod m by INT_1: 14;

        assume [x, y] in ( Cong m);

        then (x,y) are_congruent_mod m by Def1;

        then (x,(b -' 1)) are_congruent_mod m by A15, INT_1: 15;

        then ((a -' 1),(b -' 1)) are_congruent_mod m by A10, INT_1: 15;

        then

         A16: m divides ((a -' 1) - (b -' 1));



         A17: a in ( Seg m) by A2, A8, FINSEQ_1:def 3;

        then

         A18: a >= 1 by FINSEQ_1: 1;

        b <= m by A13, FINSEQ_1: 1;

        then (a - b) >= (1 - m) by A18, XREAL_1: 13;

        then

         A19: (a - b) > ( - m) by XREAL_1: 145;

        a <= m by A17, FINSEQ_1: 1;

        then (a - b) <= (m - 1) by A14, XREAL_1: 13;

        then (a - b) < m by XREAL_1: 147;

        then |.(a - b).| < m by A19, SEQ_2: 1;

        then

         A20: |.(a - b).| < |.m.| by ABSVALUE:def 1;



         A21: ((a -' 1) - (b -' 1)) = ((a - 1) - (b -' 1)) by A18, XREAL_1: 233

        .= ((a - 1) - (b - 1)) by A14, XREAL_1: 233

        .= (a - b);

        now

          assume a <> b;

          then (a - b) <> 0 ;

          hence contradiction by A16, A21, A20, Th6;

        end;

        hence contradiction by A7, A9, A12;

      end;

      for a,b be object st a in ( dom fp) & b in ( dom fp) & (fp . a) = (fp . b) holds a = b

      proof

        let a,b be object;

        assume that

         A22: a in ( dom fp) and

         A23: b in ( dom fp) and

         A24: (fp . a) = (fp . b);

        reconsider a, b as Element of NAT by A22, A23;



         A25: b in ( Seg m) by A2, A23, FINSEQ_1:def 3;

        then

         A26: b >= 1 by FINSEQ_1: 1;

        reconsider l = (fp . a), ll = (fp . b) as Element of INT by A22, A23, FINSEQ_2: 11;

        (fp . b) in ( Class (( Cong m),(b -' 1))) by A3, A23;

        then [(b -' 1), (fp . b)] in ( Cong m) by EQREL_1: 18;

        then ((b -' 1),ll) are_congruent_mod m by Def1;

        then

         A27: (l,(b -' 1)) are_congruent_mod m by A24, INT_1: 14;



         A28: a in ( Seg m) by A2, A22, FINSEQ_1:def 3;

        then

         A29: a >= 1 by FINSEQ_1: 1;



        then

         A30: ((a -' 1) - (b -' 1)) = ((a - 1) - (b -' 1)) by XREAL_1: 233

        .= ((a - 1) - (b - 1)) by A26, XREAL_1: 233

        .= (a - b);

        b <= m by A25, FINSEQ_1: 1;

        then (a - b) >= (1 - m) by A29, XREAL_1: 13;

        then

         A31: (a - b) > ( - m) by XREAL_1: 145;

        a <= m by A28, FINSEQ_1: 1;

        then (a - b) <= (m - 1) by A26, XREAL_1: 13;

        then (a - b) < m by XREAL_1: 147;

        then |.(a - b).| < m by A31, SEQ_2: 1;

        then

         A32: |.(a - b).| < |.m.| by ABSVALUE:def 1;

        (fp . a) in ( Class (( Cong m),(a -' 1))) by A3, A22;

        then [(a -' 1), (fp . a)] in ( Cong m) by EQREL_1: 18;

        then ((a -' 1),l) are_congruent_mod m by Def1;

        then ((a -' 1),(b -' 1)) are_congruent_mod m by A27, INT_1: 15;

        then

         A33: m divides (a - b) by A30;

        now

          assume a <> b;

          then (a - b) <> 0 ;

          hence contradiction by A33, A32, Th6;

        end;

        hence thesis;

      end;

      then fp is one-to-one;

      hence thesis by A1, A2, A4, FINSEQ_4: 62;

    end;

    theorem :: INT_4:50



     Th50: {} is_CRS_of m iff m = 0

    proof

      set fp = ( <*> INT );

      thus {} is_CRS_of m implies m = 0 by Th49, CARD_1: 27;

      assume m = 0 ;

      then

       A1: ( len fp) = m;

       {} = ( rng fp) & for b be Nat st b in ( dom fp) holds (fp . b) in ( Class (( Cong m),(b -' 1)));

      hence thesis by A1;

    end;

    theorem :: INT_4:51



     Th51: for X be finite set st ( card X) = m holds ex fp be FinSequence st ( len fp) = m & (for a st a in ( dom fp) holds (fp . a) in X) & fp is one-to-one

    proof

      defpred P[ Nat] means for X be finite set holds ( card X) = $1 implies ex fp be FinSequence st ( len fp) = $1 & (for a st a in ( dom fp) holds (fp . a) in X) & fp is one-to-one;

      let X be finite set;



       A1: for m be Nat st P[m] holds P[(m + 1)]

      proof

        let m be Nat such that

         A2: P[m];

        let X be finite set;

        assume

         A3: ( card X) = (m + 1);

        then

        consider x be object such that

         A4: x in X by CARD_1: 27, XBOOLE_0:def 1;

        set Y = (X \ {x});

        ( card Y) = (( card X) - ( card {x})) by A4, EULER_1: 4

        .= ((m + 1) - 1) by A3, CARD_1: 30

        .= m;

        then

        consider fp1 be FinSequence such that

         A5: ( len fp1) = m and

         A6: for a st a in ( dom fp1) holds (fp1 . a) in Y and

         A7: fp1 is one-to-one by A2;

        set fp = (fp1 ^ <*x*>);



         A8: ( len fp) = (m + 1) by A5, FINSEQ_2: 16;

        for a,b be object st a in ( dom fp) & b in ( dom fp) & a <> b holds (fp . a) <> (fp . b)

        proof

          let a,b be object;

          assume that

           A9: a in ( dom fp) and

           A10: b in ( dom fp) and

           A11: a <> b;



           A12: a in ( Seg (m + 1)) by A8, A9, FINSEQ_1:def 3;



           A13: b in ( Seg (m + 1)) by A8, A10, FINSEQ_1:def 3;

          reconsider a, b as Element of NAT by A9, A10;

          per cases by A12, FINSEQ_2: 7;

            suppose

             A14: a in ( Seg m);

            per cases by A13, FINSEQ_2: 7;

              suppose b in ( Seg m);

              then

               A15: b in ( dom fp1) by A5, FINSEQ_1:def 3;

              then

               A16: (fp . b) = (fp1 . b) by FINSEQ_1:def 7;



               A17: a in ( dom fp1) by A5, A14, FINSEQ_1:def 3;

              then (fp . a) = (fp1 . a) by FINSEQ_1:def 7;

              hence thesis by A7, A11, A17, A15, A16;

            end;

              suppose

               A18: b = (m + 1);

              a in ( dom fp1) by A5, A14, FINSEQ_1:def 3;

              then (fp1 . a) in Y & (fp . a) = (fp1 . a) by A6, FINSEQ_1:def 7;

              then

               A19: not (fp . a) in {x} by XBOOLE_0:def 5;

              (fp . b) = x by A5, A18, FINSEQ_1: 42;

              hence thesis by A19, TARSKI:def 1;

            end;

          end;

            suppose

             A20: a = (m + 1);

            then b in ( Seg m) by A11, A13, FINSEQ_2: 7;

            then b in ( dom fp1) by A5, FINSEQ_1:def 3;

            then (fp1 . b) in Y & (fp . b) = (fp1 . b) by A6, FINSEQ_1:def 7;

            then not (fp . b) in {x} by XBOOLE_0:def 5;

            then (fp . b) <> x by TARSKI:def 1;

            hence thesis by A5, A20, FINSEQ_1: 42;

          end;

        end;

        then

         A21: for a,b be object st a in ( dom fp) & b in ( dom fp) & (fp . a) = (fp . b) holds a = b;

        take fp;

        for a be object st a in ( dom fp) holds (fp . a) in X

        proof

          let a be object;

          assume a in ( dom fp);

          then

           A22: a in ( Seg (m + 1)) by A8, FINSEQ_1:def 3;

          per cases by A22, FINSEQ_2: 7;

            suppose a in ( Seg m);

            then

             A23: a in ( dom fp1) by A5, FINSEQ_1:def 3;

            then (fp . a) = (fp1 . a) by FINSEQ_1:def 7;

            then (fp . a) in Y by A6, A23;

            hence thesis;

          end;

            suppose a = (m + 1);

            hence thesis by A4, A5, FINSEQ_1: 42;

          end;

        end;

        hence thesis by A5, A21, FINSEQ_2: 16;

      end;



       A24: P[ 0 ]

      proof

        set fp = ( <*> NAT );

        let X be finite set;

        assume ( card X) = 0 ;

        take fp;

        thus ( len fp) = 0 ;

        thus thesis;

      end;

      for m be Nat holds P[m] from NAT_1:sch 2( A24, A1);

      hence thesis;

    end;

    theorem :: INT_4:52



     Th52: for X be finite Subset of INT st ( card X) = m & (for x,y be Integer st x in X & y in X & x <> y holds not [x, y] in ( Cong m)) holds X is_CRS_of m

    proof

      let X be finite Subset of INT ;

      assume that

       A1: ( card X) = m and

       A2: for x,y be Integer st x in X & y in X & x <> y holds not [x, y] in ( Cong m);

      per cases ;

        suppose X is empty;

        hence thesis by A1, Th50;

      end;

        suppose X is non empty;

        then

        reconsider X as non empty finite Subset of INT ;

        defpred P[ Nat, set] means $2 in ( Class (( Cong m),($1 -' 1)));



         A3: X <> {} ;



         A4: for a be Nat st a in ( Seg m) holds ex y be Element of X st P[a, y]

        proof

          set Y = ( Segm m);

          let a be Nat such that

           A5: a in ( Seg m);

          a <= m by A5, FINSEQ_1: 1;

          then

           A6: (a - 1) < m by XREAL_1: 147;

          consider fp be FinSequence such that

           A7: ( len fp) = m and

           A8: for b st b in ( dom fp) holds (fp . b) in X and

           A9: fp is one-to-one by A1, Th51;

          for b be Nat st b in ( dom fp) holds (fp . b) in X by A8;

          then

          reconsider fp as FinSequence of X by FINSEQ_2: 12;

          defpred PP[ Nat, set] means (fp . $1) in ( Class (( Cong m),$2));



           A10: for c st c in ( Seg m) holds ex r be Element of Y st PP[c, r]

          proof

            let c;

            assume c in ( Seg m);

            consider q,r be Integer such that

             A11: (fp . c) = ((m * q) + r) and

             A12: r >= 0 and

             A13: r < m by A1, Th13;

            ((fp . c) mod m) = (r mod m) by A11, NAT_D: 61;

            then (r,(fp . c)) are_congruent_mod m by A1, NAT_D: 64;

            then

             A14: [r, (fp . c)] in ( Cong m) by Def1;

            reconsider r as Element of NAT by A12, INT_1: 3;

            reconsider r as Element of Y by A13, NAT_1: 44;

            take r;

            thus thesis by A14, EQREL_1: 18;

          end;

          reconsider Y as non empty set by A1, A3;



           A15: for c be Nat st c in ( Seg m) holds ex r be Element of Y st PP[c, r] by A10;

          consider fr be FinSequence of Y such that

           A16: ( dom fr) = ( Seg m) & for c be Nat st c in ( Seg m) holds PP[c, (fr . c)] from FINSEQ_1:sch 5( A15);

          for x1,x2 be object st x1 in ( dom fr) & x2 in ( dom fr) & (fr . x1) = (fr . x2) holds x1 = x2

          proof

            let x1,x2 be object;

            assume that

             A17: x1 in ( dom fr) and

             A18: x2 in ( dom fr) and

             A19: (fr . x1) = (fr . x2);

            (fp . x1) in ( Class (( Cong m),(fr . x1))) & (fp . x2) in ( Class (( Cong m),(fr . x1))) by A16, A17, A18, A19;

            then

             A20: [(fp . x1), (fp . x2)] in ( Cong m) by EQREL_1: 22;

            assume

             A21: x1 <> x2;

            reconsider x1, x2 as Element of NAT by A17, A18;



             A22: x1 in ( dom fp) by A7, A16, A17, FINSEQ_1:def 3;

            then

             A23: (fp . x1) in X by FINSEQ_2: 11;



             A24: x2 in ( dom fp) by A7, A16, A18, FINSEQ_1:def 3;

            then

             A25: (fp . x2) in X by FINSEQ_2: 11;

            (fp . x1) <> (fp . x2) by A9, A21, A22, A24;

            hence contradiction by A2, A20, A23, A25;

          end;

          then fr is one-to-one;



          then

           A26: ( card ( rng fr)) = ( len fr) by FINSEQ_4: 62

          .= m by A16, FINSEQ_1:def 3;

          reconsider Y as finite set;

          a >= 1 by A5, FINSEQ_1: 1;

          then (a -' 1) < m by A6, XREAL_1: 233;

          then

           A27: (a -' 1) in Y by NAT_1: 44;

          ( card Y) = m;

          then ( rng fr) = Y by A26, CARD_2: 102;

          then

          consider w be object such that

           A28: w in ( dom fr) and

           A29: (fr . w) = (a -' 1) by A27, FUNCT_1:def 3;

          reconsider w as Element of NAT by A28;

          w in ( dom fp) by A7, A16, A28, FINSEQ_1:def 3;

          then

          reconsider y = (fp . w) as Element of X by FINSEQ_2: 11;

          take y;

          thus thesis by A16, A28, A29;

        end;

        consider fp be FinSequence of X such that

         A30: ( dom fp) = ( Seg m) & for a be Nat st a in ( Seg m) holds P[a, (fp . a)] from FINSEQ_1:sch 5( A4);



         A31: ( rng fp) c= X by FINSEQ_1:def 4;



         A32: ( len fp) = m by A30, FINSEQ_1:def 3;

        for a,b be object st a in ( dom fp) & b in ( dom fp) & (fp . a) = (fp . b) holds a = b

        proof

          let a,b be object;

          assume that

           A33: a in ( dom fp) and

           A34: b in ( dom fp) and

           A35: (fp . a) = (fp . b);

          reconsider a, b as Element of NAT by A33, A34;



           A36: b >= 1 by A30, A34, FINSEQ_1: 1;



           A37: a >= 1 by A30, A33, FINSEQ_1: 1;



          then

           A38: ((a -' 1) - (b -' 1)) = ((a - 1) - (b -' 1)) by XREAL_1: 233

          .= ((a - 1) - (b - 1)) by A36, XREAL_1: 233

          .= (a - b);

          reconsider l = (fp . a), ll = (fp . b) as Element of INT by A33, A34, FINSEQ_2: 11;

          (fp . b) in ( Class (( Cong m),(b -' 1))) by A30, A34;

          then [(b -' 1), (fp . b)] in ( Cong m) by EQREL_1: 18;

          then ((b -' 1),ll) are_congruent_mod m by Def1;

          then

           A39: (l,(b -' 1)) are_congruent_mod m by A35, INT_1: 14;

          b <= m by A30, A34, FINSEQ_1: 1;

          then (a - b) >= (1 - m) by A37, XREAL_1: 13;

          then

           A40: (a - b) > ( - m) by XREAL_1: 145;

          a <= m by A30, A33, FINSEQ_1: 1;

          then (a - b) <= (m - 1) by A36, XREAL_1: 13;

          then (a - b) < m by XREAL_1: 147;

          then |.(a - b).| < m by A40, SEQ_2: 1;

          then

           A41: |.(a - b).| < |.m.| by ABSVALUE:def 1;

          (fp . a) in ( Class (( Cong m),(a -' 1))) by A30, A33;

          then [(a -' 1), (fp . a)] in ( Cong m) by EQREL_1: 18;

          then ((a -' 1),l) are_congruent_mod m by Def1;

          then ((a -' 1),(b -' 1)) are_congruent_mod m by A39, INT_1: 15;

          then

           A42: m divides (a - b) by A38;

          now

            assume a <> b;

            then (a - b) <> 0 ;

            hence contradiction by A42, A41, Th6;

          end;

          hence thesis;

        end;

        then fp is one-to-one;

        then ( card X) = ( card ( rng fp)) by A1, A32, FINSEQ_4: 62;

        then X = ( rng fp) by A31, CARD_2: 102;

        hence thesis by A30, A32;

      end;

    end;

    reserve a for Integer;

    theorem :: INT_4:53

    for X be finite Subset of INT st X is_CRS_of m holds (a ++ X) is_CRS_of m

    proof

      let X be finite Subset of INT ;

      assume

       A1: X is_CRS_of m;

      then ( card X) = m by Th49;

      then

       A2: ( card (a ++ X)) = m by Th2;



       A3: for i,j be Integer st i in (a ++ X) & j in (a ++ X) & i <> j holds not [i, j] in ( Cong m)

      proof

        let i,j be Integer;

        assume that

         A4: i in (a ++ X) and

         A5: j in (a ++ X) and

         A6: i <> j;

        consider u be Complex such that

         A7: i = (a + u) and

         A8: u in X by A4, MEMBER_1: 143;

        consider w be Complex such that

         A9: j = (a + w) and

         A10: w in X by A5, MEMBER_1: 143;

        reconsider u9 = u, w9 = w as Integer by A8, A10;

        assume [i, j] in ( Cong m);

        then (i,j) are_congruent_mod m by Def1;

        then m divides ((a + u9) - (a + w9)) by A7, A9;

        then m divides (u9 - w9);

        then

         A11: (u9,w9) are_congruent_mod m;

         not [u9, w9] in ( Cong m) by A1, A6, A8, A7, A10, A9, Th49;

        hence contradiction by A11, Def1;

      end;

      (a ++ X) is Subset of INT by Lm1;

      hence thesis by A2, A3, Th52;

    end;

    theorem :: INT_4:54

    for X be finite Subset of INT st (a,m) are_coprime & X is_CRS_of m holds (a ** X) is_CRS_of m

    proof

      let X be finite Subset of INT ;

      assume that

       A1: (a,m) are_coprime and

       A2: X is_CRS_of m;



       A3: ( card X) = m by A2, Th49;



       A4: (a ** X) c= INT by Lm2;

      per cases ;

        suppose

         A5: a = 0 ;



        then (a gcd m) = |.m.| by WSIERP_1: 8

        .= m by ABSVALUE:def 1;

        then

         A6: m = 1 by A1, INT_2:def 3;

        then ex x be object st X = {x} by A3, CARD_2: 42;

        then

         A7: (a ** X) = { 0 } by A5, Th4;



         A8: for x,y be Integer st x in (a ** X) & y in (a ** X) & x <> y holds not [x, y] in ( Cong m)

        proof

          let x,y be Integer;

          assume that

           A9: x in (a ** X) and

           A10: y in (a ** X) & x <> y;

          assume [x, y] in ( Cong m);

          x = 0 by A7, A9, TARSKI:def 1;

          hence contradiction by A7, A10, TARSKI:def 1;

        end;

        ( card (a ** X)) = m by A6, A7, CARD_2: 42;

        hence thesis by A4, A8, Th52;

      end;

        suppose

         A11: a <> 0 ;



         A12: for x,y be Integer st x in (a ** X) & y in (a ** X) & x <> y holds not [x, y] in ( Cong m)

        proof

          let x,y be Integer;

          assume that

           A13: x in (a ** X) and

           A14: y in (a ** X) and

           A15: x <> y;

          consider y1 be Integer such that

           A16: y1 in X and

           A17: y = (a * y1) by A14, Lm3;

          consider x1 be Integer such that

           A18: x1 in X and

           A19: x = (a * x1) by A13, Lm3;

           not [x1, y1] in ( Cong m) by A2, A15, A18, A19, A16, A17, Th49;

          then

           A20: not (x1,y1) are_congruent_mod m by Def1;

          assume [x, y] in ( Cong m);

          then ((a * x1),(a * y1)) are_congruent_mod m by A19, A17, Def1;

          hence contradiction by A1, A20, Th9;

        end;

        ( card (a ** X)) = m by A3, A11, Th5;

        hence thesis by A4, A12, Th52;

      end;

    end;