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 e. Prime -> ( phi ` P ) = ( P - 1 ) )

Proof

Step Hyp Ref Expression
1 1nn 
 |-  1 e. NN
2 phiprmpw 
 |-  ( ( P e. Prime /\ 1 e. NN ) -> ( phi ` ( P ^ 1 ) ) = ( ( P ^ ( 1 - 1 ) ) x. ( P - 1 ) ) )
3 1 2 mpan2 
 |-  ( P e. Prime -> ( phi ` ( P ^ 1 ) ) = ( ( P ^ ( 1 - 1 ) ) x. ( P - 1 ) ) )
4 prmz 
 |-  ( P e. Prime -> P e. ZZ )
5 4 zcnd 
 |-  ( P e. Prime -> P e. CC )
6 5 exp1d 
 |-  ( P e. Prime -> ( P ^ 1 ) = P )
7 6 fveq2d 
 |-  ( P e. Prime -> ( phi ` ( P ^ 1 ) ) = ( phi ` P ) )
8 1m1e0 
 |-  ( 1 - 1 ) = 0
9 8 oveq2i 
 |-  ( P ^ ( 1 - 1 ) ) = ( P ^ 0 )
10 5 exp0d 
 |-  ( P e. Prime -> ( P ^ 0 ) = 1 )
11 9 10 eqtrid 
 |-  ( P e. Prime -> ( P ^ ( 1 - 1 ) ) = 1 )
12 11 oveq1d 
 |-  ( P e. Prime -> ( ( P ^ ( 1 - 1 ) ) x. ( P - 1 ) ) = ( 1 x. ( P - 1 ) ) )
13 ax-1cn 
 |-  1 e. CC
14 subcl 
 |-  ( ( P e. CC /\ 1 e. CC ) -> ( P - 1 ) e. CC )
15 5 13 14 sylancl 
 |-  ( P e. Prime -> ( P - 1 ) e. CC )
16 15 mulid2d 
 |-  ( P e. Prime -> ( 1 x. ( P - 1 ) ) = ( P - 1 ) )
17 12 16 eqtrd 
 |-  ( P e. Prime -> ( ( P ^ ( 1 - 1 ) ) x. ( P - 1 ) ) = ( P - 1 ) )
18 3 7 17 3eqtr3d 
 |-  ( P e. Prime -> ( phi ` P ) = ( P - 1 ) )