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 } ) )