The Mizar article:

Euler's Theorem and Small Fermat's Theorem

by
Yoshinori Fujisawa,
Yasushi Fuwa, and
Hidetaka Shimizu

Received June 10, 1998

Copyright (c) 1998 Association of Mizar Users

MML identifier: EULER_2
[ MML identifier index ]


environ

 vocabulary INT_1, FINSEQ_1, INT_2, ARYTM_3, ABSVALUE, ARYTM_1, NAT_1, RELAT_1,
      FUNCT_1, RFINSEQ, SQUARE_1, BOOLE, CARD_1, EULER_1, FINSET_1, FILTER_0,
      CARD_3, GROUP_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, CARD_1,
      INT_1, INT_2, SQUARE_1, FINSET_1, NAT_1, FUNCT_1, NEWTON, EULER_1,
      RFINSEQ, RVSUM_1, RELAT_1, FINSEQ_1, FINSEQ_3, SETWOP_2, TOPREAL1,
      TREES_4, WSIERP_1, GROUP_1;
 constructors SQUARE_1, FINSEQ_3, REAL_1, EULER_1, RFINSEQ, MONOID_0, SETWOP_2,
      TOPREAL1, WSIERP_1, NAT_1, INT_2, SEQ_1, MEMBERED, CARD_4;
 clusters FINSET_1, INT_1, RELSET_1, FINSUB_1, FUNCT_1, FINSEQ_3, NAT_1,
      XREAL_0, MEMBERED, NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, FUNCT_1, XBOOLE_0;
 theorems INT_2, AXIOMS, FINSEQ_1, NAT_LAT, NAT_1, ABSVALUE, REAL_1, RLVECT_1,
      INT_1, GR_CY_2, FUNCT_1, REAL_2, EULER_1, PREPOWER, GR_CY_1, JORDAN4,
      RFINSEQ, FINSUB_1, FINSEQ_2, RVSUM_1, TOPREAL1, FINSEQ_3, FINSET_1,
      NEWTON, RELAT_1, JORDAN3, GROUP_4, SCMFSA9A, XBOOLE_1, XCMPLX_0,
      XCMPLX_1, URYSOHN1;
 schemes NAT_1, FINSEQ_1;

begin :: Preliminary

reserve a,b,m,x,n,k,l,xi,xj for Nat,
        t,z for Integer,
        f,F for FinSequence of NAT;

Lm1:0 <> a & 0 <> b implies a gcd b = a hcf b
proof
  assume 0 <> a & 0 <> b;
  then 0 < a & 0 < b by NAT_1:19;
  then abs(a) = a & abs(b) = b by ABSVALUE:def 1;
  hence thesis by INT_2:def 3;
end;

Lm2:t < 1 iff t <= 0
proof
   t < 1 implies t <= 0
  proof
    assume A1:t < 1;
    assume A2:t > 0;
    then reconsider t as Nat by INT_1:16;
      t >= 1 by A2,RLVECT_1:99;
    hence contradiction by A1;
  end;
  hence thesis by AXIOMS:22;
end;

Lm3:a <> 0 implies a-1 >= 0
proof
  assume a <> 0;
  then a >= 1 by RLVECT_1:99;
  then a-1 >= 1-1 by REAL_1:49;
  hence thesis;
end;

Lm4:1 gcd z = 1
proof
  thus 1 gcd z = abs(1 ) hcf abs(z) by INT_2:def 3
         .= 1 hcf abs(z) by ABSVALUE:def 1
         .= 1 by NAT_LAT:35;
end;

Lm5:a,b are_relative_prime implies b,a are_relative_prime
proof
  assume a,b are_relative_prime;
  then a hcf b = 1 by INT_2:def 6;
  hence thesis by INT_2:def 6;
end;

::::::::::::::::::::::::::::
::                        ::
::  Very useful theorem   ::
::                        ::
::::::::::::::::::::::::::::

theorem
  Th1:a,(b qua Integer) are_relative_prime iff a,b are_relative_prime
proof
  thus a,(b qua Integer) are_relative_prime implies
                                    a,b are_relative_prime
  proof
    assume a,(b qua Integer) are_relative_prime;
    then A1:a gcd b = 1 by INT_2:def 4;
      a >= 0 & b >= 0 by NAT_1:18;
    then abs(a) = a & abs(b) = b by ABSVALUE:def 1;
    then a hcf b = 1 by A1,INT_2:def 3;
    hence thesis by INT_2:def 6;
  end;
  assume a,b are_relative_prime;
  then A2:a hcf b = 1 by INT_2:def 6;
    a >= 0 & b >= 0 by NAT_1:18;
  then abs(a) = a & abs(b) = b by ABSVALUE:def 1;
  then a gcd b = 1 by A2,INT_2:def 3;
  hence thesis by INT_2:def 4;
end;

theorem
  Th2:m > 1 & m*t >= 1 implies t >= 1
proof
  assume A1:m > 1 & m*t >= 1;
  assume A2:t < 1;
  A3:m > 0 by A1,AXIOMS:22;
    t <= 0 by A2,Lm2;
  then m*t <= 0 by A3,REAL_2:123;
  hence contradiction by A1,Lm2;
end;

Lm6:m > 1 & 1-m <= z & z <= m-1 & m divides z implies z = 0
proof
  assume A1:m > 1 & 1-m <= z & z <= m-1 & m divides z;
  assume A2:z <> 0;
  consider t being Integer such that
    A3:z = m*t by A1,INT_1:def 9;
  A4:t <> 0 by A2,A3;
    now per cases by A4;
    suppose A5:t > 0;
      then reconsider t as Nat by INT_1:16;
        t >= 1 by A5,RLVECT_1:99;
      then m*t >= m by NAT_LAT:2;
      then m*t+1 > m by NAT_1:38;
    hence contradiction by A1,A3,REAL_1:84;
    suppose A6:t < 0;
        1 <= m*t+m*1 by A1,A3,REAL_1:86;
      then A7:1 <= m*(t+1) by XCMPLX_1:8;
      reconsider r = (t+1) as Integer;
        r >= 1 by A1,A7,Th2;
      then 1-1 <= t by REAL_1:86;
    hence contradiction by A6;
  end;
  hence contradiction;
end;

theorem
  Th3:m > 1 & m*t >= 0 implies t >= 0
proof
  assume A1:m > 1 & m*t >= 0;
  assume A2:t < 0;
  then t*m < t by A1,REAL_2:145;
  hence contradiction by A1,A2,AXIOMS:22;
end;

canceled;

theorem
  Th5:a <> 0 & b <> 0 & m <> 0 &
                     a,m are_relative_prime & b,m are_relative_prime
                                       implies m,a*b mod m are_relative_prime
proof
  assume A1:a <> 0 & b <> 0 & m <> 0 &
                     a,m are_relative_prime & b,m are_relative_prime;
  then a*b,m are_relative_prime by EULER_1:15;
  then A2:a*b hcf m = 1 by INT_2:def 6;
  consider t being Nat such that
    A3:a*b = m*t+(a*b mod m) and
      (a*b mod m) < m by A1,NAT_1:def 2;
  A4:a*b mod m = a*b-m*t by A3,XCMPLX_1:26
               .= a*b+(-m*t) by XCMPLX_0:def 8
               .= a*b+(-t)*m by XCMPLX_1:175;
  A5:a*b <> a*0 by A1,XCMPLX_1:5;
  then A6:a*b+(-t)*m gcd m = a*b gcd m by A1,EULER_1:17;
  A7: a*b gcd m = 1 by A1,A2,A5,Lm1;
    a*b mod m >= 0 & m >= 0 by NAT_1:18;
  then abs(a*b mod m) = a*b mod m & abs(m) = m by ABSVALUE:def 1;
  then (a*b mod m) hcf m = 1 by A4,A6,A7,INT_2:def 3;
  hence thesis by INT_2:def 6;
