int_8.miz



    begin

    reserve i,s,t,m,n,k for Nat,

c,d,e for Element of NAT ,

fn for FinSequence of NAT ,

x,y for Integer;

    definition

      let m be Nat;

      :: INT_8:def1

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

      correctness ;

    end

    theorem :: INT_8:1

    

     Th1: ( RelPrimes m) c= ( Seg m)

    proof

      let x be object;

      assume x in ( RelPrimes m);

      then ex k be Element of NAT st k = x & (m,k) are_coprime & k >= 1 & k <= m;

      hence x in ( Seg m);

    end;

    definition

      let m be Nat;

      :: original: RelPrimes

      redefine

      func RelPrimes (m) -> Subset of NAT ;

      coherence

      proof

        ( RelPrimes m) c= ( Seg m) by Th1;

        hence thesis by XBOOLE_1: 1;

      end;

    end

    registration

      let m be Nat;

      cluster ( RelPrimes m) -> finite;

      coherence

      proof

        ( RelPrimes m) c= ( Seg m) by Th1;

        hence thesis;

      end;

    end

    theorem :: INT_8:2

    1 <= m implies ( RelPrimes m) <> {}

    proof

      assume

       A1: 1 <= m;

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

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

      then 1 in ( RelPrimes m) by A1;

      hence thesis;

    end;

    theorem :: INT_8:3

    

     Th3: 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);

      thus thesis by MEMBER_1: 193, A3;

    end;

    theorem :: INT_8:4

    

     Th4: ex r be Nat st ((1 + s) |^ t) = (((1 + (t * s)) + ((t choose 2) * (s ^2 ))) + (r * (s ^3 )))

    proof

      defpred P[ Nat] means ex r be Nat st ((1 + s) |^ $1) = (((1 + ($1 * s)) + (($1 choose 2) * (s ^2 ))) + (r * (s ^3 )));

      

       A1: for t be Nat st P[t] holds P[(t + 1)]

      proof

        let t be Nat;

        assume P[t];

        then

        consider r1 be Nat such that

         A2: ((1 + s) |^ t) = (((1 + (t * s)) + ((t choose 2) * (s ^2 ))) + (r1 * (s ^3 )));

        ((1 + s) |^ (t + 1)) = ((((1 + (t * s)) + ((t choose 2) * (s ^2 ))) + (r1 * (s ^3 ))) * (1 + s)) by A2, NEWTON: 6

        .= (((((1 + ((t + 1) * s)) + ((t + (t choose 2)) * (s ^2 ))) + (r1 * (s ^3 ))) + (((t choose 2) * (s ^2 )) * s)) + ((r1 * (s ^3 )) * s))

        .= (((((1 + ((t + 1) * s)) + ((t + ((t * (t - 1)) / 2)) * (s ^2 ))) + (r1 * (s ^3 ))) + (((t choose 2) * (s ^2 )) * s)) + ((r1 * (s ^3 )) * s)) by STIRL2_1: 51

        .= (((((1 + ((t + 1) * s)) + ((((t + 1) * ((t + 1) - 1)) / 2) * (s ^2 ))) + (r1 * (s ^3 ))) + (((t choose 2) * (s ^2 )) * s)) + ((r1 * (s ^3 )) * s))

        .= (((((1 + ((t + 1) * s)) + (((t + 1) choose 2) * (s ^2 ))) + (r1 * (s ^3 ))) + ((t choose 2) * (s ^3 ))) + ((r1 * (s ^3 )) * s)) by STIRL2_1: 51

        .= (((1 + ((t + 1) * s)) + (((t + 1) choose 2) * (s ^2 ))) + (((r1 + (t choose 2)) + (r1 * s)) * (s ^3 )));

        hence thesis;

      end;

      

       A3: P[ 0 ]

      proof

        reconsider z = 0 as Element of NAT ;

        take r = 0 ;

        (((1 + (z * s)) + ((z choose 2) * (s ^2 ))) + (r * (s ^3 ))) = (((1 + (z * s)) + (z * (s ^2 ))) + (r * (s ^3 ))) by NEWTON:def 3

        .= ((1 + s) |^ z) by NEWTON: 4;

        hence thesis;

      end;

      for t be Nat holds P[t] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: INT_8:5

    

     Th5: n > 1 & (i,n) are_coprime implies i <> 0

    proof

      assume

       A1: n > 1 & (i,n) are_coprime ;

      assume i = 0 ;

      then (i gcd n) > 1 by A1, NEWTON: 52;

      hence contradiction by A1, INT_2:def 3;

    end;

    theorem :: INT_8:6

    

     Th6: for a,b be Integer, m be Nat st ((a * b) mod m) = 1 & (a mod m) = 1 holds (b mod m) = 1

    proof

      let a,b be Integer, m be Nat;

      assume

       A1: ((a * b) mod m) = 1 & (a mod m) = 1;

      then

       A2: m <> 0 by INT_1:def 10;

      then (a mod m) = (1 mod m) by A1, PEPIN: 5, INT_1: 58;

      then ((a * b),(1 * b)) are_congruent_mod m by INT_4: 11, A2, NAT_D: 64;

      hence thesis by A1, NAT_D: 64;

    end;

    

     Lm1: for x be Integer holds 2 divides (x * (x + 1))

    proof

      let x be Integer;

      per cases ;

        suppose x is even;

        hence thesis by ABIAN:def 1;

      end;

        suppose x is odd;

        then

        consider y be Integer such that

         A1: x = ((2 * y) + 1) by ABIAN: 1;

        (x * (x + 1)) = (2 * (((2 * y) + 1) * (y + 1))) by A1;

        hence thesis by INT_1:def 3;

      end;

    end;

    theorem :: INT_8:7

    

     Th7: for x be odd Integer, k be Nat st k >= 3 holds ((x |^ (2 |^ (k -' 2))) mod (2 |^ k)) = 1

    proof

      let x be odd Integer, k be Nat;

      assume

       A1: k >= 3;

      defpred X[ Nat] means ((x |^ (2 |^ ($1 -' 2))) mod (2 |^ $1)) = 1;

      consider y be Integer such that

       A2: x = ((2 * y) + 1) by ABIAN: 1;

      

       A3: X[3]

      proof

        (3 -' 2) = (3 - 2) by XREAL_1: 233

        .= 1;

        

        then

         A4: ((x |^ (2 |^ (3 -' 2))) mod (2 |^ 3)) = ((x |^ 2) mod (2 |^ 3))

        .= ((x ^2 ) mod (2 |^ 3)) by NEWTON: 81;

        

         A5: ((x ^2 ) - 1) = ((2 ^2 ) * (y * (y + 1))) by A2;

        2 divides (y * (y + 1)) by Lm1;

        then ((2 ^2 ) * 2) divides ((x ^2 ) - 1) by A5, INT_4: 7;

        then ((2 |^ 2) * 2) divides ((x ^2 ) - 1) by NEWTON: 81;

        then (2 |^ (2 + 1)) divides ((x ^2 ) - 1) by NEWTON: 6;

        then

         A6: ((x ^2 ),1) are_congruent_mod (2 |^ 3) by INT_2: 15;

        ((2 * 2) * 2) > 1;

        then ((2 |^ 2) * 2) > 1 by NEWTON: 81;

        then (2 |^ (2 + 1)) > 1 by NEWTON: 6;

        hence thesis by A4, A6, PEPIN: 39;

      end;

      

       A7: for k be Nat st k >= 3 & X[k] holds X[(k + 1)]

      proof

        let k be Nat;

        assume

         A8: k >= 3 & X[k];

        

         A9: k > 0 & k > 1 & k > 2 by A8, XXREAL_0: 2;

        

         A10: ((k -' 3) + 1) = ((k + 1) -' 3) by A8, NAT_D: 38

        .= ((k + 1) - 3) by A8, NAT_D: 37

        .= (k - 2);

        (k -' 2) = (k - 2) by A9, XREAL_1: 233;

        

        then

         A11: (x |^ (2 |^ (k -' 2))) = (x |^ ((2 |^ (k -' 3)) * 2)) by A10, NEWTON: 6

        .= ((x |^ 2) |^ (2 |^ (k -' 3))) by NEWTON: 9

        .= ((x ^2 ) |^ (2 |^ (k -' 3))) by NEWTON: 81;

        (2 |^ k) > 1 by A8, PEPIN: 25;

        then ((x |^ (2 |^ (k -' 2))),1) are_congruent_mod (2 |^ k) by A8, A11, PEPIN: 39;

        then

        consider t be Integer such that

         A12: ((x |^ (2 |^ (k -' 2))) - 1) = ((2 |^ k) * t) by INT_1:def 3, INT_2: 15;

        ((x |^ (2 |^ (k -' 2))) ^2 ) = ((x |^ (2 |^ (k -' 2))) |^ 2) by NEWTON: 81

        .= (x |^ ((2 |^ (k -' 2)) * 2)) by NEWTON: 9

        .= (x |^ (2 |^ ((k -' 2) + 1))) by NEWTON: 6;

        

        then

         A13: (x |^ (2 |^ ((k -' 2) + 1))) = (((t * (2 |^ k)) + 1) ^2 ) by A12

        .= ((((t ^2 ) * ((2 |^ k) ^2 )) + (2 * (t * (2 |^ k)))) + 1)

        .= ((((t ^2 ) * ((2 |^ k) |^ 2)) + (2 * (t * (2 |^ k)))) + 1) by NEWTON: 81

        .= ((((t ^2 ) * (2 |^ (2 * k))) + ((2 * (2 |^ k)) * t)) + 1) by NEWTON: 9

        .= ((((t ^2 ) * (2 |^ (2 * k))) + ((2 |^ (k + 1)) * t)) + 1) by NEWTON: 6;

        (k + k) > (k + 1) by A9, XREAL_1: 8;

        then

         A14: (2 |^ (k + 1)) divides ((t ^2 ) * (2 |^ (2 * k))) by NAT_D: 9, PEPIN: 31;

        (2 |^ (k + 1)) divides ((2 |^ (k + 1)) * t) by INT_2: 2;

        then

         A15: (2 |^ (k + 1)) divides (((t ^2 ) * (2 |^ (2 * k))) + ((2 |^ (k + 1)) * t)) by A14, WSIERP_1: 4;

        

         A16: ((((t ^2 ) * (2 |^ (2 * k))) + ((2 |^ (k + 1)) * t)) mod (2 |^ (k + 1))) = 0 by A15, INT_1: 62;

        ((x |^ (2 |^ ((k + 1) -' 2))) mod (2 |^ (k + 1))) = ((x |^ (2 |^ ((k -' 2) + 1))) mod (2 |^ (k + 1))) by NAT_D: 38, A9

        .= ((((((t ^2 ) * (2 |^ (2 * k))) + ((2 |^ (k + 1)) * t)) mod (2 |^ (k + 1))) + (1 mod (2 |^ (k + 1)))) mod (2 |^ (k + 1))) by A13, NAT_D: 66

        .= (1 mod (2 |^ (k + 1))) by A16, NAT_D: 65

        .= 1 by PEPIN: 5, PEPIN: 25;

        hence thesis;

      end;

      for k be Nat st k >= 3 holds X[k] from NAT_1:sch 8( A3, A7);

      hence thesis by A1;

    end;

    reserve p for Prime;

    

     Lm2: k <= n implies (m |^ k) divides (m |^ n) by NEWTON: 89;

    theorem :: INT_8:8

    

     Th8: m >= 1 implies ( Euler (p |^ m)) = ((p |^ m) - (p |^ (m -' 1)))

    proof

      assume

       A1: m >= 1;

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

      set X1 = { k where k be Element of NAT : not ((p |^ m),k) are_coprime & k >= 1 & k <= (p |^ m) };

      set X2 = { k where k be Element of NAT : not (p,k) are_coprime & k >= 1 & k <= (p |^ m) };

      set X3 = { k where k be Element of NAT : p divides k & k >= 1 & k <= (p |^ m) };

      reconsider w = (p |^ (m -' 1)) as Element of NAT by ORDINAL1:def 12;

      

       A2: X1 = X2

      proof

        thus X1 c= X2

        proof

          let a be object;

          assume a in X1;

          then

          consider b be Element of NAT such that

           A3: b = a & not ((p |^ m),b) are_coprime & b >= 1 & b <= (p |^ m);

           not (p,b) are_coprime by A3, WSIERP_1: 10;

          hence thesis by A3;

        end;

        let a be object;

        assume a in X2;

        then

        consider k be Element of NAT such that

         A4: k = a & not (p,k) are_coprime & k >= 1 & k <= (p |^ m);

        (p gcd k) = p by A4, PEPIN: 2;

        then

         A5: p divides k by NAT_D:def 5;

        (p |^ 1) divides (p |^ m) by A1, NEWTON: 89;

        then

         A6: p divides (p |^ m);

        now

          assume ((p |^ m),k) are_coprime ;

          then p = 1 by A5, A6, PYTHTRIP:def 1;

          hence contradiction by INT_2:def 4;

        end;

        hence thesis by A4;

      end;

      

       A7: X2 = X3

      proof

        thus X2 c= X3

        proof

          let x be object;

          assume x in X2;

          then

          consider k be Element of NAT such that

           A8: x = k & not (p,k) are_coprime & k >= 1 & k <= (p |^ m);

          (p gcd k) = p by A8, PEPIN: 2;

          then p divides k by NAT_D:def 5;

          hence thesis by A8;

        end;

        let x be object;

        assume x in X3;

        then

        consider k be Element of NAT such that

         A9: x = k & p divides k & k >= 1 & k <= (p |^ m);

        (p gcd k) = p by A9, NEWTON: 49;

        then (p gcd k) > 1 by INT_2:def 4;

        then not (p,k) are_coprime by INT_2:def 3;

        hence thesis by A9;

      end;

      X3 c= ( Seg (p |^ m))

      proof

        let x be object;

        assume x in X3;

        then ex k be Element of NAT st k = x & p divides k & k >= 1 & k <= (p |^ m);

        hence x in ( Seg (p |^ m));

      end;

      then

      reconsider X1, X2, X3 as finite Subset of NAT by A2, A7, XBOOLE_1: 1;

      deffunc F( Nat) = ($1 * p);

      consider f be FinSequence such that

       A10: ( len f) = w & for d be Nat st d in ( dom f) holds (f . d) = F(d) from FINSEQ_1:sch 2;

      

       A11: ( rng f) = X3

      proof

        thus ( rng f) c= X3

        proof

          let a be object;

          assume a in ( rng f);

          then

          consider s be Nat such that

           A12: s in ( dom f) & (f . s) = a by FINSEQ_2: 10;

          

           A13: a = (s * p) by A12, A10;

          then

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

          

           A14: p divides a by A13, NAT_D:def 3;

          s in ( Seg w) by A12, A10, FINSEQ_1:def 3;

          then

           A15: s >= 1 & s <= w by FINSEQ_1: 1;

          p > 1 by INT_2:def 4;

          then

           A16: (s * p) >= (1 * 1) by A15, XREAL_1: 66;

          (s * p) <= (w * p) by A15, XREAL_1: 66;

          then

           A17: (s * p) <= (p |^ ((m -' 1) + 1)) by NEWTON: 6;

          (p |^ ((m -' 1) + 1)) = (p |^ ((m + 1) -' 1)) by A1, NAT_D: 38

          .= (p |^ m) by NAT_D: 34;

          hence thesis by A13, A14, A16, A17;

        end;

        let a be object;

        assume a in X3;

        then

        consider k be Element of NAT such that

         A18: a = k & p divides k & k >= 1 & k <= (p |^ m);

        consider t be Nat such that

         A19: k = (p * t) by A18, NAT_D:def 3;

        t <> 0 by A19, A18;

        then

         A20: t >= 1 by NAT_1: 14;

        (p |^ m) = (p |^ ((m + 1) -' 1)) by NAT_D: 34

        .= (p |^ ((m -' 1) + 1)) by A1, NAT_D: 38

        .= ((p |^ (m -' 1)) * p) by NEWTON: 6;

        then ((p * t) / p) <= (((p |^ (m -' 1)) * p) / p) by XREAL_1: 72, A18, A19;

        then t <= ((w * p) / p) by XCMPLX_1: 89;

        then t <= w by XCMPLX_1: 89;

        then t in ( Seg w) by A20;

        then

         A21: t in ( dom f) by A10, FINSEQ_1:def 3;

        (f . t) = (t * p) by A21, A10;

        hence thesis by A18, A19, A21, FUNCT_1: 3;

      end;

      for a,b be object st a in ( dom f) & b in ( dom f) & (f . a) = (f . b) holds a = b

      proof

        let a,b be object;

        assume

         A22: a in ( dom f) & b in ( dom f) & (f . a) = (f . b);

        then

        reconsider a, b as Element of NAT ;

        (f . a) = (a * p) & (f . b) = (b * p) by A22, A10;

        hence thesis by A22, XCMPLX_1: 5;

      end;

      then f is one-to-one by FUNCT_1:def 4;

      then

       A23: w = ( card X1) by A2, A7, A10, A11, FINSEQ_4: 62;

      

       A24: X1 c= ( Seg (p |^ m))

      proof

        let x be object;

        assume x in X1;

        then

        consider k be Element of NAT such that

         A25: x = k & not ((p |^ m),k) are_coprime & k >= 1 & k <= (p |^ m);

        thus thesis by A25;

      end;

      

       A26: X c= ( Seg (p |^ m))

      proof

        let x be object;

        assume x in X;

        then

        consider k be Element of NAT such that

         A27: x = k & ((p |^ m),k) are_coprime & k >= 1 & k <= (p |^ m);

        thus thesis by A27;

      end;

      then

       A28: (X1 \/ X) c= ( Seg (p |^ m)) by A24, XBOOLE_1: 8;

      reconsider X as finite Subset of NAT by A26, XBOOLE_1: 1;

      ( Seg (p |^ m)) c= (X1 \/ X)

      proof

        let x be object;

        assume

         A29: x in ( Seg (p |^ m));

        then

        reconsider x as Element of NAT ;

        

         A30: x >= 1 & x <= (p |^ m) by A29, FINSEQ_1: 1;

        per cases ;

          suppose ((p |^ m),x) are_coprime ;

          then x in X by A30;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose not ((p |^ m),x) are_coprime ;

          then x in X1 by A30;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      then

       A31: (X1 \/ X) = ( Seg (p |^ m)) by A28;

       not ex x be object st x in (X1 /\ X)

      proof

        given x be object such that

         A32: x in (X1 /\ X);

        

         A33: x in X1 & x in X by A32, XBOOLE_0:def 4;

        then

        consider k1 be Element of NAT such that

         A34: x = k1 & not ((p |^ m),k1) are_coprime & k1 >= 1 & k1 <= (p |^ m);

        consider k2 be Element of NAT such that

         A35: x = k2 & ((p |^ m),k2) are_coprime & k2 >= 1 & k2 <= (p |^ m) by A33;

        thus contradiction by A34, A35;

      end;

      then (X1 /\ X) = {} by XBOOLE_0:def 1;

      then X1 misses X;

      then (( card X1) + ( card X)) = ( card ( Seg (p |^ m))) by A31, CARD_2: 40;

      then (w + ( card X)) = (p |^ m) by A23, FINSEQ_1: 57;

      hence thesis;

    end;

    theorem :: INT_8:9

    n > 1 & (i,n) are_coprime implies ( order (i,n)) divides ( Euler n)

    proof

      assume

       A1: n > 1 & (i,n) are_coprime ;

      ((i |^ ( Euler n)) mod n) = 1 by Th5, A1, EULER_2: 18;

      hence thesis by A1, PEPIN: 47;

    end;

    theorem :: INT_8:10

    

     Th10: for i, n st n > 1 & (i,n) are_coprime holds ((i |^ s),(i |^ t)) are_congruent_mod n iff (s,t) are_congruent_mod ( order (i,n))

    proof

      let i, n;

      assume

       A1: n > 1 & (i,n) are_coprime ;

      

       A2: i <> 0 & n > 0 by A1, Th5;

      set R = ( order (i,n));

      reconsider RR = R as Element of NAT ;

      thus ((i |^ s),(i |^ t)) are_congruent_mod n implies (s,t) are_congruent_mod R

      proof

        assume

         A3: ((i |^ s),(i |^ t)) are_congruent_mod n;

        

         A4: (i gcd n) = 1 by A1, INT_2:def 3;

        per cases by XXREAL_0: 1;

          suppose s = t;

          hence thesis by INT_1: 11;

        end;

          suppose s > t;

          then

          consider l be Nat such that

           A5: s = (t + l) by NAT_1: 10;

          n divides ((i |^ s) - (i |^ t)) by A3, INT_2: 15;

          then n divides (((i |^ t) * (i |^ l)) - ((i |^ t) * 1)) by A5, NEWTON: 8;

          then

           A6: n divides ((i |^ t) * ((i |^ l) - 1));

          reconsider ll = ((i |^ l) - 1) as Element of NAT by NAT_1: 21, NAT_1: 14, A2;

          

           A7: (n gcd (i |^ t)) = 1 by A4, A2, NAT_4: 10;

          n divides ll by A6, A7, WSIERP_1: 30;

          then ((i |^ l),1) are_congruent_mod n by INT_2: 15;

          

          then ((i |^ l) mod n) = (1 mod n) by NAT_D: 64

          .= 1 by A1, PEPIN: 5;

          then R divides (s - t) by A5, A1, PEPIN: 47;

          hence thesis by INT_2: 15;

        end;

          suppose s < t;

          then

          consider l be Nat such that

           A8: t = (s + l) by NAT_1: 10;

          ((i |^ t),(i |^ s)) are_congruent_mod n by A3, INT_1: 14;

          then n divides ((i |^ t) - (i |^ s)) by INT_2: 15;

          then n divides (((i |^ s) * (i |^ l)) - ((i |^ s) * 1)) by A8, NEWTON: 8;

          then

           A9: n divides ((i |^ s) * ((i |^ l) - 1));

          

           A10: (n gcd (i |^ s)) = 1 by A4, A2, NAT_4: 10;

          reconsider ll = ((i |^ l) - 1) as Element of NAT by NAT_1: 21, NAT_1: 14, A2;

          n divides ll by A10, A9, WSIERP_1: 30;

          then ((i |^ l),1) are_congruent_mod n by INT_2: 15;

          

          then ((i |^ l) mod n) = (1 mod n) by NAT_D: 64

          .= 1 by A1, PEPIN: 5;

          then R divides (t - s) by A1, A8, PEPIN: 47;

          then (t,s) are_congruent_mod R by INT_2: 15;

          hence thesis by INT_1: 14;

        end;

      end;

      assume

       A11: (s,t) are_congruent_mod R;

      

       A12: R > 0 by A1, PEPIN:def 2;

      then

       A13: s = (((s div R) * R) + (s mod R)) & t = (((t div R) * R) + (t mod R)) by NEWTON: 66;

      

      then

       A14: (i |^ s) = ((i |^ (R * (s div R))) * (i |^ (s mod R))) by NEWTON: 8

      .= (((i |^ R) |^ (s div R)) * (i |^ (s mod R))) by NEWTON: 9;

      

       A15: ((i |^ R) mod n) = 1 by A1, PEPIN:def 2

      .= (1 mod n) by A1, PEPIN: 5;

      

      then (((i |^ R) |^ (s div R)) mod n) = ((1 |^ (s div R)) mod n) by INT_4: 8

      .= (1 mod n);

      then (((i |^ R) |^ (s div R)),1) are_congruent_mod n by A1, NAT_D: 64;

      then ((((i |^ R) |^ (s div R)) * (i |^ (s mod R))),(1 * (i |^ (s mod R)))) are_congruent_mod n by INT_4: 11;

      then

       A16: ((i |^ s) mod n) = ((i |^ (s mod R)) mod n) by A14, NAT_D: 64;

      

       A17: (i |^ t) = ((i |^ (R * (t div R))) * (i |^ (t mod R))) by NEWTON: 8, A13

      .= (((i |^ R) |^ (t div R)) * (i |^ (t mod R))) by NEWTON: 9;

      (((i |^ R) |^ (t div R)) mod n) = ((1 |^ (t div R)) mod n) by A15, INT_4: 8

      .= (1 mod n);

      then (((i |^ R) |^ (t div R)),1) are_congruent_mod n by A1, NAT_D: 64;

      then ((((i |^ R) |^ (t div R)) * (i |^ (t mod R))),(1 * (i |^ (t mod R)))) are_congruent_mod n by INT_4: 11;

      then

       A18: ((i |^ t) mod n) = ((i |^ (t mod R)) mod n) by A17, NAT_D: 64;

      (s mod R) = ((s mod R) mod R) & (t mod R) = ((t mod R) mod R) by EULER_2: 5;

      then

       A19: (s,(s mod R)) are_congruent_mod R & (t,(t mod R)) are_congruent_mod R by A12, NAT_D: 64;

      then (t,(s mod R)) are_congruent_mod R by A11, PEPIN: 40;

      then ((s mod R),(t mod R)) are_congruent_mod R by A19, PEPIN: 40;

      then

       A20: R divides ((s mod R) - (t mod R)) by INT_2: 15;

      now

        assume (s mod R) <> (t mod R);

        then ((s mod R) - (t mod R)) <> 0 ;

        then |.R.| <= |.((s mod R) - (t mod R)).| by A20, INT_4: 6;

        then

         A21: R <= |.((s mod R) - (t mod R)).| by ABSVALUE:def 1;

        reconsider sR = (s mod RR), tR = (t mod RR) as Element of REAL by XREAL_0:def 1;

        reconsider rR = ( - R) as Element of REAL by XREAL_0:def 1;

        

         A22: sR < RR & sR >= 0 & tR < RR & tR >= 0 by A12, NAT_D: 1;

        (sR - tR) <= sR by XREAL_1: 43;

        then

         A23: (sR - tR) < RR by A22, XXREAL_0: 2;

        

         A24: (( - 1) * tR) > (( - 1) * RR) by XREAL_1: 69, A22;

        (sR + ( - tR)) >= ( - tR) by XREAL_1: 31;

        then (sR + ( - tR)) > rR by XXREAL_0: 2, A24;

        hence contradiction by A21, SEQ_2: 1, A23;

      end;

      hence thesis by A1, A16, A18, NAT_D: 64;

    end;

    theorem :: INT_8:11

    for i, n st n > 1 & (i,n) are_coprime holds ((i |^ s),1) are_congruent_mod n iff ( order (i,n)) divides s

    proof

      let i, n;

      assume

       A1: n > 1 & (i,n) are_coprime ;

      thus ((i |^ s),1) are_congruent_mod n implies ( order (i,n)) divides s

      proof

        assume ((i |^ s),1) are_congruent_mod n;

        then ((i |^ s),(i |^ 0 )) are_congruent_mod n by NEWTON: 4;

        then (s, 0 ) are_congruent_mod ( order (i,n)) by A1, Th10;

        then ( order (i,n)) divides (s - 0 ) by INT_2: 15;

        hence thesis;

      end;

      assume ( order (i,n)) divides s;

      then ( order (i,n)) divides (s - 0 );

      then (s, 0 ) are_congruent_mod ( order (i,n)) by INT_2: 15;

      then ((i |^ s),(i |^ 0 )) are_congruent_mod n by A1, Th10;

      hence thesis by NEWTON: 4;

    end;

    theorem :: INT_8:12

    n > 1 & (i,n) are_coprime & ( len fn) = ( order (i,n)) & (for d st d in ( dom fn) holds (fn . d) = (i |^ (d -' 1))) implies (for d, e st d in ( dom fn) & e in ( dom fn) & d <> e holds not ((fn . d),(fn . e)) are_congruent_mod n)

    proof

      assume

       A1: n > 1 & (i,n) are_coprime & ( len fn) = ( order (i,n)) & (for d st d in ( dom fn) holds (fn . d) = (i |^ (d -' 1)));

      then

       A2: i <> 0 & n <> 0 by Th5;

      

       A3: (i gcd n) = 1 by A1, INT_2:def 3;

      assume ex d, e st d in ( dom fn) & e in ( dom fn) & d <> e & ((fn . d),(fn . e)) are_congruent_mod n;

      then

      consider d, e such that

       A4: d in ( dom fn) & e in ( dom fn) & d <> e & ((fn . d),(fn . e)) are_congruent_mod n;

      

       A5: d >= 1 & d <= ( order (i,n)) & e >= 1 & e <= ( order (i,n)) by A4, A1, FINSEQ_3: 25;

      

      then ((d -' 1) + 1) = ((d + 1) -' 1) by NAT_D: 38

      .= ((d + 1) - 1) by NAT_D: 37

      .= ((d - 1) + 1);

      then

       A6: (d -' 1) = (d - 1);

      ((e -' 1) + 1) = ((e + 1) -' 1) by NAT_D: 38, A5

      .= ((e + 1) - 1) by NAT_D: 37

      .= ((e - 1) + 1);

      then

       A7: (d - 1) = (d -' 1) & (e - 1) = (e -' 1) by A6;

      per cases by A4, XXREAL_0: 1;

        suppose d > e;

        then

         A8: (e -' 1) < (d -' 1) by A7, XREAL_1: 9;

        then

        consider k be Nat such that

         A9: (d -' 1) = ((e -' 1) + k) by NAT_1: 10;

        reconsider ll = ((i |^ k) - 1) as Element of NAT by A2, NAT_1: 21, NAT_1: 14;

        

         A10: ((i |^ (d -' 1)) - (i |^ (e -' 1))) = (((i |^ (e -' 1)) * (i |^ k)) - ((i |^ (e -' 1)) * 1)) by A9, NEWTON: 8

        .= ((i |^ (e -' 1)) * ll);

        

         A11: ((i |^ (e -' 1)) gcd n) = 1 by A2, A3, NAT_4: 10;

        ((i |^ (d -' 1)),(fn . e)) are_congruent_mod n by A1, A4;

        then ((i |^ (d -' 1)),(i |^ (e -' 1))) are_congruent_mod n by A1, A4;

        then n divides ((i |^ (d -' 1)) - (i |^ (e -' 1))) by INT_2: 15;

        then n divides ll by A10, A11, WSIERP_1: 30;

        then ((i |^ k),1) are_congruent_mod n by INT_2: 15;

        

        then

         A12: ((i |^ k) mod n) = (1 mod n) by NAT_D: 64

        .= 1 by A1, PEPIN: 5;

        

         A13: ((d -' 1) - (e -' 1)) > 0 by A8, XREAL_1: 50;

        

         A14: ( order (i,n)) <= k by A13, A9, NAT_D: 7, A1, A12, PEPIN: 47;

        (d - e) <= (( order (i,n)) - 1) by A5, XREAL_1: 13;

        hence contradiction by A7, A9, A14, XXREAL_0: 2, XREAL_1: 146;

      end;

        suppose e > d;

        then

         A15: (e -' 1) > (d -' 1) by A7, XREAL_1: 9;

        then

        consider k be Nat such that

         A16: (e -' 1) = ((d -' 1) + k) by NAT_1: 10;

        reconsider ll = ((i |^ k) - 1) as Element of NAT by A2, NAT_1: 21, NAT_1: 14;

        

         A17: ((i |^ (e -' 1)) - (i |^ (d -' 1))) = (((i |^ (d -' 1)) * (i |^ k)) - ((i |^ (d -' 1)) * 1)) by A16, NEWTON: 8

        .= ((i |^ (d -' 1)) * ll);

        

         A18: ((i |^ (d -' 1)) gcd n) = 1 by A2, A3, NAT_4: 10;

        ((i |^ (d -' 1)),(fn . e)) are_congruent_mod n by A1, A4;

        then ((i |^ (d -' 1)),(i |^ (e -' 1))) are_congruent_mod n by A1, A4;

        then ((i |^ (e -' 1)),(i |^ (d -' 1))) are_congruent_mod n by INT_1: 14;

        then n divides ((i |^ (e -' 1)) - (i |^ (d -' 1))) by INT_2: 15;

        then n divides ll by A17, A18, WSIERP_1: 30;

        then ((i |^ k),1) are_congruent_mod n by INT_2: 15;

        

        then

         A19: ((i |^ k) mod n) = (1 mod n) by NAT_D: 64

        .= 1 by A1, PEPIN: 5;

        

         A20: ((e -' 1) - (d -' 1)) > 0 by A15, XREAL_1: 50;

        

         A21: ( order (i,n)) <= k by A16, A20, NAT_D: 7, A1, A19, PEPIN: 47;

        (e - d) <= (( order (i,n)) - 1) by A5, XREAL_1: 13;

        hence contradiction by A16, A21, A7, XXREAL_0: 2, XREAL_1: 146;

      end;

    end;

    theorem :: INT_8:13

    n > 1 & (i,n) are_coprime & ( len fn) = ( order (i,n)) & (for d st d in ( dom fn) holds (fn . d) = (i |^ (d -' 1))) implies (for d st d in ( dom fn) holds (((fn . d) |^ ( order (i,n))) mod n) = 1)

    proof

      assume

       A1: n > 1 & (i,n) are_coprime & ( len fn) = ( order (i,n)) & (for d st d in ( dom fn) holds (fn . d) = (i |^ (d -' 1)));

      set K = ( order (i,n));

      let d;

      assume d in ( dom fn);

      then

       A2: (fn . d) = (i |^ (d -' 1)) by A1;

      

       A3: (((fn . d) |^ ( order (i,n))) mod n) = ((i |^ (K * (d -' 1))) mod n) by NEWTON: 9, A2

      .= (((i |^ K) |^ (d -' 1)) mod n) by NEWTON: 9;

      ((i |^ ( order (i,n))) mod n) = 1 by A1, PEPIN:def 2

      .= (1 mod n) by A1, PEPIN: 5;

      

      then (((i |^ K) |^ (d -' 1)) mod n) = ((1 |^ (d -' 1)) mod n) by INT_4: 8

      .= (1 mod n)

      .= 1 by A1, PEPIN: 5;

      hence thesis by A3;

    end;

    theorem :: INT_8:14

    

     Th14: n > 1 & (i,n) are_coprime implies ( order ((i |^ s),n)) = (( order (i,n)) div (( order (i,n)) gcd s))

    proof

      assume

       A1: n > 1 & (i,n) are_coprime ;

      then

       A2: i <> 0 & n <> 0 by Th5;

      (i gcd n) = 1 by A1, INT_2:def 3;

      then ((i |^ s) gcd n) = 1 by A2, NAT_4: 10;

      then

       A3: ((i |^ s),n) are_coprime by INT_2:def 3;

      

       A4: ( order (i,n)) > 0 by A1, PEPIN:def 2;

      set K1 = (( order (i,n)) gcd s), K2 = (( order (i,n)) div K1);

      per cases ;

        suppose

         A5: s = 0 ;

        then K1 = ( order (i,n)) by NEWTON: 52;

        then

         A6: K2 = 1 by A4, NAT_2: 3;

        (i |^ s) = 1 by A5, NEWTON: 4;

        hence thesis by A1, A6, PEPIN: 46;

      end;

        suppose

         A7: s > 0 ;

        K1 divides ( order (i,n)) & K1 divides s by NAT_D:def 5;

        then

         A8: ( order (i,n)) = (K2 * K1) & s = ((s div K1) * K1) by NAT_D: 3;

        then

         A9: K2 <> 0 & K1 <> 0 & (s div K1) <> 0 by A1, A7, PEPIN:def 2;

        

         A10: (K2,(s div K1)) are_coprime by A8, A9, EULER_1: 6;

        (s * K2) = ((s div K1) * ( order (i,n))) by A8;

        then ( order (i,n)) divides (s * K2) by NAT_D:def 3;

        then ((i |^ (s * K2)) mod n) = 1 by A1, PEPIN: 48;

        then

         A11: (((i |^ s) |^ K2) mod n) = 1 by NEWTON: 9;

        for k be Nat st k > 0 & (((i |^ s) |^ k) mod n) = 1 holds 0 < K2 & K2 <= k

        proof

          let k be Nat;

          reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

          assume

           A12: k > 0 & (((i |^ s) |^ k) mod n) = 1;

          then ((i |^ (s * k)) mod n) = 1 by NEWTON: 9;

          then (K2 * K1) divides (((s div K1) * k1) * K1) by A8, A1, PEPIN: 47;

          then K2 divides ((s div K1) * k1) by A9, PYTHTRIP: 7;

          hence thesis by A9, A12, A10, PEPIN: 3, NAT_D: 7;

        end;

        hence thesis by A1, A3, A9, A11, PEPIN:def 2;

      end;

    end;

    theorem :: INT_8:15

    for i, n st n > 1 & (i,n) are_coprime holds (( order (i,n)),s) are_coprime iff ( order ((i |^ s),n)) = ( order (i,n))

    proof

      let i, n;

      assume

       A1: n > 1 & (i,n) are_coprime ;

      thus (( order (i,n)),s) are_coprime implies ( order ((i |^ s),n)) = ( order (i,n))

      proof

        assume (( order (i,n)),s) are_coprime ;

        then (( order (i,n)) gcd s) = 1 by INT_2:def 3;

        then (( order (i,n)) div (( order (i,n)) gcd s)) = ( order (i,n)) by NAT_2: 4;

        hence thesis by A1, Th14;

      end;

      assume ( order ((i |^ s),n)) = ( order (i,n));

      then

       A2: (( order (i,n)) div (( order (i,n)) gcd s)) = ( order (i,n)) by A1, Th14;

      set d = (( order (i,n)) gcd s);

      

       A3: d divides ( order (i,n)) by NAT_D:def 5;

      then

       A4: ((( order (i,n)) div d) * 1) = ((( order (i,n)) div d) * d) by A2, NAT_D: 3;

      

       A5: ( order (i,n)) > 0 by A1, PEPIN:def 2;

      then

       A6: d <= ( order (i,n)) by A3, NAT_D: 7;

      d <> 0 by A5, INT_2: 5;

      then (( order (i,n)) div d) <> 0 by A6, NAT_2: 13;

      then d = 1 by A4, XCMPLX_1: 5;

      hence thesis by INT_2:def 3;

    end;

    theorem :: INT_8:16

    n > 1 & (i,n) are_coprime & ( order (i,n)) = (s * t) implies ( order ((i |^ s),n)) = t

    proof

      assume

       A1: n > 1 & (i,n) are_coprime & ( order (i,n)) = (s * t);

      then

       A2: i <> 0 by Th5;

      

       A3: t <> 0 & s <> 0 by A1, PEPIN:def 2;

      (i gcd n) = 1 by A1, INT_2:def 3;

      then ((i |^ s) gcd n) = 1 by A2, A1, NAT_4: 10;

      then

       A4: ((i |^ s),n) are_coprime by INT_2:def 3;

      

       A5: (((i |^ s) |^ t) mod n) = ((i |^ ( order (i,n))) mod n) by A1, NEWTON: 9

      .= 1 by A1, PEPIN:def 2;

      

       A6: for k be Nat st k > 0 & (((i |^ s) |^ k) mod n) = 1 holds 0 < t & t <= k

      proof

        let k be Nat;

        assume

         A7: k > 0 & (((i |^ s) |^ k) mod n) = 1;

        then

         A8: ((i |^ (s * k)) mod n) = 1 by NEWTON: 9;

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

        (t * s) divides (k * s) by A8, A1, PEPIN: 47;

        then t divides k by A3, PYTHTRIP: 7;

        hence thesis by A3, A7, NAT_D: 7;

      end;

      t is Element of NAT by ORDINAL1:def 12;

      hence thesis by A1, A4, A3, A6, A5, PEPIN:def 2;

    end;

    theorem :: INT_8:17

    

     Th17: n > 1 & (s,n) are_coprime & (t,n) are_coprime & (( order (s,n)),( order (t,n))) are_coprime implies ( order ((s * t),n)) = (( order (s,n)) * ( order (t,n)))

    proof

      assume

       A1: n > 1 & (s,n) are_coprime & (t,n) are_coprime & (( order (s,n)),( order (t,n))) are_coprime ;

      then (s gcd n) = 1 & (t gcd n) = 1 by INT_2:def 3;

      then ((s * t) gcd n) = 1 by WSIERP_1: 7;

      then

       A2: ((s * t),n) are_coprime by INT_2:def 3;

      set L = (( order (s,n)) * ( order (t,n)));

      

       A3: (((s * t) |^ ( order ((s * t),n))) mod n) = 1 by A1, A2, PEPIN:def 2

      .= (1 mod n) by A1, PEPIN: 5;

      then ((((s * t) |^ ( order ((s * t),n))) |^ ( order (s,n))) mod n) = ((1 |^ ( order (s,n))) mod n) by INT_4: 8;

      

      then (((s * t) |^ (( order ((s * t),n)) * ( order (s,n)))) mod n) = ((1 |^ ( order (s,n))) mod n) by NEWTON: 9

      .= (1 mod n)

      .= 1 by A1, PEPIN: 5;

      then ((((s * t) |^ ( order (s,n))) |^ ( order ((s * t),n))) mod n) = 1 by NEWTON: 9;

      then ((((s |^ ( order (s,n))) * (t |^ ( order (s,n)))) |^ ( order ((s * t),n))) mod n) = 1 by NEWTON: 7;

      then

       A4: ((((s |^ ( order (s,n))) |^ ( order ((s * t),n))) * ((t |^ ( order (s,n))) |^ ( order ((s * t),n)))) mod n) = 1 by NEWTON: 7;

      ((s |^ ( order (s,n))) mod n) = 1 by A1, PEPIN:def 2

      .= (1 mod n) by A1, PEPIN: 5;

      

      then (((s |^ ( order (s,n))) |^ ( order ((s * t),n))) mod n) = ((1 |^ ( order ((s * t),n))) mod n) by INT_4: 8

      .= (1 mod n);

      then (((s |^ ( order (s,n))) |^ ( order ((s * t),n))),1) are_congruent_mod n by A1, NAT_D: 64;

      then ((((s |^ ( order (s,n))) |^ ( order ((s * t),n))) * ((t |^ ( order (s,n))) |^ ( order ((s * t),n)))),(1 * ((t |^ ( order (s,n))) |^ ( order ((s * t),n))))) are_congruent_mod n by INT_4: 11;

      then (((t |^ ( order (s,n))) |^ ( order ((s * t),n))) mod n) = 1 by A4, NAT_D: 64;

      then

       A5: ((t |^ (( order (s,n)) * ( order ((s * t),n)))) mod n) = 1 by NEWTON: 9;

      

       A6: ( order (t,n)) divides ( order ((s * t),n)) by A1, A5, PEPIN: 47, PEPIN: 3;

      ((((s * t) |^ ( order ((s * t),n))) |^ ( order (t,n))) mod n) = ((1 |^ ( order (t,n))) mod n) by A3, INT_4: 8;

      

      then (((s * t) |^ (( order ((s * t),n)) * ( order (t,n)))) mod n) = ((1 |^ ( order (t,n))) mod n) by NEWTON: 9

      .= (1 mod n)

      .= 1 by A1, PEPIN: 5;

      then ((((s * t) |^ ( order (t,n))) |^ ( order ((s * t),n))) mod n) = 1 by NEWTON: 9;

      then ((((s |^ ( order (t,n))) * (t |^ ( order (t,n)))) |^ ( order ((s * t),n))) mod n) = 1 by NEWTON: 7;

      then

       A7: ((((s |^ ( order (t,n))) |^ ( order ((s * t),n))) * ((t |^ ( order (t,n))) |^ ( order ((s * t),n)))) mod n) = 1 by NEWTON: 7;

      ((t |^ ( order (t,n))) mod n) = 1 by A1, PEPIN:def 2

      .= (1 mod n) by A1, PEPIN: 5;

      

      then (((t |^ ( order (t,n))) |^ ( order ((s * t),n))) mod n) = ((1 |^ ( order ((s * t),n))) mod n) by INT_4: 8

      .= (1 mod n);

      then (((t |^ ( order (t,n))) |^ ( order ((s * t),n))),1) are_congruent_mod n by A1, NAT_D: 64;

      then ((((t |^ ( order (t,n))) |^ ( order ((s * t),n))) * ((s |^ ( order (t,n))) |^ ( order ((s * t),n)))),(1 * ((s |^ ( order (t,n))) |^ ( order ((s * t),n))))) are_congruent_mod n by INT_4: 11;

      then (((s |^ ( order (t,n))) |^ ( order ((s * t),n))) mod n) = 1 by A7, NAT_D: 64;

      then ((s |^ (( order (t,n)) * ( order ((s * t),n)))) mod n) = 1 by NEWTON: 9;

      then ( order (s,n)) divides ( order ((s * t),n)) by A1, PEPIN: 3, PEPIN: 47;

      then

       A8: L divides ( order ((s * t),n)) by A6, A1, PEPIN: 4;

      ( order (s,n)) divides L & ( order (t,n)) divides L by NAT_D:def 3;

      then ((s |^ L) mod n) = 1 & ((t |^ L) mod n) = 1 by A1, PEPIN: 48;

      then ((s |^ L),1) are_congruent_mod n & ((t |^ L),1) are_congruent_mod n by A1, PEPIN: 39;

      then (((s |^ L) * (t |^ L)),(1 * 1)) are_congruent_mod n by INT_1: 18;

      then (((s * t) |^ L),1) are_congruent_mod n by NEWTON: 7;

      

      then (((s * t) |^ L) mod n) = (1 mod n) by NAT_D: 64

      .= 1 by A1, PEPIN: 5;

      then ( order ((s * t),n)) divides L by A1, A2, PEPIN: 47;

      hence thesis by A8, NAT_D: 5;

    end;

    reserve fp,fr for FinSequence of NAT ;

    theorem :: INT_8:18

    n > 1 & (s,n) are_coprime & (t,n) are_coprime & ( order ((s * t),n)) = (( order (s,n)) * ( order (t,n))) implies (( order (s,n)),( order (t,n))) are_coprime

    proof

      assume

       A1: n > 1 & (s,n) are_coprime & (t,n) are_coprime & ( order ((s * t),n)) = (( order (s,n)) * ( order (t,n)));

      then (s gcd n) = 1 & (t gcd n) = 1 by INT_2:def 3;

      then ((s * t) gcd n) = 1 by WSIERP_1: 7;

      then

       A2: ((s * t),n) are_coprime by INT_2:def 3;

      set L = (( order (s,n)) lcm ( order (t,n)));

      ( order (s,n)) > 0 & ( order (t,n)) > 0 by A1, PEPIN:def 2;

      then

       A3: L <> 0 by INT_2: 4;

      ( order (s,n)) divides ( order ((s * t),n)) & ( order (t,n)) divides ( order ((s * t),n)) by A1, NAT_D:def 3;

      then

       A4: L divides ( order ((s * t),n)) by NAT_D:def 4;

      

       A5: ( order (s,n)) divides L & ( order (t,n)) divides L by NAT_D:def 4;

      

      then ((s |^ (( order (s,n)) lcm ( order (t,n)))) mod n) = 1 by A1, PEPIN: 48

      .= (1 mod n) by A1, PEPIN: 5;

      then

       A6: ((s |^ (( order (s,n)) lcm ( order (t,n)))),1) are_congruent_mod n by A1, NAT_D: 64;

      ((t |^ L) mod n) = 1 by A1, A5, PEPIN: 48

      .= (1 mod n) by A1, PEPIN: 5;

      then ((t |^ L),1) are_congruent_mod n by A1, NAT_D: 64;

      then

       A7: (((t |^ (( order (s,n)) lcm ( order (t,n)))) * (s |^ (( order (s,n)) lcm ( order (t,n))))),(1 * 1)) are_congruent_mod n by A6, INT_1: 18;

      set B = (s * t);

      ((B |^ (( order (s,n)) lcm ( order (t,n)))),(1 * 1)) are_congruent_mod n by A7, NEWTON: 7;

      

      then

       A8: ((B |^ (( order (s,n)) lcm ( order (t,n)))) mod n) = (1 mod n) by NAT_D: 64

      .= 1 by A1, PEPIN: 5;

      ( order (B,n)) divides L by A8, A1, A2, PEPIN: 47;

      then L = (( order (s,n)) * ( order (t,n))) by A1, A4, NAT_D: 5;

      then (L * (( order (s,n)) gcd ( order (t,n)))) = (L * 1) by NAT_D: 29;

      then (( order (s,n)) gcd ( order (t,n))) = 1 by A3, XCMPLX_1: 5;

      hence thesis by INT_2:def 3;

    end;

    theorem :: INT_8:19

    n > 1 & (s,n) are_coprime & ((s * t) mod n) = 1 implies ( order (s,n)) = ( order (t,n))

    proof

      assume

       A1: n > 1 & (s,n) are_coprime & ((s * t) mod n) = 1;

      set f = (t gcd n);

       A2:

      now

        assume not (t,n) are_coprime ;

        then

         A3: f <> 1 by INT_2:def 3;

        f <> 0 by A1, INT_2: 5;

        then

         A4: f > 1 by A3, NAT_1: 25;

        

         A5: n divides ((s * t) - 1) by A1, PEPIN: 8;

        

         A6: f divides t & f divides n by NAT_D:def 5;

        then

         A7: f divides ((s * t) - 1) by A5, INT_2: 9;

        f divides (s * t) by A6, NAT_D: 9;

        hence contradiction by A4, A7, INT_5: 2, NAT_D: 7;

      end;

      

       A8: ( order (s,n)) > 0 by A1, PEPIN:def 2;

      set M = (s * t);

      

       A9: (M mod n) = (1 mod n) by A1, PEPIN: 5;

      

      then ((M |^ ( order (s,n))) mod n) = ((1 |^ ( order (s,n))) mod n) by INT_4: 8

      .= (1 mod n)

      .= 1 by A1, PEPIN: 5;

      then

       A10: (((s |^ ( order (s,n))) * (t |^ ( order (s,n)))) mod n) = 1 by NEWTON: 7;

      ((s |^ ( order (s,n))) mod n) = 1 by A1, PEPIN:def 2;

      then

       A11: ((t |^ ( order (s,n))) mod n) = 1 by A10, Th6;

      for k be Nat st k > 0 & ((t |^ k) mod n) = 1 holds 0 < ( order (s,n)) & ( order (s,n)) <= k

      proof

        let k be Nat;

        assume

         A12: k > 0 & ((t |^ k) mod n) = 1;

        k is Element of NAT by ORDINAL1:def 12;

        

        then ((M |^ k) mod n) = ((1 |^ k) mod n) by A9, INT_4: 8

        .= (1 mod n)

        .= 1 by A1, PEPIN: 5;

        then (((s |^ k) * (t |^ k)) mod n) = 1 by NEWTON: 7;

        then ((s |^ k) mod n) = 1 by A12, Th6;

        hence thesis by A1, A12, PEPIN:def 2;

      end;

      hence thesis by A11, A8, A2, A1, PEPIN:def 2;

    end;

    theorem :: INT_8:20

    

     Th20: n > 1 & m > 1 & (i,n) are_coprime & m divides n implies ( order (i,m)) divides ( order (i,n))

    proof

      assume

       A1: n > 1 & m > 1 & (i,n) are_coprime & m divides n;

      (i gcd n) = 1 by A1, INT_2:def 3;

      then (i gcd m) = 1 by A1, WSIERP_1: 16;

      then

       A2: (i,m) are_coprime by INT_2:def 3;

      ((i |^ ( order (i,n))) mod n) = 1 by A1, PEPIN:def 2

      .= (1 mod n) by A1, PEPIN: 5;

      then ((i |^ ( order (i,n))),1) are_congruent_mod n by A1, NAT_D: 64;

      then n divides ((i |^ ( order (i,n))) - 1) by INT_2: 15;

      then m divides ((i |^ ( order (i,n))) - 1) by A1, INT_2: 9;

      then ((i |^ ( order (i,n))),1) are_congruent_mod m by INT_2: 15;

      

      then ((i |^ ( order (i,n))) mod m) = (1 mod m) by NAT_D: 64

      .= 1 by A1, PEPIN: 5;

      hence thesis by A1, A2, PEPIN: 47;

    end;

    theorem :: INT_8:21

    n > 1 & m > 1 & (m,n) are_coprime & (i,(m * n)) are_coprime implies ( order (i,(m * n))) = (( order (i,m)) lcm ( order (i,n)))

    proof

      assume

       A1: n > 1 & m > 1 & (m,n) are_coprime & (i,(m * n)) are_coprime ;

      then

       A2: (m * n) > (1 * 1) by XREAL_1: 98;

      then i <> 0 by A1, Th5;

      then

       A3: i > 0 ;

      set K = (( order (i,m)) lcm ( order (i,n)));

      

       A4: m divides (m * n) & n divides (m * n) by NAT_D:def 3;

      then ( order (i,m)) divides ( order (i,(m * n))) & ( order (i,n)) divides ( order (i,(m * n))) by A1, A2, Th20;

      then

       A5: K divides ( order (i,(m * n))) by NAT_D:def 4;

      (i gcd (m * n)) = 1 by A1, INT_2:def 3;

      then (i gcd m) = 1 & (i gcd n) = 1 by A4, WSIERP_1: 16;

      then

       A6: (i,m) are_coprime & (i,n) are_coprime by INT_2:def 3;

      ((i |^ K) - 1) >= 0 by NAT_1: 14, XREAL_1: 48, A3;

      then

       A7: ((i |^ K) - 1) is Element of NAT by INT_1: 3;

      ( order (i,m)) divides K & ( order (i,n)) divides K by NAT_D:def 4;

      then ((i |^ K) mod m) = 1 & ((i |^ K) mod n) = 1 by A1, A6, PEPIN: 48;

      then ((i |^ K),1) are_congruent_mod m & ((i |^ K),1) are_congruent_mod n by A1, PEPIN: 39;

      then m divides ((i |^ K) - 1) & n divides ((i |^ K) - 1) by INT_2: 15;

      then (m * n) divides ((i |^ K) - 1) by A1, A7, PEPIN: 4;

      then ((i |^ K),1) are_congruent_mod (m * n) by INT_2: 15;

      then

       A8: ((i |^ K) mod (m * n)) = 1 by A2, PEPIN: 39;

      ( order (i,(m * n))) divides K by A1, A2, A8, PEPIN: 47;

      hence thesis by A5, NAT_D: 5;

    end;

    definition

      let X be set, m be Nat;

      :: INT_8:def2

      pred X is_RRS_of m means ex fp be FinSequence of INT st ( len fp) = ( len ( Sgm ( RelPrimes m))) & (for d st d in ( dom fp) holds (fp . d) in ( Class (( Cong m),(( Sgm ( RelPrimes m)) . d)))) & X = ( rng fp);

    end

    theorem :: INT_8:22

    

     Th22: ( RelPrimes m) is_RRS_of m

    proof

      

       A1: ( RelPrimes m) c= ( Seg m) by Th1;

      

       A2: ( rng ( Sgm ( RelPrimes m))) = ( RelPrimes m) & ( len ( Sgm ( RelPrimes m))) = ( len ( Sgm ( RelPrimes m))) by A1, FINSEQ_1:def 13;

      ( rng ( Sgm ( RelPrimes m))) c= INT ;

      then

       A3: ( Sgm ( RelPrimes m)) is FinSequence of INT by FINSEQ_1:def 4;

      for a be Nat st a in ( dom ( Sgm ( RelPrimes m))) holds (( Sgm ( RelPrimes m)) . a) in ( Class (( Cong m),(( Sgm ( RelPrimes m)) . a)))

      proof

        let a be Nat;

        assume a in ( dom ( Sgm ( RelPrimes m)));

        ((( Sgm ( RelPrimes m)) . a),(( Sgm ( RelPrimes m)) . a)) are_congruent_mod m by INT_1: 11;

        then [(( Sgm ( RelPrimes m)) . a), (( Sgm ( RelPrimes m)) . a)] in ( Cong m) by INT_4:def 1;

        hence thesis by EQREL_1: 18;

      end;

      then for d st d in ( dom ( Sgm ( RelPrimes m))) holds (( Sgm ( RelPrimes m)) . d) in ( Class (( Cong m),(( Sgm ( RelPrimes m)) . d)));

      hence thesis by A2, A3;

    end;

    theorem :: INT_8:23

    

     Th23: d in ( dom ( Sgm ( RelPrimes m))) & e in ( dom ( Sgm ( RelPrimes m))) & d <> e implies not ((( Sgm ( RelPrimes m)) . d),(( Sgm ( RelPrimes m)) . e)) are_congruent_mod m

    proof

      assume

       A1: d in ( dom ( Sgm ( RelPrimes m))) & e in ( dom ( Sgm ( RelPrimes m))) & d <> e;

      

       A2: ( RelPrimes m) c= ( Seg m) by Th1;

      ( rng ( Sgm ( RelPrimes m))) = ( RelPrimes m) by A2, FINSEQ_1:def 13;

      then

       A3: (( Sgm ( RelPrimes m)) . d) in ( RelPrimes m) & (( Sgm ( RelPrimes m)) . e) in ( RelPrimes m) by A1, FUNCT_1:def 3;

      then

      consider k1 be Element of NAT such that

       A4: k1 = (( Sgm ( RelPrimes m)) . d) & (m,k1) are_coprime & k1 >= 1 & k1 <= m;

      consider k2 be Element of NAT such that

       A5: k2 = (( Sgm ( RelPrimes m)) . e) & (m,k2) are_coprime & k2 >= 1 & k2 <= m by A3;

      

       A6: ((( Sgm ( RelPrimes m)) . d) - (( Sgm ( RelPrimes m)) . e)) <= (m - 1) & (1 - m) <= ((( Sgm ( RelPrimes m)) . d) - (( Sgm ( RelPrimes m)) . e)) by A4, A5, XREAL_1: 13;

      

       A7: (m - 1) < m by XREAL_1: 146;

      

       A8: ((( Sgm ( RelPrimes m)) . d) - (( Sgm ( RelPrimes m)) . e)) < m by A6, XXREAL_0: 2, XREAL_1: 146;

      ( - m) < ( - (m - 1)) by A7, XREAL_1: 24;

      then ( - m) < ((( Sgm ( RelPrimes m)) . d) - (( Sgm ( RelPrimes m)) . e)) by A6, XXREAL_0: 2;

      then

       A9: |.((( Sgm ( RelPrimes m)) . d) - (( Sgm ( RelPrimes m)) . e)).| < m by A8, SEQ_2: 1;

      now

        assume ((( Sgm ( RelPrimes m)) . d),(( Sgm ( RelPrimes m)) . e)) are_congruent_mod m;

        then

         A10: m divides ((( Sgm ( RelPrimes m)) . d) - (( Sgm ( RelPrimes m)) . e)) by INT_2: 15;

        ( Sgm ( RelPrimes m)) is one-to-one by A2, FINSEQ_3: 92;

        then ((( Sgm ( RelPrimes m)) . d) - (( Sgm ( RelPrimes m)) . e)) <> 0 by A1, FUNCT_1:def 4;

        then |.m.| <= |.((( Sgm ( RelPrimes m)) . d) - (( Sgm ( RelPrimes m)) . e)).| by A10, INT_4: 6;

        hence contradiction by A9, ABSVALUE:def 1;

      end;

      hence thesis;

    end;

    theorem :: INT_8:24

    

     Th24: for X be finite set st X is_RRS_of m holds ( card X) = ( Euler m) & (for x,y be Integer st x in X & y in X & x <> y holds not (x,y) are_congruent_mod m) & (for x be Integer st x in X holds (x,m) are_coprime )

    proof

      let X be finite set;

      assume X is_RRS_of m;

      then

      consider fp be FinSequence of INT such that

       A1: ( len fp) = ( len ( Sgm ( RelPrimes m))) & (for d st d in ( dom fp) holds (fp . d) in ( Class (( Cong m),(( Sgm ( RelPrimes m)) . d)))) & X = ( rng fp);

      

       A2: ( dom fp) = ( dom ( Sgm ( RelPrimes m))) by A1, FINSEQ_3: 29;

      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

         A3: a in ( dom fp) & b in ( dom fp) & (fp . a) = (fp . b);

        reconsider a, b as Element of NAT by A3;

        reconsider l = (fp . a), ll = (fp . b) as Element of INT by A3, FINSEQ_2: 11;

        l in ( Class (( Cong m),(( Sgm ( RelPrimes m)) . a))) & ll in ( Class (( Cong m),(( Sgm ( RelPrimes m)) . b))) by A1, A3;

        then [(( Sgm ( RelPrimes m)) . a), l] in ( Cong m) & [(( Sgm ( RelPrimes m)) . b), ll] in ( Cong m) by EQREL_1: 18;

        then

         A4: ((( Sgm ( RelPrimes m)) . a),l) are_congruent_mod m & ((( Sgm ( RelPrimes m)) . b),ll) are_congruent_mod m by INT_4:def 1;

        then (l,(( Sgm ( RelPrimes m)) . b)) are_congruent_mod m by A3, INT_1: 14;

        hence thesis by Th23, A3, A2, A4, INT_1: 15;

      end;

      then

       A5: fp is one-to-one by FUNCT_1:def 4;

      

       A6: ( RelPrimes m) c= ( Seg m) by Th1;

      

       A7: ( card X) = ( len ( Sgm ( RelPrimes m))) by A1, FINSEQ_4: 62, A5

      .= ( Euler m) by A6, FINSEQ_3: 39;

      

       A8: for x,y be Integer st x in X & y in X & x <> y holds not (x,y) are_congruent_mod m

      proof

        let x,y be Integer;

        assume

         A9: x in X & y in X & x <> y;

        then

        consider d be Nat such that

         A10: d in ( dom fp) & (fp . d) = x by A1, FINSEQ_2: 10;

        consider e be Nat such that

         A11: e in ( dom fp) & (fp . e) = y by A1, A9, FINSEQ_2: 10;

        

         A12: d in ( dom ( Sgm ( RelPrimes m))) & e in ( dom ( Sgm ( RelPrimes m))) by A10, A11, A1, FINSEQ_3: 29;

        reconsider d, e as Element of NAT by A10, A11;

        (fp . d) in ( Class (( Cong m),(( Sgm ( RelPrimes m)) . d))) & (fp . e) in ( Class (( Cong m),(( Sgm ( RelPrimes m)) . e))) by A10, A11, A1;

        then [(( Sgm ( RelPrimes m)) . d), (fp . d)] in ( Cong m) & [(( Sgm ( RelPrimes m)) . e), (fp . e)] in ( Cong m) by EQREL_1: 18;

        then

         A13: ((( Sgm ( RelPrimes m)) . d),(fp . d)) are_congruent_mod m & ((( Sgm ( RelPrimes m)) . e),(fp . e)) are_congruent_mod m by INT_4:def 1;

        now

          assume ((fp . d),(fp . e)) are_congruent_mod m;

          then ((( Sgm ( RelPrimes m)) . d),(fp . e)) are_congruent_mod m by A13, INT_1: 15;

          then ((fp . e),(( Sgm ( RelPrimes m)) . d)) are_congruent_mod m by INT_1: 14;

          hence contradiction by A12, A10, A11, A9, Th23, A13, INT_1: 15;

        end;

        hence thesis by A10, A11;

      end;

      for x be Integer st x in X holds (x,m) are_coprime

      proof

        let x be Integer;

        assume x in X;

        then

        consider d be Nat such that

         A14: d in ( dom fp) & (fp . d) = x by A1, FINSEQ_2: 10;

        reconsider d as Element of NAT by A14;

        (fp . d) in ( Class (( Cong m),(( Sgm ( RelPrimes m)) . d))) by A1, A14;

        then [(( Sgm ( RelPrimes m)) . d), (fp . d)] in ( Cong m) by EQREL_1: 18;

        then ((( Sgm ( RelPrimes m)) . d),(fp . d)) are_congruent_mod m by INT_4:def 1;

        then

         A15: ((( Sgm ( RelPrimes m)) . d) gcd m) = ((fp . d) gcd m) by WSIERP_1: 43;

        ( RelPrimes m) c= ( Seg m) by Th1;

        then ( rng ( Sgm ( RelPrimes m))) = ( RelPrimes m) by FINSEQ_1:def 13;

        then (( Sgm ( RelPrimes m)) . d) in ( RelPrimes m) by A2, A14, FUNCT_1:def 3;

        then

        consider k be Element of NAT such that

         A16: (( Sgm ( RelPrimes m)) . d) = k & (m,k) are_coprime & k >= 1 & k <= m;

        ((fp . d) gcd m) = 1 by A15, A16, INT_2:def 3;

        hence thesis by A14, INT_2:def 3;

      end;

      hence thesis by A7, A8;

    end;

    

     Lm3: for X be finite set st ( card X) = 0 holds X = {} ;

    theorem :: INT_8:25

     {} is_RRS_of m iff m = 0

    proof

      thus {} is_RRS_of m implies m = 0

      proof

        assume {} is_RRS_of m;

        then ( Euler m) = ( card {} ) by Th24;

        hence thesis by PEPIN: 42;

      end;

      assume

       A1: m = 0 ;

      reconsider fp = ( <*> INT ) as FinSequence of INT ;

      ( RelPrimes m) c= ( Seg m) by Th1;

      then ( card ( RelPrimes m)) <= ( card ( Seg m)) by NAT_1: 43;

      then ( card ( RelPrimes m)) <= 0 by A1;

      then ( card ( RelPrimes m)) = 0 ;

      then

       A2: ( len ( Sgm ( RelPrimes m))) = ( len fp) by Lm3, FINSEQ_3: 43;

      (for d st d in ( dom fp) holds (fp . d) in ( Class (( Cong m),(( Sgm ( RelPrimes m)) . d))));

      hence thesis by RELAT_1: 38, A2;

    end;

    theorem :: INT_8:26

    

     Th26: for X be finite Subset of INT st (1 < m & ( card X) = ( Euler m) & (for x,y be Integer st x in X & y in X & x <> y holds not (x,y) are_congruent_mod m) & (for x be Integer st x in X holds (x,m) are_coprime )) holds X is_RRS_of m

    proof

      let X be finite Subset of INT ;

      assume

       A1: (1 < m & ( card X) = ( Euler m) & (for x,y be Integer st x in X & y in X & x <> y holds not (x,y) are_congruent_mod m) & (for x be Integer st x in X holds (x,m) are_coprime ));

      then ( card X) <> 0 by PEPIN: 42;

      then

      reconsider X as non empty finite Subset of INT ;

      set Y = ( RelPrimes m);

      

       A2: Y c= ( Seg m) by Th1;

      reconsider Y as finite set;

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

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

      then 1 in Y by A1;

      then

      reconsider Y as non empty finite set;

      reconsider Y as non empty finite Subset of INT by NUMBERS: 17, XBOOLE_1: 1;

      

       A3: Y is_RRS_of m by Th22;

      defpred P[ Nat, set] means $2 in ( Class (( Cong m),(( Sgm Y) . $1)));

      

       A4: for a be Nat st a in ( Seg ( Euler m)) holds ex y be Element of X st P[a, y]

      proof

        let a be Nat;

        assume

         A5: a in ( Seg ( Euler m));

        consider fp be FinSequence such that

         A6: ( len fp) = ( Euler m) & (for d st d in ( dom fp) holds (fp . d) in X) & fp is one-to-one by A1, INT_4: 51;

        for d be Nat st d in ( dom fp) holds (fp . d) in X by A6;

        then

        reconsider fp as FinSequence of X by FINSEQ_2: 12;

        

         A7: ( card ( rng fp)) = ( card X) by A1, A6, FINSEQ_4: 62;

        ( rng fp) c= X by FINSEQ_1:def 4;

        then

         A8: ( rng fp) = X by A7, CARD_2: 102;

        defpred PP[ Nat, set] means (fp . $1) in ( Class (( Cong m),$2));

        

         A9: for c be Nat st c in ( Seg ( Euler m)) holds ex r be Element of Y st PP[c, r]

        proof

          let c be Nat;

          assume c in ( Seg ( Euler m));

          then c in ( dom fp) by A6, FINSEQ_1:def 3;

          then

           A10: ((fp . c),m) are_coprime by A1, A6;

          set r = ((fp . c) mod m);

          

           A11: ((fp . c) mod m) = (((((fp . c) div m) * m) + r) mod m) by A1, INT_1: 59

          .= (r mod m) by EULER_1: 12;

          then ((fp . c),r) are_congruent_mod m by A1, NAT_D: 64;

          

          then

           A12: (r gcd m) = ((fp . c) gcd m) by WSIERP_1: 43

          .= 1 by A10, INT_2:def 3;

          then

           A13: (r,m) are_coprime by INT_2:def 3;

          reconsider r as Element of NAT by INT_1: 3, INT_1: 57;

          reconsider zz = 0 , j = 1 as Real;

          now

            assume r = 0 ;

            then |.m.| = 1 by A12, WSIERP_1: 8;

            hence contradiction by A1, ABSVALUE:def 1;

          end;

          then (r - 1) >= 0 by INT_1: 52;

          then

           A14: ((r - 1) + j) >= (zz + j) by XREAL_1: 7;

          r <= m by A1, INT_1: 58;

          then

           A15: r in Y by A14, A13;

          (r,(fp . c)) are_congruent_mod m by A11, A1, NAT_D: 64;

          then [r, (fp . c)] in ( Cong m) by INT_4:def 1;

          then (fp . c) in ( Class (( Cong m),r)) by EQREL_1: 18;

          hence thesis by A15;

        end;

        consider fr be FinSequence of Y such that

         A16: ( dom fr) = ( Seg ( Euler m)) & for c be Nat st c in ( Seg ( Euler m)) holds PP[c, (fr . c)] from FINSEQ_1:sch 5( A9);

        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

           A17: x1 in ( dom fr) & x2 in ( dom fr) & (fr . x1) = (fr . x2);

          then

          reconsider x1, x2 as Element of NAT ;

          (fp . x1) in ( Class (( Cong m),(fr . x1))) & (fp . x2) in ( Class (( Cong m),(fr . x2))) by A17, A16;

          then [(fr . x1), (fp . x1)] in ( Cong m) & [(fr . x2), (fp . x2)] in ( Cong m) by EQREL_1: 18;

          then ((fr . x1),(fp . x1)) are_congruent_mod m & ((fr . x2),(fp . x2)) are_congruent_mod m by INT_4:def 1;

          then

           A18: ((fp . x1),(fp . x2)) are_congruent_mod m by A17, PEPIN: 40;

          

           A19: x1 in ( dom fp) & x2 in ( dom fp) by A17, A6, A16, FINSEQ_1:def 3;

          then (fp . x1) in X & (fp . x2) in X by A8, FUNCT_1:def 3;

          then (fp . x1) = (fp . x2) by A1, A18;

          hence thesis by A19, A6, FUNCT_1:def 4;

        end;

        then fr is one-to-one by FUNCT_1:def 4;

        

        then

         A20: ( card ( rng fr)) = ( len fr) by FINSEQ_4: 62

        .= ( card Y) by A16, FINSEQ_1:def 3;

        ( rng fr) c= Y by FINSEQ_1:def 4;

        then

         A21: ( rng fr) = Y by A20, CARD_2: 102;

        ( len ( Sgm Y)) = ( Euler m) by A2, FINSEQ_3: 39;

        then a in ( dom ( Sgm Y)) by A5, FINSEQ_1:def 3;

        then (( Sgm Y) . a) in ( rng ( Sgm Y)) by FUNCT_1:def 3;

        then (( Sgm Y) . a) in ( rng fr) by A21, A2, FINSEQ_1:def 13;

        then

        consider i be Nat such that

         A22: i in ( dom fr) & (fr . i) = (( Sgm Y) . a) by FINSEQ_2: 10;

        i in ( dom fp) by A22, A6, A16, FINSEQ_1:def 3;

        then (fp . i) is Element of X by A8, FUNCT_1:def 3;

        hence thesis by A22, A16;

      end;

      consider f be FinSequence of X such that

       A23: ( dom f) = ( Seg ( Euler m)) & for a be Nat st a in ( Seg ( Euler m)) holds P[a, (f . a)] from FINSEQ_1:sch 5( A4);

      

       A24: ( len f) = ( Euler m) by A23, FINSEQ_1:def 3;

      for a,b be object st a in ( dom f) & b in ( dom f) & (f . a) = (f . b) holds a = b

      proof

        let a,b be object;

        assume

         A25: a in ( dom f) & b in ( dom f) & (f . a) = (f . b);

        then

        reconsider a, b as Element of NAT ;

        (f . a) in ( Class (( Cong m),(( Sgm Y) . a))) & (f . b) in ( Class (( Cong m),(( Sgm Y) . b))) by A25, A23;

        then [(( Sgm Y) . a), (f . a)] in ( Cong m) & [(( Sgm Y) . b), (f . b)] in ( Cong m) by EQREL_1: 18;

        then

         A26: ((( Sgm Y) . a),(f . a)) are_congruent_mod m & ((( Sgm Y) . b),(f . b)) are_congruent_mod m by INT_4:def 1;

        then ((f . b),(( Sgm Y) . b)) are_congruent_mod m by INT_1: 14;

        then

         A27: ((( Sgm Y) . a),(( Sgm Y) . b)) are_congruent_mod m by A26, A25, INT_1: 15;

        now

          assume

           A28: a <> b;

          ( len ( Sgm Y)) = ( Euler m) by A2, FINSEQ_3: 39;

          then

           A29: a in ( dom ( Sgm Y)) & b in ( dom ( Sgm Y)) by A25, A23, FINSEQ_1:def 3;

          ( Sgm Y) is one-to-one by A2, FINSEQ_3: 92;

          then

           A30: (( Sgm Y) . a) <> (( Sgm Y) . b) by A28, A29, FUNCT_1:def 4;

          (( Sgm Y) . a) in ( rng ( Sgm Y)) & (( Sgm Y) . b) in ( rng ( Sgm Y)) by A29, FUNCT_1:def 3;

          then (( Sgm Y) . a) in Y & (( Sgm Y) . b) in Y by A2, FINSEQ_1:def 13;

          hence contradiction by A27, A30, A3, Th24;

        end;

        hence thesis;

      end;

      then f is one-to-one by FUNCT_1:def 4;

      then

       A31: ( card X) = ( card ( rng f)) by A1, A24, FINSEQ_4: 62;

      

       A32: ( rng f) c= X by FINSEQ_1:def 4;

      take f;

      thus thesis by A2, A23, A24, A32, A31, CARD_2: 102, FINSEQ_3: 39;

    end;

    theorem :: INT_8:27

    for X be finite Subset of INT , a be Integer st (m > 1 & (a,m) are_coprime & X is_RRS_of m) holds (a ** X) is_RRS_of m

    proof

      let X be finite Subset of INT , a be Integer;

      assume

       A1: m > 1 & (a,m) are_coprime & X is_RRS_of m;

      then

       A2: ( card X) = ( Euler m) & (for x,y be Integer st x in X & y in X & x <> y holds not (x,y) are_congruent_mod m) & (for x be Integer st x in X holds (x,m) are_coprime ) by Th24;

      

       A3: (a ** X) c= INT by INT_1:def 2;

      a <> 0 by A1, Th5;

      then

       A4: ( card (a ** X)) = ( Euler m) by A2, INT_4: 5;

      

       A5: for x,y be Integer st x in (a ** X) & y in (a ** X) & x <> y holds not (x,y) are_congruent_mod m

      proof

        let x,y be Integer;

        assume

         A6: x in (a ** X) & y in (a ** X) & x <> y;

        then

        consider z1 be Integer such that

         A7: z1 in X & x = (a * z1) by Th3;

        consider z2 be Integer such that

         A8: z2 in X & y = (a * z2) by A6, Th3;

         not (z1,z2) are_congruent_mod m by A7, A6, A8, A1, Th24;

        hence thesis by A7, A8, A1, INT_4: 9;

      end;

      for x be Integer st x in (a ** X) holds (x,m) are_coprime

      proof

        let x be Integer;

        assume x in (a ** X);

        then

        consider y such that

         A9: y in X & x = (a * y) by Th3;

        (y,m) are_coprime by A9, A1, Th24;

        hence thesis by A9, A1, INT_2: 26;

      end;

      hence thesis by A1, A3, A4, A5, Th26;

    end;

    definition

      let i, n;

      :: INT_8:def3

      pred i is_primitive_root_of n means ( order (i,n)) = ( Euler n);

    end

    theorem :: INT_8:28

    n > 1 & (i,n) are_coprime implies (i is_primitive_root_of n iff for fn st ( len fn) = ( Euler n) & (for d be Nat st d in ( dom fn) holds (fn . d) = (i |^ d)) holds ( rng fn) is_RRS_of n)

    proof

      assume

       A1: n > 1 & (i,n) are_coprime ;

      then

       A2: i <> 0 by Th5;

      reconsider z = 0 , j = 1 as Element of REAL by XREAL_0:def 1;

      (i - 1) >= 0 by A2, INT_1: 52;

      then

       A3: ((i - 1) + j) >= (z + j) by XREAL_1: 7;

      

       A4: (i gcd n) = 1 by A1, INT_2:def 3;

      thus i is_primitive_root_of n implies for fn st ( len fn) = ( Euler n) & (for d be Nat st d in ( dom fn) holds (fn . d) = (i |^ d)) holds ( rng fn) is_RRS_of n

      proof

        assume i is_primitive_root_of n;

        then

         A5: ( order (i,n)) = ( Euler n);

        for fn st ( len fn) = ( Euler n) & (for d be Nat st d in ( dom fn) holds (fn . d) = (i |^ d)) holds ( rng fn) is_RRS_of n

        proof

          let fn;

          assume

           A6: ( len fn) = ( Euler n) & (for d be Nat st d in ( dom fn) holds (fn . d) = (i |^ d));

          fn is one-to-one

          proof

            per cases by A3, XXREAL_0: 1;

              suppose

               A7: i = 1;

              reconsider fn as FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

              fn = <*(fn . 1)*> by FINSEQ_5: 14, A6, A5, A1, PEPIN: 46, A7;

              hence thesis;

            end;

              suppose

               A8: i > 1;

              for x1,x2 be object st x1 in ( dom fn) & x2 in ( dom fn) & (fn . x1) = (fn . x2) holds x1 = x2

              proof

                let x1,x2 be object;

                assume

                 A9: x1 in ( dom fn) & x2 in ( dom fn) & (fn . x1) = (fn . x2);

                then

                reconsider x1, x2 as Element of NAT ;

                (i |^ x1) = (fn . x2) by A9, A6

                .= (i |^ x2) by A9, A6;

                hence thesis by A8, PEPIN: 30;

              end;

              hence thesis by FUNCT_1:def 4;

            end;

          end;

          then

           A10: ( card ( rng fn)) = ( Euler n) by A6, FINSEQ_4: 62;

          

           A11: for x,y be Integer st x in ( rng fn) & y in ( rng fn) & x <> y holds not (x,y) are_congruent_mod n

          proof

            let x,y be Integer;

            assume

             A12: x in ( rng fn) & y in ( rng fn) & x <> y & (x,y) are_congruent_mod n;

            then

            consider s such that

             A13: s in ( dom fn) & (fn . s) = x by FINSEQ_2: 10;

            consider t such that

             A14: t in ( dom fn) & (fn . t) = y by A12, FINSEQ_2: 10;

            

             A15: x = (i |^ s) & y = (i |^ t) by A13, A14, A6;

            

             A16: 1 <= s & s <= ( order (i,n)) & 1 <= t & t <= ( order (i,n)) by A13, A14, A5, A6, FINSEQ_3: 25;

            per cases by A12, A13, A14, XXREAL_0: 1;

              suppose s > t;

              then

               A17: (s - t) > 0 by XREAL_1: 50;

              then

              reconsider k = (s - t) as Element of NAT by INT_1: 3;

              ((i |^ s) - (i |^ t)) = ((i |^ (t + k)) - (i |^ t))

              .= (((i |^ t) * (i |^ k)) - ((i |^ t) * 1)) by NEWTON: 8

              .= ((i |^ t) * ((i |^ k) - 1));

              then

               A18: n divides ((i |^ t) * ((i |^ k) - 1)) by A15, A12, INT_2: 15;

              ((i |^ t) gcd n) = 1 by A2, A4, A1, NAT_4: 10;

              then n divides ((i |^ k) - 1) by A18, WSIERP_1: 29;

              then ((i |^ k),1) are_congruent_mod n by INT_2: 15;

              

              then ((i |^ k) mod n) = (1 mod n) by NAT_D: 64

              .= 1 by A1, PEPIN: 5;

              then

               A19: ( order (i,n)) <= k by A17, A1, PEPIN: 47, NAT_D: 7;

              k <= (( order (i,n)) - 1) & (( order (i,n)) - 1) < ( order (i,n)) by A16, XREAL_1: 13, XREAL_1: 146;

              hence contradiction by A19, XXREAL_0: 2;

            end;

              suppose s < t;

              then

               A20: (t - s) > 0 by XREAL_1: 50;

              then

              reconsider k = (t - s) as Element of NAT by INT_1: 3;

              

               A21: ((i |^ t) - (i |^ s)) = ((i |^ (s + k)) - (i |^ s))

              .= (((i |^ s) * (i |^ k)) - ((i |^ s) * 1)) by NEWTON: 8

              .= ((i |^ s) * ((i |^ k) - 1));

              ((i |^ t),(i |^ s)) are_congruent_mod n by A15, A12, INT_1: 14;

              then

               A22: n divides ((i |^ s) * ((i |^ k) - 1)) by A21, INT_2: 15;

              ((i |^ s) gcd n) = 1 by A2, A4, A1, NAT_4: 10;

              then n divides ((i |^ k) - 1) by A22, WSIERP_1: 29;

              then ((i |^ k),1) are_congruent_mod n by INT_2: 15;

              

              then ((i |^ k) mod n) = (1 mod n) by NAT_D: 64

              .= 1 by A1, PEPIN: 5;

              then

               A23: ( order (i,n)) <= k by A20, A1, PEPIN: 47, NAT_D: 7;

              k <= (( order (i,n)) - 1) & (( order (i,n)) - 1) < ( order (i,n)) by A16, XREAL_1: 13, XREAL_1: 146;

              hence contradiction by A23, XXREAL_0: 2;

            end;

          end;

          

           A24: for x be Integer st x in ( rng fn) holds (x,n) are_coprime

          proof

            let x be Integer;

            assume x in ( rng fn);

            then

            consider s such that

             A25: s in ( dom fn) & (fn . s) = x by FINSEQ_2: 10;

            

             A26: x = (i |^ s) by A25, A6;

            ((i |^ s) gcd n) = 1 by A2, A4, A1, NAT_4: 10;

            hence thesis by A26, INT_2:def 3;

          end;

          thus thesis by A1, A10, A11, A24, Th26;

        end;

        hence thesis;

      end;

      assume

       A27: for fn st ( len fn) = ( Euler n) & (for d be Nat st d in ( dom fn) holds (fn . d) = (i |^ d)) holds ( rng fn) is_RRS_of n;

      deffunc G( Nat) = (i |^ $1);

      consider f be FinSequence such that

       A28: ( len f) = ( Euler n) & for d be Nat st d in ( dom f) holds (f . d) = G(d) from FINSEQ_1:sch 2;

      for s st s in ( dom f) holds (f . s) in NAT

      proof

        let s;

        assume

         A29: s in ( dom f);

        (f . s) = (i |^ s) by A28, A29;

        hence thesis by ORDINAL1:def 12;

      end;

      then

      reconsider f as FinSequence of NAT by FINSEQ_2: 12;

      

       A30: ( rng f) is_RRS_of n by A28, A27;

      then ( card ( rng f)) = ( Euler n) & (for x,y be Integer st x in ( rng f) & y in ( rng f) & x <> y holds not (x,y) are_congruent_mod n) by Th24;

      then

       A31: f is one-to-one by A28, FINSEQ_4: 62;

      

       A32: ( Euler n) <> 0 by A1, PEPIN: 42;

      then

       A33: ( Euler n) > 0 ;

      

       A34: ( Euler n) >= 1 by A1, PEPIN: 42, NAT_1: 14;

      

       A35: ((i |^ ( Euler n)) mod n) = 1 by A1, Th5, EULER_2: 18;

      for s st s > 0 & ((i |^ s) mod n) = 1 holds 0 < ( Euler n) & ( Euler n) <= s

      proof

        let s;

        assume

         A36: s > 0 & ((i |^ s) mod n) = 1;

        now

          assume s < ( Euler n);

          then

           A37: (( Euler n) - s) > 0 by XREAL_1: 50;

          then

          reconsider k = (( Euler n) - s) as Element of NAT by INT_1: 3;

          

           A38: k < ( Euler n) & k >= 1 by A36, A37, XREAL_1: 44, NAT_1: 14;

          then

           A39: k in ( dom f) & ( Euler n) in ( dom f) by A28, A34, FINSEQ_3: 25;

          then

           A40: (f . k) in ( rng f) & (f . ( Euler n)) in ( rng f) by FUNCT_1: 3;

          (f . k) <> (f . ( Euler n)) by A39, A31, A38, FUNCT_1:def 4;

          then not ((f . k),(f . ( Euler n))) are_congruent_mod n by A40, A30, Th24;

          then not ((i |^ k),(f . ( Euler n))) are_congruent_mod n by A39, A28;

          then

           A41: not ((i |^ k),(i |^ ( Euler n))) are_congruent_mod n by A39, A28;

          ((i |^ ( Euler n)),(i |^ s)) are_congruent_mod n by A36, A35, A1, NAT_D: 64;

          then

           A42: n divides ((i |^ ( Euler n)) - (i |^ s)) by INT_2: 15;

          

           A43: ((i |^ ( Euler n)) - (i |^ s)) = ((i |^ (s + k)) - (i |^ s))

          .= (((i |^ s) * (i |^ k)) - ((i |^ s) * 1)) by NEWTON: 8

          .= ((i |^ s) * ((i |^ k) - 1));

          ((i |^ s) gcd n) = 1 by A2, A4, A1, NAT_4: 10;

          then

           A44: n divides ((i |^ k) - 1) by A42, A43, WSIERP_1: 29;

          ((i |^ ( Euler n)) mod n) = (1 mod n) by A1, A35, PEPIN: 5;

          then ((i |^ ( Euler n)),1) are_congruent_mod n by A1, NAT_D: 64;

          then n divides ((i |^ ( Euler n)) - 1) by INT_2: 15;

          then n divides (((i |^ k) - 1) - ((i |^ ( Euler n)) - 1)) by A44, INT_5: 1;

          then n divides ((i |^ k) - (i |^ ( Euler n)));

          hence contradiction by A41, INT_2: 15;

        end;

        hence thesis by A32;

      end;

      then ( order (i,n)) = ( Euler n) by A1, A33, A35, PEPIN:def 2;

      hence thesis;

    end;

    theorem :: INT_8:29

    p > 2 & (i,p) are_coprime & i is_primitive_root_of p implies (for k be Nat holds not (i |^ ((2 * k) + 1)) is_quadratic_residue_mod p)

    proof

      assume

       A1: p > 2 & (i,p) are_coprime & i is_primitive_root_of p;

      

       A2: ( order (i,p)) = ( Euler p) by A1

      .= (p - 1) by EULER_1: 20;

      

       A3: p > 1 by INT_2:def 4;

      

      then

       A4: ((p -' 1) + 1) = ((p + 1) -' 1) by NAT_D: 38

      .= ((p + 1) - 1) by NAT_D: 37

      .= ((p - 1) + 1);

      now

        assume ex k be Nat st (i |^ ((2 * k) + 1)) is_quadratic_residue_mod p;

        then

        consider k be Nat such that

         A5: (i |^ ((2 * k) + 1)) is_quadratic_residue_mod p;

        set L = ((2 * k) + 1);

        set Q = (p -' 1);

        ((i |^ ((2 * k) + 1)),p) are_coprime by A1, WSIERP_1: 10;

        then ((i |^ ((2 * k) + 1)) gcd p) = 1 by INT_2:def 3;

        

        then 1 = (((i |^ L) |^ (Q div 2)) mod p) by A1, A5, INT_5: 17

        .= ((i |^ (((2 * k) + 1) * ((p -' 1) div 2))) mod p) by NEWTON: 9

        .= ((i |^ (((2 * k) * ((p -' 1) div 2)) + (1 * ((p -' 1) div 2)))) mod p)

        .= (((i |^ ((2 * k) * ((p -' 1) div 2))) * (i |^ ((p -' 1) div 2))) mod p) by NEWTON: 8;

        then

         A6: (((i |^ ((2 * k) * ((p -' 1) div 2))) * (i |^ ((p -' 1) div 2))),1) are_congruent_mod p by A3, PEPIN: 39;

        p is odd by A1, PEPIN: 17;

        then 2 divides (p -' 1) by PEPIN: 22, A4;

        then

         A7: (p -' 1) = (2 * ((p -' 1) div 2)) by NAT_D: 3;

        ((i |^ (p -' 1)) mod p) = 1 by A1, PEPIN: 37;

        then (((i |^ Q) |^ k) mod p) = 1 by A3, PEPIN: 35;

        then (((i |^ Q) |^ k),1) are_congruent_mod p by A3, PEPIN: 39;

        then ((i |^ (k * (p -' 1))),1) are_congruent_mod p by NEWTON: 9;

        then (((i |^ (k * (p -' 1))) * (i |^ ((p -' 1) div 2))),(1 * (i |^ ((p -' 1) div 2)))) are_congruent_mod p by INT_4: 11;

        then ((i |^ ((p -' 1) div 2)),1) are_congruent_mod p by A6, A7, PEPIN: 40;

        then

         A8: ((i |^ ((p -' 1) div 2)) mod p) = 1 by A3, PEPIN: 39;

        (p - 1) >= 2 by A1, INT_1: 52;

        then

         A9: ((p -' 1) div 2) >= (2 div 2) by A4, NAT_2: 24;

        

         A10: (p -' 1) divides ((p -' 1) div 2) by A8, A3, A1, A2, A4, PEPIN: 47;

        ((p -' 1) div 2) divides (p -' 1) by A7, NAT_D:def 3;

        then (2 * ((p -' 1) div 2)) = (1 * ((p -' 1) div 2)) by A7, A10, NAT_D: 5;

        hence contradiction by A9, PEPIN: 44;

      end;

      hence thesis;

    end;

    theorem :: INT_8:30

    for k be Nat st k >= 3 holds (for m st (m,(2 |^ k)) are_coprime holds not m is_primitive_root_of (2 |^ k))

    proof

      let k be Nat;

      assume

       A1: k >= 3;

      now

        assume ex m st (m,(2 |^ k)) are_coprime & m is_primitive_root_of (2 |^ k);

        then

        consider m such that

         A2: (m,(2 |^ k)) are_coprime & m is_primitive_root_of (2 |^ k);

        now

          assume m is even;

          then

           A3: 2 divides m by PEPIN: 22;

          (2 |^ 1) divides (2 |^ k) by A1, XXREAL_0: 2, NEWTON: 89;

          then 2 divides (2 |^ k);

          hence contradiction by A2, A3, PYTHTRIP:def 1;

        end;

        then

         A4: ((m |^ (2 |^ (k -' 2))) mod (2 |^ k)) = 1 by A1, Th7;

        

         A5: (2 |^ k) > 1 by A1, PEPIN: 25;

        ( order (m,(2 |^ k))) <= (2 |^ (k -' 2)) by A2, A4, A5, PEPIN:def 2;

        then

         A6: ( Euler (2 |^ k)) <= (2 |^ (k -' 2)) by A2;

        

         A7: k > 1 by XXREAL_0: 2, A1;

        k = ((k -' 1) + 1) by A7, XREAL_1: 235;

        

        then

         A8: ( Euler (2 |^ k)) = ((2 |^ ((k -' 1) + 1)) - (2 |^ (k -' 1))) by A1, XXREAL_0: 2, Th8, INT_2: 28

        .= (((2 |^ (k -' 1)) * 2) - ((2 |^ (k -' 1)) * 1)) by NEWTON: 6

        .= (2 |^ (k -' 1));

        (k -' 1) = (((k - 1) - 1) + 1) by A7, XREAL_1: 233

        .= ((k - 2) + 1)

        .= ((k -' 2) + 1) by A1, XXREAL_0: 2, XREAL_1: 233;

        then ((2 |^ (k -' 2)) * 2) <= (2 |^ (k -' 2)) by A6, A8, NEWTON: 6;

        then (((2 |^ (k -' 2)) * 2) / (2 |^ (k -' 2))) <= ((2 |^ (k -' 2)) / (2 |^ (k -' 2))) by XREAL_1: 72;

        then 2 <= ((2 |^ (k -' 2)) / (2 |^ (k -' 2))) by XCMPLX_1: 89;

        then 2 <= 1 by XCMPLX_1: 60;

        hence contradiction;

      end;

      hence thesis;

    end;

    theorem :: INT_8:31

    p > 2 & k >= 2 & (i,p) are_coprime & i is_primitive_root_of p & ((i |^ (p -' 1)) mod (p ^2 )) <> 1 implies ((i |^ ( Euler (p |^ (k -' 1)))) mod (p |^ k)) <> 1

    proof

      assume

       A1: p > 2 & k >= 2 & (i,p) are_coprime & i is_primitive_root_of p & ((i |^ (p -' 1)) mod (p ^2 )) <> 1;

      

       A2: p > 1 by INT_2:def 4;

      defpred P[ Nat] means ((i |^ ( Euler (p |^ ($1 -' 1)))) mod (p |^ $1)) <> 1;

      

       A3: P[2]

      proof

        (2 -' 1) = (2 - 1) by XREAL_1: 233

        .= 1;

        then

         A4: ((i |^ ( Euler (p |^ (2 -' 1)))) mod (p |^ 2)) = ((i |^ ( Euler p)) mod (p |^ 2));

        ( Euler p) = (p - 1) by EULER_1: 20

        .= (p -' 1) by A2, XREAL_1: 233;

        hence thesis by A1, A4, NEWTON: 81;

      end;

      

       A5: for k be Nat st k >= 2 & P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A6: k >= 2 & P[k];

        

         A7: i <> 0 by A1, A2, Th5;

        

         A8: (i,(p |^ (k -' 1))) are_coprime by A1, WSIERP_1: 10;

        

         A9: k > 1 & k > 0 by A6, XXREAL_0: 2;

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

        then

         A10: (k -' 1) > 0 by A6, XXREAL_0: 2, XREAL_1: 233;

        then

         A11: (p |^ (k -' 1)) > 1 by A2, PEPIN: 25;

        ((i |^ ( Euler (p |^ (k -' 1)))) mod (p |^ (k -' 1))) = 1 by A7, A8, A10, A2, PEPIN: 25, EULER_2: 18;

        then ((i |^ ( Euler (p |^ (k -' 1)))),1) are_congruent_mod (p |^ (k -' 1)) by A11, PEPIN: 39;

        then (p |^ (k -' 1)) divides ((i |^ ( Euler (p |^ (k -' 1)))) - 1) by INT_2: 15;

        then

        consider s be Integer such that

         A12: ((i |^ ( Euler (p |^ (k -' 1)))) - 1) = ((p |^ (k -' 1)) * s) by INT_1:def 3;

        

         A13: (p |^ k) > 1 by A2, A6, PEPIN: 25;

        

         A14: ((p |^ (k -' 1)) * s) >= 0 by A12, XREAL_1: 48, NAT_1: 14, A7;

        s >= 0 by A14;

        then

        reconsider s as Element of NAT by INT_1: 3;

        reconsider M = (s ^3 ) as Element of NAT by ORDINAL1:def 12;

        

         A15: (p |^ (k -' 1)) is Element of NAT & p is Element of NAT by ORDINAL1:def 12;

         A16:

        now

          assume p divides s;

          then ((p |^ (k -' 1)) * p) divides ((p |^ (k -' 1)) * s) by A15, PYTHTRIP: 7;

          then

           A17: (p |^ ((k -' 1) + 1)) divides ((p |^ (k -' 1)) * s) by NEWTON: 6;

          (p |^ ((k -' 1) + 1)) = (p |^ ((k + 1) -' 1)) by A9, NAT_D: 38

          .= (p |^ k) by NAT_D: 34;

          then ((i |^ ( Euler (p |^ (k -' 1)))),1) are_congruent_mod (p |^ k) by INT_2: 15, A17, A12;

          hence contradiction by A6, A13, PEPIN: 39;

        end;

        

         A18: (k -' 1) >= 1 by A10, NAT_1: 14;

        

         A19: ( Euler (p |^ k)) = ((p |^ k) - (p |^ (k -' 1))) by A6, XXREAL_0: 2, Th8

        .= ((p |^ ((k + 1) -' 1)) - (p |^ (k -' 1))) by NAT_D: 34

        .= ((p |^ ((k -' 1) + 1)) - (p |^ (k -' 1))) by A6, XXREAL_0: 2, NAT_D: 38

        .= (((p |^ (k -' 1)) * p) - (p |^ (k -' 1))) by NEWTON: 6

        .= (((p |^ (k -' 1)) * p) - (p |^ (((k -' 1) + 1) -' 1))) by NAT_D: 34

        .= (((p |^ (k -' 1)) * p) - (p |^ (((k -' 1) -' 1) + 1))) by NAT_D: 38, A10, NAT_1: 14

        .= (((p |^ (k -' 1)) * p) - ((p |^ ((k -' 1) -' 1)) * p)) by NEWTON: 6

        .= (((p |^ (k -' 1)) - (p |^ ((k -' 1) -' 1))) * p)

        .= (( Euler (p |^ (k -' 1))) * p) by A10, NAT_1: 14, Th8;

        consider t be Nat such that

         A20: ((1 + ((p |^ (k -' 1)) * s)) |^ p) = (((1 + (p * ((p |^ (k -' 1)) * s))) + ((p choose 2) * (((p |^ (k -' 1)) * s) ^2 ))) + (t * (((p |^ (k -' 1)) * s) ^3 ))) by Th4;

        

         A21: p is odd by A1, PEPIN: 17;

        

         A22: (p -' 1) = (p - 1) by A2, XREAL_1: 233;

        then 2 divides (p -' 1) by A21, PEPIN: 22;

        then ((p -' 1) mod 2) = 0 by PEPIN: 6;

        then

         A23: ((p -' 1) div 2) = ((p - 1) / 2) by A22, PEPIN: 63;

        

         A24: ((1 + ((p |^ (k -' 1)) * s)) |^ p) = (((1 + ((p * (p |^ (k -' 1))) * s)) + ((p choose 2) * (((p |^ (k -' 1)) * s) ^2 ))) + (t * (((p |^ (k -' 1)) * s) ^3 ))) by A20

        .= (((1 + ((p |^ ((k -' 1) + 1)) * s)) + ((p choose 2) * (((p |^ (k -' 1)) * s) ^2 ))) + (t * (((p |^ (k -' 1)) * s) ^3 ))) by NEWTON: 6

        .= (((1 + ((p |^ ((k + 1) -' 1)) * s)) + ((p choose 2) * (((p |^ (k -' 1)) * s) ^2 ))) + (t * (((p |^ (k -' 1)) * s) ^3 ))) by A9, NAT_D: 38

        .= (((1 + ((p |^ k) * s)) + ((p choose 2) * (((p |^ (k -' 1)) * s) ^2 ))) + (t * (((p |^ (k -' 1)) * s) ^3 ))) by NAT_D: 34

        .= (((1 + ((p |^ k) * s)) + (((p * (p - 1)) / 2) * (((p |^ (k -' 1)) * s) ^2 ))) + (t * (((p |^ (k -' 1)) * s) ^3 ))) by STIRL2_1: 51

        .= (((1 + ((p |^ k) * s)) + (((((p -' 1) div 2) * ((p |^ (k -' 1)) * p)) * (p |^ (k -' 1))) * (s ^2 ))) + (t * (((p |^ (k -' 1)) * s) ^3 ))) by A23

        .= (((1 + ((p |^ k) * s)) + (((((p -' 1) div 2) * (p |^ ((k -' 1) + 1))) * (p |^ (k -' 1))) * (s ^2 ))) + (t * (((p |^ (k -' 1)) * s) ^3 ))) by NEWTON: 6

        .= (((1 + ((p |^ k) * s)) + (((((p -' 1) div 2) * (p |^ ((k + 1) -' 1))) * (p |^ (k -' 1))) * (s ^2 ))) + (t * (((p |^ (k -' 1)) * s) ^3 ))) by NAT_D: 38, A9

        .= (((1 + ((p |^ k) * s)) + (((((p -' 1) div 2) * (p |^ k)) * (p |^ (k -' 1))) * (s ^2 ))) + (t * (((p |^ (k -' 1)) * s) ^3 ))) by NAT_D: 34

        .= (((1 + ((p |^ k) * s)) + ((((p -' 1) div 2) * ((p |^ (k -' 1)) * (p |^ k))) * (s ^2 ))) + (t * (((p |^ (k -' 1)) * s) ^3 )))

        .= (((1 + ((p |^ k) * s)) + ((((p -' 1) div 2) * (p |^ ((k -' 1) + k))) * (s ^2 ))) + (t * (((p |^ (k -' 1)) * s) ^3 ))) by NEWTON: 8

        .= (((1 + ((p |^ k) * s)) + ((((p -' 1) div 2) * (p |^ ((k + k) -' 1))) * (s ^2 ))) + (t * (((p |^ (k -' 1)) * s) ^3 ))) by A9, NAT_D: 38

        .= (((1 + ((p |^ k) * s)) + ((((p -' 1) div 2) * (p |^ ((2 * k) -' 1))) * (s ^2 ))) + (((t * ((p |^ (k -' 1)) * (p |^ (k -' 1)))) * (p |^ (k -' 1))) * (s ^3 )))

        .= (((1 + ((p |^ k) * s)) + ((((p -' 1) div 2) * (p |^ ((2 * k) -' 1))) * (s ^2 ))) + (((t * (p |^ ((k -' 1) + (k -' 1)))) * (p |^ (k -' 1))) * M)) by NEWTON: 8

        .= (((1 + ((p |^ k) * s)) + ((((p -' 1) div 2) * (p |^ ((2 * k) -' 1))) * (s ^2 ))) + ((t * ((p |^ ((k -' 1) + (k -' 1))) * (p |^ (k -' 1)))) * M))

        .= (((1 + ((p |^ k) * s)) + ((((p -' 1) div 2) * (p |^ ((2 * k) -' 1))) * (s ^2 ))) + ((t * (p |^ (((k -' 1) + (k -' 1)) + (k -' 1)))) * M)) by NEWTON: 8

        .= (((1 + ((p |^ k) * s)) + ((((p -' 1) div 2) * (p |^ ((2 * k) -' 1))) * (s ^2 ))) + ((t * M) * (p |^ (3 * (k -' 1)))));

        ((k -' 1) + k) >= (1 + k) by A18, XREAL_1: 6;

        then

         A25: ((k + k) -' 1) >= (k + 1) by A6, XXREAL_0: 2, NAT_D: 38;

        then

         A26: (p |^ (k + 1)) divides ((((p -' 1) div 2) * (s ^2 )) * (p |^ ((2 * k) -' 1))) by Lm2, NAT_D: 9;

        (k + (2 * k)) >= (2 + (2 * k)) by A6, XREAL_1: 6;

        then

         A27: ((3 * k) - 3) >= (((2 * k) + 2) - 3) by XREAL_1: 9;

        (2 * k) > (2 * 1) by A9, XREAL_1: 68;

        then ((2 * k) -' 1) = ((2 * k) - 1) by XXREAL_0: 2, XREAL_1: 233;

        then (3 * (k - 1)) >= (k + 1) by A25, A27, XXREAL_0: 2;

        then (3 * (k -' 1)) >= (k + 1) by A6, XXREAL_0: 2, XREAL_1: 233;

        then (p |^ (k + 1)) divides ((t * M) * (p |^ (3 * (k -' 1)))) by Lm2, NAT_D: 9;

        then

         A28: (p |^ (k + 1)) divides (((((p -' 1) div 2) * (p |^ ((2 * k) -' 1))) * (s ^2 )) + ((t * M) * (p |^ (3 * (k -' 1))))) by A26, NAT_D: 8;

        (i |^ ( Euler (p |^ k))) = ((1 + ((p |^ (k -' 1)) * s)) |^ p) by A12, A19, NEWTON: 9;

        then

         A29: (p |^ (k + 1)) divides (((i |^ ( Euler (p |^ k))) - 1) - ((p |^ k) * s)) by A24, A28;

        now

          assume

           A30: ((i |^ ( Euler (p |^ ((k + 1) -' 1)))) mod (p |^ (k + 1))) = 1;

          (p |^ (k + 1)) > 1 by A2, PEPIN: 25;

          then ((i |^ ( Euler (p |^ ((k + 1) -' 1)))),1) are_congruent_mod (p |^ (k + 1)) by A30, PEPIN: 39;

          then (p |^ (k + 1)) divides ((i |^ ( Euler (p |^ ((k + 1) -' 1)))) - 1) by INT_2: 15;

          then (p |^ (k + 1)) divides ((i |^ ( Euler (p |^ k))) - 1) by NAT_D: 34;

          then (p |^ (k + 1)) divides ((p |^ k) * s) by A29, INT_5: 2;

          then

           A31: ((p |^ k) * p) divides ((p |^ k) * s) by NEWTON: 6;

          (p |^ k) is Element of NAT by ORDINAL1:def 12;

          hence contradiction by A16, A15, A31, PYTHTRIP: 7;

        end;

        hence thesis;

      end;

      for k be Nat st k >= 2 holds P[k] from NAT_1:sch 8( A3, A5);

      hence thesis by A1;

    end;

    theorem :: INT_8:32

    n > 1 & ( len fp) >= 2 & (for d st d in ( dom fp) holds ((fp . d),n) are_coprime ) implies for fr st ( len fr) = ( len fp) & (for d st d in ( dom fr) holds (fr . d) = ( order ((fp . d),n))) & (for d, e st d in ( dom fr) & e in ( dom fr) & d <> e holds ((fr . d),(fr . e)) are_coprime ) holds ( order (( Product fp),n)) = ( Product fr)

    proof

      defpred RP[ FinSequence of NAT ] means for d st d in ( dom $1) holds (($1 . d),n) are_coprime ;

      defpred CC[ FinSequence of NAT ] means for fr st ( len fr) = ( len $1) & (for d st d in ( dom fr) holds (fr . d) = ( order (($1 . d),n))) & (for d, e st d in ( dom fr) & e in ( dom fr) & d <> e holds ((fr . d),(fr . e)) are_coprime ) holds ( order (( Product $1),n)) = ( Product fr);

      defpred TH[ FinSequence of NAT ] means (n > 1 & ( len $1) >= 2 & RP[$1]) implies CC[$1];

      

       A1: TH[( <*> NAT ) qua FinSequence of NAT ];

      

       A2: for fp, c st TH[fp] holds TH[(fp ^ <*c*>)]

      proof

        let fp, c;

        assume

         A3: TH[fp];

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

         TH[fp1]

        proof

          assume

           A4: n > 1 & ( len fp1) >= 2 & RP[fp1];

          

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

          per cases by A4, XXREAL_0: 1;

            suppose

             A6: ( len fp1) = 2;

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

            then

             A7: ( Product fp1) = ((fp1 . 1) * (fp1 . 2)) by RVSUM_1: 99;

            ( dom fp1) = ( Seg 2) by A6, FINSEQ_1:def 3;

            then

             A8: 1 in ( dom fp1) & 2 in ( dom fp1);

            then

             A9: ((fp1 . 1),n) are_coprime & ((fp1 . 2),n) are_coprime by A4;

             CC[fp1]

            proof

              let fr;

              assume

               A10: ( len fr) = ( len fp1) & (for d st d in ( dom fr) holds (fr . d) = ( order ((fp1 . d),n))) & (for d, e st d in ( dom fr) & e in ( dom fr) & d <> e holds ((fr . d),(fr . e)) are_coprime );

              then

               A11: 1 in ( dom fr) & 2 in ( dom fr) by A8, FINSEQ_3: 29;

              then ((fr . 1),(fr . 2)) are_coprime by A10;

              then (( order ((fp1 . 1),n)),(fr . 2)) are_coprime by A10, A11;

              then

               A12: (( order ((fp1 . 1),n)),( order ((fp1 . 2),n))) are_coprime by A10, A11;

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

              

              then ( Product fr) = ((fr . 1) * (fr . 2)) by RVSUM_1: 99

              .= (( order ((fp1 . 1),n)) * (fr . 2)) by A10, A11

              .= (( order ((fp1 . 1),n)) * ( order ((fp1 . 2),n))) by A10, A11;

              hence thesis by A12, A4, A7, A9, Th17;

            end;

            hence thesis;

          end;

            suppose ( len fp1) > 2;

            then (( len fp) + 1) > 2 by FINSEQ_2: 16;

            then

             A13: ((( len fp) + 1) - 1) >= 2 by INT_1: 52;

            

             A14: RP[fp]

            proof

              let d;

              assume

               A15: d in ( dom fp);

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

              hence thesis by A4, A15, FINSEQ_2: 15;

            end;

             CC[fp1]

            proof

              let fr;

              assume

               A16: ( len fr) = ( len fp1) & (for d st d in ( dom fr) holds (fr . d) = ( order ((fp1 . d),n))) & (for d, e st d in ( dom fr) & e in ( dom fr) & d <> e holds ((fr . d),(fr . e)) are_coprime );

              then

              consider f be FinSequence of NAT , l be Element of NAT such that

               A17: fr = (f ^ <*l*>) by FINSEQ_2: 19;

              

               A18: (( len f) + 1) = (( len fp) + 1) by A5, A16, A17, FINSEQ_2: 16;

              

               A19: for d st d in ( dom f) holds (f . d) = ( order ((fp . d),n))

              proof

                let d;

                assume

                 A20: d in ( dom f);

                then

                 A21: (f . d) = (fr . d) by A17, FINSEQ_1:def 7;

                

                 A22: d in ( dom fr) by A20, A17, FINSEQ_2: 15;

                ( dom f) = ( dom fp) by A18, FINSEQ_3: 29;

                then (fp . d) = (fp1 . d) by A20, FINSEQ_1:def 7;

                hence thesis by A22, A16, A21;

              end;

              for d, e st d in ( dom f) & e in ( dom f) & d <> e holds ((f . d),(f . e)) are_coprime

              proof

                let d, e;

                assume

                 A23: d in ( dom f) & e in ( dom f) & d <> e;

                then

                 A24: (f . d) = (fr . d) & (f . e) = (fr . e) by A17, FINSEQ_1:def 7;

                d in ( dom fr) & e in ( dom fr) by A23, A17, FINSEQ_2: 15;

                hence thesis by A23, A16, A24;

              end;

              then

               A25: ( order (( Product fp),n)) = ( Product f) by A18, A19, A14, A3, A4, A13;

              

               A26: for d be Nat st d in ( dom fp) holds ((fp . d) gcd n) = 1 by A14, INT_2:def 3;

              (( Product fp) gcd n) = 1 by A26, WSIERP_1: 36;

              then

               A27: (( Product fp),n) are_coprime by INT_2:def 3;

              reconsider z = 0 , j = 1 as Element of NAT ;

              (( len fp) + j) >= (z + j) by XREAL_1: 7;

              then (( len fp) + 1) in ( dom fp1) by A5, FINSEQ_3: 25;

              then ((fp1 . (( len fp) + 1)),n) are_coprime by A4;

              then

               A28: (c,n) are_coprime by FINSEQ_1: 42;

              (( len f) + j) >= (z + j) by XREAL_1: 7;

              then ( len fr) >= j by A17, FINSEQ_2: 16;

              then

               A29: ( len fr) in ( dom fr) by FINSEQ_3: 25;

              

              then (fr . ( len fr)) = ( order ((fp1 . ( len fr)),n)) by A16

              .= ( order ((fp1 . (( len fp) + 1)),n)) by A16, FINSEQ_2: 16

              .= ( order (c,n)) by FINSEQ_1: 42;

              then

               A30: (fr . (( len f) + 1)) = ( order (c,n)) by A17, FINSEQ_2: 16;

              

               A31: ( Product fp1) = (( Product fp) * c) & ( Product fr) = (( Product f) * l) by A17, RVSUM_1: 96;

              for d be Nat st d in ( dom f) holds ((f . d) gcd (fr . (( len f) + 1))) = 1

              proof

                let d be Nat;

                assume

                 A32: d in ( dom f);

                then

                 A33: d in ( dom fr) by A17, FINSEQ_2: 15;

                d <= ( len f) by A32, FINSEQ_3: 25;

                then

                 A34: d < (( len f) + 1) by XREAL_1: 145;

                (( len f) + 1) in ( dom fr) by A17, A29, FINSEQ_2: 16;

                then ((fr . d),(fr . (( len f) + 1))) are_coprime by A16, A33, A34;

                then ((f . d),(fr . (( len f) + 1))) are_coprime by A17, A32, FINSEQ_1:def 7;

                hence thesis by INT_2:def 3;

              end;

              then (( Product f) gcd (fr . (( len f) + 1))) = 1 by WSIERP_1: 36;

              then (( Product f),( order (c,n))) are_coprime by A30, INT_2:def 3;

              then ( order ((( Product fp) * c),n)) = (( order (( Product fp),n)) * ( order (c,n))) by A4, A28, A27, A25, Th17;

              hence ( order (( Product fp1),n)) = ( Product fr) by A31, A30, A17, A25, FINSEQ_1: 42;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      for fp be FinSequence of NAT holds TH[fp] from FINSEQ_2:sch 2( A1, A2);

      hence thesis;

    end;