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

Metamath Proof Explorer

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 mullidd ⊢ ( 𝑃 ∈ ℙ → ( 1 · ( 𝑃 − 1 ) ) = ( 𝑃 − 1 ) )
17 12 16 eqtrd ⊢ ( 𝑃 ∈ ℙ → ( ( 𝑃 ↑ ( 1 − 1 ) ) · ( 𝑃 − 1 ) ) = ( 𝑃 − 1 ) )
18 3 7 17 3eqtr3d ⊢ ( 𝑃 ∈ ℙ → ( ϕ ‘ 𝑃 ) = ( 𝑃 − 1 ) )