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	⊢ ϕ = ( 𝑛 ∈ ℕ ↦ ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑛 ) ∣ ( 𝑥 gcd 𝑛 ) = 1 } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cphi	⊢ ϕ
1		vn	⊢ 𝑛
2		cn	⊢ ℕ
3		chash	⊢ ♯
4		vx	⊢ 𝑥
5		c1	⊢ 1
6		cfz	⊢ ...
7	1	cv	⊢ 𝑛
8	5 7 6	co	⊢ ( 1 ... 𝑛 )
9	4	cv	⊢ 𝑥
10		cgcd	⊢ gcd
11	9 7 10	co	⊢ ( 𝑥 gcd 𝑛 )
12	11 5	wceq	⊢ ( 𝑥 gcd 𝑛 ) = 1
13	12 4 8	crab	⊢ { 𝑥 ∈ ( 1 ... 𝑛 ) ∣ ( 𝑥 gcd 𝑛 ) = 1 }
14	13 3	cfv	⊢ ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑛 ) ∣ ( 𝑥 gcd 𝑛 ) = 1 } )
15	1 2 14	cmpt	⊢ ( 𝑛 ∈ ℕ ↦ ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑛 ) ∣ ( 𝑥 gcd 𝑛 ) = 1 } ) )
16	0 15	wceq	⊢ ϕ = ( 𝑛 ∈ ℕ ↦ ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑛 ) ∣ ( 𝑥 gcd 𝑛 ) = 1 } ) )