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 PKϕPK=PK1P1

Proof

Step Hyp Ref Expression
1 prmnn PP
2 nnnn0 KK0
3 nnexpcl PK0PK
4 1 2 3 syl2an PKPK
5 phival PKϕPK=x1PK|xgcdPK=1
6 4 5 syl PKϕPK=x1PK|xgcdPK=1
7 nnm1nn0 KK10
8 nnexpcl PK10PK1
9 1 7 8 syl2an PKPK1
10 9 nncnd PKPK1
11 1 nncnd PP
12 11 adantr PKP
13 ax-1cn 1
14 subdi PK1P1PK1P1=PK1PPK11
15 13 14 mp3an3 PK1PPK1P1=PK1PPK11
16 10 12 15 syl2anc PKPK1P1=PK1PPK11
17 10 mulid1d PKPK11=PK1
18 17 oveq2d PKPK1PPK11=PK1PPK1
19 fzfi 1PKFin
20 ssrab2 x1PK|xgcdPK=11PK
21 ssfi 1PKFinx1PK|xgcdPK=11PKx1PK|xgcdPK=1Fin
22 19 20 21 mp2an x1PK|xgcdPK=1Fin
23 ssrab2 x1PK|Px01PK
24 ssfi 1PKFinx1PK|Px01PKx1PK|Px0Fin
25 19 23 24 mp2an x1PK|Px0Fin
26 inrab x1PK|xgcdPK=1x1PK|Px0=x1PK|xgcdPK=1Px0
27 elfzelz x1PKx
28 prmz PP
29 rpexp PxKPKgcdx=1Pgcdx=1
30 28 29 syl3an1 PxKPKgcdx=1Pgcdx=1
31 30 3expa PxKPKgcdx=1Pgcdx=1
32 31 an32s PKxPKgcdx=1Pgcdx=1
33 simpr PKxx
34 zexpcl PK0PK
35 28 2 34 syl2an PKPK
36 35 adantr PKxPK
37 33 36 gcdcomd PKxxgcdPK=PKgcdx
38 37 eqeq1d PKxxgcdPK=1PKgcdx=1
39 coprm Px¬PxPgcdx=1
40 39 adantlr PKx¬PxPgcdx=1
41 32 38 40 3bitr4d PKxxgcdPK=1¬Px
42 zcn xx
43 42 adantl PKxx
44 43 subid1d PKxx0=x
45 44 breq2d PKxPx0Px
46 45 notbid PKx¬Px0¬Px
47 41 46 bitr4d PKxxgcdPK=1¬Px0
48 27 47 sylan2 PKx1PKxgcdPK=1¬Px0
49 48 biimpd PKx1PKxgcdPK=1¬Px0
50 imnan xgcdPK=1¬Px0¬xgcdPK=1Px0
51 49 50 sylib PKx1PK¬xgcdPK=1Px0
52 51 ralrimiva PKx1PK¬xgcdPK=1Px0
53 rabeq0 x1PK|xgcdPK=1Px0=x1PK¬xgcdPK=1Px0
54 52 53 sylibr PKx1PK|xgcdPK=1Px0=
55 26 54 eqtrid PKx1PK|xgcdPK=1x1PK|Px0=
56 hashun x1PK|xgcdPK=1Finx1PK|Px0Finx1PK|xgcdPK=1x1PK|Px0=x1PK|xgcdPK=1x1PK|Px0=x1PK|xgcdPK=1+x1PK|Px0
57 22 25 55 56 mp3an12i PKx1PK|xgcdPK=1x1PK|Px0=x1PK|xgcdPK=1+x1PK|Px0
58 unrab x1PK|xgcdPK=1x1PK|Px0=x1PK|xgcdPK=1Px0
59 48 biimprd PKx1PK¬Px0xgcdPK=1
60 59 con1d PKx1PK¬xgcdPK=1Px0
61 60 orrd PKx1PKxgcdPK=1Px0
62 61 ralrimiva PKx1PKxgcdPK=1Px0
63 rabid2 1PK=x1PK|xgcdPK=1Px0x1PKxgcdPK=1Px0
64 62 63 sylibr PK1PK=x1PK|xgcdPK=1Px0
65 58 64 eqtr4id PKx1PK|xgcdPK=1x1PK|Px0=1PK
66 65 fveq2d PKx1PK|xgcdPK=1x1PK|Px0=1PK
67 4 nnnn0d PKPK0
68 hashfz1 PK01PK=PK
69 67 68 syl PK1PK=PK
70 expm1t PKPK=PK1P
71 11 70 sylan PKPK=PK1P
72 66 69 71 3eqtrd PKx1PK|xgcdPK=1x1PK|Px0=PK1P
73 1 adantr PKP
74 1zzd PK1
75 nn0uz 0=0
76 1m1e0 11=0
77 76 fveq2i 11=0
78 75 77 eqtr4i 0=11
79 67 78 eleqtrdi PKPK11
80 0zd PK0
81 73 74 79 80 hashdvds PKx1PK|Px0=PK0P1-1-0P
82 4 nncnd PKPK
83 82 subid1d PKPK0=PK
84 83 oveq1d PKPK0P=PKP
85 73 nnne0d PKP0
86 nnz KK
87 86 adantl PKK
88 12 85 87 expm1d PKPK1=PKP
89 84 88 eqtr4d PKPK0P=PK1
90 89 fveq2d PKPK0P=PK1
91 9 nnzd PKPK1
92 flid PK1PK1=PK1
93 91 92 syl PKPK1=PK1
94 90 93 eqtrd PKPK0P=PK1
95 76 oveq1i 1-1-0=00
96 0m0e0 00=0
97 95 96 eqtri 1-1-0=0
98 97 oveq1i 1-1-0P=0P
99 12 85 div0d PK0P=0
100 98 99 eqtrid PK1-1-0P=0
101 100 fveq2d PK1-1-0P=0
102 0z 0
103 flid 00=0
104 102 103 ax-mp 0=0
105 101 104 eqtrdi PK1-1-0P=0
106 94 105 oveq12d PKPK0P1-1-0P=PK10
107 10 subid1d PKPK10=PK1
108 81 106 107 3eqtrd PKx1PK|Px0=PK1
109 108 oveq2d PKx1PK|xgcdPK=1+x1PK|Px0=x1PK|xgcdPK=1+PK1
110 hashcl x1PK|xgcdPK=1Finx1PK|xgcdPK=10
111 22 110 ax-mp x1PK|xgcdPK=10
112 111 nn0cni x1PK|xgcdPK=1
113 addcom x1PK|xgcdPK=1PK1x1PK|xgcdPK=1+PK1=PK1+x1PK|xgcdPK=1
114 112 10 113 sylancr PKx1PK|xgcdPK=1+PK1=PK1+x1PK|xgcdPK=1
115 109 114 eqtrd PKx1PK|xgcdPK=1+x1PK|Px0=PK1+x1PK|xgcdPK=1
116 57 72 115 3eqtr3rd PKPK1+x1PK|xgcdPK=1=PK1P
117 10 12 mulcld PKPK1P
118 112 a1i PKx1PK|xgcdPK=1
119 117 10 118 subaddd PKPK1PPK1=x1PK|xgcdPK=1PK1+x1PK|xgcdPK=1=PK1P
120 116 119 mpbird PKPK1PPK1=x1PK|xgcdPK=1
121 16 18 120 3eqtrrd PKx1PK|xgcdPK=1=PK1P1
122 6 121 eqtrd PKϕPK=PK1P1