The abstract of the Mizar article:

Euler's Theorem and Small Fermat's Theorem

by

Yoshinori Fujisawa,

Yasushi Fuwa, and

Hidetaka Shimizu

Received June 10, 1998

MML identifier: EULER_2

[ Mizar article, 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;


begin :: Preliminary

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

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

theorem :: EULER_2:1
  a,(b qua Integer) are_relative_prime iff a,b are_relative_prime;

theorem :: EULER_2:2
  m > 1 & m*t >= 1 implies t >= 1;

theorem :: EULER_2:3
  m > 1 & m*t >= 0 implies t >= 0;

canceled;

theorem :: EULER_2:5
  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;

theorem :: EULER_2:6
  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;

theorem :: EULER_2:7
  for n holds (m mod n) mod n = m mod n;

theorem :: EULER_2:8
    for n holds (l+m) mod n = ((l mod n)+(m mod n)) mod n;

theorem :: EULER_2:9
  for n holds (l*m) mod n = (l*(m mod n)) mod n;

theorem :: EULER_2:10
  for n holds (l*m) mod n = ((l mod n)*m) mod n;

theorem :: EULER_2:11
  for n holds (l*m) mod n = ((l mod n)*(m mod n)) mod n;

begin

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

definition let a,f;
  redefine func a*f -> FinSequence of NAT;
end;

canceled 13;

theorem :: EULER_2:25
  for R1,R2 be FinSequence of NAT
         st R1,R2 are_fiberwise_equipotent holds Product R1 = Product R2;

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
:: EULER_2:def 1

  len(it) = len(f) & for i being Nat st i in dom f holds it.i = (f.i) mod m;
end;

theorem :: EULER_2:26
    for f be FinSequence of NAT st m <> 0 holds
                          (Product(f mod m)) mod m = (Product f) mod m;

theorem :: EULER_2:27
  a <> 0 & m > 1 & n <> 0 &
      a*n mod m = n mod m & m,n are_relative_prime implies a mod m = 1;

theorem :: EULER_2:28
    for F holds (F mod m) mod m = F mod m;

theorem :: EULER_2:29
    for F holds (a*(F mod m)) mod m = (a*F) mod m;

theorem :: EULER_2:30
    for F,G being FinSequence of NAT
             holds (F ^ G) mod m = (F mod m) ^ (G mod m);

theorem :: EULER_2:31
    for F,G being FinSequence of NAT
             holds (a*(F ^ G)) mod m = ((a*F) mod m) ^ ((a*G) mod m);


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

definition let n,k;
  redefine func n |^ k -> Nat;
end;

theorem :: EULER_2:32
    a <> 0 & m <> 0 & a,m are_relative_prime
           implies for b holds (a |^ b),m are_relative_prime;

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

theorem :: EULER_2:33 ::Euler's theorem
  a <> 0 & m > 1 & a,m are_relative_prime
                  implies (a |^ Euler m) mod m = 1;
::End of Euler's Theorem

theorem :: EULER_2:34 ::Small Fermat's theorem
    a <> 0 & m is prime & a,m are_relative_prime
                       implies (a |^ m) mod m = a mod m;