Theorem phival

Description: Value of the Euler phi function. (Contributed by Mario Carneiro, 23-Feb-2014)

	Ref	Expression
Assertion	phival	$$⊢N\in \mathbb{N}\to \mathrm{\varphi }\left(N\right)=\left|\left\{x\in \left(1\dots N\right)|x\gcd N=1\right\}\right|$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢n=N\to \left(1\dots n\right)=\left(1\dots N\right)$$
2		oveq2	$$⊢n=N\to x\gcd n=x\gcd N$$
3	2	eqeq1d	$$⊢n=N\to \left(x\gcd n=1\leftrightarrow x\gcd N=1\right)$$
4	1 3	rabeqbidv	$$⊢n=N\to \left\{x\in \left(1\dots n\right)|x\gcd n=1\right\}=\left\{x\in \left(1\dots N\right)|x\gcd N=1\right\}$$
5	4	fveq2d	$$⊢n=N\to \left|\left\{x\in \left(1\dots n\right)|x\gcd n=1\right\}\right|=\left|\left\{x\in \left(1\dots N\right)|x\gcd N=1\right\}\right|$$
6		df-phi	$$⊢\mathrm{\varphi }=\left(n\in \mathbb{N}⟼\left|\left\{x\in \left(1\dots n\right)|x\gcd n=1\right\}\right|\right)$$
7		fvex	$$⊢\left|\left\{x\in \left(1\dots N\right)|x\gcd N=1\right\}\right|\in \mathrm{V}$$
8	5 6 7	fvmpt	$$⊢N\in \mathbb{N}\to \mathrm{\varphi }\left(N\right)=\left|\left\{x\in \left(1\dots N\right)|x\gcd N=1\right\}\right|$$