This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-phi

Description: Define the Euler phi function (also called "Euler totient function"), which counts the number of integers less than n and coprime to it, see definition in ApostolNT p. 25. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion df-phi 
|- phi = ( n e. NN |-> ( # ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cphi 
 |-  phi
1 vn 
 |-  n
2 cn 
 |-  NN
3 chash 
 |-  #
4 vx 
 |-  x
5 c1 
 |-  1
6 cfz 
 |-  ...
7 1 cv 
 |-  n
8 5 7 6 co 
 |-  ( 1 ... n )
9 4 cv 
 |-  x
10 cgcd 
 |-  gcd
11 9 7 10 co 
 |-  ( x gcd n )
12 11 5 wceq 
 |-  ( x gcd n ) = 1
13 12 4 8 crab 
 |-  { x e. ( 1 ... n ) | ( x gcd n ) = 1 }
14 13 3 cfv 
 |-  ( # ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } )
15 1 2 14 cmpt 
 |-  ( n e. NN |-> ( # ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
16 0 15 wceq 
 |-  phi = ( n e. NN |-> ( # ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )