Theorem phicl

Description: Closure for the value of the Euler phi function. (Contributed by Mario Carneiro, 28-Feb-2014)

	Ref	Expression
Assertion	phicl	⊢ ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		phicl2	⊢ ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) ∈ ( 1 ... 𝑁 ) )
2		elfznn	⊢ ( ( ϕ ‘ 𝑁 ) ∈ ( 1 ... 𝑁 ) → ( ϕ ‘ 𝑁 ) ∈ ℕ )
3	1 2	syl	⊢ ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) ∈ ℕ )