end;

theorem
  Th6:m > 1 & b <> 0 &
       m,n are_relative_prime & a,m are_relative_prime & n = a*b mod m
           implies m,b are_relative_prime
proof
  assume A1:m > 1 & b <> 0 & m,n are_relative_prime
         & a,m are_relative_prime & n = a*b mod m;
  assume not m,b are_relative_prime;
  then A2:m hcf b <> 1 by INT_2:def 6;
  set k = m hcf b;
  A3: m <> 0 by A1;
  then m > 0 & b > 0 by A1,NAT_1:19;
  then A4:k > 0 by NAT_LAT:43;
  A5:k divides m & k divides b by NAT_1:def 5;
  then consider km being Nat such that
    A6:m = k*km by NAT_1:def 3;
  A7:k <> 0 & km <> 0 by A1,A6;
  consider kb being Nat such that
    A8:b = k*kb by A5,NAT_1:def 3;
  consider p being Nat such that
    A9:a*(k*kb) = (k*km)*p+(a*(k*kb) mod (k*km)) &
          (a*(k*kb) mod (k*km)) < k*km by A3,A6,NAT_1:def 2;
  A10:(a*(k*kb) mod (k*km)) = a*(k*kb)-(k*km)*p by A9,XCMPLX_1:26
                          .= (a*k)*kb-(k*km)*p by XCMPLX_1:4
                          .= (k*a)*kb-k*(km*p) by XCMPLX_1:4
                          .= k*(a*kb)-k*(km*p) by XCMPLX_1:4
                          .= k*((a*kb)-(km*p)) by XCMPLX_1:40;
  set tm = (a*kb)-(km*p);
  A11:tm = 0 implies m gcd n <> 1
  proof
    assume A12: tm = 0;
    A13:0 = abs(0) by ABSVALUE:7;
      k*km >= 0 by NAT_1:18;
    then k*km = abs(k*km) by ABSVALUE:def 1;
    then k*km gcd 0 = k*km hcf 0 by A13,INT_2:def 3
              .= k*km by NAT_LAT:36;
    hence thesis by A1,A6,A8,A10,A12;
  end;
  A14:tm <> 0 implies m gcd n <> 1
  proof
    assume A15:tm <> 0;
    assume A16:m gcd n = 1;
    A17:k <> -1 by NAT_1:18;
      m gcd n = k*(km gcd tm) by A1,A4,A6,A7,A8,A10,A15,EULER_1:16;
    hence contradiction by A2,A16,A17,INT_1:22;
  end;
  A18:m gcd n = abs(m) hcf abs(n) by INT_2:def 3;
    m >= 0 & n >= 0 by NAT_1:18;
  then m = abs(m) & n = abs(n) by ABSVALUE:def 1;
  hence contradiction by A1,A11,A14,A18,INT_2:def 6;
end;

theorem
  Th7:for n holds (m mod n) mod n = m mod n
proof
   let n;
   per cases;
   suppose n <> 0;
   then ex t being Nat st m = n*t+(m mod n) & m mod n < n by NAT_1:def 2;
   hence thesis by GR_CY_1:4;
   suppose
A1:   n = 0;
   hence (m mod n) mod n = 0 by NAT_1:def 2
      .= m mod n by A1,NAT_1:def 2;
 end;

theorem
    for n holds (l+m) mod n = ((l mod n)+(m mod n)) mod n
proof
  let n;
  thus (l+m) mod n = ((l mod n)+m) mod n by GR_CY_1:2
               .= ((l mod n)+(m mod n)) mod n by GR_CY_1:3;
end;

theorem
  Th9:for n holds (l*m) mod n = (l*(m mod n)) mod n
proof
  let n;
  per cases;
  suppose n <> 0;
    then consider t being Nat such that
      A1: m = n*t+(m mod n) & (m mod n)<n by NAT_1:def 2;
      (l*m) mod n =(l*(n*t)+l*(m mod n)) mod n by A1,XCMPLX_1:8
               .=((l*t)*n+l*(m mod n)) mod n by XCMPLX_1:4;
    hence (l*m) mod n = (l*(m mod n)) mod n by GR_CY_1:1;
   suppose
A2:   n = 0;
   hence (l*m) mod n = 0 by NAT_1:def 2
      .= (l*(m mod n)) mod n by A2,NAT_1:def 2;
end;

theorem
  Th10:for n holds (l*m) mod n = ((l mod n)*m) mod n
proof
  let n;
  per cases;
  suppose n <> 0;
    then consider t being Nat such that
      A1: l = n*t+(l mod n) & (l mod n)<n by NAT_1:def 2;
      (l*m) mod n = (m*(n*t)+m*(l mod n)) mod n by A1,XCMPLX_1:8
             .=((m*t)*n+m*(l mod n)) mod n by XCMPLX_1:4;
    hence (l*m) mod n = ((l mod n)*m) mod n by GR_CY_1:1;
   suppose
A2:   n = 0;
   hence (l*m) mod n = 0 by NAT_1:def 2
      .= ((l mod n)*m) mod n by A2,NAT_1:def 2;
end;

theorem
  Th11:for n holds (l*m) mod n = ((l mod n)*(m mod n)) mod n
proof
  let n;
    (l*m) mod n = (l*(m mod n)) mod n by Th9;
  hence thesis by Th10;
end;

begin

::::::::::::::::::::::::::::::::::::::::::::
::                                        ::
::  Function of Nat*(FinSequence of NAT)  ::
::                                        ::
::::::::::::::::::::::::::::::::::::::::::::

definition let a,f;
  redefine func a*f -> FinSequence of NAT;
coherence
  proof
      rng(a*f) c= NAT
    proof
      let x be set;
      assume x in rng (a*f);
      then consider xx being set such that
             A1:xx in dom (a*f) & x = (a*f).xx by FUNCT_1:def 5;
      A2:xx in Seg len (a*f) by A1,FINSEQ_1:def 3;
        Seg len (a*f) is Subset of NAT by FINSUB_1:def 5;
      then reconsider xx as Nat by A2;
        (a*f).xx = a*(f.xx) by RVSUM_1:66;
      hence thesis by A1;
    end;
    hence thesis by FINSEQ_1:def 4;
  end;
end;

:::::::::::::::::::::::::::::::::::::::::
::                                     ::
::  Function of Product(FinSequence of NAT) ::
::                                     ::
:::::::::::::::::::::::::::::::::::::::::

  Lm7:for f be FinSequence of NAT, r be Nat holds
  Product(f^<*r*>) = Product f*r
   by RVSUM_1:126;

  Lm8:for f1,f2 be FinSequence of NAT holds
  Product(f1^f2) = Product f1*Product f2
   by RVSUM_1:127;

canceled 13;

