This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem phi1

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

		Ref	Expression
	Assertion	phi1	$⊢ ϕ (1) = 1$

Step	Hyp	Ref	Expression
1		1nn	$⊢ 1 \in ℕ$
2		phicl2	$⊢ 1 \in ℕ \to ϕ (1) \in (1 \dots 1)$
3	1 2	ax-mp	$⊢ ϕ (1) \in (1 \dots 1)$
4		1z	$⊢ 1 \in ℤ$
5		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
6	4 5	ax-mp	$⊢ (1 \dots 1) = \{1\}$
7	3 6	eleqtri	$⊢ ϕ (1) \in \{1\}$
8		elsni	$⊢ ϕ (1) \in \{1\} \to ϕ (1) = 1$
9	7 8	ax-mp	$⊢ ϕ (1) = 1$