Metamath Proof Explorer

Theorem phiprmpw

Description: Value of the Euler phi function at a prime power. Theorem 2.5(a) in ApostolNT p. 28. (Contributed by Mario Carneiro, 24-Feb-2014)

Ref Expression
Assertion phiprmpw 
|- ( ( P e. Prime /\ K e. NN ) -> ( phi ` ( P ^ K ) ) = ( ( P ^ ( K - 1 ) ) x. ( P - 1 ) ) )

Proof

Step Hyp Ref Expression
1 prmnn 
 |-  ( P e. Prime -> P e. NN )
2 nnnn0 
 |-  ( K e. NN -> K e. NN0 )
3 nnexpcl 
 |-  ( ( P e. NN /\ K e. NN0 ) -> ( P ^ K ) e. NN )
4 1 2 3 syl2an 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( P ^ K ) e. NN )
5 phival 
 |-  ( ( P ^ K ) e. NN -> ( phi ` ( P ^ K ) ) = ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) )
6 4 5 syl 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( phi ` ( P ^ K ) ) = ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) )
7 nnm1nn0 
 |-  ( K e. NN -> ( K - 1 ) e. NN0 )
8 nnexpcl 
 |-  ( ( P e. NN /\ ( K - 1 ) e. NN0 ) -> ( P ^ ( K - 1 ) ) e. NN )
9 1 7 8 syl2an 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( P ^ ( K - 1 ) ) e. NN )
10 9 nncnd 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( P ^ ( K - 1 ) ) e. CC )
11 1 nncnd 
 |-  ( P e. Prime -> P e. CC )
12 11 adantr 
 |-  ( ( P e. Prime /\ K e. NN ) -> P e. CC )
13 ax-1cn 
 |-  1 e. CC
14 subdi 
 |-  ( ( ( P ^ ( K - 1 ) ) e. CC /\ P e. CC /\ 1 e. CC ) -> ( ( P ^ ( K - 1 ) ) x. ( P - 1 ) ) = ( ( ( P ^ ( K - 1 ) ) x. P ) - ( ( P ^ ( K - 1 ) ) x. 1 ) ) )
15 13 14 mp3an3 
 |-  ( ( ( P ^ ( K - 1 ) ) e. CC /\ P e. CC ) -> ( ( P ^ ( K - 1 ) ) x. ( P - 1 ) ) = ( ( ( P ^ ( K - 1 ) ) x. P ) - ( ( P ^ ( K - 1 ) ) x. 1 ) ) )
16 10 12 15 syl2anc 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( ( P ^ ( K - 1 ) ) x. ( P - 1 ) ) = ( ( ( P ^ ( K - 1 ) ) x. P ) - ( ( P ^ ( K - 1 ) ) x. 1 ) ) )
17 10 mulridd 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( ( P ^ ( K - 1 ) ) x. 1 ) = ( P ^ ( K - 1 ) ) )
18 17 oveq2d 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( ( ( P ^ ( K - 1 ) ) x. P ) - ( ( P ^ ( K - 1 ) ) x. 1 ) ) = ( ( ( P ^ ( K - 1 ) ) x. P ) - ( P ^ ( K - 1 ) ) ) )
19 fzfi 
 |-  ( 1 ... ( P ^ K ) ) e. Fin
20 ssrab2 
 |-  { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } C_ ( 1 ... ( P ^ K ) )
21 ssfi 
 |-  ( ( ( 1 ... ( P ^ K ) ) e. Fin /\ { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } C_ ( 1 ... ( P ^ K ) ) ) -> { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } e. Fin )
22 19 20 21 mp2an 
 |-  { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } e. Fin
23 ssrab2 
 |-  { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } C_ ( 1 ... ( P ^ K ) )
24 ssfi 
 |-  ( ( ( 1 ... ( P ^ K ) ) e. Fin /\ { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } C_ ( 1 ... ( P ^ K ) ) ) -> { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } e. Fin )
25 19 23 24 mp2an 
 |-  { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } e. Fin
26 inrab 
 |-  ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } i^i { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) = { x e. ( 1 ... ( P ^ K ) ) | ( ( x gcd ( P ^ K ) ) = 1 /\ P || ( x - 0 ) ) }
27 elfzelz 
 |-  ( x e. ( 1 ... ( P ^ K ) ) -> x e. ZZ )
28 prmz 
 |-  ( P e. Prime -> P e. ZZ )
29 rpexp 
 |-  ( ( P e. ZZ /\ x e. ZZ /\ K e. NN ) -> ( ( ( P ^ K ) gcd x ) = 1 <-> ( P gcd x ) = 1 ) )
30 28 29 syl3an1 
 |-  ( ( P e. Prime /\ x e. ZZ /\ K e. NN ) -> ( ( ( P ^ K ) gcd x ) = 1 <-> ( P gcd x ) = 1 ) )
31 30 3expa 
 |-  ( ( ( P e. Prime /\ x e. ZZ ) /\ K e. NN ) -> ( ( ( P ^ K ) gcd x ) = 1 <-> ( P gcd x ) = 1 ) )
32 31 an32s 
 |-  ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( ( ( P ^ K ) gcd x ) = 1 <-> ( P gcd x ) = 1 ) )
33 simpr 
 |-  ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> x e. ZZ )
34 zexpcl 
 |-  ( ( P e. ZZ /\ K e. NN0 ) -> ( P ^ K ) e. ZZ )
35 28 2 34 syl2an 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( P ^ K ) e. ZZ )
36 35 adantr 
 |-  ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( P ^ K ) e. ZZ )
37 33 36 gcdcomd 
 |-  ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( x gcd ( P ^ K ) ) = ( ( P ^ K ) gcd x ) )
38 37 eqeq1d 
 |-  ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( ( x gcd ( P ^ K ) ) = 1 <-> ( ( P ^ K ) gcd x ) = 1 ) )
39 coprm 
 |-  ( ( P e. Prime /\ x e. ZZ ) -> ( -. P || x <-> ( P gcd x ) = 1 ) )
40 39 adantlr 
 |-  ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( -. P || x <-> ( P gcd x ) = 1 ) )
41 32 38 40 3bitr4d 
 |-  ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( ( x gcd ( P ^ K ) ) = 1 <-> -. P || x ) )
42 zcn 
 |-  ( x e. ZZ -> x e. CC )
43 42 adantl 
 |-  ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> x e. CC )
44 43 subid1d 
 |-  ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( x - 0 ) = x )
45 44 breq2d 
 |-  ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( P || ( x - 0 ) <-> P || x ) )
46 45 notbid 
 |-  ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( -. P || ( x - 0 ) <-> -. P || x ) )
47 41 46 bitr4d 
 |-  ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( ( x gcd ( P ^ K ) ) = 1 <-> -. P || ( x - 0 ) ) )
48 27 47 sylan2 
 |-  ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> ( ( x gcd ( P ^ K ) ) = 1 <-> -. P || ( x - 0 ) ) )
49 48 biimpd 
 |-  ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> ( ( x gcd ( P ^ K ) ) = 1 -> -. P || ( x - 0 ) ) )
50 imnan 
 |-  ( ( ( x gcd ( P ^ K ) ) = 1 -> -. P || ( x - 0 ) ) <-> -. ( ( x gcd ( P ^ K ) ) = 1 /\ P || ( x - 0 ) ) )
51 49 50 sylib 
 |-  ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> -. ( ( x gcd ( P ^ K ) ) = 1 /\ P || ( x - 0 ) ) )
52 51 ralrimiva 
 |-  ( ( P e. Prime /\ K e. NN ) -> A. x e. ( 1 ... ( P ^ K ) ) -. ( ( x gcd ( P ^ K ) ) = 1 /\ P || ( x - 0 ) ) )
53 rabeq0 
 |-  ( { x e. ( 1 ... ( P ^ K ) ) | ( ( x gcd ( P ^ K ) ) = 1 /\ P || ( x - 0 ) ) } = (/) <-> A. x e. ( 1 ... ( P ^ K ) ) -. ( ( x gcd ( P ^ K ) ) = 1 /\ P || ( x - 0 ) ) )
54 52 53 sylibr 
 |-  ( ( P e. Prime /\ K e. NN ) -> { x e. ( 1 ... ( P ^ K ) ) | ( ( x gcd ( P ^ K ) ) = 1 /\ P || ( x - 0 ) ) } = (/) )
55 26 54 eqtrid 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } i^i { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) = (/) )
56 hashun 
 |-  ( ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } e. Fin /\ { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } e. Fin /\ ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } i^i { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) = (/) ) -> ( # ` ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } u. { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) ) = ( ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) + ( # ` { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) ) )
57 22 25 55 56 mp3an12i 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( # ` ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } u. { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) ) = ( ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) + ( # ` { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) ) )
58 unrab 
 |-  ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } u. { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) = { x e. ( 1 ... ( P ^ K ) ) | ( ( x gcd ( P ^ K ) ) = 1 \/ P || ( x - 0 ) ) }
59 48 biimprd 
 |-  ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> ( -. P || ( x - 0 ) -> ( x gcd ( P ^ K ) ) = 1 ) )
