Metamath Proof Explorer

Theorem phicl

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

Ref Expression
Assertion phicl 
|- ( N e. NN -> ( phi ` N ) e. NN )

Proof

Step Hyp Ref Expression
1 phicl2 
 |-  ( N e. NN -> ( phi ` N ) e. ( 1 ... N ) )
2 elfznn 
 |-  ( ( phi ` N ) e. ( 1 ... N ) -> ( phi ` N ) e. NN )
3 1 2 syl 
 |-  ( N e. NN -> ( phi ` N ) e. NN )