The abstract of the Mizar article:

The Euler's Function

by

Yoshinori Fujisawa, and

Yasushi Fuwa

Received December 10, 1997

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;