theorem
  Th25:for R1,R2 be FinSequence of NAT
         st R1,R2 are_fiberwise_equipotent holds Product R1 = Product R2
proof
  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:P[0]
  proof let f,g be FinSequence of NAT; assume
      f,g are_fiberwise_equipotent & len f = 0;
    then len g = 0 & f = <*>NAT by FINSEQ_1:32,RFINSEQ:16;
    hence thesis by FINSEQ_1:32;
  end;
  A2:for n st P[n] holds P[n+1]
  proof let n; assume
    A3:P[n];
    let f,g be FinSequence of NAT; assume
    A4:f,g are_fiberwise_equipotent & len f = n+1;
    then A5:rng f = rng g & len f = len g by RFINSEQ:1,16;
      0<n+1 by NAT_1:19;
    then 0+1<=n+1 by NAT_1:38;
    then A6:n+1 in dom f by A4,FINSEQ_3:27;
    reconsider a = f.(n+1) as Nat;
      a in rng g by A5,A6,FUNCT_1:def 5;
    then consider m such that
    A7:m in dom g & g.m = a by FINSEQ_2:11;
    A8:g = (g|m)^(g/^m) by RFINSEQ:21;
    A9:1<=m & m<=len g by A7,FINSEQ_3:27;
    then max(0,m-1) = m-1 by FINSEQ_2:4;
    then reconsider m1 = m-1 as Nat by FINSEQ_2:5;
    set gg = g/^m,
        gm = g|m;
    A10:len gm = m by A9,TOPREAL1:3;
    A11:m = m1+1 by XCMPLX_1:27;
      m in Seg m by A9,FINSEQ_1:3;
    then gm.m = a & m in dom g by A7,RFINSEQ:19;
    then A12:gm = (gm|m1)^<*a*> by A10,A11,RFINSEQ:20;
      m1<=m by A11,NAT_1:29;
    then A13:Seg m1 c= Seg m by FINSEQ_1:7;
    A14:gm|m1 = gm|(Seg m1) by TOPREAL1:def 1
             .= (g|(Seg m))|(Seg m1) by TOPREAL1:def 1
             .= g|((Seg m)/\(Seg m1)) by RELAT_1:100
             .= g|(Seg m1) by A13,XBOOLE_1:28
             .= g|m1 by TOPREAL1:def 1;
    set fn = f|n;
      n<=n+1 by NAT_1:29;
    then A15:len fn = n by A4,TOPREAL1:3;
    A16:f = fn ^ <*a*> by A4,RFINSEQ:20;
      now let x be set;
        card(f"{x}) = card(g"{x}) by A4,RFINSEQ:def 1;
      then card(fn"{x})+card(<*a*>"{x}) = card(((g|m1)^<*a*>^(g/^m))"{x})
                                           by A8,A12,A14,A16,FINSEQ_3:63
      .= card(((g|m1)^<*a*>)"{x})+card((g/^m)"{x}) by FINSEQ_3:63
      .= card((g|m1)"{x})+card(<*a*>"{x})+card((g/^m)"{x}) by FINSEQ_3:63
      .= card((g|m1)"{x})+card((g/^m)"{x})+card(<*a*>"{x}) by XCMPLX_1:1
      .= card(((g|m1)^(g/^m))"{x})+card(<*a*>"{x}) by FINSEQ_3:63;
      hence card(fn"{x}) = card(((g|m1)^(g/^m))"{x}) by XCMPLX_1:2;
    end;
    then fn, (g|m1)^(g/^m) are_fiberwise_equipotent by RFINSEQ:def 1;
    then Product fn = Product((g|m1)^gg) by A3,A15;
    hence Product f = Product((g|m1)^gg)*Product <*a*> by A16,Lm8
             .= Product(g|m1)*Product gg*Product <*a*> by Lm8
             .= Product(g|m1)*Product <*a*>*Product gg by XCMPLX_1:4
             .= Product gm*Product gg by A12,A14,Lm8
             .= Product g by A8,Lm8;
  end;
  A17:for n holds P[n] from Ind(A1,A2);
  let R1,R2 be FinSequence of NAT; assume
  A18:R1,R2 are_fiberwise_equipotent;
    len R1 = len R1;
  hence thesis by A17,A18;
end;

begin::Modulus for Finite Sequence of Natural

::::::::::::::::::::::::::::::::::::::::::::::::
::                                            ::
::  Function of (FinSequence of NAT) mod Nat  ::
::                                            ::
::::::::::::::::::::::::::::::::::::::::::::::::

definition let f be FinSequence of NAT,m be Nat;
  func f mod m -> FinSequence of NAT means
:Def1:
  len(it) = len(f) & for i being 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 being Nat st k in Seg len f holds g.k = F(k) from SeqLambda;
      rng g c= NAT
    proof
      let x be set;
      assume x in rng g;
      then consider y being set such that
        A3:y in dom g & x = g.y by FUNCT_1:def 5;
        A4:y in Seg len g by A3,FINSEQ_1:def 3;
        Seg len g is Subset of NAT by FINSUB_1:def 5;
      then reconsider y as Nat by A4;
        g.y = (f.y) mod m by A1,A2,A4;
      hence x in NAT by A3;
    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 Seg len f by FINSEQ_1:def 3;
    hence g.k = (f.k) mod m by A2;
  end;
uniqueness
  proof
    let fa,fb be FinSequence of NAT such that
    A5:len(f) = len(fa) &
          for i being Nat st i in dom f holds fa.i = (f.i) mod m and
    A6:len(f) = len(fb) &
          for i being Nat st i in dom f holds fb.i = (f.i) mod m;
      now let X be set such that
      A7:dom f = X;
      A8: dom f = Seg len f by FINSEQ_1:def 3
           .= dom fa by A5,FINSEQ_1:def 3;
      A9: dom f = Seg len f by FINSEQ_1:def 3
           .= dom fb by A6,FINSEQ_1:def 3;
        for i being Nat st i in X holds fa.i = fb.i
      proof
        given j being Nat such that A10: j in X & fa.j <> fb.j;
          j in X & fa.j <> (f.j) mod m by A6,A7,A10;
        hence contradiction by A5,A7;
      end;
      hence fa = fb by A7,A8,A9,FINSEQ_1:17;
    end;
    hence thesis;
  end;
end;

theorem
    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;
  A1:P[0]
  proof
    let f be FinSequence of NAT;
    assume A2:m <> 0 & len f=0;
    then A3:f = <*> NAT by FINSEQ_1:32;
      len (f mod m) = 0 by A2,Def1;
    hence thesis by A3,FINSEQ_1:32;
  end;
  A4:for n st P[n] holds P[n+1]
  proof
    let n;
    assume A5:P[n];
    let f be FinSequence of NAT;
    assume A6:m <> 0 & len f = n+1;
    reconsider fn = f|n as FinSequence of NAT;
    A7:n <= n+1 by NAT_1:29;
    A8:n <= len f by A6,NAT_1:29;
    A9:len fn = n by A6,A7,TOPREAL1:3;
    A10: (Product f) mod m = (Product (fn ^ <* f.(n+1) *>)) mod m by A6,RFINSEQ
:20
                    .= ((Product fn)*f.(n+1)) mod m by RVSUM_1:126;
    A11:len (f mod m) = n+1 by A6,Def1;
    A12:(f mod m)|n = fn mod m
    proof
      A13:len((f mod m)|n) = n by A7,A11,TOPREAL1:3;
      then A14:len((f mod m)|n) = len(fn mod m) by A9,Def1;
        for i being 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 A15:1 <= i & i <= len ((f mod m)|n);
        then A16:i in Seg n by A13,FINSEQ_1:3;
        then A17: ((f mod m)|Seg n).i = (f mod m).i by FUNCT_1:72;
          i <= len f by A8,A13,A15,AXIOMS:22;
        then A18:i in dom f by A15,FINSEQ_3:27;
        A19: (f|n).i = ((f|Seg n).i) by TOPREAL1:def 1;
          i in dom fn by A9,A13,A15,FINSEQ_3:27;
        then (fn mod m).i = fn.i mod m by Def1
                         .= f.i mod m by A16,A19,FUNCT_1:72
                         .= (f mod m).i by A18,Def1;
        hence thesis by A17,TOPREAL1:def 1;
      end;
      hence thesis by A14,FINSEQ_1:18;
    end;
      0<n+1 by NAT_1:19;
    then 0+1<=n+1 by NAT_1:38;
    then n+1 in dom f by A6,FINSEQ_3:27;
    then (f mod m).(n+1) = f.(n+1) mod m by Def1;
    then f mod m = (fn mod m) ^ <* f.(n+1) mod m *> by A11,A12,RFINSEQ:20;
    then Product (f mod m) mod m
         = ((Product (fn mod m))*(f.(n+1) mod m)) mod m by RVSUM_1:126
        .= (((Product (fn mod m)) mod m)*((f.(n+1) mod m) mod m)) mod m by Th11
        .= (((Product fn) mod m)*((f.(n+1) mod m) mod m)) mod m by A5,A6,A9
        .= (((Product fn) mod m)*(f.(n+1) mod m)) mod m by Th7;
    hence thesis by A10,Th11;
  end;
  A20:for n holds P[n] from Ind(A1,A4);
  let f be FinSequence of NAT;
  assume A21:m <> 0;
    len(f) is Nat;
  hence thesis by A20,A21;
end;

theorem
  Th27:a <> 0 & m > 1 & n <> 0 &
      a*n mod m = n mod m & m,n are_relative_prime implies a mod m = 1
proof
  assume A1:a <> 0 & m > 1 & n <> 0 &
               a*n mod m = n mod m & m,n are_relative_prime;
  then A2:m <> 0;
  then consider k1 be Nat such that
    A3:a*n = m*k1+(a*n mod m) and
      (a*n mod m) < m by NAT_1:def 2;
  A4:(a*n mod m) = a*n-m*k1 by A3,XCMPLX_1:26;
  consider k2 be Nat such that
    A5:n = m*k2+(n mod m) and
      (n mod m) < m by A2,NAT_1:def 2;
    (n mod m) = n-m*k2 by A5,XCMPLX_1:26;
  then a*n-1*n = m*k1-m*k2 by A1,A4,XCMPLX_1:24;
  then (a-1)*n = m*k1-m*k2 by XCMPLX_1:40;
  then (a-1)*n = m*(k1-k2) by XCMPLX_1:40;
  then A6:m divides (a-1)*n by INT_1:def 9;
  reconsider t = (a-1),m,n as Integer;
    m,n are_relative_prime by A1,Th1;
  then m divides t by A6,INT_2:40;
  then consider tt be Integer such that
    A7:(a-1) = m*tt by INT_1:def 9;
  A8:a = m*tt+1 by A7,XCMPLX_1:27;
    a-1 >= 0 by A1,Lm3;
  then tt >= 0 by A1,A7,Th3;
  then reconsider tt,m as Nat by INT_1:16;
    a mod m = (((m*tt) mod m)+1) mod m by A8,GR_CY_1:2
         .= (0+1) mod m by GROUP_4:101
         .= 1 by A1,GR_CY_1:4;
  hence thesis;
end;

theorem
    for F holds (F mod m) mod m = F mod m
proof
  let F;
  A1: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;
  A2: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;
    for x being set st x in dom F holds ((F mod m) mod m).x = (F mod m).x
  proof
    let x be set;
    assume A3:x in dom F;
    then A4:x in Seg len F by FINSEQ_1:def 3;
      Seg len F is Subset of NAT by FINSUB_1:def 5;
    then reconsider x as Nat by A4;
      ((F mod m) mod m).x = ((F mod m).x) mod m by A2,A3,Def1
                       .= (F.x mod m) mod m by A3,Def1
                       .= F.x mod m by Th7
                       .= (F mod m).x by A3,Def1;
    hence thesis;
  end;
  hence thesis by A1,A2,FUNCT_1:9;
end;

theorem
    for F holds (a*(F mod m)) mod m = (a*F) mod m
proof
  let F;
  A1: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 NEWTON:6
                      .= Seg(len F) by Def1
                      .= dom F by FINSEQ_1:def 3;
  A2:dom (a*(F mod m)) = Seg(len(a*(F mod m))) by FINSEQ_1:def 3
                        .= Seg(len(F mod m)) by NEWTON:6
                        .= Seg(len F) by Def1
                        .= dom F by FINSEQ_1:def 3;
  A3: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 NEWTON:6
                        .= dom F by FINSEQ_1:def 3;
  A4:dom (a*F) = Seg(len(a*F)) by FINSEQ_1:def 3
                .= Seg(len F) by NEWTON:6
                .= dom F by FINSEQ_1:def 3;
    for x being set st x in dom F holds
                     ((a*(F mod m)) mod m).x = ((a*F) mod m).x
  proof
    let x be set;
    assume A5:x in dom F;
    then A6:x in Seg len F by FINSEQ_1:def 3;
      Seg len F is Subset of NAT by FINSUB_1:def 5;
    then reconsider x as Nat by A6;
      ((a*(F mod m)) mod m).x = (a*(F mod m)).x mod m by A2,A5,Def1
                             .= (a*(F mod m).x ) mod m by RVSUM_1:66
                             .= (a*(F.x mod m)) mod m by A5,Def1
                             .= (a*F.x) mod m by Th9
                             .= (a*F).x mod m by RVSUM_1:66
                             .= ((a*F) mod m).x by A4,A5,Def1;
    hence thesis;
  end;
  hence thesis by A1,A3,FUNCT_1:9;
end;

theorem
    for F,G being 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 ((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:35
                 .= Seg(len(F)+len(G mod m)) by Def1
                 .= Seg(len(F)+len(G)) by Def1
                 .= Seg(len(F ^ G)) by FINSEQ_1:35
                 .= dom (F ^ 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: 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;
    for x being set st x in dom (F ^ G)
                holds ((F ^ G) mod m).x = ((F mod m) ^ (G mod m)).x
  proof
    let x be set;
    assume A5:x in dom (F ^ G);
    then A6: x in Seg len (F ^ G) by FINSEQ_1:def 3;
      Seg len (F ^ G) is Subset of NAT by FINSUB_1:def 5;
    then reconsider x as Nat by A6;
      now per cases by A5,FINSEQ_1:38;
      suppose A7: x in dom F;
        A8:((F ^ G) mod m).x = (F ^ G).x mod m by A5,Def1
                             .= F.x mod m by A7,FINSEQ_1:def 7;
          ((F mod m) ^ (G mod m)).x = (F mod m).x by A3,A7,FINSEQ_1:def 7
                                 .= F.x mod m by A7,Def1;
      hence ((F ^ G) mod m).x = ((F mod m) ^ (G mod m)).x by A8;
      suppose ex n being Nat st n in dom G & x=len F+n;
        then consider n being Nat such that
          A9:n in dom G & x=len F+n;
        A10: len (F mod m) = len F by Def1;
        A11:((F ^ G) mod m).x = (F ^ G).x mod m by A5,Def1
                             .= G.n mod m by A9,FINSEQ_1:def 7;
          ((F mod m) ^ (G mod m)).x = (G mod m).n by A4,A9,A10,FINSEQ_1:def 7
                                 .= G.n mod m by A9,Def1;
        hence ((F ^ G) mod m).x = ((F mod m) ^ (G mod m)).x by A11;
    end;
    hence thesis;
  end;
  hence thesis by A1,A2,FUNCT_1:9;
end;

theorem
    for F,G being 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;
  reconsider FG = F ^ G as FinSequence of NAT;
  A1: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 NEWTON:6
                            .= dom (F ^ G) by FINSEQ_1:def 3;
  A2: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:35
                 .= 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 NEWTON:6
                 .= Seg(len(F)+len(G)) by NEWTON:6
                 .= Seg(len(F ^ G)) by FINSEQ_1:35
                 .= dom(F ^ G) by FINSEQ_1:def 3;
  A3:dom (a*(F ^ G)) = Seg(len(a*FG)) by FINSEQ_1:def 3
                    .= Seg(len(FG)) by NEWTON:6
                    .= dom (F ^ G) by FINSEQ_1:def 3;
  A4:dom (a*F) = Seg(len(a*F)) by FINSEQ_1:def 3
              .= Seg(len F) by NEWTON:6
              .= dom F by FINSEQ_1:def 3;
  A5: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 NEWTON:6
                      .= dom F by FINSEQ_1:def 3;
  A6:dom (a*G) = Seg(len(a*G)) by FINSEQ_1:def 3
              .= Seg(len G) by NEWTON:6
              .= dom G by FINSEQ_1:def 3;
  A7: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 NEWTON:6
                      .= dom G by FINSEQ_1:def 3;
    for x being set st x in dom (F ^ G)
             holds ((a*(F ^ G)) mod m).x = (((a*F) mod m) ^ ((a*G) mod m)).x
  proof
    let x be set;
    assume A8:x in dom (F ^ G);
    reconsider H = F ^ G as FinSequence of NAT;
    A9: x in Seg len (F ^ G) by A8,FINSEQ_1:def 3;
      Seg len (F ^ G) is Subset of NAT by FINSUB_1:def 5;
    then reconsider x as Nat by A9;
      now per cases by A8,FINSEQ_1:38;
      suppose A10: x in dom F;
        A11:((a*(F ^ G)) mod m).x = ((a*(F ^ G)).x) mod m by A3,A8,Def1
                                 .= (a*H.x) mod m by RVSUM_1:66
                                 .= (a*(F.x)) mod m by A10,FINSEQ_1:def 7;
          (((a*F) mod m) ^ ((a*G) mod m)).x
                                  = ((a*F) mod m).x by A5,A10,FINSEQ_1:def 7
                                 .= ((a*F).x) mod m by A4,A10,Def1
                                 .= (a*(F.x)) mod m by RVSUM_1:66;
      hence ((a*(F ^ G)) mod m).x = (((a*F) mod m) ^ ((a*G) mod m)).x by A11;
      suppose ex n being Nat st n in dom G & x=len F+n;
        then consider n being Nat such that
          A12:n in dom G & x=len F+n;
        A13: len ((a*F) mod m) = len(a*F) by Def1
                         .= len F by NEWTON:6;
        A14:((a*(F ^ G)) mod m).x = ((a*(F ^ G)).x) mod m by A3,A8,Def1
                                 .= (a*H.x) mod m by RVSUM_1:66
                                 .= (a*G.n) mod m by A12,FINSEQ_1:def 7;
          (((a*F) mod m) ^ ((a*G) mod m)).x
                                  = ((a*G) mod m).n by A7,A12,A13,FINSEQ_1:def
7
                                 .= ((a*G).n) mod m by A6,A12,Def1
                                 .= (a*G.n) mod m by RVSUM_1:66;
      hence ((a*(F ^ G)) mod m).x = (((a*F) mod m) ^ ((a*G) mod m)).x by A14;
    end;
    hence thesis;
  end;
  hence thesis by A1,A2,FUNCT_1:9;
end;


:::::::::::::::::::::::::::::::::::
::                               ::
::  Function of (Nat) |^ (Nat)   ::
::                               ::
:::::::::::::::::::::::::::::::::::

definition let n,k;
  redefine func n |^ k -> Nat;
coherence by URYSOHN1:8;
end;

theorem
    a <> 0 & m <> 0 & a,m are_relative_prime
           implies for b holds (a |^ b),m are_relative_prime
proof
  assume A1:a <> 0 & m <> 0 & a,m are_relative_prime;
  A2:(a |^ 0) hcf m = 1 hcf m by NEWTON:9;
  defpred P[Nat] means (a |^ $1),m are_relative_prime;
  m hcf 1 = 1 by NAT_LAT:35;
  then A3:P[0] by A2,INT_2:def 6;
  A4:for b holds P[b] implies P[b+1]
  proof
    let b;
    assume A5:(a |^ b),m are_relative_prime;
    A6:(a |^ (b+1)) = (a |^ b)*(a |^ 1) by NEWTON:13
                    .= (a |^ b)*a by NEWTON:10;
      a |^ b <> 0 by A1,PREPOWER:12;
    hence thesis by A1,A5,A6,EULER_1:15;
  end;
  for b holds P[b] from Ind(A3,A4);
  hence thesis;
end;

begin:: Euler's Theorem and Small Fermat's Theorem
::::::::::::::::::::::::::::::::::::::::::::::::
::                                            ::
::  Euler's Theorem & Small Fermat's Theorem  ::
::                                            ::
::::::::::::::::::::::::::::::::::::::::::::::::

theorem ::Euler's theorem
  Th33:a <> 0 & m > 1 & a,m are_relative_prime
                  implies (a |^ Euler m) mod m = 1
proof
  assume A1:a <> 0 & m > 1 & a,m are_relative_prime;
  then A2:m <> 0;

  set X = {k where k is Nat : m,k are_relative_prime & k >= 1 & k <= m};
  set Y = {l where l is Nat : ex u being Nat st l = a*u mod m & u in X};

::Begin Euler's Lemma1
  A3:x in X implies a*x mod m in X
  proof
    assume x in X;
    then consider t being Nat such that
      A4:t = x and
      A5:m,t are_relative_prime and
      A6:t >= 1 & t <= m;
      m hcf t = 1 by A5,INT_2:def 6;
    then A7:t,m are_relative_prime by INT_2:def 6;
    A8:t <> 0 by A6;
    then A9:a*t,m are_relative_prime by A1,A2,A7,EULER_1:15;
      m hcf t = 1 by A5,INT_2:def 6;
    then t,m are_relative_prime by INT_2:def 6;
    then A10:m,a*t mod m are_relative_prime by A1,A2,A8,Th5;
      a*t mod m <> 0
    proof
      assume a*t mod m = 0;
      then consider s being Nat such that
        A11:a*t = m*s+0 and
            0 < m by A2,NAT_1:def 2;
        s hcf 1 = 1 by NAT_LAT:35;
      then m*s hcf m*1 = m by EULER_1:6;
      hence contradiction by A1,A9,A11,INT_2:def 6;
    end;
    then A12:a*t mod m >= 1 by RLVECT_1:99;
      m > 0 by A2,NAT_1:19;
    then a*t mod m <= m by NAT_1:46;
    hence thesis by A4,A10,A12;
  end;
::End of Euler's Lemma1

::Begin Euler's Lemma2
  A13:xi in X & xj in X & xi <> xj implies a*xi mod m <> a*xj mod m
  proof
    assume A14:xi in X & xj in X & xi <> xj;
    assume A15:a*xi mod m = a*xj mod m;
    set tm = a*xi mod m,sm = a*xj mod m;
    A16:m > 0 by A2,NAT_1:19;
    consider t being Nat such that
      A17:t = xi and
        m,t are_relative_prime and
      A18:t >= 1 & t <= m by A14;
    A19:tm = (a*t)-m*((a*t) div m) by A16,A17,GR_CY_2:1;
    consider s being Nat such that
      A20:s = xj and
        m,s are_relative_prime and
    A21:s >= 1 & s <= m by A14;
    A22:sm = (a*s)-m*((a*s) div m) by A16,A20,GR_CY_2:1;
      tm-sm = 0 by A15,XCMPLX_1:14;
    then 0 = ((a*t)-m*((a*t) div m))-(a*s)+m*((a*s) div m)
             by A19,A22,XCMPLX_1:37
          .= ((a*t)-(a*s)-m*((a*t) div m))+m*((a*s) div m) by XCMPLX_1:21
          .= a*(t-s)-m*((a*t) div m)+m*((a*s) div m) by XCMPLX_1:40
          .= a*(t-s)-(m*((a*t) div m)-m*((a*s) div m)) by XCMPLX_1:37
          .= a*(t-s)-m*(((a*t) div m)-((a*s) div m)) by XCMPLX_1:40;
    then a*(t-s) = m*(((a*t) div m)-((a*s) div m)) by XCMPLX_1:15;
    then A23:m divides a*(t-s) by INT_1:def 9;
    reconsider m,a,c = (t-s) as Integer;
      a,m are_relative_prime by A1,Th1;
    then A24:m divides c by A23,INT_2:40;
      1-m <= c & c <= m-1 by A18,A21,REAL_1:92;
    then t-s = 0 by A1,A24,Lm6;
    hence contradiction by A14,A17,A20,XCMPLX_1:15;
  end;
::End of Euler's Lemma2

::Begin Euler's Lemma3
  A25:X = Y
  proof
    thus X c= Y
    proof
      let x be set;
      assume x in X;
      then consider xx being Nat such that
        A26:x = xx and
        A27:m,xx are_relative_prime and
        A28:xx >= 1 & xx <= m;
        xx <> m by A1,A27,EULER_1:2;
      then xx < m by A28,AXIOMS:21;
      then A29:xx mod m = xx by GR_CY_1:4;
      A30:xx <> 0 by A28;
      consider i,j being Integer such that
        A31:i*a+j*m = xx by A1,EULER_1:11;
        i = (i div m)*m+(i mod m) by A2,GR_CY_2:4;
      then A32: xx = (i div m)*m*a+(i mod m)*a+j*m by A31,XCMPLX_1:8
                 .= (i mod m)*a+((i div m)*a)*m+j*m by XCMPLX_1:4
                 .= (i mod m)*a+(m*((i div m)*a)+m*j) by XCMPLX_1:1
                 .= (i mod m)*a+(((i div m)*a)+j)*m by XCMPLX_1:8;
      A33:m > 0 by A2,NAT_1:19;
      A34:i mod m <> 0
      proof
        assume i mod m = 0;
        then 0 = i-(i div m)*m by A2,INT_1:def 8;
        then i = (i div m)*m by XCMPLX_1:15;
        then A35:xx = ((i div m)*a)*m+j*m by A31,XCMPLX_1:4
                   .= m*((i div m)*a+j) by XCMPLX_1:8;
        then A36:((i div m)*a+j) <> 0 & 1 <> 0 by A28;
          m gcd xx = m*1 gcd m*((i div m)*a+j) by A35
                    .= m*(1 gcd ((i div m)*a+j)) by A33,A36,EULER_1:16
                    .= m*1 by Lm4
                    .= m;
        then m hcf xx = m by A2,A30,Lm1;
        hence contradiction by A1,A27,INT_2:def 6;
      end;
        i mod m >= 0 by A33,GR_CY_2:2;
      then reconsider im = i mod m as Nat by INT_1:16;
      A37:im >= 1 by A34,RLVECT_1:99;
      A38:im <= m by A33,GR_CY_2:3;
      reconsider ij = (i mod m)*a+(((i div m)*a)+j)*m as Nat by A32;
      A39: ij mod m = ((i mod m)*a+(((i div m)*a)+j)*m) mod m by SCMFSA9A:5
              .= (i mod m)*a mod m by EULER_1:13
              .= im*a mod m by SCMFSA9A:5;
      then m,im are_relative_prime by A1,A27,A29,A32,A34,Th6;
      then im in X by A37,A38;
      hence x in Y by A26,A29,A32,A39;
    end;
    let y be set;
    assume y in Y;
    then consider yy being Nat such that
      A40:y = yy and
      A41:ex u being Nat st yy = a*u mod m & u in X;
    consider uu being Nat such that
      A42:yy = a*uu mod m and
      A43:uu in X by A41;
    thus y in X by A3,A40,A42,A43;
  end;
::End of Euler'S Lemma3

  reconsider FX = Sgm X as FinSequence of NAT;
  reconsider FYY = (a*FX) as FinSequence of NAT;
  reconsider FY = FYY mod m as FinSequence of NAT;

::Begin Euler's Lemma4
  A44:X c= Seg m
  proof
    let x be set;
    assume x in X;
    then consider xx being Nat such that
      A45:x = xx and
        m,xx are_relative_prime and
      A46:xx >= 1 & xx <= m;
    thus thesis by A45,A46,FINSEQ_1:3;
  end;
::End of Euler's Lemma4

  then reconsider X as finite set by FINSET_1:13;
  A47:len(FX) = card X by A44,FINSEQ_3:44
        .= Euler m by EULER_1:def 1;

  A48: dom FY = Seg(len FY) by FINSEQ_1:def 3
        .= Seg(len FYY) by Def1
        .= Seg(len FX) by NEWTON:6;
  then A49:dom FX = dom FY by FINSEQ_1:def 3;
    dom FYY = Seg(len FYY) by FINSEQ_1:def 3
         .= Seg(len FX) by NEWTON:6;
  then A50:dom FX = dom FYY by FINSEQ_1:def 3;

::Begin Euler's Lemma5
  A51:rng FY = Y
  proof
    thus rng FY c= Y
    proof
      let x be set;
      assume x in rng FY;
      then consider y being set such that
        A52:y in dom FY & x = FY.y by FUNCT_1:def 5;
      A53:y in Seg len FY by A52,FINSEQ_1:def 3;
        Seg len FY is Subset of NAT by FINSUB_1:def 5;
      then reconsider y as Nat by A53;
        y in dom FX by A48,A52,FINSEQ_1:def 3;
      then A54: FY.y = (FYY.y) mod m by A50,Def1
               .= (a*FX.y) mod m by RVSUM_1:66;
        FX.y in rng FX by A49,A52,FUNCT_1:def 5;
      then FX.y in X by A44,FINSEQ_1:def 13;
      hence thesis by A52,A54;
    end;
    let y be set;
    assume y in Y;
    then consider yy being Nat such that
      A55:y = yy and
      A56:ex u being Nat st yy = a*u mod m & u in X;
    consider uu being Nat such that
      A57:yy = a*uu mod m and
      A58:uu in X by A56;
    A59: Seg len FX is Subset of NAT by FINSUB_1:def 5;
      uu in rng FX by A44,A58,FINSEQ_1:def 13;
    then consider xx being set such that
      A60:xx in dom FX & uu = FX.xx by FUNCT_1:def 5;
      xx in Seg len FX by A60,FINSEQ_1:def 3;
    then reconsider xx as Nat by A59;
      FY.xx = (FYY.xx) mod m by A50,A60,Def1
         .= y by A55,A57,A60,RVSUM_1:66;
    hence y in rng FY by A49,A60,FUNCT_1:def 5;
  end;
::End of Euler's Lemma5

::Begin Euler's Lemma6
  A61: FY is one-to-one
  proof
    let x1,x2 be set;
    assume A62: x1 in dom FY & x2 in dom FY & FY.x1 = FY.x2;
    then A63:x1 in dom FX & x2 in dom FX & FY.x1 = FY.x2 by A48,FINSEQ_1:def 3;
    A64:Seg len FX is Subset of NAT by FINSUB_1:def 5;
    then reconsider x1 as Nat by A48,A62;
    reconsider x2 as Nat by A48,A62,A64;
    A65: FY.x1 = (FYY.x1) mod m by A50,A63,Def1
              .= (a*FX.x1) mod m by RVSUM_1:66;
    A66: FY.x2 = (FYY.x2) mod m by A50,A63,Def1
              .= (a*FX.x2) mod m by RVSUM_1:66;
    A67: FX.x1 in rng FX by A49,A62,FUNCT_1:def 5;
    A68: FX.x2 in rng FX by A49,A62,FUNCT_1:def 5;
    A69:FX is one-to-one by A44,FINSEQ_3:99;
      not(FX.x1 in X & FX.x2 in X & FX.x1 <> FX.x2) by A13,A62,A65,A66;
    hence thesis by A44,A63,A67,A68,A69,FINSEQ_1:def 13,FUNCT_1:def 8;
  end;
::End of Euler's Lemma6

::Begin Euler's Lemma7
    for x be set holds card (FX"{x}) = card (FY"{x})
  proof
    let x be set;
      now per cases;
      suppose A70: x in X;
        then A71: x in rng FX by A44,FINSEQ_1:def 13;
          FX is one-to-one by A44,FINSEQ_3:99;
        then len(FX-{x}) = len(FX)-1 by A71,FINSEQ_3:97;
        then 0 = len(FX)-1-len(FX-{x}) by XCMPLX_1:14
              .= len(FX)-(1+len(FX-{x})) by XCMPLX_1:36
              .= len(FX)-len(FX-{x})-1 by XCMPLX_1:36;
        then 0+1 = len(FX)-len(FX-{x})-1+1;
        then A72: 1 = len(FX)-len(FX-{x})-(1-1) by XCMPLX_1:37
              .= len(FX)-len(FX-{x})-0;
          len(FX-{x})-len(FX-{x})
                 = len(FX)-card(FX"{x})-len(FX-{x}) by FINSEQ_3:66;
        then 0 = len(FX)-card(FX"{x})-len(FX-{x}) by XCMPLX_1:14
              .= len(FX)-(card(FX"{x})+len(FX-{x})) by XCMPLX_1:36
              .= len(FX)-len(FX-{x})-card(FX"{x}) by XCMPLX_1:36;
        then 0+card(FX"{x})
               = len(FX)-len(FX-{x})-card(FX"{x})+card(FX"{x});
        then A73: card(FX"{x})
               = len(FX)-len(FX-{x})-(card(FX"{x})-card(FX"{x}))
                                                        by XCMPLX_1:37
              .= len(FX)-len(FX-{x})-0 by XCMPLX_1:14;
          len(FY-{x}) = len(FY)-1 by A25,A51,A61,A70,FINSEQ_3:97;
        then 0 = len(FY)-1-len(FY-{x}) by XCMPLX_1:14
              .= len(FY)-(1+len(FY-{x})) by XCMPLX_1:36
              .= len(FY)-len(FY-{x})-1 by XCMPLX_1:36;
        then 0+1 = len(FY)-len(FY-{x})-1 +1;
        then A74: 1 = len(FY)-len(FY-{x})-(1-1) by XCMPLX_1:37
              .= len(FY)-len(FY-{x})-0;
          len(FY-{x}) = len(FY)-card(FY"{x}) by FINSEQ_3:66;
        then 0 = len(FY)-card(FY"{x})-len(FY-{x}) by XCMPLX_1:14
              .= len(FY)-(card(FY"{x})+len(FY-{x})) by XCMPLX_1:36
              .= len(FY)-len(FY-{x})-card(FY"{x}) by XCMPLX_1:36;
        then 0+card(FY"{x})
               = len(FY)-len(FY-{x})-card(FY"{x})+card(FY"{x});
        then card(FY"{x})
          = len(FY)-len(FY-{x})-(card(FY"{x})-card(FY"{x})) by XCMPLX_1:37
         .= len(FY)-len(FY-{x})-0 by XCMPLX_1:14;
        hence thesis by A72,A73,A74;
      suppose A75: not(x in X);
        then A76: not(x in rng FX) by A44,FINSEQ_1:def 13;
          FY"{x} = {} by A25,A51,A75,FUNCT_1:142;
        hence thesis by A76,FUNCT_1:142;
    end;
    hence thesis;
  end;
::End of Euler's Lemma7

  then A77:FX,FY are_fiberwise_equipotent by RFINSEQ:def 1;
  then A78:(Product FX) mod m = (Product FY) mod m by Th25;
  A79:len(FX) = len(FY) by A77,RFINSEQ:16;

::Begin Euler's Lemma8
  A80:(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;
    A81: P[0]
    proof
        0 <= len FY by NAT_1:18;
      then A82: len (FY|0) = 0 by TOPREAL1:3;
        0 <= len FX by NAT_1:18;
      then len (FX|0) = 0 by TOPREAL1:3;
      then Product (FX|0) = 1 by FINSEQ_1:25,RVSUM_1:124;
      then a |^ len(FY|0)*Product (FX|0) = 1 by A82,NEWTON:9;
      hence thesis by A82,FINSEQ_1:25,RVSUM_1:124;
    end;
    A83: for n st P[n] holds P[n+1]
    proof
      let n;
        now per cases;
        suppose A84: n+1 <= len FY;
          assume A85:P[n];
          A86:n <= n+1 by NAT_1:29;
          then n <= len FY by A84,AXIOMS:22;
          then A87:len(FY|n) = n by TOPREAL1:3;
          A88:len (FY|(n+1)) = n+1 by A84,TOPREAL1:3;
          then A89:FY|(n+1)
                 = (FY|(n+1))|n ^ <* (FY|(n+1)).(n+1) *> by RFINSEQ:20;
            0 < n+1 by NAT_1:19;
          then 0+1 <= n+1 by NAT_1:38;
          then A90: n+1 in dom FY by A84,FINSEQ_3:27;
          A91:(FY|(n+1))|n = FY|n by A86,JORDAN4:15;
          A92: (FY|(n+1)).(n+1) = FY.(n+1) by JORDAN3:20;
            len (FX|(n+1)) = n+1 by A79,A84,TOPREAL1:3;
          then A93:FX|(n+1)
                 = (FX|(n+1))|n ^ <* (FX|(n+1)).(n+1) *> by RFINSEQ:20;
          A94:(FX|(n+1))|n = FX|n by A86,JORDAN4:15;
          A95: (FX|(n+1)).(n+1) = FX.(n+1) by JORDAN3:20;
            (Product(FY|(n+1))) mod m = (Product(FY|n)*FY.(n+1)) mod m
          by A89,A91,A92,Lm7
            .= (((a |^ len(FY|n)*Product(FX|n)) mod m)
                      *(FY.(n+1) mod m)) mod m by A84,A85,A86,Th11,AXIOMS:22
            .= (((a |^ len(FY|n)*Product(FX|n)) mod m)
                      *((FYY.(n+1) mod m) mod m)) mod m by A49,A50,A90,Def1
            .= (((a |^ len(FY|n)*Product(FX|n)) mod m)
                      *((a*FX).(n+1) mod m)) mod m by Th7
            .= ((a |^ len(FY|n)*Product(FX|n))*(a*FX).(n+1)) mod m by Th11
            .= (a |^ len(FY|n)*Product
(FX|n))*(a*(FX.(n+1))) mod m by RVSUM_1:66
            .= a |^ len(FY|n)*Product(FX|n)*a*(FX.(n+1)) mod m by XCMPLX_1:4
            .= (a |^ len(FY|n)*a)*Product(FX|n)*(FX.(n+1)) mod m by XCMPLX_1:4
            .= (a |^ n*a)*(Product(FX|n)*(FX.(n+1))) mod m by A87,XCMPLX_1:4
            .= (a |^ len(FY|(n+1)))*(Product(FX|n)*(FX.(n+1))) mod m
               by A88,NEWTON:11
            .= (a |^ len(FY|(n+1)))*(Product(FX|(n+1))) mod m by A93,A94,A95,
Lm7;
        hence P[n+1];
        suppose n+1 > len FY;
        hence thesis;
      end;
      hence thesis;
    end;
    A96: for n holds P[n] from Ind(A81,A83);
      FY|len FY = FY|(Seg len FY) by TOPREAL1:def 1;
    then A97:FY = FY|len FY by FINSEQ_2:23;
      FX|len FX = FX|(Seg len FX) by TOPREAL1:def 1;
    then FX = FX|len FY by A79,FINSEQ_2:23;
    hence thesis by A96,A97;
  end;

::End of Euler's Lemma8

  A98: len FY = Euler m by A47,A77,RFINSEQ:16;
  A99:a |^ Euler m <> 0 by A1,PREPOWER:12;

::Begin Euler's Lemma9
  A100:Product FX <> 0
  proof
    assume Product FX = 0;
    then consider k such that
      A101:k in dom FX and
      A102:FX.k = 0 by RVSUM_1:133;
    A103:rng FX = X by A44,FINSEQ_1:def 13;
      FX.k in rng FX by A101,FUNCT_1:def 5;
    then consider p being Nat such that
      A104:FX.k = p and
        m,p are_relative_prime and
      A105:p >= 1 & p <= m by A103;
    thus contradiction by A102,A104,A105;
  end;
::End of Euler's Lemma9

::Begin Euler's Lemma10
    (Product FX),m are_relative_prime
  proof
    defpred P[Nat] means
      $1 <= len FX implies (Product (FX|$1)),m are_relative_prime;
    A106: P[0]
    proof
        0 <= len FX by NAT_1:18;
      then len (FX|0) = 0 by TOPREAL1:3;
      then (Product (FX|0)) = 1 by FINSEQ_1:25,RVSUM_1:124;
      then (Product (FX|0)) hcf m = 1 by NAT_LAT:35;
      hence thesis by INT_2:def 6;
    end;
    A107: for n st P[n] holds P[n+1]
    proof
      let n;
        now per cases;
        suppose A108:len FX >= n+1;
          assume A109:P[n];
          A110: n <= n+1 by NAT_1:29;
          reconsider FF = (FX|(n+1)) as FinSequence of NAT;
          reconsider ff = FF.(n+1) as Nat;
            len FF = n+1 by A108,TOPREAL1:3;
          then A111:FF = (FF|n) ^ <*ff*> by RFINSEQ:20;
            n <= n+1 by NAT_1:29;
          then A112:FX|n = FF|n by JORDAN4:15;
          A113:rng FX = X by A44,FINSEQ_1:def 13;
          A114:(FX|(n+1)).(n+1) = FX.(n+1) by JORDAN3:20;
            n >= 0 by NAT_1:18;
          then 0+1 <= (n+1) by AXIOMS:24;
          then n+1 in dom FX by A108,FINSEQ_3:27;
          then (FX|(n+1)).(n+1) in rng FX by A114,FUNCT_1:def 5;
          then consider p being Nat such that
            A115:ff = p and
            A116:m,p are_relative_prime and
            p >= 1 & p <= m by A113;
          reconsider a = (Product (FF|n)),b = ff,m' = m as Integer;
          A117:a,m' are_relative_prime by A108,A109,A110,A112,Th1,AXIOMS:22;
            b,m' are_relative_prime by A115,A116,Th1;
          then a*b,m' are_relative_prime by A117,INT_2:41;
          then (Product ((FF|n) ^ <*ff*>)),m' are_relative_prime by Lm7;
        hence P[n+1] by A111,Th1;
        suppose len FX < n+1;
        hence thesis;
      end;
      hence thesis;
    end;
    A118:for n holds P[n] from Ind(A106,A107);
      FX|len(FX) = FX by TOPREAL1:2;
    hence thesis by A118;
  end;
::End of Euler's Lemma10

  then m,(Product FX) are_relative_prime by Lm5;
  hence thesis by A1,A78,A80,A98,A99,A100,Th27;
end;
::End of Euler's Theorem

theorem ::Small Fermat's theorem
    a <> 0 & m is prime & a,m are_relative_prime
                       implies (a |^ m) mod m = a mod m
proof
  assume A1: a<>0 & m is prime & a,m are_relative_prime;
  then A2: m > 1 by INT_2:def 5;
  then m-1 > 1-1 by REAL_1:54;
  then reconsider mm = m-1 as Nat by INT_1:16;
  A3:mm+1 = m-(1-1) by XCMPLX_1:37
         .= m;
     Euler m = m-1 by A1,EULER_1:21;
  then ((a |^ mm) mod m)*a = 1*a by A1,A2,Th33;
  then ((a |^ mm)*a) mod m = a mod m by Th10;
  hence thesis by A3,NEWTON:11;
end;

Back to top