Step | Hyp | Ref
| Expression |
1 | | prmnn 16008 |
. . . 4
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
2 | | nnnn0 11892 |
. . . 4
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℕ0) |
3 | | nnexpcl 13438 |
. . . 4
⊢ ((𝑃 ∈ ℕ ∧ 𝐾 ∈ ℕ0)
→ (𝑃↑𝐾) ∈
ℕ) |
4 | 1, 2, 3 | syl2an 598 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℕ) |
5 | | phival 16094 |
. . 3
⊢ ((𝑃↑𝐾) ∈ ℕ → (ϕ‘(𝑃↑𝐾)) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) |
6 | 4, 5 | syl 17 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(ϕ‘(𝑃↑𝐾)) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) |
7 | | nnm1nn0 11926 |
. . . . . 6
⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈
ℕ0) |
8 | | nnexpcl 13438 |
. . . . . 6
⊢ ((𝑃 ∈ ℕ ∧ (𝐾 − 1) ∈
ℕ0) → (𝑃↑(𝐾 − 1)) ∈
ℕ) |
9 | 1, 7, 8 | syl2an 598 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) ∈
ℕ) |
10 | 9 | nncnd 11641 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) ∈
ℂ) |
11 | 1 | nncnd 11641 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℂ) |
12 | 11 | adantr 484 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝑃 ∈
ℂ) |
13 | | ax-1cn 10584 |
. . . . 5
⊢ 1 ∈
ℂ |
14 | | subdi 11062 |
. . . . 5
⊢ (((𝑃↑(𝐾 − 1)) ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1))) |
15 | 13, 14 | mp3an3 1447 |
. . . 4
⊢ (((𝑃↑(𝐾 − 1)) ∈ ℂ ∧ 𝑃 ∈ ℂ) → ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1))) |
16 | 10, 12, 15 | syl2anc 587 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1))) |
17 | 10 | mulid1d 10647 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) · 1) = (𝑃↑(𝐾 − 1))) |
18 | 17 | oveq2d 7151 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − (𝑃↑(𝐾 − 1)))) |
19 | | fzfi 13335 |
. . . . . . 7
⊢
(1...(𝑃↑𝐾)) ∈ Fin |
20 | | ssrab2 4007 |
. . . . . . 7
⊢ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ⊆ (1...(𝑃↑𝐾)) |
21 | | ssfi 8722 |
. . . . . . 7
⊢
(((1...(𝑃↑𝐾)) ∈ Fin ∧ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ⊆ (1...(𝑃↑𝐾))) → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin) |
22 | 19, 20, 21 | mp2an 691 |
. . . . . 6
⊢ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin |
23 | | ssrab2 4007 |
. . . . . . 7
⊢ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ⊆ (1...(𝑃↑𝐾)) |
24 | | ssfi 8722 |
. . . . . . 7
⊢
(((1...(𝑃↑𝐾)) ∈ Fin ∧ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ⊆ (1...(𝑃↑𝐾))) → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ∈ Fin) |
25 | 19, 23, 24 | mp2an 691 |
. . . . . 6
⊢ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ∈ Fin |
26 | | inrab 4227 |
. . . . . . 7
⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∩ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))} |
27 | | elfzelz 12902 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1...(𝑃↑𝐾)) → 𝑥 ∈ ℤ) |
28 | | prmz 16009 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
29 | | rpexp 16054 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1)) |
30 | 28, 29 | syl3an1 1160 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1)) |
31 | 30 | 3expa 1115 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ) ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1)) |
32 | 31 | an32s 651 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1)) |
33 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈
ℤ) |
34 | | zexpcl 13440 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℤ ∧ 𝐾 ∈ ℕ0)
→ (𝑃↑𝐾) ∈
ℤ) |
35 | 28, 2, 34 | syl2an 598 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℤ) |
36 | 35 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑃↑𝐾) ∈ ℤ) |
37 | | gcdcom 15852 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ (𝑃↑𝐾) ∈ ℤ) → (𝑥 gcd (𝑃↑𝐾)) = ((𝑃↑𝐾) gcd 𝑥)) |
38 | 33, 36, 37 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑥 gcd (𝑃↑𝐾)) = ((𝑃↑𝐾) gcd 𝑥)) |
39 | 38 | eqeq1d 2800 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ((𝑃↑𝐾) gcd 𝑥) = 1)) |
40 | | coprm 16045 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ) → (¬
𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1)) |
41 | 40 | adantlr 714 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (¬
𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1)) |
42 | 32, 39, 41 | 3bitr4d 314 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ¬ 𝑃 ∥ 𝑥)) |
43 | | zcn 11974 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
44 | 43 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈
ℂ) |
45 | 44 | subid1d 10975 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑥 − 0) = 𝑥) |
46 | 45 | breq2d 5042 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑃 ∥ (𝑥 − 0) ↔ 𝑃 ∥ 𝑥)) |
47 | 46 | notbid 321 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (¬
𝑃 ∥ (𝑥 − 0) ↔ ¬ 𝑃 ∥ 𝑥)) |
48 | 42, 47 | bitr4d 285 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ¬ 𝑃 ∥ (𝑥 − 0))) |
49 | 27, 48 | sylan2 595 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ¬ 𝑃 ∥ (𝑥 − 0))) |
50 | 49 | biimpd 232 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ((𝑥 gcd (𝑃↑𝐾)) = 1 → ¬ 𝑃 ∥ (𝑥 − 0))) |
51 | | imnan 403 |
. . . . . . . . . 10
⊢ (((𝑥 gcd (𝑃↑𝐾)) = 1 → ¬ 𝑃 ∥ (𝑥 − 0)) ↔ ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))) |
52 | 50, 51 | sylib 221 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))) |
53 | 52 | ralrimiva 3149 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
∀𝑥 ∈
(1...(𝑃↑𝐾)) ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))) |
54 | | rabeq0 4292 |
. . . . . . . 8
⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))} = ∅ ↔ ∀𝑥 ∈ (1...(𝑃↑𝐾)) ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))) |
55 | 53, 54 | sylibr 237 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))} = ∅) |
56 | 26, 55 | syl5eq 2845 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∩ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = ∅) |
57 | | hashun 13739 |
. . . . . 6
⊢ (({𝑥 ∈ (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 1462 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘({𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}))) |
59 | | unrab 4226 |
. . . . . . . 8
⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))} |
60 | 49 | biimprd 251 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (¬ 𝑃 ∥ (𝑥 − 0) → (𝑥 gcd (𝑃↑𝐾)) = 1)) |
61 | 60 | con1d 147 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (¬ (𝑥 gcd (𝑃↑𝐾)) = 1 → 𝑃 ∥ (𝑥 − 0))) |
62 | 61 | orrd 860 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))) |
63 | 62 | ralrimiva 3149 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
∀𝑥 ∈
(1...(𝑃↑𝐾))((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))) |
64 | | rabid2 3334 |
. . . . . . . . 9
⊢
((1...(𝑃↑𝐾)) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))} ↔ ∀𝑥 ∈ (1...(𝑃↑𝐾))((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))) |
65 | 63, 64 | sylibr 237 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(1...(𝑃↑𝐾)) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))}) |
66 | 59, 65 | eqtr4id 2852 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = (1...(𝑃↑𝐾))) |
67 | 66 | fveq2d 6649 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘({𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = (♯‘(1...(𝑃↑𝐾)))) |
68 | 4 | nnnn0d 11943 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈
ℕ0) |
69 | | hashfz1 13702 |
. . . . . . 7
⊢ ((𝑃↑𝐾) ∈ ℕ0 →
(♯‘(1...(𝑃↑𝐾))) = (𝑃↑𝐾)) |
70 | 68, 69 | syl 17 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘(1...(𝑃↑𝐾))) = (𝑃↑𝐾)) |
71 | | expm1t 13453 |
. . . . . . 7
⊢ ((𝑃 ∈ ℂ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) = ((𝑃↑(𝐾 − 1)) · 𝑃)) |
72 | 11, 71 | sylan 583 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) = ((𝑃↑(𝐾 − 1)) · 𝑃)) |
73 | 67, 70, 72 | 3eqtrd 2837 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘({𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((𝑃↑(𝐾 − 1)) · 𝑃)) |
74 | 1 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝑃 ∈
ℕ) |
75 | | 1zzd 12001 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 1 ∈
ℤ) |
76 | | nn0uz 12268 |
. . . . . . . . . . 11
⊢
ℕ0 = (ℤ≥‘0) |
77 | | 1m1e0 11697 |
. . . . . . . . . . . 12
⊢ (1
− 1) = 0 |
78 | 77 | fveq2i 6648 |
. . . . . . . . . . 11
⊢
(ℤ≥‘(1 − 1)) =
(ℤ≥‘0) |
79 | 76, 78 | eqtr4i 2824 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘(1 −
1)) |
80 | 68, 79 | eleqtrdi 2900 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ (ℤ≥‘(1
− 1))) |
81 | | 0zd 11981 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 0 ∈
ℤ) |
82 | 74, 75, 80, 81 | hashdvds 16102 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = ((⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) − (⌊‘(((1 − 1)
− 0) / 𝑃)))) |
83 | 4 | nncnd 11641 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℂ) |
84 | 83 | subid1d 10975 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑𝐾) − 0) = (𝑃↑𝐾)) |
85 | 84 | oveq1d 7150 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) − 0) / 𝑃) = ((𝑃↑𝐾) / 𝑃)) |
86 | 74 | nnne0d 11675 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝑃 ≠ 0) |
87 | | nnz 11992 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℤ) |
88 | 87 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝐾 ∈
ℤ) |
89 | 12, 86, 88 | expm1d 13516 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) = ((𝑃↑𝐾) / 𝑃)) |
90 | 85, 89 | eqtr4d 2836 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) − 0) / 𝑃) = (𝑃↑(𝐾 − 1))) |
91 | 90 | fveq2d 6649 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) = (⌊‘(𝑃↑(𝐾 − 1)))) |
92 | 9 | nnzd 12074 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) ∈
ℤ) |
93 | | flid 13173 |
. . . . . . . . . . 11
⊢ ((𝑃↑(𝐾 − 1)) ∈ ℤ →
(⌊‘(𝑃↑(𝐾 − 1))) = (𝑃↑(𝐾 − 1))) |
94 | 92, 93 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(𝑃↑(𝐾 − 1))) = (𝑃↑(𝐾 − 1))) |
95 | 91, 94 | eqtrd 2833 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) = (𝑃↑(𝐾 − 1))) |
96 | 77 | oveq1i 7145 |
. . . . . . . . . . . . . 14
⊢ ((1
− 1) − 0) = (0 − 0) |
97 | | 0m0e0 11745 |
. . . . . . . . . . . . . 14
⊢ (0
− 0) = 0 |
98 | 96, 97 | eqtri 2821 |
. . . . . . . . . . . . 13
⊢ ((1
− 1) − 0) = 0 |
99 | 98 | oveq1i 7145 |
. . . . . . . . . . . 12
⊢ (((1
− 1) − 0) / 𝑃)
= (0 / 𝑃) |
100 | 12, 86 | div0d 11404 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (0 /
𝑃) = 0) |
101 | 99, 100 | syl5eq 2845 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((1
− 1) − 0) / 𝑃)
= 0) |
102 | 101 | fveq2d 6649 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(((1 − 1) − 0) / 𝑃)) = (⌊‘0)) |
103 | | 0z 11980 |
. . . . . . . . . . 11
⊢ 0 ∈
ℤ |
104 | | flid 13173 |
. . . . . . . . . . 11
⊢ (0 ∈
ℤ → (⌊‘0) = 0) |
105 | 103, 104 | ax-mp 5 |
. . . . . . . . . 10
⊢
(⌊‘0) = 0 |
106 | 102, 105 | eqtrdi 2849 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(((1 − 1) − 0) / 𝑃)) = 0) |
107 | 95, 106 | oveq12d 7153 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
((⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) − (⌊‘(((1 − 1)
− 0) / 𝑃))) = ((𝑃↑(𝐾 − 1)) − 0)) |
108 | 10 | subid1d 10975 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) − 0) = (𝑃↑(𝐾 − 1))) |
109 | 82, 107, 108 | 3eqtrd 2837 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = (𝑃↑(𝐾 − 1))) |
110 | 109 | oveq2d 7151 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
((♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (𝑃↑(𝐾 − 1)))) |
111 | | hashcl 13713 |
. . . . . . . . 9
⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin →
(♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈
ℕ0) |
112 | 22, 111 | ax-mp 5 |
. . . . . . . 8
⊢
(♯‘{𝑥
∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈
ℕ0 |
113 | 112 | nn0cni 11897 |
. . . . . . 7
⊢
(♯‘{𝑥
∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈ ℂ |
114 | | addcom 10815 |
. . . . . . 7
⊢
(((♯‘{𝑥
∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈ ℂ ∧ (𝑃↑(𝐾 − 1)) ∈ ℂ) →
((♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (𝑃↑(𝐾 − 1))) = ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}))) |
115 | 113, 10, 114 | sylancr 590 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
((♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (𝑃↑(𝐾 − 1))) = ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}))) |
116 | 110, 115 | eqtrd 2833 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
((♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}))) |
117 | 58, 73, 116 | 3eqtr3rd 2842 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) = ((𝑃↑(𝐾 − 1)) · 𝑃)) |
118 | 10, 12 | mulcld 10650 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) · 𝑃) ∈ ℂ) |
119 | 113 | a1i 11 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈ ℂ) |
120 | 118, 10, 119 | subaddd 11004 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
((((𝑃↑(𝐾 − 1)) · 𝑃) − (𝑃↑(𝐾 − 1))) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ↔ ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) = ((𝑃↑(𝐾 − 1)) · 𝑃))) |
121 | 117, 120 | mpbird 260 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑(𝐾 − 1)) · 𝑃) − (𝑃↑(𝐾 − 1))) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) |
122 | 16, 18, 121 | 3eqtrrd 2838 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) = ((𝑃↑(𝐾 − 1)) · (𝑃 − 1))) |
123 | 6, 122 | eqtrd 2833 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(ϕ‘(𝑃↑𝐾)) = ((𝑃↑(𝐾 − 1)) · (𝑃 − 1))) |