60 59 con1d 
 |-  ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> ( -. ( x gcd ( P ^ K ) ) = 1 -> P || ( x - 0 ) ) )
61 60 orrd 
 |-  ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> ( ( x gcd ( P ^ K ) ) = 1 \/ P || ( x - 0 ) ) )
62 61 ralrimiva 
 |-  ( ( P e. Prime /\ K e. NN ) -> A. x e. ( 1 ... ( P ^ K ) ) ( ( x gcd ( P ^ K ) ) = 1 \/ P || ( x - 0 ) ) )
63 rabid2 
 |-  ( ( 1 ... ( P ^ K ) ) = { x e. ( 1 ... ( P ^ K ) ) | ( ( x gcd ( P ^ K ) ) = 1 \/ P || ( x - 0 ) ) } <-> A. x e. ( 1 ... ( P ^ K ) ) ( ( x gcd ( P ^ K ) ) = 1 \/ P || ( x - 0 ) ) )
64 62 63 sylibr 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( 1 ... ( P ^ K ) ) = { x e. ( 1 ... ( P ^ K ) ) | ( ( x gcd ( P ^ K ) ) = 1 \/ P || ( x - 0 ) ) } )
65 58 64 eqtr4id 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } u. { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) = ( 1 ... ( P ^ K ) ) )
66 65 fveq2d 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( # ` ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } u. { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) ) = ( # ` ( 1 ... ( P ^ K ) ) ) )
67 4 nnnn0d 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( P ^ K ) e. NN0 )
68 hashfz1 
 |-  ( ( P ^ K ) e. NN0 -> ( # ` ( 1 ... ( P ^ K ) ) ) = ( P ^ K ) )
69 67 68 syl 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( # ` ( 1 ... ( P ^ K ) ) ) = ( P ^ K ) )
70 expm1t 
 |-  ( ( P e. CC /\ K e. NN ) -> ( P ^ K ) = ( ( P ^ ( K - 1 ) ) x. P ) )
71 11 70 sylan 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( P ^ K ) = ( ( P ^ ( K - 1 ) ) x. P ) )
72 66 69 71 3eqtrd 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( # ` ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } u. { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) ) = ( ( P ^ ( K - 1 ) ) x. P ) )
73 1 adantr 
 |-  ( ( P e. Prime /\ K e. NN ) -> P e. NN )
74 1zzd 
 |-  ( ( P e. Prime /\ K e. NN ) -> 1 e. ZZ )
75 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
76 1m1e0 
 |-  ( 1 - 1 ) = 0
77 76 fveq2i 
 |-  ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
78 75 77 eqtr4i 
 |-  NN0 = ( ZZ>= ` ( 1 - 1 ) )
79 67 78 eleqtrdi 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( P ^ K ) e. ( ZZ>= ` ( 1 - 1 ) ) )
80 0zd 
 |-  ( ( P e. Prime /\ K e. NN ) -> 0 e. ZZ )
81 73 74 79 80 hashdvds 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( # ` { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) = ( ( |_ ` ( ( ( P ^ K ) - 0 ) / P ) ) - ( |_ ` ( ( ( 1 - 1 ) - 0 ) / P ) ) ) )
82 4 nncnd 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( P ^ K ) e. CC )
83 82 subid1d 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( ( P ^ K ) - 0 ) = ( P ^ K ) )
84 83 oveq1d 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( ( ( P ^ K ) - 0 ) / P ) = ( ( P ^ K ) / P ) )
85 73 nnne0d 
 |-  ( ( P e. Prime /\ K e. NN ) -> P =/= 0 )
