Theorem phicl

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

	Ref	Expression
Assertion	phicl	$$⊢N\in \mathbb{N}\to \mathrm{\varphi }\left(N\right)\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		phicl2	$$⊢N\in \mathbb{N}\to \mathrm{\varphi }\left(N\right)\in \left(1\dots N\right)$$
2		elfznn	$$⊢\mathrm{\varphi }\left(N\right)\in \left(1\dots N\right)\to \mathrm{\varphi }\left(N\right)\in \mathbb{N}$$
3	1 2	syl	$$⊢N\in \mathbb{N}\to \mathrm{\varphi }\left(N\right)\in \mathbb{N}$$