euler_2.miz



    begin

    reserve a,b,m,x,n,l,xi,xj for Nat,

t,z for Integer,

f,F for FinSequence of NAT ;

    

     Lm1: t < 1 iff t <= 0

    proof

      t < 1 implies t <= 0

      proof

        assume

         A1: t < 1;

        assume

         A2: t > 0 ;

        then

        reconsider t as Element of NAT by INT_1: 3;

        t >= 1 by A2, NAT_1: 14;

        hence contradiction by A1;

      end;

      hence thesis;

    end;

    

     Lm2: a <> 0 implies (a - 1) >= 0

    proof

      assume a <> 0 ;

      then a >= 1 by NAT_1: 14;

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

      hence thesis;

    end;

    

     Lm3: (1 gcd z) = 1

    proof

      

      thus (1 gcd z) = ( |.1.| gcd |.z.|) by INT_2: 34

      .= (1 gcd |.z.|) by ABSVALUE:def 1

      .= 1 by NEWTON: 51;

    end;

    theorem :: EULER_2:1

    (a,b qua Integer) are_coprime iff (a,b) are_coprime ;

    theorem :: EULER_2:2

    

     Th2: (m * t) >= 1 implies t >= 1

    proof

      assume

       A1: (m * t) >= 1;

      assume t < 1;

      then t <= 0 by Lm1;

      hence contradiction by A1;

    end;

    

     Lm4: (1 - m) <= z & z <= (m - 1) & m divides z implies z = 0

    proof

      assume that

       A1: (1 - m) <= z and

       A2: z <= (m - 1) and

       A3: m divides z;

      consider t be Integer such that

       A4: z = (m * t) by A3, INT_1:def 3;

      assume

       A5: z <> 0 ;

      now

        per cases by A5, A4;

          suppose

           A6: t > 0 ;

          then

          reconsider t as Element of NAT by INT_1: 3;

          (m * t) >= m by A6, NAT_1: 14, NEWTON: 33;

          then ((m * t) + 1) > m by NAT_1: 13;

          hence contradiction by A2, A4, XREAL_1: 19;

        end;

          suppose

           A7: t < 0 ;

          reconsider r = (t + 1) as Integer;

          1 <= ((m * t) + (m * 1)) by A1, A4, XREAL_1: 20;

          then 1 <= (m * (t + 1));

          then r >= 1 by Th2;

          then (1 - 1) <= t by XREAL_1: 20;

          hence contradiction by A7;

        end;

      end;

      hence contradiction;

    end;

    theorem :: EULER_2:3

    

     Th3: a <> 0 & b <> 0 & m <> 0 & (a,m) are_coprime & (b,m) are_coprime implies (m,((a * b) mod m)) are_coprime

    proof

      assume that

       A1: a <> 0 and

       A2: b <> 0 and

       A3: m <> 0 and

       A4: (a,m) are_coprime & (b,m) are_coprime ;

      ((a * b),m) are_coprime by A1, A3, A4, EULER_1: 14;

      then

       A5: ((a * b) gcd m) = 1 by INT_2:def 3;

      consider t be Nat such that

       A6: (a * b) = ((m * t) + ((a * b) mod m)) and ((a * b) mod m) < m by A3, NAT_D:def 2;

      (a * b) <> (a * 0 ) by A1, A2, XCMPLX_1: 5;

      then (((a * b) + (( - t) * m)) gcd m) = ((a * b) gcd m) by EULER_1: 16;

      hence thesis by A6, A5, INT_2:def 3;

    end;

    theorem :: EULER_2:4

    

     Th4: m > 1 & (m,n) are_coprime & n = ((a * b) mod m) implies (m,b) are_coprime

    proof

      assume that

       A1: m > 1 and

       A2: (m,n) are_coprime and

       A3: n = ((a * b) mod m);

      set k = (m gcd b);

      k divides m by NAT_D:def 5;

      then

      consider km be Nat such that

       A4: m = (k * km) by NAT_D:def 3;

      

       A5: k <> 0 & km <> 0 by A1, A4;

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

      k divides b by NAT_D:def 5;

      then

      consider kb be Nat such that

       A6: b = (k * kb) by NAT_D:def 3;

      consider p be Nat such that

       A7: (a * (k * kb)) = (((k * km) * p) + ((a * (k * kb)) mod (k * km))) and ((a * (k * kb)) mod (k * km)) < (k * km) by A1, A4, NAT_D:def 2;

      set tm = ((a * kb) - (km * p));

      

       A8: ((a * (k * kb)) mod (k * km)) = (k * ((a * kb) - (km * p))) by A7;

      assume not (m,b) are_coprime ;

      then

       A9: (m gcd b) <> 1 by INT_2:def 3;

      

       A10: k <> ( - 1) by NAT_1: 2;

      

       A11: tm <> 0 implies (m gcd n) <> 1

      proof

        assume tm <> 0 ;

        (m gcd n) = (k * (km gcd tm)) by A3, A4, A5, A6, A8, EULER_1: 15;

        hence thesis by A9, A10, INT_1: 9;

      end;

      tm = 0 implies (m gcd n) <> 1 by A1, A3, A4, A6, A8, NEWTON: 52;

      hence contradiction by A2, A11, INT_2:def 3;

    end;

    theorem :: EULER_2:5

    

     Th5: ((m mod n) mod n) = (m mod n)

    proof

      per cases ;

        suppose n <> 0 ;

        then ex t be Nat st m = ((n * t) + (m mod n)) & (m mod n) < n by NAT_D:def 2;

        hence thesis by NAT_D: 24;

      end;

        suppose

         A1: n = 0 ;

        

        hence ((m mod n) mod n) = 0 by NAT_D:def 2

        .= (m mod n) by A1, NAT_D:def 2;

      end;

    end;

    theorem :: EULER_2:6

    ((l + m) mod n) = (((l mod n) + (m mod n)) mod n)

    proof

      

      thus ((l + m) mod n) = (((l mod n) + m) mod n) by NAT_D: 22

      .= (((l mod n) + (m mod n)) mod n) by NAT_D: 23;

    end;

    theorem :: EULER_2:7

    

     Th7: ((l * m) mod n) = ((l * (m mod n)) mod n)

    proof

      per cases ;

        suppose n <> 0 ;

        then

        consider t be Nat such that

         A1: m = ((n * t) + (m mod n)) and (m mod n) < n by NAT_D:def 2;

        ((l * m) mod n) = ((((l * t) * n) + (l * (m mod n))) mod n) by A1;

        hence thesis by NAT_D: 21;

      end;

        suppose

         A2: n = 0 ;

        

        hence ((l * m) mod n) = 0 by NAT_D:def 2

        .= ((l * (m mod n)) mod n) by A2, NAT_D:def 2;

      end;

    end;

    theorem :: EULER_2:8

    ((l * m) mod n) = (((l mod n) * m) mod n) by Th7;

    theorem :: EULER_2:9

    

     Th9: ((l * m) mod n) = (((l mod n) * (m mod n)) mod n)

    proof

      ((l * m) mod n) = ((l * (m mod n)) mod n) by Th7;

      hence thesis by Th7;

    end;

    begin

    definition

      let f, a;

      :: original: *

      redefine

      func a * f -> FinSequence of NAT ;

      coherence

      proof

        ( rng (a * f)) c= NAT

        proof

          let x be object;

          assume x in ( rng (a * f));

          then

          consider xx be object such that

           A1: xx in ( dom (a * f)) and

           A2: x = ((a * f) . xx) by FUNCT_1:def 3;

          reconsider xx as Element of NAT by A1;

          ((a * f) . xx) = (a * (f . xx)) by RVSUM_1: 44;

          hence thesis by A2, ORDINAL1:def 12;

        end;

        hence thesis by FINSEQ_1:def 4;

      end;

    end

    theorem :: EULER_2:10

    

     Th10: for R1,R2 be FinSequence of NAT st (R1,R2) are_fiberwise_equipotent holds ( Product R1) = ( Product R2)

    proof

      let R1,R2 be FinSequence of NAT ;

      defpred P[ Nat] means for f,g be FinSequence of NAT st (f,g) are_fiberwise_equipotent & ( len f) = $1 holds ( Product f) = ( Product g);

      

       A1: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A2: P[n];

        let f,g be FinSequence of NAT ;

        assume that

         A3: (f,g) are_fiberwise_equipotent and

         A4: ( len f) = (n + 1);

        reconsider a = (f . (n + 1)) as Element of NAT ;

        

         A5: ( rng f) = ( rng g) by A3, CLASSES1: 75;

        set fn = (f | n);

        

         A6: f = (fn ^ <*a*>) by A4, RFINSEQ: 7;

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

        then (n + 1) in ( dom f) by A4, FINSEQ_3: 25;

        then a in ( rng g) by A5, FUNCT_1:def 3;

        then

        consider m be Nat such that

         A7: m in ( dom g) and

         A8: (g . m) = a by FINSEQ_2: 10;

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

        set gg = (g /^ m), gm = (g | m);

        m <= ( len g) by A7, FINSEQ_3: 25;

        then

         A9: ( len gm) = m by FINSEQ_1: 59;

        

         A10: 1 <= m by A7, FINSEQ_3: 25;

        then ( max ( 0 ,(m - 1))) = (m - 1) by FINSEQ_2: 4;

        then

        reconsider m1 = (m - 1) as Element of NAT by FINSEQ_2: 5;

        

         A11: m = (m1 + 1);

        then m1 <= m by NAT_1: 11;

        then

         A12: ( Seg m1) c= ( Seg m) by FINSEQ_1: 5;

        m in ( Seg m) by A10, FINSEQ_1: 1;

        then (gm . m) = a by A7, A8, RFINSEQ: 6;

        then

         A13: gm = ((gm | m1) ^ <*a*>) by A9, A11, RFINSEQ: 7;

        

         A14: g = ((g | m) ^ (g /^ m)) by RFINSEQ: 8;

        

         A15: (gm | m1) = (gm | ( Seg m1)) by FINSEQ_1:def 15

        .= ((g | ( Seg m)) | ( Seg m1)) by FINSEQ_1:def 15

        .= (g | (( Seg m) /\ ( Seg m1))) by RELAT_1: 71

        .= (g | ( Seg m1)) by A12, XBOOLE_1: 28

        .= (g | m1) by FINSEQ_1:def 15;

        now

          let x be object;

          ( card ( Coim (f,x))) = ( card ( Coim (g,x))) by A3, CLASSES1:def 10;

          

          then (( card (fn " {x})) + ( card ( <*a*> " {x}))) = ( card ((((g | m1) ^ <*a*>) ^ (g /^ m)) " {x})) by A14, A13, A15, A6, FINSEQ_3: 57

          .= (( card (((g | m1) ^ <*a*>) " {x})) + ( card ((g /^ m) " {x}))) by FINSEQ_3: 57

          .= ((( card ((g | m1) " {x})) + ( card ( <*a*> " {x}))) + ( card ((g /^ m) " {x}))) by FINSEQ_3: 57

          .= ((( card ((g | m1) " {x})) + ( card ((g /^ m) " {x}))) + ( card ( <*a*> " {x})))

          .= (( card (((g | m1) ^ (g /^ m)) " {x})) + ( card ( <*a*> " {x}))) by FINSEQ_3: 57;

          hence ( card ( Coim (fn,x))) = ( card ( Coim (((g | m1) ^ (g /^ m)),x)));

        end;

        then

         A16: (fn,((g | m1) ^ (g /^ m))) are_fiberwise_equipotent by CLASSES1:def 10;

        ( len fn) = n by A4, FINSEQ_1: 59, NAT_1: 11;

        then ( Product fn) = ( Product ((g | m1) ^ gg)) by A2, A16;

        

        hence ( Product f) = (( Product ((g | m1) ^ gg)) * ( Product <*a*>)) by A6, RVSUM_1: 97

        .= ((( Product (g | m1)) * ( Product gg)) * ( Product <*a*>)) by RVSUM_1: 97

        .= ((( Product (g | m1)) * ( Product <*a*>)) * ( Product gg))

        .= (( Product gm) * ( Product gg)) by A13, A15, RVSUM_1: 97

        .= ( Product g) by A14, RVSUM_1: 97;

      end;

      assume

       A17: (R1,R2) are_fiberwise_equipotent ;

      

       A18: ( len R1) = ( len R1);

      

       A19: P[ 0 ]

      proof

        let f,g be FinSequence of NAT ;

        assume (f,g) are_fiberwise_equipotent & ( len f) = 0 ;

        then

         A20: ( len g) = 0 & f = ( <*> NAT ) by RFINSEQ: 3;

        then g = ( <*> NAT );

        hence thesis by A20;

      end;

      for n holds P[n] from NAT_1:sch 2( A19, A1);

      hence thesis by A17, A18;

    end;

    begin

    definition

      let f be FinSequence of NAT , m be Nat;

      :: EULER_2:def1

      func f mod m -> FinSequence of NAT means

      : Def1: ( len it ) = ( len f) & for i be Nat st i in ( dom f) holds (it . i) = ((f . i) mod m);

      existence

      proof

        deffunc F( Nat) = ((f . $1) mod m);

        consider g be FinSequence such that

         A1: ( len g) = ( len f) and

         A2: for k be Nat st k in ( dom g) holds (g . k) = F(k) from FINSEQ_1:sch 2;

        ( rng g) c= NAT

        proof

          let x be object;

          assume x in ( rng g);

          then

          consider y be object such that

           A3: y in ( dom g) and

           A4: x = (g . y) by FUNCT_1:def 3;

          reconsider y as Element of NAT by A3;

          (g . y) = ((f . y) mod m) by A2, A3;

          hence thesis by A4;

        end;

        then

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

        take g;

        thus ( len g) = ( len f) by A1;

        let k be Nat;

        assume k in ( dom f);

        then k in ( dom g) by A1, FINSEQ_3: 29;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let fa,fb be FinSequence of NAT such that

         A5: ( len f) = ( len fa) and

         A6: for i be Nat st i in ( dom f) holds (fa . i) = ((f . i) mod m) and

         A7: ( len f) = ( len fb) and

         A8: for i be Nat st i in ( dom f) holds (fb . i) = ((f . i) mod m);

        now

          let X be set such that

           A9: ( dom f) = X;

          

           A10: for i be Nat st i in X holds (fa . i) = (fb . i)

          proof

            given j be Nat such that

             A11: j in X and

             A12: (fa . j) <> (fb . j);

            (fa . j) <> ((f . j) mod m) by A8, A9, A11, A12;

            hence contradiction by A6, A9, A11;

          end;

          

           A13: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3

          .= ( dom fb) by A7, FINSEQ_1:def 3;

          ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3

          .= ( dom fa) by A5, FINSEQ_1:def 3;

          hence thesis by A9, A13, A10;

        end;

        hence thesis;

      end;

    end

    theorem :: EULER_2:11

    for f be FinSequence of NAT st m <> 0 holds (( Product (f mod m)) mod m) = (( Product f) mod m)

    proof

      defpred P[ Nat] means for f be FinSequence of NAT st m <> 0 & ( len f) = $1 holds (( Product (f mod m)) mod m) = (( Product f) mod m);

      let f be FinSequence of NAT ;

      assume

       A1: m <> 0 ;

      

       A2: ( len f) is Element of NAT ;

      

       A3: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A4: P[n];

        let f be FinSequence of NAT ;

        assume that

         A5: m <> 0 and

         A6: ( len f) = (n + 1);

        reconsider fn = (f | n) as FinSequence of NAT ;

        

         A7: ( len fn) = n by A6, FINSEQ_1: 59, NAT_1: 11;

        

         A8: ( len (f mod m)) = (n + 1) by A6, Def1;

        then

         A9: ( len ((f mod m) | n)) = n by FINSEQ_1: 59, NAT_1: 11;

        

         A10: n <= ( len f) by A6, NAT_1: 11;

        

         A11: for i be Nat st 1 <= i & i <= ( len ((f mod m) | n)) holds (((f mod m) | n) . i) = ((fn mod m) . i)

        proof

          let i be Nat;

          assume that

           A12: 1 <= i and

           A13: i <= ( len ((f mod m) | n));

          

           A14: ((f | n) . i) = ((f | ( Seg n)) . i) by FINSEQ_1:def 15;

          

           A15: i in ( Seg n) by A9, A12, A13, FINSEQ_1: 1;

          then

           A16: (((f mod m) | ( Seg n)) . i) = ((f mod m) . i) by FUNCT_1: 49;

          i <= ( len f) by A10, A9, A13, XXREAL_0: 2;

          then

           A17: i in ( dom f) by A12, FINSEQ_3: 25;

          i in ( dom fn) by A7, A9, A12, A13, FINSEQ_3: 25;

          

          then ((fn mod m) . i) = ((fn . i) mod m) by Def1

          .= ((f . i) mod m) by A15, A14, FUNCT_1: 49

          .= ((f mod m) . i) by A17, Def1;

          hence thesis by A16, FINSEQ_1:def 15;

        end;

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

        then (n + 1) in ( dom f) by A6, FINSEQ_3: 25;

        then

         A18: ((f mod m) . (n + 1)) = ((f . (n + 1)) mod m) by Def1;

        ( len ((f mod m) | n)) = ( len (fn mod m)) by A7, A9, Def1;

        then ((f mod m) | n) = (fn mod m) by A11, FINSEQ_1: 14;

        then (f mod m) = ((fn mod m) ^ <*((f . (n + 1)) mod m)*>) by A8, A18, RFINSEQ: 7;

        

        then

         A19: (( Product (f mod m)) mod m) = ((( Product (fn mod m)) * ((f . (n + 1)) mod m)) mod m) by RVSUM_1: 96

        .= (((( Product (fn mod m)) mod m) * (((f . (n + 1)) mod m) mod m)) mod m) by Th9

        .= (((( Product fn) mod m) * (((f . (n + 1)) mod m) mod m)) mod m) by A4, A5, A7

        .= (((( Product fn) mod m) * ((f . (n + 1)) mod m)) mod m) by Th5;

        (( Product f) mod m) = (( Product (fn ^ <*(f . (n + 1))*>)) mod m) by A6, RFINSEQ: 7

        .= ((( Product fn) * (f . (n + 1))) mod m) by RVSUM_1: 96;

        hence thesis by A19, Th9;

      end;

      

       A20: P[ 0 ]

      proof

        let f be FinSequence of NAT ;

        assume that m <> 0 and

         A21: ( len f) = 0 ;

        

         A22: f = ( <*> NAT ) & ( len (f mod m)) = 0 by A21, Def1;

        then (f mod m) = ( <*> NAT );

        hence thesis by A22;

      end;

      for n holds P[n] from NAT_1:sch 2( A20, A3);

      hence thesis by A1, A2;

    end;

    theorem :: EULER_2:12

    

     Th12: a <> 0 & m > 1 & ((a * n) mod m) = (n mod m) & (m,n) are_coprime implies (a mod m) = 1

    proof

      assume that

       A1: a <> 0 and

       A2: m > 1 and

       A3: ((a * n) mod m) = (n mod m) and

       A4: (m,n) are_coprime ;

      consider k2 be Nat such that

       A5: n = ((m * k2) + (n mod m)) and (n mod m) < m by A2, NAT_D:def 2;

      consider k1 be Nat such that

       A6: (a * n) = ((m * k1) + ((a * n) mod m)) and ((a * n) mod m) < m by A2, NAT_D:def 2;

      ((a - 1) * n) = (m * (k1 - k2)) by A3, A6, A5;

      then

       A7: m divides ((a - 1) * n) by INT_1:def 3;

      reconsider t = (a - 1), m as Integer;

      m divides t by A4, A7, INT_2: 25;

      then

      consider tt be Integer such that

       A8: (a - 1) = (m * tt) by INT_1:def 3;

      (a - 1) >= 0 by A1, Lm2;

      then

       A9: tt >= 0 by A2, A8, XREAL_1: 158;

      

       A10: a = ((m * tt) + 1) by A8;

      reconsider tt, m as Element of NAT by A9, INT_1: 3;

      (a mod m) = ((((m * tt) mod m) + 1) mod m) by A10, NAT_D: 22

      .= (( 0 + 1) mod m) by NAT_D: 13

      .= 1 by A2, NAT_D: 24;

      hence thesis;

    end;

    theorem :: EULER_2:13

    ((F mod m) mod m) = (F mod m)

    proof

      

       A1: ( dom (F mod m)) = ( Seg ( len (F mod m))) by FINSEQ_1:def 3

      .= ( Seg ( len F)) by Def1

      .= ( dom F) by FINSEQ_1:def 3;

      

       A2: for x be object st x in ( dom F) holds (((F mod m) mod m) . x) = ((F mod m) . x)

      proof

        let x be object;

        assume

         A3: x in ( dom F);

        then

        reconsider x as Element of NAT ;

        (((F mod m) mod m) . x) = (((F mod m) . x) mod m) by A1, A3, Def1

        .= (((F . x) mod m) mod m) by A3, Def1

        .= ((F . x) mod m) by Th5

        .= ((F mod m) . x) by A3, Def1;

        hence thesis;

      end;

      ( dom ((F mod m) mod m)) = ( Seg ( len ((F mod m) mod m))) by FINSEQ_1:def 3

      .= ( Seg ( len (F mod m))) by Def1

      .= ( Seg ( len F)) by Def1

      .= ( dom F) by FINSEQ_1:def 3;

      hence thesis by A1, A2;

    end;

    theorem :: EULER_2:14

    ((a * (F mod m)) mod m) = ((a * F) mod m)

    proof

      

       A1: F is FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

      

       A2: (F mod m) is FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

      

       A3: ( dom (a * F)) = ( Seg ( len (a * F))) by FINSEQ_1:def 3

      .= ( Seg ( len F)) by A1, NEWTON: 2

      .= ( dom F) by FINSEQ_1:def 3;

      

       A4: ( dom (a * (F mod m))) = ( Seg ( len (a * (F mod m)))) by FINSEQ_1:def 3

      .= ( Seg ( len (F mod m))) by A2, NEWTON: 2

      .= ( Seg ( len F)) by Def1

      .= ( dom F) by FINSEQ_1:def 3;

      

       A5: for x be object st x in ( dom F) holds (((a * (F mod m)) mod m) . x) = (((a * F) mod m) . x)

      proof

        let x be object;

        assume

         A6: x in ( dom F);

        then

        reconsider x as Element of NAT ;

        (((a * (F mod m)) mod m) . x) = (((a * (F mod m)) . x) mod m) by A4, A6, Def1

        .= ((a * ((F mod m) . x)) mod m) by RVSUM_1: 44

        .= ((a * ((F . x) mod m)) mod m) by A6, Def1

        .= ((a * (F . x)) mod m) by Th7

        .= (((a * F) . x) mod m) by RVSUM_1: 44

        .= (((a * F) mod m) . x) by A3, A6, Def1;

        hence thesis;

      end;

      

       A7: ( dom ((a * F) mod m)) = ( Seg ( len ((a * F) mod m))) by FINSEQ_1:def 3

      .= ( Seg ( len (a * F))) by Def1

      .= ( Seg ( len F)) by A1, NEWTON: 2

      .= ( dom F) by FINSEQ_1:def 3;

      ( dom ((a * (F mod m)) mod m)) = ( Seg ( len ((a * (F mod m)) mod m))) by FINSEQ_1:def 3

      .= ( Seg ( len (a * (F mod m)))) by Def1

      .= ( Seg ( len (F mod m))) by A2, NEWTON: 2

      .= ( Seg ( len F)) by Def1

      .= ( dom F) by FINSEQ_1:def 3;

      hence thesis by A7, A5;

    end;

    theorem :: EULER_2:15

    for F,G be FinSequence of NAT holds ((F ^ G) mod m) = ((F mod m) ^ (G mod m))

    proof

      let F,G be FinSequence of NAT ;

      

       A1: ( dom ((F ^ G) mod m)) = ( Seg ( len ((F ^ G) mod m))) by FINSEQ_1:def 3

      .= ( Seg ( len (F ^ G))) by Def1

      .= ( dom (F ^ G)) by FINSEQ_1:def 3;

      

       A2: ( dom (G mod m)) = ( Seg ( len (G mod m))) by FINSEQ_1:def 3

      .= ( Seg ( len G)) by Def1

      .= ( dom G) by FINSEQ_1:def 3;

      

       A3: ( dom (F mod m)) = ( Seg ( len (F mod m))) by FINSEQ_1:def 3

      .= ( Seg ( len F)) by Def1

      .= ( dom F) by FINSEQ_1:def 3;

      

       A4: for x be object st x in ( dom (F ^ G)) holds (((F ^ G) mod m) . x) = (((F mod m) ^ (G mod m)) . x)

      proof

        let x be object;

        assume

         A5: x in ( dom (F ^ G));

        then

        reconsider x as Element of NAT ;

        now

          per cases by A5, FINSEQ_1: 25;

            suppose

             A6: x in ( dom F);

            

             A7: (((F ^ G) mod m) . x) = (((F ^ G) . x) mod m) by A5, Def1

            .= ((F . x) mod m) by A6, FINSEQ_1:def 7;

            (((F mod m) ^ (G mod m)) . x) = ((F mod m) . x) by A3, A6, FINSEQ_1:def 7

            .= ((F . x) mod m) by A6, Def1;

            hence (((F ^ G) mod m) . x) = (((F mod m) ^ (G mod m)) . x) by A7;

          end;

            suppose ex n be Nat st n in ( dom G) & x = (( len F) + n);

            then

            consider n be Element of NAT such that

             A8: n in ( dom G) and

             A9: x = (( len F) + n);

            

             A10: (((F ^ G) mod m) . x) = (((F ^ G) . x) mod m) by A5, Def1

            .= ((G . n) mod m) by A8, A9, FINSEQ_1:def 7;

            ( len (F mod m)) = ( len F) by Def1;

            

            then (((F mod m) ^ (G mod m)) . x) = ((G mod m) . n) by A2, A8, A9, FINSEQ_1:def 7

            .= ((G . n) mod m) by A8, Def1;

            hence (((F ^ G) mod m) . x) = (((F mod m) ^ (G mod m)) . x) by A10;

          end;

        end;

        hence thesis;

      end;

      ( dom ((F mod m) ^ (G mod m))) = ( Seg ( len ((F mod m) ^ (G mod m)))) by FINSEQ_1:def 3

      .= ( Seg (( len (F mod m)) + ( len (G mod m)))) by FINSEQ_1: 22

      .= ( Seg (( len F) + ( len (G mod m)))) by Def1

      .= ( Seg (( len F) + ( len G))) by Def1

      .= ( Seg ( len (F ^ G))) by FINSEQ_1: 22

      .= ( dom (F ^ G)) by FINSEQ_1:def 3;

      hence thesis by A1, A4;

    end;

    theorem :: EULER_2:16

    for F,G be FinSequence of NAT holds ((a * (F ^ G)) mod m) = (((a * F) mod m) ^ ((a * G) mod m))

    proof

      let F,G be FinSequence of NAT ;

      

       A1: F is FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

      

       A2: G is FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

      reconsider FG = (F ^ G) as FinSequence of NAT ;

      

       A3: FG is FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

      

       A4: ( dom (a * (F ^ G))) = ( Seg ( len (a * FG))) by FINSEQ_1:def 3

      .= ( Seg ( len FG)) by A3, NEWTON: 2

      .= ( dom (F ^ G)) by FINSEQ_1:def 3;

      

       A5: ( dom (a * G)) = ( Seg ( len (a * G))) by FINSEQ_1:def 3

      .= ( Seg ( len G)) by A2, NEWTON: 2

      .= ( dom G) by FINSEQ_1:def 3;

      

       A6: ( dom ((a * G) mod m)) = ( Seg ( len ((a * G) mod m))) by FINSEQ_1:def 3

      .= ( Seg ( len (a * G))) by Def1

      .= ( Seg ( len G)) by A2, NEWTON: 2

      .= ( dom G) by FINSEQ_1:def 3;

      

       A7: ( dom (a * F)) = ( Seg ( len (a * F))) by FINSEQ_1:def 3

      .= ( Seg ( len F)) by A1, NEWTON: 2

      .= ( dom F) by FINSEQ_1:def 3;

      

       A8: ( dom ((a * F) mod m)) = ( Seg ( len ((a * F) mod m))) by FINSEQ_1:def 3

      .= ( Seg ( len (a * F))) by Def1

      .= ( Seg ( len F)) by A1, NEWTON: 2

      .= ( dom F) by FINSEQ_1:def 3;

      

       A9: for x be object st x in ( dom (F ^ G)) holds (((a * (F ^ G)) mod m) . x) = ((((a * F) mod m) ^ ((a * G) mod m)) . x)

      proof

        reconsider H = (F ^ G) as FinSequence of NAT ;

        let x be object;

        assume

         A10: x in ( dom (F ^ G));

        then

        reconsider x as Element of NAT ;

        now

          per cases by A10, FINSEQ_1: 25;

            suppose

             A11: x in ( dom F);

            

             A12: (((a * (F ^ G)) mod m) . x) = (((a * (F ^ G)) . x) mod m) by A4, A10, Def1

            .= ((a * (H . x)) mod m) by RVSUM_1: 44

            .= ((a * (F . x)) mod m) by A11, FINSEQ_1:def 7;

            ((((a * F) mod m) ^ ((a * G) mod m)) . x) = (((a * F) mod m) . x) by A8, A11, FINSEQ_1:def 7

            .= (((a * F) . x) mod m) by A7, A11, Def1

            .= ((a * (F . x)) mod m) by RVSUM_1: 44;

            hence (((a * (F ^ G)) mod m) . x) = ((((a * F) mod m) ^ ((a * G) mod m)) . x) by A12;

          end;

            suppose ex n be Nat st n in ( dom G) & x = (( len F) + n);

            then

            consider n be Element of NAT such that

             A13: n in ( dom G) and

             A14: x = (( len F) + n);

            

             A15: (((a * (F ^ G)) mod m) . x) = (((a * (F ^ G)) . x) mod m) by A4, A10, Def1

            .= ((a * (H . x)) mod m) by RVSUM_1: 44

            .= ((a * (G . n)) mod m) by A13, A14, FINSEQ_1:def 7;

            ( len ((a * F) mod m)) = ( len (a * F)) by Def1

            .= ( len F) by A1, NEWTON: 2;

            

            then ((((a * F) mod m) ^ ((a * G) mod m)) . x) = (((a * G) mod m) . n) by A6, A13, A14, FINSEQ_1:def 7

            .= (((a * G) . n) mod m) by A5, A13, Def1

            .= ((a * (G . n)) mod m) by RVSUM_1: 44;

            hence (((a * (F ^ G)) mod m) . x) = ((((a * F) mod m) ^ ((a * G) mod m)) . x) by A15;

          end;

        end;

        hence thesis;

      end;

      

       A16: ( dom ((a * (F ^ G)) mod m)) = ( Seg ( len ((a * FG) mod m))) by FINSEQ_1:def 3

      .= ( Seg ( len (a * FG))) by Def1

      .= ( Seg ( len FG)) by A3, NEWTON: 2

      .= ( dom (F ^ G)) by FINSEQ_1:def 3;

      ( dom (((a * F) mod m) ^ ((a * G) mod m))) = ( Seg ( len (((a * F) mod m) ^ ((a * G) mod m)))) by FINSEQ_1:def 3

      .= ( Seg (( len ((a * F) mod m)) + ( len ((a * G) mod m)))) by FINSEQ_1: 22

      .= ( Seg (( len (a * F)) + ( len ((a * G) mod m)))) by Def1

      .= ( Seg (( len (a * F)) + ( len (a * G)))) by Def1

      .= ( Seg (( len F) + ( len (a * G)))) by A1, NEWTON: 2

      .= ( Seg (( len F) + ( len G))) by A2, NEWTON: 2

      .= ( Seg ( len (F ^ G))) by FINSEQ_1: 22

      .= ( dom (F ^ G)) by FINSEQ_1:def 3;

      hence thesis by A16, A9;

    end;

    theorem :: EULER_2:17

    a <> 0 & m <> 0 & (a,m) are_coprime implies for b holds ((a |^ b),m) are_coprime

    proof

      defpred P[ Nat] means ((a |^ $1),m) are_coprime ;

      assume

       A1: a <> 0 & m <> 0 & (a,m) are_coprime ;

      

       A2: for b holds P[b] implies P[(b + 1)]

      proof

        let b;

        

         A3: (a |^ (b + 1)) = ((a |^ b) * (a |^ 1)) by NEWTON: 8

        .= ((a |^ b) * a);

        assume ((a |^ b),m) are_coprime ;

        hence thesis by A1, A3, EULER_1: 14;

      end;

      ((a |^ 0 ) gcd m) = (1 gcd m) & (m gcd 1) = 1 by NEWTON: 4, NEWTON: 51;

      then

       A4: P[ 0 ] by INT_2:def 3;

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

      hence thesis;

    end;

    begin

    ::$Notion-Name

    theorem :: EULER_2:18

    

     Th18: a <> 0 & m > 1 & (a,m) are_coprime implies ((a |^ ( Euler m)) mod m) = 1

    proof

      assume that

       A1: a <> 0 and

       A2: m > 1 and

       A3: (a,m) are_coprime ;

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

      

       A4: (a |^ ( Euler m)) <> 0 by A1, PREPOWER: 5;

      set Y = { l where l be Element of NAT : ex u be Element of NAT st l = ((a * u) mod m) & u in X };

      

       A5: x in X implies ((a * x) mod m) in X

      proof

        assume x in X;

        then

        consider t be Element of NAT such that

         A6: t = x and

         A7: (m,t) are_coprime and

         A8: t >= 1 and t <= m;

        

         A9: ((a * t),m) are_coprime by A1, A2, A3, A7, EULER_1: 14;

        ((a * t) mod m) <> 0

        proof

          assume ((a * t) mod m) = 0 ;

          then

          consider s be Nat such that

           A10: (a * t) = ((m * s) + 0 ) and 0 < m by A2, NAT_D:def 2;

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

          then ((m * s) gcd (m * 1)) = m by EULER_1: 5;

          hence contradiction by A2, A9, A10, INT_2:def 3;

        end;

        then

         A11: ((a * t) mod m) >= 1 by NAT_1: 14;

        

         A12: ((a * t) mod m) <= m by A2, NAT_D: 1;

        (m,((a * t) mod m)) are_coprime by A1, A2, A3, A7, A8, Th3;

        hence thesis by A6, A11, A12;

      end;

      

       A13: X = Y

      proof

        thus X c= Y

        proof

          let x be object;

          assume x in X;

          then

          consider xx be Element of NAT such that

           A14: x = xx and

           A15: (m,xx) are_coprime and xx >= 1 and

           A16: xx <= m;

          consider i,j be Integer such that

           A17: ((i * a) + (j * m)) = xx by A3, EULER_1: 10;

          xx <> m by A2, A15, EULER_1: 1;

          then xx < m by A16, XXREAL_0: 1;

          then

           A18: (xx mod m) = xx by NAT_D: 24;

          reconsider im = (i mod m) as Element of NAT by INT_1: 3, NEWTON: 64;

          (i mod m) <> 0

          proof

            assume (i mod m) = 0 ;

            then 0 = (i - ((i div m) * m)) by A2, INT_1:def 10;

            

            then (m gcd xx) = ((m * 1) gcd (m * (((i div m) * a) + j))) by A17

            .= (m * (1 gcd (((i div m) * a) + j))) by EULER_1: 15

            .= (m * 1) by Lm3

            .= m;

            hence contradiction by A2, A15, INT_2:def 3;

          end;

          then

           A19: im >= 1 by NAT_1: 14;

          

           A20: i = (((i div m) * m) + (i mod m)) by A2, NEWTON: 66;

          then

          reconsider ij = (((i mod m) * a) + ((((i div m) * a) + j) * m)) as Element of NAT by A17;

          

           A21: im <= m by A2, NEWTON: 65;

          

           A22: (ij mod m) = ((im * a) mod m) by EULER_1: 12;

          then (m,im) are_coprime by A2, A15, A18, A17, A20, Th4;

          then im in X by A19, A21;

          hence thesis by A14, A18, A17, A20, A22;

        end;

        let y be object;

        assume y in Y;

        then ex yy be Element of NAT st y = yy & ex u be Element of NAT st yy = ((a * u) mod m) & u in X;

        hence thesis by A5;

      end;

      

       A23: xi in X & xj in X & xi <> xj implies ((a * xi) mod m) <> ((a * xj) mod m)

      proof

        assume that

         A24: xi in X and

         A25: xj in X and

         A26: xi <> xj;

        set tm = ((a * xi) mod m), sm = ((a * xj) mod m);

        assume

         A27: ((a * xi) mod m) = ((a * xj) mod m);

        consider s be Element of NAT such that

         A28: s = xj and (m,s) are_coprime and

         A29: s >= 1 & s <= m by A25;

        

         A30: sm = ((a * s) - (m * ((a * s) div m))) by A2, A28, NEWTON: 63;

        consider t be Element of NAT such that

         A31: t = xi and (m,t) are_coprime and

         A32: t >= 1 & t <= m by A24;

        tm = ((a * t) - (m * ((a * t) div m))) by A2, A31, NEWTON: 63;

        then 0 = ((a * (t - s)) - (m * (((a * t) div m) - ((a * s) div m)))) by A27, A30;

        then

         A33: m divides (a * (t - s)) by INT_1:def 3;

        reconsider m, c = (t - s) as Integer;

        (1 - m) <= c & c <= (m - 1) by A32, A29, XREAL_1: 13;

        then (t - s) = 0 by A3, A33, Lm4, INT_2: 25;

        hence contradiction by A26, A31, A28;

      end;

      reconsider FX = ( Sgm X) as FinSequence of NAT ;

      

       A34: FX is FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

      reconsider FYY = (a * FX) as FinSequence of NAT ;

      reconsider FY = (FYY mod m) as FinSequence of NAT ;

      

       A35: X c= ( Seg m)

      proof

        let x be object;

        assume x in X;

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

        hence thesis by FINSEQ_1: 1;

      end;

      then

      reconsider X as finite set;

      ( dom FYY) = ( Seg ( len FYY)) by FINSEQ_1:def 3

      .= ( Seg ( len FX)) by A34, NEWTON: 2;

      then

       A36: ( dom FX) = ( dom FYY) by FINSEQ_1:def 3;

      

       A37: ( dom FY) = ( Seg ( len FY)) by FINSEQ_1:def 3

      .= ( Seg ( len FYY)) by Def1

      .= ( Seg ( len FX)) by A34, NEWTON: 2;

      then

       A38: ( dom FX) = ( dom FY) by FINSEQ_1:def 3;

      

       A39: ( rng FY) = Y

      proof

        thus ( rng FY) c= Y

        proof

          let x be object;

          assume x in ( rng FY);

          then

          consider y be object such that

           A40: y in ( dom FY) and

           A41: x = (FY . y) by FUNCT_1:def 3;

          reconsider y as Element of NAT by A40;

          (FX . y) in ( rng FX) by A38, A40, FUNCT_1:def 3;

          then

           A42: (FX . y) in X by A35, FINSEQ_1:def 13;

          y in ( dom FX) by A37, A40, FINSEQ_1:def 3;

          

          then (FY . y) = ((FYY . y) mod m) by A36, Def1

          .= ((a * (FX . y)) mod m) by RVSUM_1: 44;

          hence thesis by A41, A42;

        end;

        let y be object;

        assume y in Y;

        then

        consider yy be Element of NAT such that

         A43: y = yy and

         A44: ex u be Element of NAT st yy = ((a * u) mod m) & u in X;

        consider uu be Element of NAT such that

         A45: yy = ((a * uu) mod m) and

         A46: uu in X by A44;

        uu in ( rng FX) by A35, A46, FINSEQ_1:def 13;

        then

        consider xx be object such that

         A47: xx in ( dom FX) and

         A48: uu = (FX . xx) by FUNCT_1:def 3;

        reconsider xx as Element of NAT by A47;

        (FY . xx) = ((FYY . xx) mod m) by A36, A47, Def1

        .= y by A43, A45, A48, RVSUM_1: 44;

        hence thesis by A38, A47, FUNCT_1:def 3;

      end;

      

       A49: FY is one-to-one

      proof

        

         A50: FX is one-to-one by A35, FINSEQ_3: 92;

        let x1,x2 be object;

        assume that

         A51: x1 in ( dom FY) and

         A52: x2 in ( dom FY) and

         A53: (FY . x1) = (FY . x2);

        

         A54: x2 in ( dom FX) by A37, A52, FINSEQ_1:def 3;

        reconsider x2 as Element of NAT by A52;

        

         A55: x1 in ( dom FX) by A37, A51, FINSEQ_1:def 3;

        reconsider x1 as Element of NAT by A51;

        

         A56: (FX . x1) in ( rng FX) & (FX . x2) in ( rng FX) by A38, A51, A52, FUNCT_1:def 3;

        

         A57: (FY . x2) = ((FYY . x2) mod m) by A36, A54, Def1

        .= ((a * (FX . x2)) mod m) by RVSUM_1: 44;

        (FY . x1) = ((FYY . x1) mod m) by A36, A55, Def1

        .= ((a * (FX . x1)) mod m) by RVSUM_1: 44;

        then not ((FX . x1) in X & (FX . x2) in X & (FX . x1) <> (FX . x2)) by A23, A53, A57;

        hence thesis by A35, A55, A54, A56, A50, FINSEQ_1:def 13;

      end;

      for x be object holds ( card ( Coim (FX,x))) = ( card ( Coim (FY,x)))

      proof

        let x be object;

        per cases ;

          suppose

           A58: x in X;

          

           A59: FX is one-to-one by A35, FINSEQ_3: 92;

          x in ( rng FX) by A35, A58, FINSEQ_1:def 13;

          then

           A60: ( len (FX - {x})) = (( len FX) - 1) by A59, FINSEQ_3: 90;

          

           A61: (( len (FX - {x})) - ( len (FX - {x}))) = ((( len FX) - ( card (FX " {x}))) - ( len (FX - {x}))) & ( len (FY - {x})) = (( len FY) - ( card (FY " {x}))) by FINSEQ_3: 59;

          ( len (FY - {x})) = (( len FY) - 1) by A13, A39, A49, A58, FINSEQ_3: 90;

          hence thesis by A60, A61;

        end;

          suppose not x in X;

          then ( not x in ( rng FX)) & (FY " {x}) = {} by A13, A35, A39, FINSEQ_1:def 13, FUNCT_1: 72;

          hence thesis by FUNCT_1: 72;

        end;

      end;

      then

       A62: (FX,FY) are_fiberwise_equipotent by CLASSES1:def 10;

      then

       A63: ( len FX) = ( len FY) by RFINSEQ: 3;

      

       A64: (( Product FY) mod m) = (((a |^ ( len FY)) * ( Product FX)) mod m)

      proof

        defpred P[ Nat] means $1 <= ( len FY) implies (( Product (FY | $1)) mod m) = (((a |^ ( len (FY | $1))) * ( Product (FX | $1))) mod m);

        (FY | ( len FY)) = (FY | ( Seg ( len FY))) by FINSEQ_1:def 15;

        then

         A65: FY = (FY | ( len FY)) by FINSEQ_2: 20;

        

         A66: for n st P[n] holds P[(n + 1)]

        proof

          let n;

          now

            per cases ;

              suppose

               A67: (n + 1) <= ( len FY);

              then ( len (FX | (n + 1))) = (n + 1) by A63, FINSEQ_1: 59;

              then

               A68: (FX | (n + 1)) = (((FX | (n + 1)) | n) ^ <*((FX | (n + 1)) . (n + 1))*>) by RFINSEQ: 7;

              assume

               A69: P[n];

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

              then

               A70: (n + 1) in ( dom FY) by A67, FINSEQ_3: 25;

              

               A71: ((FY | (n + 1)) . (n + 1)) = (FY . (n + 1)) by FINSEQ_3: 112;

              

               A72: ((FX | (n + 1)) . (n + 1)) = (FX . (n + 1)) by FINSEQ_3: 112;

              

               A73: n <= (n + 1) by NAT_1: 11;

              then

               A74: ( len (FY | n)) = n by A67, FINSEQ_1: 59, XXREAL_0: 2;

              

               A75: ((FX | (n + 1)) | n) = (FX | n) by A73, FINSEQ_5: 77;

              

               A76: ((FY | (n + 1)) | n) = (FY | n) by A73, FINSEQ_5: 77;

              

               A77: ( len (FY | (n + 1))) = (n + 1) by A67, FINSEQ_1: 59;

              then (FY | (n + 1)) = (((FY | (n + 1)) | n) ^ <*((FY | (n + 1)) . (n + 1))*>) by RFINSEQ: 7;

              

              then (( Product (FY | (n + 1))) mod m) = ((( Product (FY | n)) * (FY . (n + 1))) mod m) by A76, A71, RVSUM_1: 96

              .= (((((a |^ ( len (FY | n))) * ( Product (FX | n))) mod m) * ((FY . (n + 1)) mod m)) mod m) by A67, A69, A73, Th9, XXREAL_0: 2

              .= (((((a |^ ( len (FY | n))) * ( Product (FX | n))) mod m) * (((FYY . (n + 1)) mod m) mod m)) mod m) by A38, A36, A70, Def1

              .= (((((a |^ ( len (FY | n))) * ( Product (FX | n))) mod m) * (((a * FX) . (n + 1)) mod m)) mod m) by Th5

              .= ((((a |^ ( len (FY | n))) * ( Product (FX | n))) * ((a * FX) . (n + 1))) mod m) by Th9

              .= ((((a |^ n) * ( Product (FX | n))) * (a * (FX . (n + 1)))) mod m) by A74, RVSUM_1: 44

              .= ((((a |^ n) * a) * (( Product (FX | n)) * (FX . (n + 1)))) mod m)

              .= (((a |^ ( len (FY | (n + 1)))) * (( Product (FX | n)) * (FX . (n + 1)))) mod m) by A77, NEWTON: 6

              .= (((a |^ ( len (FY | (n + 1)))) * ( Product (FX | (n + 1)))) mod m) by A68, A75, A72, RVSUM_1: 96;

              hence P[(n + 1)];

            end;

              suppose (n + 1) > ( len FY);

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        (FX | ( len FX)) = (FX | ( Seg ( len FX))) by FINSEQ_1:def 15;

        then

         A78: FX = (FX | ( len FY)) by A63, FINSEQ_2: 20;

        

         A79: P[ 0 ] by NEWTON: 4, RVSUM_1: 94;

        for n holds P[n] from NAT_1:sch 2( A79, A66);

        hence thesis by A65, A78;

      end;

      

       A80: (( Product FX),m) are_coprime

      proof

        defpred P[ Nat] means $1 <= ( len FX) implies (( Product (FX | $1)),m) are_coprime ;

        

         A81: (FX | ( len FX)) = FX by FINSEQ_1: 58;

        

         A82: for n st P[n] holds P[(n + 1)]

        proof

          let n;

          now

            per cases ;

              suppose

               A83: ( len FX) >= (n + 1);

              reconsider FF = (FX | (n + 1)) as FinSequence of NAT ;

              reconsider ff = (FF . (n + 1)) as Element of NAT ;

              ( len FF) = (n + 1) by A83, FINSEQ_1: 59;

              then

               A84: FF = ((FF | n) ^ <*ff*>) by RFINSEQ: 7;

              reconsider a = ( Product (FF | n)), b = ff, m9 = m as Integer;

              

               A85: n <= (n + 1) by NAT_1: 11;

              ( 0 + 1) <= (n + 1) by XREAL_1: 6;

              then ((FX | (n + 1)) . (n + 1)) = (FX . (n + 1)) & (n + 1) in ( dom FX) by A83, FINSEQ_3: 25, FINSEQ_3: 112;

              then

               A86: ((FX | (n + 1)) . (n + 1)) in ( rng FX) by FUNCT_1:def 3;

              ( rng FX) = X by A35, FINSEQ_1:def 13;

              then

               A87: ex p be Element of NAT st ff = p & (m,p) are_coprime & p >= 1 & p <= m by A86;

              assume P[n];

              then (a,m9) are_coprime by A83, A85, FINSEQ_5: 77, XXREAL_0: 2;

              then ((a * b),m9) are_coprime by A87, INT_2: 26;

              hence P[(n + 1)] by A84, RVSUM_1: 96;

            end;

              suppose ( len FX) < (n + 1);

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        (( Product (FX | 0 )) gcd m) = 1 by NEWTON: 51, RVSUM_1: 94;

        then

         A88: P[ 0 ] by INT_2:def 3;

        for n holds P[n] from NAT_1:sch 2( A88, A82);

        hence thesis by A81;

      end;

      ( len FX) = ( card X) by A35, FINSEQ_3: 39

      .= ( Euler m) by EULER_1:def 1;

      then

       A89: ( len FY) = ( Euler m) by A62, RFINSEQ: 3;

      (( Product FX) mod m) = (( Product FY) mod m) by A62, Th10;

      hence thesis by A2, A64, A89, A4, A80, Th12;

    end;

    ::$Notion-Name

    theorem :: EULER_2:19

    a <> 0 & m is prime & (a,m) are_coprime implies ((a |^ m) mod m) = (a mod m)

    proof

      assume that

       A1: a <> 0 and

       A2: m is prime and

       A3: (a,m) are_coprime ;

      

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

      then (m - 1) > (1 - 1) by XREAL_1: 9;

      then

      reconsider mm = (m - 1) as Element of NAT by INT_1: 3;

      ( Euler m) = (m - 1) by A2, EULER_1: 20;

      then (((a |^ mm) mod m) * a) = (1 * a) by A1, A3, A4, Th18;

      then (mm + 1) = m & (((a |^ mm) * a) mod m) = (a mod m) by Th7;

      hence thesis by NEWTON: 6;

    end;