86 nnz 
 |-  ( K e. NN -> K e. ZZ )
87 86 adantl 
 |-  ( ( P e. Prime /\ K e. NN ) -> K e. ZZ )
88 12 85 87 expm1d 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( P ^ ( K - 1 ) ) = ( ( P ^ K ) / P ) )
89 84 88 eqtr4d 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( ( ( P ^ K ) - 0 ) / P ) = ( P ^ ( K - 1 ) ) )
90 89 fveq2d 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( |_ ` ( ( ( P ^ K ) - 0 ) / P ) ) = ( |_ ` ( P ^ ( K - 1 ) ) ) )
91 9 nnzd 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( P ^ ( K - 1 ) ) e. ZZ )
92 flid 
 |-  ( ( P ^ ( K - 1 ) ) e. ZZ -> ( |_ ` ( P ^ ( K - 1 ) ) ) = ( P ^ ( K - 1 ) ) )
93 91 92 syl 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( |_ ` ( P ^ ( K - 1 ) ) ) = ( P ^ ( K - 1 ) ) )
94 90 93 eqtrd 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( |_ ` ( ( ( P ^ K ) - 0 ) / P ) ) = ( P ^ ( K - 1 ) ) )
95 76 oveq1i 
 |-  ( ( 1 - 1 ) - 0 ) = ( 0 - 0 )
96 0m0e0 
 |-  ( 0 - 0 ) = 0
97 95 96 eqtri 
 |-  ( ( 1 - 1 ) - 0 ) = 0
98 97 oveq1i 
 |-  ( ( ( 1 - 1 ) - 0 ) / P ) = ( 0 / P )
99 12 85 div0d 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( 0 / P ) = 0 )
100 98 99 eqtrid 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( ( ( 1 - 1 ) - 0 ) / P ) = 0 )
101 100 fveq2d 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( |_ ` ( ( ( 1 - 1 ) - 0 ) / P ) ) = ( |_ ` 0 ) )
102 0z 
 |-  0 e. ZZ
103 flid 
 |-  ( 0 e. ZZ -> ( |_ ` 0 ) = 0 )
