Theorem phiprm

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

	Ref	Expression
Assertion	phiprm	⊢ ( 𝑃 ∈ ℙ → ( ϕ ‘ 𝑃 ) = ( 𝑃 − 1 ) )

Proof

Step	Hyp	Ref	Expression
1		1nn	⊢ 1 ∈ ℕ
2		phiprmpw	⊢ ( ( 𝑃 ∈ ℙ ∧ 1 ∈ ℕ ) → ( ϕ ‘ ( 𝑃 ↑ 1 ) ) = ( ( 𝑃 ↑ ( 1 − 1 ) ) · ( 𝑃 − 1 ) ) )
3	1 2	mpan2	⊢ ( 𝑃 ∈ ℙ → ( ϕ ‘ ( 𝑃 ↑ 1 ) ) = ( ( 𝑃 ↑ ( 1 − 1 ) ) · ( 𝑃 − 1 ) ) )
4		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
5	4	zcnd	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℂ )
6	5	exp1d	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ↑ 1 ) = 𝑃 )
7	6	fveq2d	⊢ ( 𝑃 ∈ ℙ → ( ϕ ‘ ( 𝑃 ↑ 1 ) ) = ( ϕ ‘ 𝑃 ) )
8		1m1e0	⊢ ( 1 − 1 ) = 0
9	8	oveq2i	⊢ ( 𝑃 ↑ ( 1 − 1 ) ) = ( 𝑃 ↑ 0 )
10	5	exp0d	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ↑ 0 ) = 1 )
11	9 10	eqtrid	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ↑ ( 1 − 1 ) ) = 1 )
12	11	oveq1d	⊢ ( 𝑃 ∈ ℙ → ( ( 𝑃 ↑ ( 1 − 1 ) ) · ( 𝑃 − 1 ) ) = ( 1 · ( 𝑃 − 1 ) ) )
13		ax-1cn	⊢ 1 ∈ ℂ
14		subcl	⊢ ( ( 𝑃 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑃 − 1 ) ∈ ℂ )
15	5 13 14	sylancl	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 − 1 ) ∈ ℂ )
16	15	mulid2d	⊢ ( 𝑃 ∈ ℙ → ( 1 · ( 𝑃 − 1 ) ) = ( 𝑃 − 1 ) )
17	12 16	eqtrd	⊢ ( 𝑃 ∈ ℙ → ( ( 𝑃 ↑ ( 1 − 1 ) ) · ( 𝑃 − 1 ) ) = ( 𝑃 − 1 ) )
18	3 7 17	3eqtr3d	⊢ ( 𝑃 ∈ ℙ → ( ϕ ‘ 𝑃 ) = ( 𝑃 − 1 ) )