Theorem phicld

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

	Ref	Expression
Hypothesis	phicld.1	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	phicld	$$⊢\phi \to \mathrm{\varphi }\left(N\right)\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		phicld.1	$$⊢\phi \to N\in \mathbb{N}$$
2		phicl	$$⊢N\in \mathbb{N}\to \mathrm{\varphi }\left(N\right)\in \mathbb{N}$$
3	1 2	syl	$$⊢\phi \to \mathrm{\varphi }\left(N\right)\in \mathbb{N}$$