104 102 103 ax-mp 
 |-  ( |_ ` 0 ) = 0
105 101 104 eqtrdi 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( |_ ` ( ( ( 1 - 1 ) - 0 ) / P ) ) = 0 )
106 94 105 oveq12d 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( ( |_ ` ( ( ( P ^ K ) - 0 ) / P ) ) - ( |_ ` ( ( ( 1 - 1 ) - 0 ) / P ) ) ) = ( ( P ^ ( K - 1 ) ) - 0 ) )
107 10 subid1d 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( ( P ^ ( K - 1 ) ) - 0 ) = ( P ^ ( K - 1 ) ) )
108 81 106 107 3eqtrd 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( # ` { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) = ( P ^ ( K - 1 ) ) )
109 108 oveq2d 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) + ( # ` { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) ) = ( ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) + ( P ^ ( K - 1 ) ) ) )
110 hashcl 
 |-  ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } e. Fin -> ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) e. NN0 )
111 22 110 ax-mp 
 |-  ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) e. NN0
112 111 nn0cni 
 |-  ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) e. CC
113 addcom 
 |-  ( ( ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) e. CC /\ ( P ^ ( K - 1 ) ) e. CC ) -> ( ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) + ( P ^ ( K - 1 ) ) ) = ( ( P ^ ( K - 1 ) ) + ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) ) )
114 112 10 113 sylancr 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) + ( P ^ ( K - 1 ) ) ) = ( ( P ^ ( K - 1 ) ) + ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) ) )
115 109 114 eqtrd 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) + ( # ` { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) ) = ( ( P ^ ( K - 1 ) ) + ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) ) )
116 57 72 115 3eqtr3rd 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( ( P ^ ( K - 1 ) ) + ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) ) = ( ( P ^ ( K - 1 ) ) x. P ) )
117 10 12 mulcld 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( ( P ^ ( K - 1 ) ) x. P ) e. CC )
118 112 a1i 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) e. CC )
119 117 10 118 subaddd 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( ( ( ( P ^ ( K - 1 ) ) x. P ) - ( P ^ ( K - 1 ) ) ) = ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) <-> ( ( P ^ ( K - 1 ) ) + ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) ) = ( ( P ^ ( K - 1 ) ) x. P ) ) )
120 116 119 mpbird 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( ( ( P ^ ( K - 1 ) ) x. P ) - ( P ^ ( K - 1 ) ) ) = ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) )
121 16 18 120 3eqtrrd 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( # ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) = ( ( P ^ ( K - 1 ) ) x. ( P - 1 ) ) )
122 6 121 eqtrd 
 |-  ( ( P e. Prime /\ K e. NN ) -> ( phi ` ( P ^ K ) ) = ( ( P ^ ( K - 1 ) ) x. ( P - 1 ) ) )