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∈ℕ→ϕ⁡P1=P1−1⁢P−1
3 1 2 mpan2 ⊢P∈ℙ→ϕ⁡P1=P1−1⁢P−1
4 prmz ⊢P∈ℙ→P∈ℤ
5 4 zcnd ⊢P∈ℙ→P∈ℂ
6 5 exp1d ⊢P∈ℙ→P1=P
7 6 fveq2d ⊢P∈ℙ→ϕ⁡P1=ϕ⁡P
8 1m1e0 ⊢1−1=0
9 8 oveq2i ⊢P1−1=P0
10 5 exp0d ⊢P∈ℙ→P0=1
11 9 10 eqtrid ⊢P∈ℙ→P1−1=1
12 11 oveq1d ⊢P∈ℙ→P1−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 mullidd ⊢P∈ℙ→1⁢P−1=P−1
17 12 16 eqtrd ⊢P∈ℙ→P1−1⁢P−1=P−1
18 3 7 17 3eqtr3d ⊢P∈ℙ→ϕ⁡P=P−1