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 26516 |
. 2
⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(-1 · (𝑘 · 2)) mod 𝑃)) |
6 | | fzfi 13690 |
. . . . . 6
⊢ ((𝑀 + 1)...𝐻) ∈ Fin |
7 | 6 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((𝑀 + 1)...𝐻) ∈ Fin) |
8 | | neg1cn 12087 |
. . . . . 6
⊢ -1 ∈
ℂ |
9 | 8 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → -1 ∈
ℂ) |
10 | | elfzelz 13255 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 𝑘 ∈ ℤ) |
11 | | 2z 12352 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
12 | 11 | a1i 11 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 2 ∈ ℤ) |
13 | 10, 12 | zmulcld 12431 |
. . . . . . 7
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (𝑘 · 2) ∈ ℤ) |
14 | 13 | zcnd 12426 |
. . . . . 6
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (𝑘 · 2) ∈ ℂ) |
15 | 14 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑘 · 2) ∈ ℂ) |
16 | 7, 9, 15 | fprodmul 15668 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(-1 · (𝑘 · 2)) = (∏𝑘 ∈ ((𝑀 + 1)...𝐻)-1 · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) |
17 | 6, 8 | pm3.2i 471 |
. . . . . . 7
⊢ (((𝑀 + 1)...𝐻) ∈ Fin ∧ -1 ∈
ℂ) |
18 | | fprodconst 15686 |
. . . . . . 7
⊢ ((((𝑀 + 1)...𝐻) ∈ Fin ∧ -1 ∈ ℂ) →
∏𝑘 ∈ ((𝑀 + 1)...𝐻)-1 = (-1↑(♯‘((𝑀 + 1)...𝐻)))) |
19 | 17, 18 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)-1 = (-1↑(♯‘((𝑀 + 1)...𝐻)))) |
20 | | nnoddn2prm 16510 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∈ ℕ
∧ ¬ 2 ∥ 𝑃)) |
21 | | nnre 11980 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ) |
22 | 21 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → 𝑃 ∈
ℝ) |
23 | 1, 20, 22 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ ℝ) |
24 | | 4re 12057 |
. . . . . . . . . . . . . . 15
⊢ 4 ∈
ℝ |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 4 ∈
ℝ) |
26 | | 4ne0 12081 |
. . . . . . . . . . . . . . 15
⊢ 4 ≠
0 |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 4 ≠ 0) |
28 | 23, 25, 27 | redivcld 11803 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 / 4) ∈ ℝ) |
29 | 28 | flcld 13516 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⌊‘(𝑃 / 4)) ∈
ℤ) |
30 | 4, 29 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
31 | 30 | peano2zd 12428 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) |
32 | | nnz 12342 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℤ) |
33 | | oddm1d2 16067 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℤ → (¬ 2
∥ 𝑃 ↔ ((𝑃 − 1) / 2) ∈
ℤ)) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℕ → (¬ 2
∥ 𝑃 ↔ ((𝑃 − 1) / 2) ∈
ℤ)) |
35 | 34 | biimpa 477 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → ((𝑃 − 1) / 2) ∈
ℤ) |
36 | 1, 20, 35 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℤ) |
37 | 2, 36 | eqeltrid 2845 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 ∈ ℤ) |
38 | 1, 4, 2 | gausslemma2dlem0f 26507 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 + 1) ≤ 𝐻) |
39 | | eluz2 12587 |
. . . . . . . . . 10
⊢ (𝐻 ∈
(ℤ≥‘(𝑀 + 1)) ↔ ((𝑀 + 1) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝐻)) |
40 | 31, 37, 38, 39 | syl3anbrc 1342 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻 ∈ (ℤ≥‘(𝑀 + 1))) |
41 | | hashfz 14140 |
. . . . . . . . 9
⊢ (𝐻 ∈
(ℤ≥‘(𝑀 + 1)) → (♯‘((𝑀 + 1)...𝐻)) = ((𝐻 − (𝑀 + 1)) + 1)) |
42 | 40, 41 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (♯‘((𝑀 + 1)...𝐻)) = ((𝐻 − (𝑀 + 1)) + 1)) |
43 | 37 | zcnd 12426 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 ∈ ℂ) |
44 | 30 | zcnd 12426 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℂ) |
45 | | 1cnd 10971 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℂ) |
46 | 43, 44, 45 | nppcan2d 11358 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐻 − (𝑀 + 1)) + 1) = (𝐻 − 𝑀)) |
47 | | gausslemma2d.n |
. . . . . . . . 9
⊢ 𝑁 = (𝐻 − 𝑀) |
48 | 46, 47 | eqtr4di 2798 |
. . . . . . . 8
⊢ (𝜑 → ((𝐻 − (𝑀 + 1)) + 1) = 𝑁) |
49 | 42, 48 | eqtrd 2780 |
. . . . . . 7
⊢ (𝜑 → (♯‘((𝑀 + 1)...𝐻)) = 𝑁) |
50 | 49 | oveq2d 7287 |
. . . . . 6
⊢ (𝜑 →
(-1↑(♯‘((𝑀
+ 1)...𝐻))) =
(-1↑𝑁)) |
51 | 19, 50 | eqtrd 2780 |
. . . . 5
⊢ (𝜑 → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)-1 = (-1↑𝑁)) |
52 | 51 | oveq1d 7286 |
. . . 4
⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)-1 · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) = ((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) |
53 | 16, 52 | eqtrd 2780 |
. . 3
⊢ (𝜑 → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(-1 · (𝑘 · 2)) = ((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) |
54 | 53 | oveq1d 7286 |
. 2
⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(-1 · (𝑘 · 2)) mod 𝑃) = (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃)) |
55 | 5, 54 | eqtrd 2780 |
1
⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃)) |