Theorem phi1

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

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

Proof

Step	Hyp	Ref	Expression
1		1nn	⊢ 1 ∈ ℕ
2		phicl2	⊢ ( 1 ∈ ℕ → ( ϕ ‘ 1 ) ∈ ( 1 ... 1 ) )
3	1 2	ax-mp	⊢ ( ϕ ‘ 1 ) ∈ ( 1 ... 1 )
4		1z	⊢ 1 ∈ ℤ
5		fzsn	⊢ ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
6	4 5	ax-mp	⊢ ( 1 ... 1 ) = { 1 }
7	3 6	eleqtri	⊢ ( ϕ ‘ 1 ) ∈ { 1 }
8		elsni	⊢ ( ( ϕ ‘ 1 ) ∈ { 1 } → ( ϕ ‘ 1 ) = 1 )
9	7 8	ax-mp	⊢ ( ϕ ‘ 1 ) = 1