Step | Hyp | Ref
| Expression |
1 | | prmnn 16020 |
. . . 4
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
2 | | nnnn0 11907 |
. . . 4
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℕ0) |
3 | | nnexpcl 13445 |
. . . 4
⊢ ((𝑃 ∈ ℕ ∧ 𝐾 ∈ ℕ0)
→ (𝑃↑𝐾) ∈
ℕ) |
4 | 1, 2, 3 | syl2an 597 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℕ) |
5 | | phival 16106 |
. . 3
⊢ ((𝑃↑𝐾) ∈ ℕ → (ϕ‘(𝑃↑𝐾)) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) |
6 | 4, 5 | syl 17 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(ϕ‘(𝑃↑𝐾)) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) |
7 | | nnm1nn0 11941 |
. . . . . 6
⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈
ℕ0) |
8 | | nnexpcl 13445 |
. . . . . 6
⊢ ((𝑃 ∈ ℕ ∧ (𝐾 − 1) ∈
ℕ0) → (𝑃↑(𝐾 − 1)) ∈
ℕ) |
9 | 1, 7, 8 | syl2an 597 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) ∈
ℕ) |
10 | 9 | nncnd 11656 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) ∈
ℂ) |
11 | 1 | nncnd 11656 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℂ) |
12 | 11 | adantr 483 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝑃 ∈
ℂ) |
13 | | ax-1cn 10597 |
. . . . 5
⊢ 1 ∈
ℂ |
14 | | subdi 11075 |
. . . . 5
⊢ (((𝑃↑(𝐾 − 1)) ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1))) |
15 | 13, 14 | mp3an3 1446 |
. . . 4
⊢ (((𝑃↑(𝐾 − 1)) ∈ ℂ ∧ 𝑃 ∈ ℂ) → ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1))) |
16 | 10, 12, 15 | syl2anc 586 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1))) |
17 | 10 | mulid1d 10660 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) · 1) = (𝑃↑(𝐾 − 1))) |
18 | 17 | oveq2d 7174 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − (𝑃↑(𝐾 − 1)))) |
19 | | fzfi 13343 |
. . . . . . 7
⊢
(1...(𝑃↑𝐾)) ∈ Fin |
20 | | ssrab2 4058 |
. . . . . . 7
⊢ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ⊆ (1...(𝑃↑𝐾)) |
21 | | ssfi 8740 |
. . . . . . 7
⊢
(((1...(𝑃↑𝐾)) ∈ Fin ∧ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ⊆ (1...(𝑃↑𝐾))) → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin) |
22 | 19, 20, 21 | mp2an 690 |
. . . . . 6
⊢ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin |
23 | | ssrab2 4058 |
. . . . . . 7
⊢ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ⊆ (1...(𝑃↑𝐾)) |
24 | | ssfi 8740 |
. . . . . . 7
⊢
(((1...(𝑃↑𝐾)) ∈ Fin ∧ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ⊆ (1...(𝑃↑𝐾))) → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ∈ Fin) |
25 | 19, 23, 24 | mp2an 690 |
. . . . . 6
⊢ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ∈ Fin |
26 | | inrab 4277 |
. . . . . . 7
⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∩ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))} |
27 | | elfzelz 12911 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1...(𝑃↑𝐾)) → 𝑥 ∈ ℤ) |
28 | | prmz 16021 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
29 | | rpexp 16066 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1)) |
30 | 28, 29 | syl3an1 1159 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1)) |
31 | 30 | 3expa 1114 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ) ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1)) |
32 | 31 | an32s 650 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1)) |
33 | | simpr 487 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈
ℤ) |
34 | | zexpcl 13447 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℤ ∧ 𝐾 ∈ ℕ0)
→ (𝑃↑𝐾) ∈
ℤ) |
35 | 28, 2, 34 | syl2an 597 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℤ) |
36 | 35 | adantr 483 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑃↑𝐾) ∈ ℤ) |
37 | | gcdcom 15864 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ (𝑃↑𝐾) ∈ ℤ) → (𝑥 gcd (𝑃↑𝐾)) = ((𝑃↑𝐾) gcd 𝑥)) |
38 | 33, 36, 37 | syl2anc 586 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑥 gcd (𝑃↑𝐾)) = ((𝑃↑𝐾) gcd 𝑥)) |
39 | 38 | eqeq1d 2825 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ((𝑃↑𝐾) gcd 𝑥) = 1)) |
40 | | coprm 16057 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ) → (¬
𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1)) |
41 | 40 | adantlr 713 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (¬
𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1)) |
42 | 32, 39, 41 | 3bitr4d 313 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ¬ 𝑃 ∥ 𝑥)) |
43 | | zcn 11989 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
44 | 43 | adantl 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈
ℂ) |
45 | 44 | subid1d 10988 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑥 − 0) = 𝑥) |
46 | 45 | breq2d 5080 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑃 ∥ (𝑥 − 0) ↔ 𝑃 ∥ 𝑥)) |
47 | 46 | notbid 320 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (¬
𝑃 ∥ (𝑥 − 0) ↔ ¬ 𝑃 ∥ 𝑥)) |
48 | 42, 47 | bitr4d 284 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ¬ 𝑃 ∥ (𝑥 − 0))) |
49 | 27, 48 | sylan2 594 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ¬ 𝑃 ∥ (𝑥 − 0))) |
50 | 49 | biimpd 231 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ((𝑥 gcd (𝑃↑𝐾)) = 1 → ¬ 𝑃 ∥ (𝑥 − 0))) |
51 | | imnan 402 |
. . . . . . . . . 10
⊢ (((𝑥 gcd (𝑃↑𝐾)) = 1 → ¬ 𝑃 ∥ (𝑥 − 0)) ↔ ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))) |
52 | 50, 51 | sylib 220 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))) |
53 | 52 | ralrimiva 3184 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
∀𝑥 ∈
(1...(𝑃↑𝐾)) ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))) |
54 | | rabeq0 4340 |
. . . . . . . 8
⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))} = ∅ ↔ ∀𝑥 ∈ (1...(𝑃↑𝐾)) ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))) |
55 | 53, 54 | sylibr 236 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))} = ∅) |
56 | 26, 55 | syl5eq 2870 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∩ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = ∅) |
57 | | hashun 13746 |
. . . . . 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 1461 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘({𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}))) |
59 | 49 | biimprd 250 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (¬ 𝑃 ∥ (𝑥 − 0) → (𝑥 gcd (𝑃↑𝐾)) = 1)) |
60 | 59 | con1d 147 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (¬ (𝑥 gcd (𝑃↑𝐾)) = 1 → 𝑃 ∥ (𝑥 − 0))) |
61 | 60 | orrd 859 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))) |
62 | 61 | ralrimiva 3184 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
∀𝑥 ∈
(1...(𝑃↑𝐾))((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))) |
63 | | rabid2 3383 |
. . . . . . . . 9
⊢
((1...(𝑃↑𝐾)) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))} ↔ ∀𝑥 ∈ (1...(𝑃↑𝐾))((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))) |
64 | 62, 63 | sylibr 236 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(1...(𝑃↑𝐾)) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))}) |
65 | | unrab 4276 |
. . . . . . . 8
⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))} |
66 | 64, 65 | syl6reqr 2877 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = (1...(𝑃↑𝐾))) |
67 | 66 | fveq2d 6676 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘({𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = (♯‘(1...(𝑃↑𝐾)))) |
68 | 4 | nnnn0d 11958 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈
ℕ0) |
69 | | hashfz1 13709 |
. . . . . . 7
⊢ ((𝑃↑𝐾) ∈ ℕ0 →
(♯‘(1...(𝑃↑𝐾))) = (𝑃↑𝐾)) |
70 | 68, 69 | syl 17 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘(1...(𝑃↑𝐾))) = (𝑃↑𝐾)) |
71 | | expm1t 13460 |
. . . . . . 7
⊢ ((𝑃 ∈ ℂ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) = ((𝑃↑(𝐾 − 1)) · 𝑃)) |
72 | 11, 71 | sylan 582 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) = ((𝑃↑(𝐾 − 1)) · 𝑃)) |
73 | 67, 70, 72 | 3eqtrd 2862 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘({𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((𝑃↑(𝐾 − 1)) · 𝑃)) |
74 | 1 | adantr 483 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝑃 ∈
ℕ) |
75 | | 1zzd 12016 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 1 ∈
ℤ) |
76 | | nn0uz 12283 |
. . . . . . . . . . 11
⊢
ℕ0 = (ℤ≥‘0) |
77 | | 1m1e0 11712 |
. . . . . . . . . . . 12
⊢ (1
− 1) = 0 |
78 | 77 | fveq2i 6675 |
. . . . . . . . . . 11
⊢
(ℤ≥‘(1 − 1)) =
(ℤ≥‘0) |
79 | 76, 78 | eqtr4i 2849 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘(1 −
1)) |
80 | 68, 79 | eleqtrdi 2925 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ (ℤ≥‘(1
− 1))) |
81 | | 0zd 11996 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 0 ∈
ℤ) |
82 | 74, 75, 80, 81 | hashdvds 16114 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = ((⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) − (⌊‘(((1 − 1)
− 0) / 𝑃)))) |
83 | 4 | nncnd 11656 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℂ) |
84 | 83 | subid1d 10988 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑𝐾) − 0) = (𝑃↑𝐾)) |
85 | 84 | oveq1d 7173 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) − 0) / 𝑃) = ((𝑃↑𝐾) / 𝑃)) |
86 | 74 | nnne0d 11690 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝑃 ≠ 0) |
87 | | nnz 12007 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℤ) |
88 | 87 | adantl 484 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝐾 ∈
ℤ) |
89 | 12, 86, 88 | expm1d 13523 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) = ((𝑃↑𝐾) / 𝑃)) |
90 | 85, 89 | eqtr4d 2861 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) − 0) / 𝑃) = (𝑃↑(𝐾 − 1))) |
91 | 90 | fveq2d 6676 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) = (⌊‘(𝑃↑(𝐾 − 1)))) |
92 | 9 | nnzd 12089 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) ∈
ℤ) |
93 | | flid 13181 |
. . . . . . . . . . 11
⊢ ((𝑃↑(𝐾 − 1)) ∈ ℤ →
(⌊‘(𝑃↑(𝐾 − 1))) = (𝑃↑(𝐾 − 1))) |
94 | 92, 93 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(𝑃↑(𝐾 − 1))) = (𝑃↑(𝐾 − 1))) |
95 | 91, 94 | eqtrd 2858 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) = (𝑃↑(𝐾 − 1))) |
96 | 77 | oveq1i 7168 |
. . . . . . . . . . . . . 14
⊢ ((1
− 1) − 0) = (0 − 0) |
97 | | 0m0e0 11760 |
. . . . . . . . . . . . . 14
⊢ (0
− 0) = 0 |
98 | 96, 97 | eqtri 2846 |
. . . . . . . . . . . . 13
⊢ ((1
− 1) − 0) = 0 |
99 | 98 | oveq1i 7168 |
. . . . . . . . . . . 12
⊢ (((1
− 1) − 0) / 𝑃)
= (0 / 𝑃) |
100 | 12, 86 | div0d 11417 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (0 /
𝑃) = 0) |
101 | 99, 100 | syl5eq 2870 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((1
− 1) − 0) / 𝑃)
= 0) |
102 | 101 | fveq2d 6676 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(((1 − 1) − 0) / 𝑃)) = (⌊‘0)) |
103 | | 0z 11995 |
. . . . . . . . . . 11
⊢ 0 ∈
ℤ |
104 | | flid 13181 |
. . . . . . . . . . 11
⊢ (0 ∈
ℤ → (⌊‘0) = 0) |
105 | 103, 104 | ax-mp 5 |
. . . . . . . . . 10
⊢
(⌊‘0) = 0 |
106 | 102, 105 | syl6eq 2874 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(((1 − 1) − 0) / 𝑃)) = 0) |
107 | 95, 106 | oveq12d 7176 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
((⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) − (⌊‘(((1 − 1)
− 0) / 𝑃))) = ((𝑃↑(𝐾 − 1)) − 0)) |
108 | 10 | subid1d 10988 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) − 0) = (𝑃↑(𝐾 − 1))) |
109 | 82, 107, 108 | 3eqtrd 2862 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = (𝑃↑(𝐾 − 1))) |
110 | 109 | oveq2d 7174 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
((♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (𝑃↑(𝐾 − 1)))) |
111 | | hashcl 13720 |
. . . . . . . . 9
⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin →
(♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈
ℕ0) |
112 | 22, 111 | ax-mp 5 |
. . . . . . . 8
⊢
(♯‘{𝑥
∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈
ℕ0 |
113 | 112 | nn0cni 11912 |
. . . . . . 7
⊢
(♯‘{𝑥
∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈ ℂ |
114 | | addcom 10828 |
. . . . . . 7
⊢
(((♯‘{𝑥
∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈ ℂ ∧ (𝑃↑(𝐾 − 1)) ∈ ℂ) →
((♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (𝑃↑(𝐾 − 1))) = ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}))) |
115 | 113, 10, 114 | sylancr 589 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
((♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (𝑃↑(𝐾 − 1))) = ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}))) |
116 | 110, 115 | eqtrd 2858 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
((♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}))) |
117 | 58, 73, 116 | 3eqtr3rd 2867 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) = ((𝑃↑(𝐾 − 1)) · 𝑃)) |
118 | 10, 12 | mulcld 10663 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) · 𝑃) ∈ ℂ) |
119 | 113 | a1i 11 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈ ℂ) |
120 | 118, 10, 119 | subaddd 11017 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
((((𝑃↑(𝐾 − 1)) · 𝑃) − (𝑃↑(𝐾 − 1))) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ↔ ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) = ((𝑃↑(𝐾 − 1)) · 𝑃))) |
121 | 117, 120 | mpbird 259 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑(𝐾 − 1)) · 𝑃) − (𝑃↑(𝐾 − 1))) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) |
122 | 16, 18, 121 | 3eqtrrd 2863 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) = ((𝑃↑(𝐾 − 1)) · (𝑃 − 1))) |
123 | 6, 122 | eqtrd 2858 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(ϕ‘(𝑃↑𝐾)) = ((𝑃↑(𝐾 − 1)) · (𝑃 − 1))) |