Metamath Proof Explorer


Theorem phicld

Description: Closure for the value of the Euler phi function. (Contributed by Mario Carneiro, 29-May-2016)

Ref Expression
Hypothesis phicld.1 ( 𝜑𝑁 ∈ ℕ )
Assertion phicld ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 phicld.1 ( 𝜑𝑁 ∈ ℕ )
2 phicl ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) ∈ ℕ )
3 1 2 syl ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℕ )