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 ⊢ P ∈ ℙ → ϕ ⁡ P = P − 1

Proof

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