Proof of Theorem gausslemma2dlem5
Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.p |
. . 3
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
2 | | gausslemma2d.h |
. . 3
⊢ 𝐻 = ((𝑃 − 1) / 2) |
3 | | gausslemma2d.r |
. . 3
⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))) |
4 | | gausslemma2d.m |
. . 3
⊢ 𝑀 = (⌊‘(𝑃 / 4)) |
5 | 1, 2, 3, 4 | gausslemma2dlem5a 15123 |
. 2
⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(-1 · (𝑘 · 2)) mod 𝑃)) |
6 | 1 | gausslemma2dlem0a 15107 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ ℕ) |
7 | 6 | nnzd 9428 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℤ) |
8 | | 4nn 9135 |
. . . . . . . . . 10
⊢ 4 ∈
ℕ |
9 | | znq 9679 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℤ ∧ 4 ∈
ℕ) → (𝑃 / 4)
∈ ℚ) |
10 | 7, 8, 9 | sylancl 413 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 / 4) ∈ ℚ) |
11 | 10 | flqcld 10336 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(𝑃 / 4)) ∈
ℤ) |
12 | 4, 11 | eqeltrid 2280 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) |
13 | 12 | peano2zd 9432 |
. . . . . 6
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) |
14 | 1, 2 | gausslemma2dlem0b 15108 |
. . . . . . 7
⊢ (𝜑 → 𝐻 ∈ ℕ) |
15 | 14 | nnzd 9428 |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ ℤ) |
16 | 13, 15 | fzfigd 10492 |
. . . . 5
⊢ (𝜑 → ((𝑀 + 1)...𝐻) ∈ Fin) |
17 | | neg1cn 9077 |
. . . . . 6
⊢ -1 ∈
ℂ |
18 | 17 | a1i 9 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → -1 ∈
ℂ) |
19 | | elfzelz 10081 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 𝑘 ∈ ℤ) |
20 | | 2z 9335 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
21 | 20 | a1i 9 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 2 ∈ ℤ) |
22 | 19, 21 | zmulcld 9435 |
. . . . . . 7
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (𝑘 · 2) ∈ ℤ) |
23 | 22 | zcnd 9430 |
. . . . . 6
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (𝑘 · 2) ∈ ℂ) |
24 | 23 | adantl 277 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑘 · 2) ∈ ℂ) |
25 | 16, 18, 24 | fprodmul 11721 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(-1 · (𝑘 · 2)) = (∏𝑘 ∈ ((𝑀 + 1)...𝐻)-1 · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) |
26 | | fprodconst 11750 |
. . . . . . 7
⊢ ((((𝑀 + 1)...𝐻) ∈ Fin ∧ -1 ∈ ℂ) →
∏𝑘 ∈ ((𝑀 + 1)...𝐻)-1 = (-1↑(♯‘((𝑀 + 1)...𝐻)))) |
27 | 16, 17, 26 | sylancl 413 |
. . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)-1 = (-1↑(♯‘((𝑀 + 1)...𝐻)))) |
28 | | nnoddn2prm 12385 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∈ ℕ
∧ ¬ 2 ∥ 𝑃)) |
29 | | nnz 9326 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℤ) |
30 | | oddm1d2 12020 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℤ → (¬ 2
∥ 𝑃 ↔ ((𝑃 − 1) / 2) ∈
ℤ)) |
31 | 29, 30 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℕ → (¬ 2
∥ 𝑃 ↔ ((𝑃 − 1) / 2) ∈
ℤ)) |
32 | 31 | biimpa 296 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → ((𝑃 − 1) / 2) ∈
ℤ) |
33 | 1, 28, 32 | 3syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℤ) |
34 | 2, 33 | eqeltrid 2280 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 ∈ ℤ) |
35 | 1, 4, 2 | gausslemma2dlem0f 15112 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 + 1) ≤ 𝐻) |
36 | | eluz2 9588 |
. . . . . . . . . 10
⊢ (𝐻 ∈
(ℤ≥‘(𝑀 + 1)) ↔ ((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝐻)) |
37 | 13, 34, 35, 36 | syl3anbrc 1183 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻 ∈ (ℤ≥‘(𝑀 + 1))) |
38 | | hashfz 10879 |
. . . . . . . . 9
⊢ (𝐻 ∈
(ℤ≥‘(𝑀 + 1)) → (♯‘((𝑀 + 1)...𝐻)) = ((𝐻 − (𝑀 + 1)) + 1)) |
39 | 37, 38 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → (♯‘((𝑀 + 1)...𝐻)) = ((𝐻 − (𝑀 + 1)) + 1)) |
40 | 34 | zcnd 9430 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 ∈ ℂ) |
41 | 12 | zcnd 9430 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℂ) |
42 | | 1cnd 8025 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℂ) |
43 | 40, 41, 42 | nppcan2d 8346 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐻 − (𝑀 + 1)) + 1) = (𝐻 − 𝑀)) |
44 | | gausslemma2d.n |
. . . . . . . . 9
⊢ 𝑁 = (𝐻 − 𝑀) |
45 | 43, 44 | eqtr4di 2244 |
. . . . . . . 8
⊢ (𝜑 → ((𝐻 − (𝑀 + 1)) + 1) = 𝑁) |
46 | 39, 45 | eqtrd 2226 |
. . . . . . 7
⊢ (𝜑 → (♯‘((𝑀 + 1)...𝐻)) = 𝑁) |
47 | 46 | oveq2d 5926 |
. . . . . 6
⊢ (𝜑 →
(-1↑(♯‘((𝑀
+ 1)...𝐻))) =
(-1↑𝑁)) |
48 | 27, 47 | eqtrd 2226 |
. . . . 5
⊢ (𝜑 → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)-1 = (-1↑𝑁)) |
49 | 48 | oveq1d 5925 |
. . . 4
⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)-1 · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) = ((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) |
50 | 25, 49 | eqtrd 2226 |
. . 3
⊢ (𝜑 → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(-1 · (𝑘 · 2)) = ((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) |
51 | 50 | oveq1d 5925 |
. 2
⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(-1 · (𝑘 · 2)) mod 𝑃) = (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃)) |
52 | 5, 51 | eqtrd 2226 |
1
⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃)) |