Step | Hyp | Ref
| Expression |
1 | | prmnn 11631 |
. . . 4
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
2 | | nnnn0 8882 |
. . . 4
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℕ0) |
3 | | nnexpcl 10193 |
. . . 4
⊢ ((𝑃 ∈ ℕ ∧ 𝐾 ∈ ℕ0)
→ (𝑃↑𝐾) ∈
ℕ) |
4 | 1, 2, 3 | syl2an 285 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℕ) |
5 | | phival 11728 |
. . 3
⊢ ((𝑃↑𝐾) ∈ ℕ → (ϕ‘(𝑃↑𝐾)) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) |
6 | 4, 5 | syl 14 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(ϕ‘(𝑃↑𝐾)) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) |
7 | | nnm1nn0 8916 |
. . . . . 6
⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈
ℕ0) |
8 | | nnexpcl 10193 |
. . . . . 6
⊢ ((𝑃 ∈ ℕ ∧ (𝐾 − 1) ∈
ℕ0) → (𝑃↑(𝐾 − 1)) ∈
ℕ) |
9 | 1, 7, 8 | syl2an 285 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) ∈
ℕ) |
10 | 9 | nncnd 8638 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) ∈
ℂ) |
11 | 1 | nncnd 8638 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℂ) |
12 | 11 | adantr 272 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝑃 ∈
ℂ) |
13 | | ax-1cn 7632 |
. . . . 5
⊢ 1 ∈
ℂ |
14 | | subdi 8060 |
. . . . 5
⊢ (((𝑃↑(𝐾 − 1)) ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1))) |
15 | 13, 14 | mp3an3 1285 |
. . . 4
⊢ (((𝑃↑(𝐾 − 1)) ∈ ℂ ∧ 𝑃 ∈ ℂ) → ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1))) |
16 | 10, 12, 15 | syl2anc 406 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1))) |
17 | 10 | mulid1d 7701 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) · 1) = (𝑃↑(𝐾 − 1))) |
18 | 17 | oveq2d 5742 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − (𝑃↑(𝐾 − 1)))) |
19 | | phivalfi 11727 |
. . . . . . 7
⊢ ((𝑃↑𝐾) ∈ ℕ → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin) |
20 | 4, 19 | syl 14 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin) |
21 | | 1zzd 8979 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 1 ∈
ℤ) |
22 | | prmz 11632 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
23 | | zexpcl 10195 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℤ ∧ 𝐾 ∈ ℕ0)
→ (𝑃↑𝐾) ∈
ℤ) |
24 | 22, 2, 23 | syl2an 285 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℤ) |
25 | 21, 24 | fzfigd 10091 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(1...(𝑃↑𝐾)) ∈ Fin) |
26 | 22 | ad2antrr 477 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → 𝑃 ∈ ℤ) |
27 | | elfzelz 9693 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1...(𝑃↑𝐾)) → 𝑥 ∈ ℤ) |
28 | 27 | adantl 273 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → 𝑥 ∈ ℤ) |
29 | | 0zd 8964 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → 0 ∈
ℤ) |
30 | 28, 29 | zsubcld 9076 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (𝑥 − 0) ∈ ℤ) |
31 | | zdvdsdc 11356 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℤ ∧ (𝑥 − 0) ∈ ℤ)
→ DECID 𝑃 ∥ (𝑥 − 0)) |
32 | 26, 30, 31 | syl2anc 406 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → DECID 𝑃 ∥ (𝑥 − 0)) |
33 | 32 | ralrimiva 2477 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
∀𝑥 ∈
(1...(𝑃↑𝐾))DECID 𝑃 ∥ (𝑥 − 0)) |
34 | 25, 33 | ssfirab 6772 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ∈ Fin) |
35 | | inrab 3312 |
. . . . . . 7
⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∩ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))} |
36 | | rpexp 11671 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1)) |
37 | 22, 36 | syl3an1 1230 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1)) |
38 | 37 | 3expa 1162 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ) ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1)) |
39 | 38 | an32s 540 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1)) |
40 | | simpr 109 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈
ℤ) |
41 | 24 | adantr 272 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑃↑𝐾) ∈ ℤ) |
42 | | gcdcom 11504 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ (𝑃↑𝐾) ∈ ℤ) → (𝑥 gcd (𝑃↑𝐾)) = ((𝑃↑𝐾) gcd 𝑥)) |
43 | 40, 41, 42 | syl2anc 406 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑥 gcd (𝑃↑𝐾)) = ((𝑃↑𝐾) gcd 𝑥)) |
44 | 43 | eqeq1d 2121 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ((𝑃↑𝐾) gcd 𝑥) = 1)) |
45 | | coprm 11662 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ) → (¬
𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1)) |
46 | 45 | adantlr 466 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (¬
𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1)) |
47 | 39, 44, 46 | 3bitr4d 219 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ¬ 𝑃 ∥ 𝑥)) |
48 | | zcn 8957 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
49 | 48 | adantl 273 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈
ℂ) |
50 | 49 | subid1d 7979 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑥 − 0) = 𝑥) |
51 | 50 | breq2d 3905 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑃 ∥ (𝑥 − 0) ↔ 𝑃 ∥ 𝑥)) |
52 | 51 | notbid 639 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (¬
𝑃 ∥ (𝑥 − 0) ↔ ¬ 𝑃 ∥ 𝑥)) |
53 | 47, 52 | bitr4d 190 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ¬ 𝑃 ∥ (𝑥 − 0))) |
54 | 27, 53 | sylan2 282 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ¬ 𝑃 ∥ (𝑥 − 0))) |
55 | 54 | biimpd 143 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ((𝑥 gcd (𝑃↑𝐾)) = 1 → ¬ 𝑃 ∥ (𝑥 − 0))) |
56 | | imnan 662 |
. . . . . . . . . 10
⊢ (((𝑥 gcd (𝑃↑𝐾)) = 1 → ¬ 𝑃 ∥ (𝑥 − 0)) ↔ ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))) |
57 | 55, 56 | sylib 121 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))) |
58 | 57 | ralrimiva 2477 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
∀𝑥 ∈
(1...(𝑃↑𝐾)) ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))) |
59 | | rabeq0 3356 |
. . . . . . . 8
⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))} = ∅ ↔ ∀𝑥 ∈ (1...(𝑃↑𝐾)) ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))) |
60 | 58, 59 | sylibr 133 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))} = ∅) |
61 | 35, 60 | syl5eq 2157 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∩ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = ∅) |
62 | | hashun 10438 |
. . . . . 6
⊢ (({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin ∧ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ∈ Fin ∧ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∩ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = ∅) →
(♯‘({𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}))) |
63 | 20, 34, 61, 62 | syl3anc 1197 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘({𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}))) |
64 | 54 | biimprd 157 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (¬ 𝑃 ∥ (𝑥 − 0) → (𝑥 gcd (𝑃↑𝐾)) = 1)) |
65 | | con1dc 822 |
. . . . . . . . . . . 12
⊢
(DECID 𝑃 ∥ (𝑥 − 0) → ((¬ 𝑃 ∥ (𝑥 − 0) → (𝑥 gcd (𝑃↑𝐾)) = 1) → (¬ (𝑥 gcd (𝑃↑𝐾)) = 1 → 𝑃 ∥ (𝑥 − 0)))) |
66 | 32, 64, 65 | sylc 62 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (¬ (𝑥 gcd (𝑃↑𝐾)) = 1 → 𝑃 ∥ (𝑥 − 0))) |
67 | 24 | adantr 272 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (𝑃↑𝐾) ∈ ℤ) |
68 | 28, 67 | gcdcld 11499 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (𝑥 gcd (𝑃↑𝐾)) ∈
ℕ0) |
69 | 68 | nn0zd 9069 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (𝑥 gcd (𝑃↑𝐾)) ∈ ℤ) |
70 | | 1zzd 8979 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → 1 ∈
ℤ) |
71 | | zdceq 9024 |
. . . . . . . . . . . . 13
⊢ (((𝑥 gcd (𝑃↑𝐾)) ∈ ℤ ∧ 1 ∈ ℤ)
→ DECID (𝑥 gcd (𝑃↑𝐾)) = 1) |
72 | 69, 70, 71 | syl2anc 406 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → DECID (𝑥 gcd (𝑃↑𝐾)) = 1) |
73 | | dfordc 858 |
. . . . . . . . . . . 12
⊢
(DECID (𝑥 gcd (𝑃↑𝐾)) = 1 → (((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0)) ↔ (¬ (𝑥 gcd (𝑃↑𝐾)) = 1 → 𝑃 ∥ (𝑥 − 0)))) |
74 | 72, 73 | syl 14 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0)) ↔ (¬ (𝑥 gcd (𝑃↑𝐾)) = 1 → 𝑃 ∥ (𝑥 − 0)))) |
75 | 66, 74 | mpbird 166 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))) |
76 | 75 | ralrimiva 2477 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
∀𝑥 ∈
(1...(𝑃↑𝐾))((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))) |
77 | | rabid2 2579 |
. . . . . . . . 9
⊢
((1...(𝑃↑𝐾)) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))} ↔ ∀𝑥 ∈ (1...(𝑃↑𝐾))((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))) |
78 | 76, 77 | sylibr 133 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(1...(𝑃↑𝐾)) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))}) |
79 | | unrab 3311 |
. . . . . . . 8
⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))} |
80 | 78, 79 | syl6reqr 2164 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = (1...(𝑃↑𝐾))) |
81 | 80 | fveq2d 5377 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘({𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = (♯‘(1...(𝑃↑𝐾)))) |
82 | 4 | nnnn0d 8928 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈
ℕ0) |
83 | | hashfz1 10416 |
. . . . . . 7
⊢ ((𝑃↑𝐾) ∈ ℕ0 →
(♯‘(1...(𝑃↑𝐾))) = (𝑃↑𝐾)) |
84 | 82, 83 | syl 14 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘(1...(𝑃↑𝐾))) = (𝑃↑𝐾)) |
85 | | expm1t 10208 |
. . . . . . 7
⊢ ((𝑃 ∈ ℂ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) = ((𝑃↑(𝐾 − 1)) · 𝑃)) |
86 | 11, 85 | sylan 279 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) = ((𝑃↑(𝐾 − 1)) · 𝑃)) |
87 | 81, 84, 86 | 3eqtrd 2149 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘({𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((𝑃↑(𝐾 − 1)) · 𝑃)) |
88 | | hashcl 10414 |
. . . . . . . 8
⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin →
(♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈
ℕ0) |
89 | 20, 88 | syl 14 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈
ℕ0) |
90 | 89 | nn0cnd 8930 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈ ℂ) |
91 | 1 | adantr 272 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝑃 ∈
ℕ) |
92 | | nn0uz 9256 |
. . . . . . . . . . 11
⊢
ℕ0 = (ℤ≥‘0) |
93 | | 1m1e0 8693 |
. . . . . . . . . . . 12
⊢ (1
− 1) = 0 |
94 | 93 | fveq2i 5376 |
. . . . . . . . . . 11
⊢
(ℤ≥‘(1 − 1)) =
(ℤ≥‘0) |
95 | 92, 94 | eqtr4i 2136 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘(1 −
1)) |
96 | 82, 95 | syl6eleq 2205 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ (ℤ≥‘(1
− 1))) |
97 | | 0zd 8964 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 0 ∈
ℤ) |
98 | 91, 21, 96, 97 | hashdvds 11736 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = ((⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) − (⌊‘(((1 − 1)
− 0) / 𝑃)))) |
99 | 4 | nncnd 8638 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℂ) |
100 | 99 | subid1d 7979 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑𝐾) − 0) = (𝑃↑𝐾)) |
101 | 100 | oveq1d 5741 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) − 0) / 𝑃) = ((𝑃↑𝐾) / 𝑃)) |
102 | 91 | nnap0d 8670 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝑃 # 0) |
103 | | nnz 8971 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℤ) |
104 | 103 | adantl 273 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝐾 ∈
ℤ) |
105 | 12, 102, 104 | expm1apd 10321 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) = ((𝑃↑𝐾) / 𝑃)) |
106 | 101, 105 | eqtr4d 2148 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) − 0) / 𝑃) = (𝑃↑(𝐾 − 1))) |
107 | 106 | fveq2d 5377 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) = (⌊‘(𝑃↑(𝐾 − 1)))) |
108 | 9 | nnzd 9070 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) ∈
ℤ) |
109 | | flid 9944 |
. . . . . . . . . . 11
⊢ ((𝑃↑(𝐾 − 1)) ∈ ℤ →
(⌊‘(𝑃↑(𝐾 − 1))) = (𝑃↑(𝐾 − 1))) |
110 | 108, 109 | syl 14 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(𝑃↑(𝐾 − 1))) = (𝑃↑(𝐾 − 1))) |
111 | 107, 110 | eqtrd 2145 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) = (𝑃↑(𝐾 − 1))) |
112 | 93 | oveq1i 5736 |
. . . . . . . . . . . . . 14
⊢ ((1
− 1) − 0) = (0 − 0) |
113 | | 0m0e0 8736 |
. . . . . . . . . . . . . 14
⊢ (0
− 0) = 0 |
114 | 112, 113 | eqtri 2133 |
. . . . . . . . . . . . 13
⊢ ((1
− 1) − 0) = 0 |
115 | 114 | oveq1i 5736 |
. . . . . . . . . . . 12
⊢ (((1
− 1) − 0) / 𝑃)
= (0 / 𝑃) |
116 | 12, 102 | div0apd 8454 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (0 /
𝑃) = 0) |
117 | 115, 116 | syl5eq 2157 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((1
− 1) − 0) / 𝑃)
= 0) |
118 | 117 | fveq2d 5377 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(((1 − 1) − 0) / 𝑃)) = (⌊‘0)) |
119 | | 0z 8963 |
. . . . . . . . . . 11
⊢ 0 ∈
ℤ |
120 | | flid 9944 |
. . . . . . . . . . 11
⊢ (0 ∈
ℤ → (⌊‘0) = 0) |
121 | 119, 120 | ax-mp 7 |
. . . . . . . . . 10
⊢
(⌊‘0) = 0 |
122 | 118, 121 | syl6eq 2161 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(((1 − 1) − 0) / 𝑃)) = 0) |
123 | 111, 122 | oveq12d 5744 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
((⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) − (⌊‘(((1 − 1)
− 0) / 𝑃))) = ((𝑃↑(𝐾 − 1)) − 0)) |
124 | 10 | subid1d 7979 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) − 0) = (𝑃↑(𝐾 − 1))) |
125 | 98, 123, 124 | 3eqtrd 2149 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = (𝑃↑(𝐾 − 1))) |
126 | 125 | oveq2d 5742 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
((♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (𝑃↑(𝐾 − 1)))) |
127 | 90, 10, 126 | comraddd 7836 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
((♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}))) |
128 | 63, 87, 127 | 3eqtr3rd 2154 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) = ((𝑃↑(𝐾 − 1)) · 𝑃)) |
129 | 10, 12 | mulcld 7704 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) · 𝑃) ∈ ℂ) |
130 | 129, 10, 90 | subaddd 8008 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
((((𝑃↑(𝐾 − 1)) · 𝑃) − (𝑃↑(𝐾 − 1))) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ↔ ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) = ((𝑃↑(𝐾 − 1)) · 𝑃))) |
131 | 128, 130 | mpbird 166 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑(𝐾 − 1)) · 𝑃) − (𝑃↑(𝐾 − 1))) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) |
132 | 16, 18, 131 | 3eqtrrd 2150 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(♯‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) = ((𝑃↑(𝐾 − 1)) · (𝑃 − 1))) |
133 | 6, 132 | eqtrd 2145 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(ϕ‘(𝑃↑𝐾)) = ((𝑃↑(𝐾 − 1)) · (𝑃 − 1))) |