Theorem phival

Description: Value of the Euler phi function. (Contributed by Mario Carneiro, 23-Feb-2014)

	Ref	Expression
Assertion	phival	⊢ ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) = ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑛 = 𝑁 → ( 1 ... 𝑛 ) = ( 1 ... 𝑁 ) )
2		oveq2	⊢ ( 𝑛 = 𝑁 → ( 𝑥 gcd 𝑛 ) = ( 𝑥 gcd 𝑁 ) )
3	2	eqeq1d	⊢ ( 𝑛 = 𝑁 → ( ( 𝑥 gcd 𝑛 ) = 1 ↔ ( 𝑥 gcd 𝑁 ) = 1 ) )
4	1 3	rabeqbidv	⊢ ( 𝑛 = 𝑁 → { 𝑥 ∈ ( 1 ... 𝑛 ) ∣ ( 𝑥 gcd 𝑛 ) = 1 } = { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } )
5	4	fveq2d	⊢ ( 𝑛 = 𝑁 → ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑛 ) ∣ ( 𝑥 gcd 𝑛 ) = 1 } ) = ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) )
6		df-phi	⊢ ϕ = ( 𝑛 ∈ ℕ ↦ ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑛 ) ∣ ( 𝑥 gcd 𝑛 ) = 1 } ) )
7		fvex	⊢ ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) ∈ V
8	5 6 7	fvmpt	⊢ ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) = ( ♯ ‘ { 𝑥 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) )