Step | Hyp | Ref
| Expression |
1 | | prmnn 15226 |
. . . 4
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
2 | | nnnn0 11176 |
. . . 4
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℕ0) |
3 | | nnexpcl 12735 |
. . . 4
⊢ ((𝑃 ∈ ℕ ∧ 𝐾 ∈ ℕ0)
→ (𝑃↑𝐾) ∈
ℕ) |
4 | 1, 2, 3 | syl2an 493 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℕ) |
5 | | phival 15310 |
. . 3
⊢ ((𝑃↑𝐾) ∈ ℕ → (ϕ‘(𝑃↑𝐾)) = (#‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) |
6 | 4, 5 | syl 17 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(ϕ‘(𝑃↑𝐾)) = (#‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) |
7 | | nnm1nn0 11211 |
. . . . . 6
⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈
ℕ0) |
8 | | nnexpcl 12735 |
. . . . . 6
⊢ ((𝑃 ∈ ℕ ∧ (𝐾 − 1) ∈
ℕ0) → (𝑃↑(𝐾 − 1)) ∈
ℕ) |
9 | 1, 7, 8 | syl2an 493 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) ∈
ℕ) |
10 | 9 | nncnd 10913 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) ∈
ℂ) |
11 | 1 | nncnd 10913 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℂ) |
12 | 11 | adantr 480 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝑃 ∈
ℂ) |
13 | | ax-1cn 9873 |
. . . . 5
⊢ 1 ∈
ℂ |
14 | | subdi 10342 |
. . . . 5
⊢ (((𝑃↑(𝐾 − 1)) ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1))) |
15 | 13, 14 | mp3an3 1405 |
. . . 4
⊢ (((𝑃↑(𝐾 − 1)) ∈ ℂ ∧ 𝑃 ∈ ℂ) → ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1))) |
16 | 10, 12, 15 | syl2anc 691 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1))) |
17 | 10 | mulid1d 9936 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) · 1) = (𝑃↑(𝐾 − 1))) |
18 | 17 | oveq2d 6565 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − (𝑃↑(𝐾 − 1)))) |
19 | | inrab 3858 |
. . . . . . 7
⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∩ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))} |
20 | | elfzelz 12213 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1...(𝑃↑𝐾)) → 𝑥 ∈ ℤ) |
21 | | prmz 15227 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
22 | | rpexp 15270 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1)) |
23 | 21, 22 | syl3an1 1351 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1)) |
24 | 23 | 3expa 1257 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ) ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1)) |
25 | 24 | an32s 842 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1)) |
26 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈
ℤ) |
27 | | zexpcl 12737 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℤ ∧ 𝐾 ∈ ℕ0)
→ (𝑃↑𝐾) ∈
ℤ) |
28 | 21, 2, 27 | syl2an 493 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℤ) |
29 | 28 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑃↑𝐾) ∈ ℤ) |
30 | | gcdcom 15073 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ (𝑃↑𝐾) ∈ ℤ) → (𝑥 gcd (𝑃↑𝐾)) = ((𝑃↑𝐾) gcd 𝑥)) |
31 | 26, 29, 30 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑥 gcd (𝑃↑𝐾)) = ((𝑃↑𝐾) gcd 𝑥)) |
32 | 31 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ((𝑃↑𝐾) gcd 𝑥) = 1)) |
33 | | coprm 15261 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ) → (¬
𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1)) |
34 | 33 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (¬
𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1)) |
35 | 25, 32, 34 | 3bitr4d 299 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ¬ 𝑃 ∥ 𝑥)) |
36 | | zcn 11259 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈
ℂ) |
38 | 37 | subid1d 10260 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑥 − 0) = 𝑥) |
39 | 38 | breq2d 4595 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑃 ∥ (𝑥 − 0) ↔ 𝑃 ∥ 𝑥)) |
40 | 39 | notbid 307 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (¬
𝑃 ∥ (𝑥 − 0) ↔ ¬ 𝑃 ∥ 𝑥)) |
41 | 35, 40 | bitr4d 270 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ¬ 𝑃 ∥ (𝑥 − 0))) |
42 | 20, 41 | sylan2 490 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ¬ 𝑃 ∥ (𝑥 − 0))) |
43 | 42 | biimpd 218 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ((𝑥 gcd (𝑃↑𝐾)) = 1 → ¬ 𝑃 ∥ (𝑥 − 0))) |
44 | | imnan 437 |
. . . . . . . . . 10
⊢ (((𝑥 gcd (𝑃↑𝐾)) = 1 → ¬ 𝑃 ∥ (𝑥 − 0)) ↔ ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))) |
45 | 43, 44 | sylib 207 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))) |
46 | 45 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
∀𝑥 ∈
(1...(𝑃↑𝐾)) ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))) |
47 | | rabeq0 3911 |
. . . . . . . 8
⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))} = ∅ ↔ ∀𝑥 ∈ (1...(𝑃↑𝐾)) ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))) |
48 | 46, 47 | sylibr 223 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))} = ∅) |
49 | 19, 48 | syl5eq 2656 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∩ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = ∅) |
50 | | fzfi 12633 |
. . . . . . . 8
⊢
(1...(𝑃↑𝐾)) ∈ Fin |
51 | | ssrab2 3650 |
. . . . . . . 8
⊢ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ⊆ (1...(𝑃↑𝐾)) |
52 | | ssfi 8065 |
. . . . . . . 8
⊢
(((1...(𝑃↑𝐾)) ∈ Fin ∧ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ⊆ (1...(𝑃↑𝐾))) → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin) |
53 | 50, 51, 52 | mp2an 704 |
. . . . . . 7
⊢ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin |
54 | | ssrab2 3650 |
. . . . . . . 8
⊢ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ⊆ (1...(𝑃↑𝐾)) |
55 | | ssfi 8065 |
. . . . . . . 8
⊢
(((1...(𝑃↑𝐾)) ∈ Fin ∧ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ⊆ (1...(𝑃↑𝐾))) → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ∈ Fin) |
56 | 50, 54, 55 | mp2an 704 |
. . . . . . 7
⊢ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ∈ Fin |
57 | | hashun 13032 |
. . . . . . 7
⊢ (({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin ∧ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ∈ Fin ∧ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∩ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = ∅) →
(#‘({𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((#‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (#‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}))) |
58 | 53, 56, 57 | mp3an12 1406 |
. . . . . 6
⊢ (({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∩ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = ∅ →
(#‘({𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((#‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (#‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}))) |
59 | 49, 58 | syl 17 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(#‘({𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((#‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (#‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}))) |
60 | 42 | biimprd 237 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (¬ 𝑃 ∥ (𝑥 − 0) → (𝑥 gcd (𝑃↑𝐾)) = 1)) |
61 | 60 | con1d 138 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (¬ (𝑥 gcd (𝑃↑𝐾)) = 1 → 𝑃 ∥ (𝑥 − 0))) |
62 | 61 | orrd 392 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))) |
63 | 62 | ralrimiva 2949 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
∀𝑥 ∈
(1...(𝑃↑𝐾))((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))) |
64 | | rabid2 3096 |
. . . . . . . . 9
⊢
((1...(𝑃↑𝐾)) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))} ↔ ∀𝑥 ∈ (1...(𝑃↑𝐾))((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))) |
65 | 63, 64 | sylibr 223 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(1...(𝑃↑𝐾)) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))}) |
66 | | unrab 3857 |
. . . . . . . 8
⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))} |
67 | 65, 66 | syl6reqr 2663 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = (1...(𝑃↑𝐾))) |
68 | 67 | fveq2d 6107 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(#‘({𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = (#‘(1...(𝑃↑𝐾)))) |
69 | 4 | nnnn0d 11228 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈
ℕ0) |
70 | | hashfz1 12996 |
. . . . . . 7
⊢ ((𝑃↑𝐾) ∈ ℕ0 →
(#‘(1...(𝑃↑𝐾))) = (𝑃↑𝐾)) |
71 | 69, 70 | syl 17 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(#‘(1...(𝑃↑𝐾))) = (𝑃↑𝐾)) |
72 | | expm1t 12750 |
. . . . . . 7
⊢ ((𝑃 ∈ ℂ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) = ((𝑃↑(𝐾 − 1)) · 𝑃)) |
73 | 11, 72 | sylan 487 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) = ((𝑃↑(𝐾 − 1)) · 𝑃)) |
74 | 68, 71, 73 | 3eqtrd 2648 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(#‘({𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((𝑃↑(𝐾 − 1)) · 𝑃)) |
75 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝑃 ∈
ℕ) |
76 | | 1zzd 11285 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 1 ∈
ℤ) |
77 | | nn0uz 11598 |
. . . . . . . . . . 11
⊢
ℕ0 = (ℤ≥‘0) |
78 | | 1m1e0 10966 |
. . . . . . . . . . . 12
⊢ (1
− 1) = 0 |
79 | 78 | fveq2i 6106 |
. . . . . . . . . . 11
⊢
(ℤ≥‘(1 − 1)) =
(ℤ≥‘0) |
80 | 77, 79 | eqtr4i 2635 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘(1 −
1)) |
81 | 69, 80 | syl6eleq 2698 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ (ℤ≥‘(1
− 1))) |
82 | | 0zd 11266 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 0 ∈
ℤ) |
83 | 75, 76, 81, 82 | hashdvds 15318 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(#‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = ((⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) − (⌊‘(((1 − 1)
− 0) / 𝑃)))) |
84 | 4 | nncnd 10913 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℂ) |
85 | 84 | subid1d 10260 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑𝐾) − 0) = (𝑃↑𝐾)) |
86 | 85 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) − 0) / 𝑃) = ((𝑃↑𝐾) / 𝑃)) |
87 | 75 | nnne0d 10942 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝑃 ≠ 0) |
88 | | nnz 11276 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℤ) |
89 | 88 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝐾 ∈
ℤ) |
90 | 12, 87, 89 | expm1d 12880 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) = ((𝑃↑𝐾) / 𝑃)) |
91 | 86, 90 | eqtr4d 2647 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) − 0) / 𝑃) = (𝑃↑(𝐾 − 1))) |
92 | 91 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) = (⌊‘(𝑃↑(𝐾 − 1)))) |
93 | 9 | nnzd 11357 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) ∈
ℤ) |
94 | | flid 12471 |
. . . . . . . . . . 11
⊢ ((𝑃↑(𝐾 − 1)) ∈ ℤ →
(⌊‘(𝑃↑(𝐾 − 1))) = (𝑃↑(𝐾 − 1))) |
95 | 93, 94 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(𝑃↑(𝐾 − 1))) = (𝑃↑(𝐾 − 1))) |
96 | 92, 95 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) = (𝑃↑(𝐾 − 1))) |
97 | 78 | oveq1i 6559 |
. . . . . . . . . . . . . 14
⊢ ((1
− 1) − 0) = (0 − 0) |
98 | | 0m0e0 11007 |
. . . . . . . . . . . . . 14
⊢ (0
− 0) = 0 |
99 | 97, 98 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢ ((1
− 1) − 0) = 0 |
100 | 99 | oveq1i 6559 |
. . . . . . . . . . . 12
⊢ (((1
− 1) − 0) / 𝑃)
= (0 / 𝑃) |
101 | 12, 87 | div0d 10679 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (0 /
𝑃) = 0) |
102 | 100, 101 | syl5eq 2656 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((1
− 1) − 0) / 𝑃)
= 0) |
103 | 102 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(((1 − 1) − 0) / 𝑃)) = (⌊‘0)) |
104 | | 0z 11265 |
. . . . . . . . . . 11
⊢ 0 ∈
ℤ |
105 | | flid 12471 |
. . . . . . . . . . 11
⊢ (0 ∈
ℤ → (⌊‘0) = 0) |
106 | 104, 105 | ax-mp 5 |
. . . . . . . . . 10
⊢
(⌊‘0) = 0 |
107 | 103, 106 | syl6eq 2660 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(⌊‘(((1 − 1) − 0) / 𝑃)) = 0) |
108 | 96, 107 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
((⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) − (⌊‘(((1 − 1)
− 0) / 𝑃))) = ((𝑃↑(𝐾 − 1)) − 0)) |
109 | 10 | subid1d 10260 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) − 0) = (𝑃↑(𝐾 − 1))) |
110 | 83, 108, 109 | 3eqtrd 2648 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(#‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = (𝑃↑(𝐾 − 1))) |
111 | 110 | oveq2d 6565 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
((#‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (#‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((#‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (𝑃↑(𝐾 − 1)))) |
112 | | hashcl 13009 |
. . . . . . . . 9
⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin → (#‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈
ℕ0) |
113 | 53, 112 | ax-mp 5 |
. . . . . . . 8
⊢
(#‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈
ℕ0 |
114 | 113 | nn0cni 11181 |
. . . . . . 7
⊢
(#‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈ ℂ |
115 | | addcom 10101 |
. . . . . . 7
⊢
(((#‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈ ℂ ∧ (𝑃↑(𝐾 − 1)) ∈ ℂ) →
((#‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (𝑃↑(𝐾 − 1))) = ((𝑃↑(𝐾 − 1)) + (#‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}))) |
116 | 114, 10, 115 | sylancr 694 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
((#‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (𝑃↑(𝐾 − 1))) = ((𝑃↑(𝐾 − 1)) + (#‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}))) |
117 | 111, 116 | eqtrd 2644 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
((#‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (#‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((𝑃↑(𝐾 − 1)) + (#‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}))) |
118 | 59, 74, 117 | 3eqtr3rd 2653 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) + (#‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) = ((𝑃↑(𝐾 − 1)) · 𝑃)) |
119 | 10, 12 | mulcld 9939 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) · 𝑃) ∈ ℂ) |
120 | 114 | a1i 11 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(#‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈ ℂ) |
121 | 119, 10, 120 | subaddd 10289 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
((((𝑃↑(𝐾 − 1)) · 𝑃) − (𝑃↑(𝐾 − 1))) = (#‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ↔ ((𝑃↑(𝐾 − 1)) + (#‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) = ((𝑃↑(𝐾 − 1)) · 𝑃))) |
122 | 118, 121 | mpbird 246 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑(𝐾 − 1)) · 𝑃) − (𝑃↑(𝐾 − 1))) = (#‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) |
123 | 16, 18, 122 | 3eqtrrd 2649 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(#‘{𝑥 ∈
(1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) = ((𝑃↑(𝐾 − 1)) · (𝑃 − 1))) |
124 | 6, 123 | eqtrd 2644 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) →
(ϕ‘(𝑃↑𝐾)) = ((𝑃↑(𝐾 − 1)) · (𝑃 − 1))) |