Definition df-phi 12379

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

Assertion

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

Distinct variable group:   x, n

Detailed syntax breakdown of Definition df-phi

Step	Hyp	Ref	Expression
1		cphi 12377	. 2 class phi
2		vn	. . 3 setvar n
3		cn 8990	. . 3 class NN
4		vx	. . . . . . . 8 setvar x
5	4	cv 1363	. . . . . . 7 class x
6	2	cv 1363	. . . . . . 7 class n
7		cgcd 12120	. . . . . . 7 class gcd
8	5, 6, 7	co 5922	. . . . . 6 class ( x gcd n )
9		c1 7880	. . . . . 6 class 1
10	8, 9	wceq 1364	. . . . 5 wff ( x gcd n ) = 1
11		cfz 10083	. . . . . 6 class ...
12	9, 6, 11	co 5922	. . . . 5 class ( 1 ... n )
13	10, 4, 12	crab 2479	. . . 4 class { x e. ( 1 ... n ) | ( x gcd n ) = 1 }
14		chash 10867	. . . 4 class ♯
15	13, 14	cfv 5258	. . 3 class (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } )
16	2, 3, 15	cmpt 4094	. 2 class ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )
17	1, 16	wceq 1364	1 wff phi = ( n e. NN |-> (♯ ` { x e. ( 1 ... n ) | ( x gcd n ) = 1 } ) )

This definition is referenced by:  phival  12381