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 ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ϕ ‘ ( 𝑃 ↑ 𝐾 ) ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · ( 𝑃 − 1 ) ) )

Proof

Step Hyp Ref Expression
1 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
2 nnnn0 ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℕ0 )
3 nnexpcl ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ) → ( 𝑃 ↑ 𝐾 ) ∈ ℕ )
4 1 2 3 syl2an ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ↑ 𝐾 ) ∈ ℕ )
5 phival ⊢ ( ( 𝑃 ↑ 𝐾 ) ∈ ℕ → ( ϕ ‘ ( 𝑃 ↑ 𝐾 ) ) = ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) )
6 4 5 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ϕ ‘ ( 𝑃 ↑ 𝐾 ) ) = ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) )
7 nnm1nn0 ⊢ ( 𝐾 ∈ ℕ → ( 𝐾 − 1 ) ∈ ℕ0 )
8 nnexpcl ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝐾 − 1 ) ∈ ℕ0 ) → ( 𝑃 ↑ ( 𝐾 − 1 ) ) ∈ ℕ )
9 1 7 8 syl2an ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ↑ ( 𝐾 − 1 ) ) ∈ ℕ )
10 9 nncnd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ↑ ( 𝐾 − 1 ) ) ∈ ℂ )
11 1 nncnd ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℂ )
12 11 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → 𝑃 ∈ ℂ )
13 ax-1cn ⊢ 1 ∈ ℂ
14 subdi ⊢ ( ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · ( 𝑃 − 1 ) ) = ( ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) − ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 1 ) ) )
15 13 14 mp3an3 ⊢ ( ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) ∈ ℂ ∧ 𝑃 ∈ ℂ ) → ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · ( 𝑃 − 1 ) ) = ( ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) − ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 1 ) ) )
16 10 12 15 syl2anc ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · ( 𝑃 − 1 ) ) = ( ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) − ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 1 ) ) )
17 10 mulid1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 1 ) = ( 𝑃 ↑ ( 𝐾 − 1 ) ) )
18 17 oveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) − ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 1 ) ) = ( ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) − ( 𝑃 ↑ ( 𝐾 − 1 ) ) ) )
19 fzfi ⊢ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∈ Fin
20 ssrab2 ⊢ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ⊆ ( 1 ... ( 𝑃 ↑ 𝐾 ) )
21 ssfi ⊢ ( ( ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∈ Fin ∧ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ⊆ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ) → { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∈ Fin )
22 19 20 21 mp2an ⊢ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∈ Fin
23 ssrab2 ⊢ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ⊆ ( 1 ... ( 𝑃 ↑ 𝐾 ) )
24 ssfi ⊢ ( ( ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∈ Fin ∧ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ⊆ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ) → { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ∈ Fin )
25 19 23 24 mp2an ⊢ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ∈ Fin
26 inrab ⊢ ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∩ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) = { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∧ 𝑃 ∥ ( 𝑥 − 0 ) ) }
27 elfzelz ⊢ ( 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) → 𝑥 ∈ ℤ )
28 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
29 rpexp ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝐾 ∈ ℕ ) → ( ( ( 𝑃 ↑ 𝐾 ) gcd 𝑥 ) = 1 ↔ ( 𝑃 gcd 𝑥 ) = 1 ) )
30 28 29 syl3an1 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ ∧ 𝐾 ∈ ℕ ) → ( ( ( 𝑃 ↑ 𝐾 ) gcd 𝑥 ) = 1 ↔ ( 𝑃 gcd 𝑥 ) = 1 ) )
31 30 3expa ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ ) ∧ 𝐾 ∈ ℕ ) → ( ( ( 𝑃 ↑ 𝐾 ) gcd 𝑥 ) = 1 ↔ ( 𝑃 gcd 𝑥 ) = 1 ) )
32 31 an32s ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑃 ↑ 𝐾 ) gcd 𝑥 ) = 1 ↔ ( 𝑃 gcd 𝑥 ) = 1 ) )
33 simpr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → 𝑥 ∈ ℤ )
34 zexpcl ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝐾 ∈ ℕ0 ) → ( 𝑃 ↑ 𝐾 ) ∈ ℤ )
35 28 2 34 syl2an ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ↑ 𝐾 ) ∈ ℤ )
36 35 adantr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑃 ↑ 𝐾 ) ∈ ℤ )
37 33 36 gcdcomd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = ( ( 𝑃 ↑ 𝐾 ) gcd 𝑥 ) )
38 37 eqeq1d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ↔ ( ( 𝑃 ↑ 𝐾 ) gcd 𝑥 ) = 1 ) )
39 coprm ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝑥 ↔ ( 𝑃 gcd 𝑥 ) = 1 ) )
40 39 adantlr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝑥 ↔ ( 𝑃 gcd 𝑥 ) = 1 ) )
41 32 38 40 3bitr4d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ↔ ¬ 𝑃 ∥ 𝑥 ) )
42 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
43 42 adantl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → 𝑥 ∈ ℂ )
44 43 subid1d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 − 0 ) = 𝑥 )
45 44 breq2d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑃 ∥ ( 𝑥 − 0 ) ↔ 𝑃 ∥ 𝑥 ) )
46 45 notbid ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ¬ 𝑃 ∥ ( 𝑥 − 0 ) ↔ ¬ 𝑃 ∥ 𝑥 ) )
47 41 46 bitr4d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ↔ ¬ 𝑃 ∥ ( 𝑥 − 0 ) ) )
48 27 47 sylan2 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ) → ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ↔ ¬ 𝑃 ∥ ( 𝑥 − 0 ) ) )
49 48 biimpd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ) → ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 → ¬ 𝑃 ∥ ( 𝑥 − 0 ) ) )
50 imnan ⊢ ( ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 → ¬ 𝑃 ∥ ( 𝑥 − 0 ) ) ↔ ¬ ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∧ 𝑃 ∥ ( 𝑥 − 0 ) ) )
51 49 50 sylib ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ) → ¬ ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∧ 𝑃 ∥ ( 𝑥 − 0 ) ) )
52 51 ralrimiva ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ∀ 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ¬ ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∧ 𝑃 ∥ ( 𝑥 − 0 ) ) )
53 rabeq0 ⊢ ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∧ 𝑃 ∥ ( 𝑥 − 0 ) ) } = ∅ ↔ ∀ 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ¬ ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∧ 𝑃 ∥ ( 𝑥 − 0 ) ) )
54 52 53 sylibr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∧ 𝑃 ∥ ( 𝑥 − 0 ) ) } = ∅ )
55 26 54 syl5eq ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∩ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) = ∅ )
56 hashun ⊢ ( ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∈ Fin ∧ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ∈ Fin ∧ ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∩ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) = ∅ ) → ( ♯ ‘ ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∪ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) ) = ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) + ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) ) )
57 22 25 55 56 mp3an12i ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ♯ ‘ ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∪ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) ) = ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) + ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) ) )
58 unrab ⊢ ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∪ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) = { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∨ 𝑃 ∥ ( 𝑥 − 0 ) ) }
59 48 biimprd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ) → ( ¬ 𝑃 ∥ ( 𝑥 − 0 ) → ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ) )
60 59 con1d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ) → ( ¬ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 → 𝑃 ∥ ( 𝑥 − 0 ) ) )
61 60 orrd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ) → ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∨ 𝑃 ∥ ( 𝑥 − 0 ) ) )
62 61 ralrimiva ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ∀ 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∨ 𝑃 ∥ ( 𝑥 − 0 ) ) )
63 rabid2 ⊢ ( ( 1 ... ( 𝑃 ↑ 𝐾 ) ) = { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∨ 𝑃 ∥ ( 𝑥 − 0 ) ) } ↔ ∀ 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∨ 𝑃 ∥ ( 𝑥 − 0 ) ) )
64 62 63 sylibr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 1 ... ( 𝑃 ↑ 𝐾 ) ) = { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∨ 𝑃 ∥ ( 𝑥 − 0 ) ) } )
65 58 64 eqtr4id ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∪ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) = ( 1 ... ( 𝑃 ↑ 𝐾 ) ) )
66 65 fveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ♯ ‘ ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∪ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) ) = ( ♯ ‘ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ) )
67 4 nnnn0d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ↑ 𝐾 ) ∈ ℕ0 )
68 hashfz1 ⊢ ( ( 𝑃 ↑ 𝐾 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ) = ( 𝑃 ↑ 𝐾 ) )
69 67 68 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ♯ ‘ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ) = ( 𝑃 ↑ 𝐾 ) )
70 expm1t ⊢ ( ( 𝑃 ∈ ℂ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ↑ 𝐾 ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) )
71 11 70 sylan ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ↑ 𝐾 ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) )
72 66 69 71 3eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ♯ ‘ ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∪ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) )
73 1 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → 𝑃 ∈ ℕ )
74 1zzd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → 1 ∈ ℤ )
75 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
76 1m1e0 ⊢ ( 1 − 1 ) = 0
77 76 fveq2i ⊢ ( ℤ≥ ‘ ( 1 − 1 ) ) = ( ℤ≥ ‘ 0 )
78 75 77 eqtr4i ⊢ ℕ0 = ( ℤ≥ ‘ ( 1 − 1 ) )
79 67 78 eleqtrdi ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ↑ 𝐾 ) ∈ ( ℤ≥ ‘ ( 1 − 1 ) ) )
80 0zd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → 0 ∈ ℤ )
81 73 74 79 80 hashdvds ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) = ( ( ⌊ ‘ ( ( ( 𝑃 ↑ 𝐾 ) − 0 ) / 𝑃 ) ) − ( ⌊ ‘ ( ( ( 1 − 1 ) − 0 ) / 𝑃 ) ) ) )
82 4 nncnd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ↑ 𝐾 ) ∈ ℂ )
83 82 subid1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( 𝑃 ↑ 𝐾 ) − 0 ) = ( 𝑃 ↑ 𝐾 ) )
84 83 oveq1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( ( 𝑃 ↑ 𝐾 ) − 0 ) / 𝑃 ) = ( ( 𝑃 ↑ 𝐾 ) / 𝑃 ) )
85 73 nnne0d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → 𝑃 ≠ 0 )
86 nnz ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℤ )
87 86 adantl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → 𝐾 ∈ ℤ )
88 12 85 87 expm1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ↑ ( 𝐾 − 1 ) ) = ( ( 𝑃 ↑ 𝐾 ) / 𝑃 ) )
89 84 88 eqtr4d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( ( 𝑃 ↑ 𝐾 ) − 0 ) / 𝑃 ) = ( 𝑃 ↑ ( 𝐾 − 1 ) ) )
90 89 fveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ⌊ ‘ ( ( ( 𝑃 ↑ 𝐾 ) − 0 ) / 𝑃 ) ) = ( ⌊ ‘ ( 𝑃 ↑ ( 𝐾 − 1 ) ) ) )
91 9 nnzd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ↑ ( 𝐾 − 1 ) ) ∈ ℤ )
92 flid ⊢ ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) ∈ ℤ → ( ⌊ ‘ ( 𝑃 ↑ ( 𝐾 − 1 ) ) ) = ( 𝑃 ↑ ( 𝐾 − 1 ) ) )
93 91 92 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ⌊ ‘ ( 𝑃 ↑ ( 𝐾 − 1 ) ) ) = ( 𝑃 ↑ ( 𝐾 − 1 ) ) )
94 90 93 eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ⌊ ‘ ( ( ( 𝑃 ↑ 𝐾 ) − 0 ) / 𝑃 ) ) = ( 𝑃 ↑ ( 𝐾 − 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 ) / 𝑃 ) = ( 0 / 𝑃 )
99 12 85 div0d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 0 / 𝑃 ) = 0 )
100 98 99 syl5eq ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( ( 1 − 1 ) − 0 ) / 𝑃 ) = 0 )
101 100 fveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ⌊ ‘ ( ( ( 1 − 1 ) − 0 ) / 𝑃 ) ) = ( ⌊ ‘ 0 ) )
102 0z ⊢ 0 ∈ ℤ
103 flid ⊢ ( 0 ∈ ℤ → ( ⌊ ‘ 0 ) = 0 )
104 102 103 ax-mp ⊢ ( ⌊ ‘ 0 ) = 0
105 101 104 eqtrdi ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ⌊ ‘ ( ( ( 1 − 1 ) − 0 ) / 𝑃 ) ) = 0 )
106 94 105 oveq12d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( ⌊ ‘ ( ( ( 𝑃 ↑ 𝐾 ) − 0 ) / 𝑃 ) ) − ( ⌊ ‘ ( ( ( 1 − 1 ) − 0 ) / 𝑃 ) ) ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) − 0 ) )
107 10 subid1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) − 0 ) = ( 𝑃 ↑ ( 𝐾 − 1 ) ) )
108 81 106 107 3eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) = ( 𝑃 ↑ ( 𝐾 − 1 ) ) )
109 108 oveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) + ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) ) = ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) + ( 𝑃 ↑ ( 𝐾 − 1 ) ) ) )
110 hashcl ⊢ ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∈ Fin → ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ∈ ℕ0 )
111 22 110 ax-mp ⊢ ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ∈ ℕ0
112 111 nn0cni ⊢ ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ∈ ℂ
113 addcom ⊢ ( ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ∈ ℂ ∧ ( 𝑃 ↑ ( 𝐾 − 1 ) ) ∈ ℂ ) → ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) + ( 𝑃 ↑ ( 𝐾 − 1 ) ) ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) + ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ) )
114 112 10 113 sylancr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) + ( 𝑃 ↑ ( 𝐾 − 1 ) ) ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) + ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ) )
115 109 114 eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) + ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) + ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ) )
116 57 72 115 3eqtr3rd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) + ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) )
117 10 12 mulcld ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) ∈ ℂ )
118 112 a1i ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ∈ ℂ )
119 117 10 118 subaddd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) − ( 𝑃 ↑ ( 𝐾 − 1 ) ) ) = ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ↔ ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) + ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) ) )
120 116 119 mpbird ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) − ( 𝑃 ↑ ( 𝐾 − 1 ) ) ) = ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) )
121 16 18 120 3eqtrrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · ( 𝑃 − 1 ) ) )
122 6 121 eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ϕ ‘ ( 𝑃 ↑ 𝐾 ) ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · ( 𝑃 − 1 ) ) )