Journal of Formalized Mathematics
Volume 9, 1997
University of Bialystok
Copyright (c) 1997 Association of Mizar Users

### The Euler's Function

by
Yoshinori Fujisawa, and
Yasushi Fuwa

MML identifier: EULER_1
[ Mizar article, MML identifier index ]

```environ

vocabulary INT_1, INT_2, ARYTM_3, ABSVALUE, NAT_1, ARYTM_1, ORDINAL2, ARYTM,
FILTER_0, FINSET_1, CARD_1, BOOLE, FUNCT_1, SGRAPH1, RELAT_1, FINSEQ_1,
EULER_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL2, ORDINAL1, NUMBERS,
XCMPLX_0, XREAL_0, CARD_1, INT_1, GROUP_1, NAT_1, INT_2, FINSEQ_1,
FINSET_1, RELAT_1, FUNCT_1, FUNCT_2;
constructors NAT_1, GROUP_1, INT_2, REAL_1, DOMAIN_1, MEMBERED;
clusters SUBSET_1, FINSET_1, INT_1, CARD_1, XREAL_0, FINSEQ_1, RELSET_1,
ARYTM_3, MEMBERED, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin :: Preliminary

reserve a,b,c,k,l,m,n for Nat,
i,j,x,y for Integer;

theorem :: EULER_1:1
for k, n being natural number holds k in n iff k < n;

theorem :: EULER_1:2
n,n are_relative_prime iff n = 1;

theorem :: EULER_1:3
k <> 0 & k < n & n is prime implies k,n are_relative_prime;

theorem :: EULER_1:4
n is prime &
k in {kk where kk is Nat:n,kk are_relative_prime & kk >= 1 & kk <= n}
iff n is prime & k in n & not k in {0};

theorem :: EULER_1:5
for A being finite set, x being set st x in A holds
Card(A \ {x}) = Card A - Card{x};

theorem :: EULER_1:6
a hcf b = 1 implies for c holds a*c hcf b*c = c;

theorem :: EULER_1:7
a <> 0 & b <> 0 & c <> 0 & a*c hcf b*c = c
implies a,b are_relative_prime;

theorem :: EULER_1:8
a hcf b = 1 implies (a + b) hcf b = 1;

theorem :: EULER_1:9
for c holds (a + b*c) hcf b = a hcf b;

theorem :: EULER_1:10
m,n are_relative_prime implies
ex k st (ex i0,j0 being Integer st k = i0*m + j0*n & k > 0) &
for l st (ex i,j being Integer st l = i*m + j*n & l > 0)
holds k <= l;

theorem :: EULER_1:11
m,n are_relative_prime implies for k holds ex i,j st i*m + j*n = k;

theorem :: EULER_1:12
for A,B being non empty finite set holds
(ex f being Function of A, B st f is one-to-one onto)
implies Card A = Card B;

theorem :: EULER_1:13
for i,k,n being Integer holds (i + k*n) mod n = i mod n;

theorem :: EULER_1:14
a <> 0 & b <> 0 & c <> 0 & c divides a*b & a,c are_relative_prime implies c
divides b;

theorem :: EULER_1:15
a <> 0 & b <> 0 & c <> 0 &
a,c are_relative_prime & b,c are_relative_prime
implies a*b,c are_relative_prime;

theorem :: EULER_1:16
x <> 0 & y <> 0 & i > 0 implies i*x gcd i*y = i*(x gcd y);

theorem :: EULER_1:17
for x st a <> 0 & b <> 0 holds (a + x*b) gcd b = a gcd b;

begin :: Euler's function

definition
let n be Nat;
func Euler n -> Nat
equals
:: EULER_1:def 1
Card {k where k is Nat : n,k are_relative_prime & k >= 1 & k <= n};
end;

theorem :: EULER_1:18
Euler 1 = 1;

theorem :: EULER_1:19
Euler 2 = 1;

theorem :: EULER_1:20
n > 1 implies Euler n <= n - 1;

theorem :: EULER_1:21
n is prime implies Euler n = n - 1;

theorem :: EULER_1:22
m > 1 & n > 1 & m,n are_relative_prime
implies Euler (m*n) = Euler m * Euler n;
```