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 gcdcom ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ↑ 𝐾 ) ∈ ℤ ) → ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = ( ( 𝑃 ↑ 𝐾 ) gcd 𝑥 ) )
38 33 36 37 syl2anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = ( ( 𝑃 ↑ 𝐾 ) gcd 𝑥 ) )
39 38 eqeq1d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ↔ ( ( 𝑃 ↑ 𝐾 ) gcd 𝑥 ) = 1 ) )
40 coprm ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝑥 ↔ ( 𝑃 gcd 𝑥 ) = 1 ) )
41 40 adantlr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝑥 ↔ ( 𝑃 gcd 𝑥 ) = 1 ) )
42 32 39 41 3bitr4d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ↔ ¬ 𝑃 ∥ 𝑥 ) )
43 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
44 43 adantl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → 𝑥 ∈ ℂ )
45 44 subid1d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 − 0 ) = 𝑥 )
46 45 breq2d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑃 ∥ ( 𝑥 − 0 ) ↔ 𝑃 ∥ 𝑥 ) )
47 46 notbid ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ¬ 𝑃 ∥ ( 𝑥 − 0 ) ↔ ¬ 𝑃 ∥ 𝑥 ) )
48 42 47 bitr4d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ↔ ¬ 𝑃 ∥ ( 𝑥 − 0 ) ) )
49 27 48 sylan2 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ) → ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ↔ ¬ 𝑃 ∥ ( 𝑥 − 0 ) ) )
50 49 biimpd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ) → ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 → ¬ 𝑃 ∥ ( 𝑥 − 0 ) ) )
51 imnan ⊢ ( ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 → ¬ 𝑃 ∥ ( 𝑥 − 0 ) ) ↔ ¬ ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∧ 𝑃 ∥ ( 𝑥 − 0 ) ) )
52 50 51 sylib ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ) → ¬ ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∧ 𝑃 ∥ ( 𝑥 − 0 ) ) )
53 52 ralrimiva ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ∀ 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ¬ ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∧ 𝑃 ∥ ( 𝑥 − 0 ) ) )
54 rabeq0 ⊢ ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∧ 𝑃 ∥ ( 𝑥 − 0 ) ) } = ∅ ↔ ∀ 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ¬ ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∧ 𝑃 ∥ ( 𝑥 − 0 ) ) )
55 53 54 sylibr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∧ 𝑃 ∥ ( 𝑥 − 0 ) ) } = ∅ )
56 26 55 syl5eq ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∩ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) = ∅ )
57 hashun ⊢ ( ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∈ Fin ∧ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ∈ Fin ∧ ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∩ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) = ∅ ) → ( ♯ ‘ ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∪ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) ) = ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) + ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) ) )
58 22 25 56 57 mp3an12i ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ♯ ‘ ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∪ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) ) = ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) + ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) ) )
59 49 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 unrab ⊢ ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∪ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) = { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 ∨ 𝑃 ∥ ( 𝑥 − 0 ) ) }
66 64 65 syl6reqr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∪ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) = ( 1 ... ( 𝑃 ↑ 𝐾 ) ) )
67 66 fveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ♯ ‘ ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∪ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) ) = ( ♯ ‘ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ) )
68 4 nnnn0d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ↑ 𝐾 ) ∈ ℕ0 )
69 hashfz1 ⊢ ( ( 𝑃 ↑ 𝐾 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ) = ( 𝑃 ↑ 𝐾 ) )
70 68 69 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ♯ ‘ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ) = ( 𝑃 ↑ 𝐾 ) )
71 expm1t ⊢ ( ( 𝑃 ∈ ℂ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ↑ 𝐾 ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) )
72 11 71 sylan ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ↑ 𝐾 ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) )
73 67 70 72 3eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ♯ ‘ ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∪ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) )
74 1 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → 𝑃 ∈ ℕ )
75 1zzd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → 1 ∈ ℤ )
76 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
77 1m1e0 ⊢ ( 1 − 1 ) = 0
78 77 fveq2i ⊢ ( ℤ≥ ‘ ( 1 − 1 ) ) = ( ℤ≥ ‘ 0 )
79 76 78 eqtr4i ⊢ ℕ0 = ( ℤ≥ ‘ ( 1 − 1 ) )
80 68 79 eleqtrdi ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ↑ 𝐾 ) ∈ ( ℤ≥ ‘ ( 1 − 1 ) ) )
81 0zd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → 0 ∈ ℤ )
82 74 75 80 81 hashdvds ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) = ( ( ⌊ ‘ ( ( ( 𝑃 ↑ 𝐾 ) − 0 ) / 𝑃 ) ) − ( ⌊ ‘ ( ( ( 1 − 1 ) − 0 ) / 𝑃 ) ) ) )
83 4 nncnd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ↑ 𝐾 ) ∈ ℂ )
84 83 subid1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( 𝑃 ↑ 𝐾 ) − 0 ) = ( 𝑃 ↑ 𝐾 ) )
85 84 oveq1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( ( 𝑃 ↑ 𝐾 ) − 0 ) / 𝑃 ) = ( ( 𝑃 ↑ 𝐾 ) / 𝑃 ) )
86 74 nnne0d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → 𝑃 ≠ 0 )
87 nnz ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℤ )
88 87 adantl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → 𝐾 ∈ ℤ )
89 12 86 88 expm1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ↑ ( 𝐾 − 1 ) ) = ( ( 𝑃 ↑ 𝐾 ) / 𝑃 ) )
90 85 89 eqtr4d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( ( 𝑃 ↑ 𝐾 ) − 0 ) / 𝑃 ) = ( 𝑃 ↑ ( 𝐾 − 1 ) ) )
91 90 fveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ⌊ ‘ ( ( ( 𝑃 ↑ 𝐾 ) − 0 ) / 𝑃 ) ) = ( ⌊ ‘ ( 𝑃 ↑ ( 𝐾 − 1 ) ) ) )
92 9 nnzd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 𝑃 ↑ ( 𝐾 − 1 ) ) ∈ ℤ )
93 flid ⊢ ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) ∈ ℤ → ( ⌊ ‘ ( 𝑃 ↑ ( 𝐾 − 1 ) ) ) = ( 𝑃 ↑ ( 𝐾 − 1 ) ) )
94 92 93 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ⌊ ‘ ( 𝑃 ↑ ( 𝐾 − 1 ) ) ) = ( 𝑃 ↑ ( 𝐾 − 1 ) ) )
95 91 94 eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ⌊ ‘ ( ( ( 𝑃 ↑ 𝐾 ) − 0 ) / 𝑃 ) ) = ( 𝑃 ↑ ( 𝐾 − 1 ) ) )
96 77 oveq1i ⊢ ( ( 1 − 1 ) − 0 ) = ( 0 − 0 )
97 0m0e0 ⊢ ( 0 − 0 ) = 0
98 96 97 eqtri ⊢ ( ( 1 − 1 ) − 0 ) = 0
99 98 oveq1i ⊢ ( ( ( 1 − 1 ) − 0 ) / 𝑃 ) = ( 0 / 𝑃 )
100 12 86 div0d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( 0 / 𝑃 ) = 0 )
101 99 100 syl5eq ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( ( 1 − 1 ) − 0 ) / 𝑃 ) = 0 )
102 101 fveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ⌊ ‘ ( ( ( 1 − 1 ) − 0 ) / 𝑃 ) ) = ( ⌊ ‘ 0 ) )
103 0z ⊢ 0 ∈ ℤ
104 flid ⊢ ( 0 ∈ ℤ → ( ⌊ ‘ 0 ) = 0 )
105 103 104 ax-mp ⊢ ( ⌊ ‘ 0 ) = 0
106 102 105 syl6eq ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ⌊ ‘ ( ( ( 1 − 1 ) − 0 ) / 𝑃 ) ) = 0 )
107 95 106 oveq12d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( ⌊ ‘ ( ( ( 𝑃 ↑ 𝐾 ) − 0 ) / 𝑃 ) ) − ( ⌊ ‘ ( ( ( 1 − 1 ) − 0 ) / 𝑃 ) ) ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) − 0 ) )
108 10 subid1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) − 0 ) = ( 𝑃 ↑ ( 𝐾 − 1 ) ) )
109 82 107 108 3eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) = ( 𝑃 ↑ ( 𝐾 − 1 ) ) )
110 109 oveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) + ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) ) = ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) + ( 𝑃 ↑ ( 𝐾 − 1 ) ) ) )
111 hashcl ⊢ ( { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ∈ Fin → ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ∈ ℕ0 )
112 22 111 ax-mp ⊢ ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ∈ ℕ0
113 112 nn0cni ⊢ ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ∈ ℂ
114 addcom ⊢ ( ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ∈ ℂ ∧ ( 𝑃 ↑ ( 𝐾 − 1 ) ) ∈ ℂ ) → ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) + ( 𝑃 ↑ ( 𝐾 − 1 ) ) ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) + ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ) )
115 113 10 114 sylancr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) + ( 𝑃 ↑ ( 𝐾 − 1 ) ) ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) + ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ) )
116 110 115 eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) + ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ 𝑃 ∥ ( 𝑥 − 0 ) } ) ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) + ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ) )
117 58 73 116 3eqtr3rd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) + ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) )
118 10 12 mulcld ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) ∈ ℂ )
119 113 a1i ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ∈ ℂ )
120 118 10 119 subaddd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) − ( 𝑃 ↑ ( 𝐾 − 1 ) ) ) = ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ↔ ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) + ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) ) )
121 117 120 mpbird ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · 𝑃 ) − ( 𝑃 ↑ ( 𝐾 − 1 ) ) ) = ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) )
122 16 18 121 3eqtrrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( 𝑃 ↑ 𝐾 ) ) ∣ ( 𝑥 gcd ( 𝑃 ↑ 𝐾 ) ) = 1 } ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · ( 𝑃 − 1 ) ) )
123 6 122 eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ ) → ( ϕ ‘ ( 𝑃 ↑ 𝐾 ) ) = ( ( 𝑃 ↑ ( 𝐾 − 1 ) ) · ( 𝑃 − 1 ) ) )