:: by Yoshinori Fujisawa and Yasushi Fuwa

::

:: Received December 10, 1997

:: Copyright (c) 1997-2012 Association of Mizar Users

begin

Lm1: for k being Nat

for j being Integer st k <> 0 & [\(j / k)/] + 1 >= j / k holds

k >= j - ([\(j / k)/] * k)

proof end;

Lm2: not 1 is prime

by INT_2:def 4;

theorem Th3: :: EULER_1:3

for n, k being Nat holds

( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } iff ( n is prime & k in n & not k in {0} ) )

( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } iff ( n is prime & k in n & not k in {0} ) )

proof end;

theorem Th9: :: EULER_1:9

for m, n being Nat st m,n are_relative_prime holds

ex k being Nat st

( ex i0, j0 being Integer st

( k = (i0 * m) + (j0 * n) & k > 0 ) & ( for l being Nat st ex i, j being Integer st

( l = (i * m) + (j * n) & l > 0 ) holds

k <= l ) )

ex k being Nat st

( ex i0, j0 being Integer st

( k = (i0 * m) + (j0 * n) & k > 0 ) & ( for l being Nat st ex i, j being Integer st

( l = (i * m) + (j * n) & l > 0 ) holds

k <= l ) )

proof end;

theorem Th10: :: EULER_1:10

for m, n being Nat st m,n are_relative_prime holds

for k being Nat ex i, j being Integer st (i * m) + (j * n) = k

for k being Nat ex i, j being Integer st (i * m) + (j * n) = k

proof end;

theorem Th11: :: EULER_1:11

for A being set

for B being non empty set

for f being Function of A,B st f is bijective holds

card A = card B

for B being non empty set

for f being Function of A,B st f is bijective holds

card A = card B

proof end;

theorem Th14: :: EULER_1:14

for a, c, b being Nat st a <> 0 & c <> 0 & a,c are_relative_prime & b,c are_relative_prime holds

a * b,c are_relative_prime

a * b,c are_relative_prime

proof end;

begin

definition

let n be Nat;

card { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } is Element of NAT

end;
func Euler n -> Element of NAT equals :: EULER_1:def 1

card { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } ;

coherence card { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } ;

card { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } is Element of NAT

proof end;

:: deftheorem defines Euler EULER_1:def 1 :

for n being Nat holds Euler n = card { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } ;

for n being Nat holds Euler n = card { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } ;

set X = { k where k is Element of NAT : ( 1,k are_relative_prime & k >= 1 & k <= 1 ) } ;

for x being set holds

( x in { k where k is Element of NAT : ( 1,k are_relative_prime & k >= 1 & k <= 1 ) } iff x = 1 )

proof end;

then Lm3: card {1} = Euler 1

by TARSKI:def 1;

set X = { k where k is Element of NAT : ( 2,k are_relative_prime & k >= 1 & k <= 2 ) } ;

for x being set holds

( x in { k where k is Element of NAT : ( 2,k are_relative_prime & k >= 1 & k <= 2 ) } iff x = 1 )

proof end;

then Lm4: card {1} = Euler 2

by TARSKI:def 1;

theorem :: EULER_1:21

for m, n being Nat st m > 1 & n > 1 & m,n are_relative_prime holds

Euler (m * n) = (Euler m) * (Euler n)

Euler (m * n) = (Euler m) * (Euler n)

proof end;