Proof of Theorem gausslemma2dlem5a
Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.p |
. . . 4
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
2 | | gausslemma2d.h |
. . . 4
⊢ 𝐻 = ((𝑃 − 1) / 2) |
3 | | gausslemma2d.r |
. . . 4
⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
4 | | gausslemma2d.m |
. . . 4
⊢ 𝑀 = (⌊‘(𝑃 / 4)) |
5 | 1, 2, 3, 4 | gausslemma2dlem3 15121 |
. . 3
⊢ (𝜑 → ∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2))) |
6 | | prodeq2 11687 |
. . . 4
⊢
(∀𝑘 ∈
((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2)) → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑃 − (𝑘 · 2))) |
7 | 6 | oveq1d 5925 |
. . 3
⊢
(∀𝑘 ∈
((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2)) → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑃 − (𝑘 · 2)) mod 𝑃)) |
8 | 5, 7 | syl 14 |
. 2
⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑃 − (𝑘 · 2)) mod 𝑃)) |
9 | 1 | eldifad 3164 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℙ) |
10 | | prmz 12236 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
11 | 9, 10 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℤ) |
12 | | 4nn 9135 |
. . . . . . . 8
⊢ 4 ∈
ℕ |
13 | | znq 9679 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧ 4 ∈
ℕ) → (𝑃 / 4)
∈ ℚ) |
14 | 11, 12, 13 | sylancl 413 |
. . . . . . 7
⊢ (𝜑 → (𝑃 / 4) ∈ ℚ) |
15 | 14 | flqcld 10336 |
. . . . . 6
⊢ (𝜑 → (⌊‘(𝑃 / 4)) ∈
ℤ) |
16 | 4, 15 | eqeltrid 2280 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
17 | 16 | peano2zd 9432 |
. . . 4
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) |
18 | 1, 2 | gausslemma2dlem0b 15108 |
. . . . 5
⊢ (𝜑 → 𝐻 ∈ ℕ) |
19 | 18 | nnzd 9428 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ ℤ) |
20 | 17, 19 | fzfigd 10492 |
. . 3
⊢ (𝜑 → ((𝑀 + 1)...𝐻) ∈ Fin) |
21 | 10 | adantr 276 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → 𝑃 ∈ ℤ) |
22 | | elfzelz 10081 |
. . . . . . 7
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 𝑘 ∈ ℤ) |
23 | | 2z 9335 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
24 | 23 | a1i 9 |
. . . . . . 7
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 2 ∈ ℤ) |
25 | 22, 24 | zmulcld 9435 |
. . . . . 6
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (𝑘 · 2) ∈ ℤ) |
26 | 25 | adantl 277 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑘 · 2) ∈ ℤ) |
27 | 21, 26 | zsubcld 9434 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑃 − (𝑘 · 2)) ∈
ℤ) |
28 | 9, 27 | sylan 283 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑃 − (𝑘 · 2)) ∈
ℤ) |
29 | | neg1z 9339 |
. . . . . 6
⊢ -1 ∈
ℤ |
30 | 29 | a1i 9 |
. . . . 5
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → -1 ∈ ℤ) |
31 | 30, 25 | zmulcld 9435 |
. . . 4
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (-1 · (𝑘 · 2)) ∈
ℤ) |
32 | 31 | adantl 277 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (-1 · (𝑘 · 2)) ∈
ℤ) |
33 | | prmnn 12235 |
. . . 4
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
34 | 9, 33 | syl 14 |
. . 3
⊢ (𝜑 → 𝑃 ∈ ℕ) |
35 | 25 | zcnd 9430 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (𝑘 · 2) ∈ ℂ) |
36 | 35 | mulm1d 8419 |
. . . . . . 7
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (-1 · (𝑘 · 2)) = -(𝑘 · 2)) |
37 | 36 | adantl 277 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (-1 · (𝑘 · 2)) = -(𝑘 · 2)) |
38 | 37 | oveq1d 5925 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → ((-1 · (𝑘 · 2)) mod 𝑃) = (-(𝑘 · 2) mod 𝑃)) |
39 | | zq 9681 |
. . . . . . 7
⊢ ((𝑘 · 2) ∈ ℤ
→ (𝑘 · 2)
∈ ℚ) |
40 | 26, 39 | syl 14 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑘 · 2) ∈ ℚ) |
41 | | zq 9681 |
. . . . . . 7
⊢ (𝑃 ∈ ℤ → 𝑃 ∈
ℚ) |
42 | 21, 41 | syl 14 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → 𝑃 ∈ ℚ) |
43 | 33 | nngt0d 9016 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 0 <
𝑃) |
44 | 43 | adantr 276 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → 0 < 𝑃) |
45 | | qnegmod 10430 |
. . . . . 6
⊢ (((𝑘 · 2) ∈ ℚ
∧ 𝑃 ∈ ℚ
∧ 0 < 𝑃) →
(-(𝑘 · 2) mod 𝑃) = ((𝑃 − (𝑘 · 2)) mod 𝑃)) |
46 | 40, 42, 44, 45 | syl3anc 1249 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (-(𝑘 · 2) mod 𝑃) = ((𝑃 − (𝑘 · 2)) mod 𝑃)) |
47 | 38, 46 | eqtr2d 2227 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → ((𝑃 − (𝑘 · 2)) mod 𝑃) = ((-1 · (𝑘 · 2)) mod 𝑃)) |
48 | 9, 47 | sylan 283 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → ((𝑃 − (𝑘 · 2)) mod 𝑃) = ((-1 · (𝑘 · 2)) mod 𝑃)) |
49 | 20, 28, 32, 34, 48 | fprodmodd 11771 |
. 2
⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑃 − (𝑘 · 2)) mod 𝑃) = (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(-1 · (𝑘 · 2)) mod 𝑃)) |
50 | 8, 49 | eqtrd 2226 |
1
⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(-1 · (𝑘 · 2)) mod 𝑃)) |