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 | gausslemma2dlem4 15122 |
. . 3
⊢ (𝜑 → (!‘𝐻) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) |
6 | 5 | oveq1d 5925 |
. 2
⊢ (𝜑 → ((!‘𝐻) mod 𝑃) = ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)) mod 𝑃)) |
7 | | 1zzd 9334 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℤ) |
8 | 1 | gausslemma2dlem0a 15107 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℕ) |
9 | 8 | nnzd 9428 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℤ) |
10 | | 4nn 9135 |
. . . . . . . 8
⊢ 4 ∈
ℕ |
11 | | znq 9679 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧ 4 ∈
ℕ) → (𝑃 / 4)
∈ ℚ) |
12 | 9, 10, 11 | sylancl 413 |
. . . . . . 7
⊢ (𝜑 → (𝑃 / 4) ∈ ℚ) |
13 | 12 | flqcld 10336 |
. . . . . 6
⊢ (𝜑 → (⌊‘(𝑃 / 4)) ∈
ℤ) |
14 | 4, 13 | eqeltrid 2280 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
15 | 7, 14 | fzfigd 10492 |
. . . 4
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
16 | 1, 2, 3, 4 | gausslemma2dlem2 15120 |
. . . . . 6
⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2)) |
17 | 16 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2)) |
18 | | rspa 2542 |
. . . . . . . 8
⊢
((∀𝑘 ∈
(1...𝑀)(𝑅‘𝑘) = (𝑘 · 2) ∧ 𝑘 ∈ (1...𝑀)) → (𝑅‘𝑘) = (𝑘 · 2)) |
19 | 18 | expcom 116 |
. . . . . . 7
⊢ (𝑘 ∈ (1...𝑀) → (∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2) → (𝑅‘𝑘) = (𝑘 · 2))) |
20 | 19 | adantl 277 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2) → (𝑅‘𝑘) = (𝑘 · 2))) |
21 | | elfzelz 10081 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ ℤ) |
22 | | 2z 9335 |
. . . . . . . . . 10
⊢ 2 ∈
ℤ |
23 | 22 | a1i 9 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑀) → 2 ∈ ℤ) |
24 | 21, 23 | zmulcld 9435 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...𝑀) → (𝑘 · 2) ∈ ℤ) |
25 | 24 | adantl 277 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝑘 · 2) ∈ ℤ) |
26 | | eleq1 2256 |
. . . . . . 7
⊢ ((𝑅‘𝑘) = (𝑘 · 2) → ((𝑅‘𝑘) ∈ ℤ ↔ (𝑘 · 2) ∈
ℤ)) |
27 | 25, 26 | syl5ibrcom 157 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑅‘𝑘) = (𝑘 · 2) → (𝑅‘𝑘) ∈ ℤ)) |
28 | 20, 27 | syld 45 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2) → (𝑅‘𝑘) ∈ ℤ)) |
29 | 17, 28 | mpd 13 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝑅‘𝑘) ∈ ℤ) |
30 | 15, 29 | fprodzcl 11739 |
. . 3
⊢ (𝜑 → ∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) ∈ ℤ) |
31 | 14 | peano2zd 9432 |
. . . . . 6
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) |
32 | 1, 2 | gausslemma2dlem0b 15108 |
. . . . . . 7
⊢ (𝜑 → 𝐻 ∈ ℕ) |
33 | 32 | nnzd 9428 |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ ℤ) |
34 | 31, 33 | fzfigd 10492 |
. . . . 5
⊢ (𝜑 → ((𝑀 + 1)...𝐻) ∈ Fin) |
35 | 1, 2, 3, 4 | gausslemma2dlem3 15121 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2))) |
36 | 35 | adantr 276 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → ∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2))) |
37 | | rspa 2542 |
. . . . . . . . 9
⊢
((∀𝑘 ∈
((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2)) ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑅‘𝑘) = (𝑃 − (𝑘 · 2))) |
38 | 37 | expcom 116 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2)) → (𝑅‘𝑘) = (𝑃 − (𝑘 · 2)))) |
39 | 38 | adantl 277 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2)) → (𝑅‘𝑘) = (𝑃 − (𝑘 · 2)))) |
40 | | elfzelz 10081 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 𝑘 ∈ ℤ) |
41 | 22 | a1i 9 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 2 ∈ ℤ) |
42 | 40, 41 | zmulcld 9435 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (𝑘 · 2) ∈ ℤ) |
43 | | zsubcl 9348 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℤ ∧ (𝑘 · 2) ∈ ℤ)
→ (𝑃 − (𝑘 · 2)) ∈
ℤ) |
44 | 9, 42, 43 | syl2an 289 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑃 − (𝑘 · 2)) ∈
ℤ) |
45 | | eleq1 2256 |
. . . . . . . 8
⊢ ((𝑅‘𝑘) = (𝑃 − (𝑘 · 2)) → ((𝑅‘𝑘) ∈ ℤ ↔ (𝑃 − (𝑘 · 2)) ∈
ℤ)) |
46 | 44, 45 | syl5ibrcom 157 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → ((𝑅‘𝑘) = (𝑃 − (𝑘 · 2)) → (𝑅‘𝑘) ∈ ℤ)) |
47 | 39, 46 | syld 45 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2)) → (𝑅‘𝑘) ∈ ℤ)) |
48 | 36, 47 | mpd 13 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑅‘𝑘) ∈ ℤ) |
49 | 34, 48 | fprodzcl 11739 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) ∈ ℤ) |
50 | | zq 9681 |
. . . 4
⊢
(∏𝑘 ∈
((𝑀 + 1)...𝐻)(𝑅‘𝑘) ∈ ℤ → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) ∈ ℚ) |
51 | 49, 50 | syl 14 |
. . 3
⊢ (𝜑 → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) ∈ ℚ) |
52 | | nnq 9688 |
. . . 4
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℚ) |
53 | 8, 52 | syl 14 |
. . 3
⊢ (𝜑 → 𝑃 ∈ ℚ) |
54 | 8 | nngt0d 9016 |
. . 3
⊢ (𝜑 → 0 < 𝑃) |
55 | | modqmulmodr 10451 |
. . . 4
⊢
(((∏𝑘 ∈
(1...𝑀)(𝑅‘𝑘) ∈ ℤ ∧ ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) ∈ ℚ) ∧ (𝑃 ∈ ℚ ∧ 0 < 𝑃)) → ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃)) mod 𝑃) = ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)) mod 𝑃)) |
56 | 55 | eqcomd 2199 |
. . 3
⊢
(((∏𝑘 ∈
(1...𝑀)(𝑅‘𝑘) ∈ ℤ ∧ ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) ∈ ℚ) ∧ (𝑃 ∈ ℚ ∧ 0 < 𝑃)) → ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)) mod 𝑃) = ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃)) mod 𝑃)) |
57 | 30, 51, 53, 54, 56 | syl22anc 1250 |
. 2
⊢ (𝜑 → ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)) mod 𝑃) = ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃)) mod 𝑃)) |
58 | | gausslemma2d.n |
. . . . . 6
⊢ 𝑁 = (𝐻 − 𝑀) |
59 | 1, 2, 3, 4, 58 | gausslemma2dlem5 15124 |
. . . . 5
⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃)) |
60 | 59 | oveq2d 5926 |
. . . 4
⊢ (𝜑 → (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃)) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃))) |
61 | 60 | oveq1d 5925 |
. . 3
⊢ (𝜑 → ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃)) mod 𝑃) = ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃)) mod 𝑃)) |
62 | | neg1z 9339 |
. . . . . . 7
⊢ -1 ∈
ℤ |
63 | 1, 4, 2, 58 | gausslemma2dlem0h 15114 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
64 | | zexpcl 10612 |
. . . . . . 7
⊢ ((-1
∈ ℤ ∧ 𝑁
∈ ℕ0) → (-1↑𝑁) ∈ ℤ) |
65 | 62, 63, 64 | sylancr 414 |
. . . . . 6
⊢ (𝜑 → (-1↑𝑁) ∈ ℤ) |
66 | 40 | adantl 277 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → 𝑘 ∈ ℤ) |
67 | 22 | a1i 9 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → 2 ∈ ℤ) |
68 | 66, 67 | zmulcld 9435 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑘 · 2) ∈ ℤ) |
69 | 34, 68 | fprodzcl 11739 |
. . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2) ∈ ℤ) |
70 | 65, 69 | zmulcld 9435 |
. . . . 5
⊢ (𝜑 → ((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) ∈
ℤ) |
71 | | zq 9681 |
. . . . 5
⊢
(((-1↑𝑁)
· ∏𝑘 ∈
((𝑀 + 1)...𝐻)(𝑘 · 2)) ∈ ℤ →
((-1↑𝑁) ·
∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) ∈
ℚ) |
72 | 70, 71 | syl 14 |
. . . 4
⊢ (𝜑 → ((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) ∈
ℚ) |
73 | | modqmulmodr 10451 |
. . . 4
⊢
(((∏𝑘 ∈
(1...𝑀)(𝑅‘𝑘) ∈ ℤ ∧ ((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) ∈ ℚ) ∧ (𝑃 ∈ ℚ ∧ 0 <
𝑃)) → ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃)) mod 𝑃) = ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) mod 𝑃)) |
74 | 30, 72, 53, 54, 73 | syl22anc 1250 |
. . 3
⊢ (𝜑 → ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃)) mod 𝑃) = ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) mod 𝑃)) |
75 | 16 | prodeq2d 11695 |
. . . . . . . 8
⊢ (𝜑 → ∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = ∏𝑘 ∈ (1...𝑀)(𝑘 · 2)) |
76 | 75 | oveq1d 5925 |
. . . . . . 7
⊢ (𝜑 → (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) = (∏𝑘 ∈ (1...𝑀)(𝑘 · 2) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) |
77 | 7, 33 | fzfigd 10492 |
. . . . . . . . 9
⊢ (𝜑 → (1...𝐻) ∈ Fin) |
78 | | elfzelz 10081 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝐻) → 𝑘 ∈ ℤ) |
79 | 78 | zcnd 9430 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝐻) → 𝑘 ∈ ℂ) |
80 | 79 | adantl 277 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → 𝑘 ∈ ℂ) |
81 | | 2cnd 9045 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → 2 ∈ ℂ) |
82 | 77, 80, 81 | fprodmul 11721 |
. . . . . . . 8
⊢ (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑘 · 2) = (∏𝑘 ∈ (1...𝐻)𝑘 · ∏𝑘 ∈ (1...𝐻)2)) |
83 | 1, 4 | gausslemma2dlem0d 15110 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
84 | 83 | nn0red 9284 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) |
85 | 84 | ltp1d 8939 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
86 | | fzdisj 10108 |
. . . . . . . . . 10
⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝐻)) = ∅) |
87 | 85, 86 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝐻)) = ∅) |
88 | | nn0pzuz 9642 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 1 ∈ ℤ) → (𝑀 + 1) ∈
(ℤ≥‘1)) |
89 | 83, 7, 88 | syl2anc 411 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 + 1) ∈
(ℤ≥‘1)) |
90 | 83 | nn0zd 9427 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
91 | 1, 4, 2 | gausslemma2dlem0g 15113 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ≤ 𝐻) |
92 | | eluz2 9588 |
. . . . . . . . . . 11
⊢ (𝐻 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑀 ≤ 𝐻)) |
93 | 90, 33, 91, 92 | syl3anbrc 1183 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 ∈ (ℤ≥‘𝑀)) |
94 | | fzsplit2 10106 |
. . . . . . . . . 10
⊢ (((𝑀 + 1) ∈
(ℤ≥‘1) ∧ 𝐻 ∈ (ℤ≥‘𝑀)) → (1...𝐻) = ((1...𝑀) ∪ ((𝑀 + 1)...𝐻))) |
95 | 89, 93, 94 | syl2anc 411 |
. . . . . . . . 9
⊢ (𝜑 → (1...𝐻) = ((1...𝑀) ∪ ((𝑀 + 1)...𝐻))) |
96 | 22 | a1i 9 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝐻) → 2 ∈ ℤ) |
97 | 78, 96 | zmulcld 9435 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝐻) → (𝑘 · 2) ∈ ℤ) |
98 | 97 | adantl 277 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑘 · 2) ∈ ℤ) |
99 | 98 | zcnd 9430 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑘 · 2) ∈ ℂ) |
100 | 87, 95, 77, 99 | fprodsplit 11727 |
. . . . . . . 8
⊢ (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑘 · 2) = (∏𝑘 ∈ (1...𝑀)(𝑘 · 2) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) |
101 | | nnoddn2prm 12385 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∈ ℕ
∧ ¬ 2 ∥ 𝑃)) |
102 | | nnnn0 9237 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℕ0) |
103 | 102 | anim1i 340 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → (𝑃 ∈ ℕ0
∧ ¬ 2 ∥ 𝑃)) |
104 | 101, 103 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∈
ℕ0 ∧ ¬ 2 ∥ 𝑃)) |
105 | | nn0oddm1d2 12037 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℕ0
→ (¬ 2 ∥ 𝑃
↔ ((𝑃 − 1) / 2)
∈ ℕ0)) |
106 | 105 | biimpa 296 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℕ0
∧ ¬ 2 ∥ 𝑃)
→ ((𝑃 − 1) / 2)
∈ ℕ0) |
107 | 2, 106 | eqeltrid 2280 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℕ0
∧ ¬ 2 ∥ 𝑃)
→ 𝐻 ∈
ℕ0) |
108 | 1, 104, 107 | 3syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ∈
ℕ0) |
109 | | fprodfac 11745 |
. . . . . . . . . . . 12
⊢ (𝐻 ∈ ℕ0
→ (!‘𝐻) =
∏𝑘 ∈ (1...𝐻)𝑘) |
110 | 108, 109 | syl 14 |
. . . . . . . . . . 11
⊢ (𝜑 → (!‘𝐻) = ∏𝑘 ∈ (1...𝐻)𝑘) |
111 | 110 | eqcomd 2199 |
. . . . . . . . . 10
⊢ (𝜑 → ∏𝑘 ∈ (1...𝐻)𝑘 = (!‘𝐻)) |
112 | | 2cn 9043 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
113 | | fprodconst 11750 |
. . . . . . . . . . 11
⊢
(((1...𝐻) ∈ Fin
∧ 2 ∈ ℂ) → ∏𝑘 ∈ (1...𝐻)2 = (2↑(♯‘(1...𝐻)))) |
114 | 77, 112, 113 | sylancl 413 |
. . . . . . . . . 10
⊢ (𝜑 → ∏𝑘 ∈ (1...𝐻)2 = (2↑(♯‘(1...𝐻)))) |
115 | 111, 114 | oveq12d 5928 |
. . . . . . . . 9
⊢ (𝜑 → (∏𝑘 ∈ (1...𝐻)𝑘 · ∏𝑘 ∈ (1...𝐻)2) = ((!‘𝐻) · (2↑(♯‘(1...𝐻))))) |
116 | | hashfz1 10841 |
. . . . . . . . . . . 12
⊢ (𝐻 ∈ ℕ0
→ (♯‘(1...𝐻)) = 𝐻) |
117 | 108, 116 | syl 14 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘(1...𝐻)) = 𝐻) |
118 | 117 | oveq2d 5926 |
. . . . . . . . . 10
⊢ (𝜑 →
(2↑(♯‘(1...𝐻))) = (2↑𝐻)) |
119 | 118 | oveq2d 5926 |
. . . . . . . . 9
⊢ (𝜑 → ((!‘𝐻) ·
(2↑(♯‘(1...𝐻)))) = ((!‘𝐻) · (2↑𝐻))) |
120 | 108 | faccld 10794 |
. . . . . . . . . . 11
⊢ (𝜑 → (!‘𝐻) ∈ ℕ) |
121 | 120 | nncnd 8986 |
. . . . . . . . . 10
⊢ (𝜑 → (!‘𝐻) ∈ ℂ) |
122 | | 2nn0 9247 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
123 | | nn0expcl 10611 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℕ0 ∧ 𝐻 ∈ ℕ0) →
(2↑𝐻) ∈
ℕ0) |
124 | 123 | nn0cnd 9285 |
. . . . . . . . . . 11
⊢ ((2
∈ ℕ0 ∧ 𝐻 ∈ ℕ0) →
(2↑𝐻) ∈
ℂ) |
125 | 122, 108,
124 | sylancr 414 |
. . . . . . . . . 10
⊢ (𝜑 → (2↑𝐻) ∈ ℂ) |
126 | 121, 125 | mulcomd 8031 |
. . . . . . . . 9
⊢ (𝜑 → ((!‘𝐻) · (2↑𝐻)) = ((2↑𝐻) · (!‘𝐻))) |
127 | 115, 119,
126 | 3eqtrd 2230 |
. . . . . . . 8
⊢ (𝜑 → (∏𝑘 ∈ (1...𝐻)𝑘 · ∏𝑘 ∈ (1...𝐻)2) = ((2↑𝐻) · (!‘𝐻))) |
128 | 82, 100, 127 | 3eqtr3d 2234 |
. . . . . . 7
⊢ (𝜑 → (∏𝑘 ∈ (1...𝑀)(𝑘 · 2) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) = ((2↑𝐻) · (!‘𝐻))) |
129 | 76, 128 | eqtrd 2226 |
. . . . . 6
⊢ (𝜑 → (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) = ((2↑𝐻) · (!‘𝐻))) |
130 | 129 | oveq2d 5926 |
. . . . 5
⊢ (𝜑 → ((-1↑𝑁) · (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) = ((-1↑𝑁) · ((2↑𝐻) · (!‘𝐻)))) |
131 | 30 | zcnd 9430 |
. . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) ∈ ℂ) |
132 | | neg1rr 9078 |
. . . . . . . . 9
⊢ -1 ∈
ℝ |
133 | 132 | a1i 9 |
. . . . . . . 8
⊢ (𝜑 → -1 ∈
ℝ) |
134 | 133, 63 | reexpcld 10748 |
. . . . . . 7
⊢ (𝜑 → (-1↑𝑁) ∈ ℝ) |
135 | 134 | recnd 8038 |
. . . . . 6
⊢ (𝜑 → (-1↑𝑁) ∈ ℂ) |
136 | 69 | zcnd 9430 |
. . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2) ∈ ℂ) |
137 | 131, 135,
136 | mul12d 8161 |
. . . . 5
⊢ (𝜑 → (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) = ((-1↑𝑁) · (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)))) |
138 | 135, 125,
121 | mulassd 8033 |
. . . . 5
⊢ (𝜑 → (((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) = ((-1↑𝑁) · ((2↑𝐻) · (!‘𝐻)))) |
139 | 130, 137,
138 | 3eqtr4d 2236 |
. . . 4
⊢ (𝜑 → (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) = (((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻))) |
140 | 139 | oveq1d 5925 |
. . 3
⊢ (𝜑 → ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃)) |
141 | 61, 74, 140 | 3eqtrd 2230 |
. 2
⊢ (𝜑 → ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃)) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃)) |
142 | 6, 57, 141 | 3eqtrd 2230 |
1
⊢ (𝜑 → ((!‘𝐻) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃)) |