phival

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

		Ref	Expression
	Assertion	phival	$⊢ N \in ℕ \to ϕ (N) = \|\{x \in (1 \dots N) \| x \gcd N = 1\}\|$

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

Metamath Proof Explorer