Theorem phi1

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

	Ref	Expression
Assertion	phi1	$$⊢\mathrm{\varphi }\left(1\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		1nn	$$⊢1\in \mathbb{N}$$
2		phicl2	$$⊢1\in \mathbb{N}\to \mathrm{\varphi }\left(1\right)\in \left(1\dots 1\right)$$
3	1 2	ax-mp	$$⊢\mathrm{\varphi }\left(1\right)\in \left(1\dots 1\right)$$
4		1z	$$⊢1\in \mathbb{Z}$$
5		fzsn	$$⊢1\in \mathbb{Z}\to \left(1\dots 1\right)=\left\{1\right\}$$
6	4 5	ax-mp	$$⊢\left(1\dots 1\right)=\left\{1\right\}$$
7	3 6	eleqtri	$$⊢\mathrm{\varphi }\left(1\right)\in \left\{1\right\}$$
8		elsni	$$⊢\mathrm{\varphi }\left(1\right)\in \left\{1\right\}\to \mathrm{\varphi }\left(1\right)=1$$
9	7 8	ax-mp	$$⊢\mathrm{\varphi }\left(1\right)=1$$