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

Metamath Proof Explorer

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