Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998 Association of Mizar Users

### 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;
```