| 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 27413 | . . 3
⊢ (𝜑 → (!‘𝐻) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘))) | 
| 6 | 5 | oveq1d 7446 | . 2
⊢ (𝜑 → ((!‘𝐻) mod 𝑃) = ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)) mod 𝑃)) | 
| 7 |  | fzfid 14014 | . . . 4
⊢ (𝜑 → (1...𝑀) ∈ Fin) | 
| 8 | 1, 2, 3, 4 | gausslemma2dlem2 27411 | . . . . . 6
⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2)) | 
| 9 | 8 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2)) | 
| 10 |  | rspa 3248 | . . . . . . . 8
⊢
((∀𝑘 ∈
(1...𝑀)(𝑅‘𝑘) = (𝑘 · 2) ∧ 𝑘 ∈ (1...𝑀)) → (𝑅‘𝑘) = (𝑘 · 2)) | 
| 11 | 10 | expcom 413 | . . . . . . 7
⊢ (𝑘 ∈ (1...𝑀) → (∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2) → (𝑅‘𝑘) = (𝑘 · 2))) | 
| 12 | 11 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2) → (𝑅‘𝑘) = (𝑘 · 2))) | 
| 13 |  | elfzelz 13564 | . . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ ℤ) | 
| 14 |  | 2z 12649 | . . . . . . . . . 10
⊢ 2 ∈
ℤ | 
| 15 | 14 | a1i 11 | . . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑀) → 2 ∈ ℤ) | 
| 16 | 13, 15 | zmulcld 12728 | . . . . . . . 8
⊢ (𝑘 ∈ (1...𝑀) → (𝑘 · 2) ∈ ℤ) | 
| 17 | 16 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝑘 · 2) ∈ ℤ) | 
| 18 |  | eleq1 2829 | . . . . . . 7
⊢ ((𝑅‘𝑘) = (𝑘 · 2) → ((𝑅‘𝑘) ∈ ℤ ↔ (𝑘 · 2) ∈
ℤ)) | 
| 19 | 17, 18 | syl5ibrcom 247 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑅‘𝑘) = (𝑘 · 2) → (𝑅‘𝑘) ∈ ℤ)) | 
| 20 | 12, 19 | syld 47 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (∀𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = (𝑘 · 2) → (𝑅‘𝑘) ∈ ℤ)) | 
| 21 | 9, 20 | mpd 15 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝑅‘𝑘) ∈ ℤ) | 
| 22 | 7, 21 | fprodzcl 15990 | . . 3
⊢ (𝜑 → ∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) ∈ ℤ) | 
| 23 |  | fzfid 14014 | . . . . 5
⊢ (𝜑 → ((𝑀 + 1)...𝐻) ∈ Fin) | 
| 24 | 1, 2, 3, 4 | gausslemma2dlem3 27412 | . . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2))) | 
| 25 | 24 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → ∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2))) | 
| 26 |  | rspa 3248 | . . . . . . . . 9
⊢
((∀𝑘 ∈
((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2)) ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑅‘𝑘) = (𝑃 − (𝑘 · 2))) | 
| 27 | 26 | expcom 413 | . . . . . . . 8
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2)) → (𝑅‘𝑘) = (𝑃 − (𝑘 · 2)))) | 
| 28 | 27 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2)) → (𝑅‘𝑘) = (𝑃 − (𝑘 · 2)))) | 
| 29 | 1 | gausslemma2dlem0a 27400 | . . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℕ) | 
| 30 | 29 | nnzd 12640 | . . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℤ) | 
| 31 |  | elfzelz 13564 | . . . . . . . . . 10
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 𝑘 ∈ ℤ) | 
| 32 | 14 | a1i 11 | . . . . . . . . . 10
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → 2 ∈ ℤ) | 
| 33 | 31, 32 | zmulcld 12728 | . . . . . . . . 9
⊢ (𝑘 ∈ ((𝑀 + 1)...𝐻) → (𝑘 · 2) ∈ ℤ) | 
| 34 |  | zsubcl 12659 | . . . . . . . . 9
⊢ ((𝑃 ∈ ℤ ∧ (𝑘 · 2) ∈ ℤ)
→ (𝑃 − (𝑘 · 2)) ∈
ℤ) | 
| 35 | 30, 33, 34 | syl2an 596 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑃 − (𝑘 · 2)) ∈
ℤ) | 
| 36 |  | eleq1 2829 | . . . . . . . 8
⊢ ((𝑅‘𝑘) = (𝑃 − (𝑘 · 2)) → ((𝑅‘𝑘) ∈ ℤ ↔ (𝑃 − (𝑘 · 2)) ∈
ℤ)) | 
| 37 | 35, 36 | syl5ibrcom 247 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → ((𝑅‘𝑘) = (𝑃 − (𝑘 · 2)) → (𝑅‘𝑘) ∈ ℤ)) | 
| 38 | 28, 37 | syld 47 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (∀𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) = (𝑃 − (𝑘 · 2)) → (𝑅‘𝑘) ∈ ℤ)) | 
| 39 | 25, 38 | mpd 15 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑅‘𝑘) ∈ ℤ) | 
| 40 | 23, 39 | fprodzcl 15990 | . . . 4
⊢ (𝜑 → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) ∈ ℤ) | 
| 41 | 40 | zred 12722 | . . 3
⊢ (𝜑 → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) ∈ ℝ) | 
| 42 |  | nnoddn2prm 16849 | . . . 4
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∈ ℕ
∧ ¬ 2 ∥ 𝑃)) | 
| 43 |  | nnrp 13046 | . . . . 5
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ+) | 
| 44 | 43 | adantr 480 | . . . 4
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → 𝑃 ∈
ℝ+) | 
| 45 | 1, 42, 44 | 3syl 18 | . . 3
⊢ (𝜑 → 𝑃 ∈
ℝ+) | 
| 46 |  | modmulmodr 13978 | . . . 4
⊢
((∏𝑘 ∈
(1...𝑀)(𝑅‘𝑘) ∈ ℤ ∧ ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) ∈ ℝ ∧ 𝑃 ∈ ℝ+) →
((∏𝑘 ∈
(1...𝑀)(𝑅‘𝑘) · (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃)) mod 𝑃) = ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)) mod 𝑃)) | 
| 47 | 46 | eqcomd 2743 | . . 3
⊢
((∏𝑘 ∈
(1...𝑀)(𝑅‘𝑘) ∈ ℤ ∧ ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) ∈ ℝ ∧ 𝑃 ∈ ℝ+) →
((∏𝑘 ∈
(1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)) mod 𝑃) = ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃)) mod 𝑃)) | 
| 48 | 22, 41, 45, 47 | syl3anc 1373 | . 2
⊢ (𝜑 → ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘)) mod 𝑃) = ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃)) mod 𝑃)) | 
| 49 |  | gausslemma2d.n | . . . . . 6
⊢ 𝑁 = (𝐻 − 𝑀) | 
| 50 | 1, 2, 3, 4, 49 | gausslemma2dlem5 27415 | . . . . 5
⊢ (𝜑 → (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃) = (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃)) | 
| 51 | 50 | oveq2d 7447 | . . . 4
⊢ (𝜑 → (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃)) = (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃))) | 
| 52 | 51 | oveq1d 7446 | . . 3
⊢ (𝜑 → ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃)) mod 𝑃) = ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃)) mod 𝑃)) | 
| 53 |  | neg1rr 12381 | . . . . . . 7
⊢ -1 ∈
ℝ | 
| 54 | 53 | a1i 11 | . . . . . 6
⊢ (𝜑 → -1 ∈
ℝ) | 
| 55 | 1, 4, 2, 49 | gausslemma2dlem0h 27407 | . . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 56 | 54, 55 | reexpcld 14203 | . . . . 5
⊢ (𝜑 → (-1↑𝑁) ∈ ℝ) | 
| 57 | 31 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → 𝑘 ∈ ℤ) | 
| 58 | 14 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → 2 ∈ ℤ) | 
| 59 | 57, 58 | zmulcld 12728 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)...𝐻)) → (𝑘 · 2) ∈ ℤ) | 
| 60 | 23, 59 | fprodzcl 15990 | . . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2) ∈ ℤ) | 
| 61 | 60 | zred 12722 | . . . . 5
⊢ (𝜑 → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2) ∈ ℝ) | 
| 62 | 56, 61 | remulcld 11291 | . . . 4
⊢ (𝜑 → ((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) ∈
ℝ) | 
| 63 |  | modmulmodr 13978 | . . . 4
⊢
((∏𝑘 ∈
(1...𝑀)(𝑅‘𝑘) ∈ ℤ ∧ ((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) ∈ ℝ ∧ 𝑃 ∈ ℝ+)
→ ((∏𝑘 ∈
(1...𝑀)(𝑅‘𝑘) · (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃)) mod 𝑃) = ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) mod 𝑃)) | 
| 64 | 22, 62, 45, 63 | syl3anc 1373 | . . 3
⊢ (𝜑 → ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · (((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) mod 𝑃)) mod 𝑃) = ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) mod 𝑃)) | 
| 65 | 8 | prodeq2d 15957 | . . . . . . . 8
⊢ (𝜑 → ∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) = ∏𝑘 ∈ (1...𝑀)(𝑘 · 2)) | 
| 66 | 65 | oveq1d 7446 | . . . . . . 7
⊢ (𝜑 → (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) = (∏𝑘 ∈ (1...𝑀)(𝑘 · 2) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) | 
| 67 |  | fzfid 14014 | . . . . . . . . 9
⊢ (𝜑 → (1...𝐻) ∈ Fin) | 
| 68 |  | elfzelz 13564 | . . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝐻) → 𝑘 ∈ ℤ) | 
| 69 | 68 | zcnd 12723 | . . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝐻) → 𝑘 ∈ ℂ) | 
| 70 | 69 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → 𝑘 ∈ ℂ) | 
| 71 |  | 2cn 12341 | . . . . . . . . . 10
⊢ 2 ∈
ℂ | 
| 72 | 71 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → 2 ∈ ℂ) | 
| 73 | 67, 70, 72 | fprodmul 15996 | . . . . . . . 8
⊢ (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑘 · 2) = (∏𝑘 ∈ (1...𝐻)𝑘 · ∏𝑘 ∈ (1...𝐻)2)) | 
| 74 | 1, 4 | gausslemma2dlem0d 27403 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈
ℕ0) | 
| 75 | 74 | nn0red 12588 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 76 | 75 | ltp1d 12198 | . . . . . . . . . 10
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) | 
| 77 |  | fzdisj 13591 | . . . . . . . . . 10
⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝐻)) = ∅) | 
| 78 | 76, 77 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝐻)) = ∅) | 
| 79 |  | 1zzd 12648 | . . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℤ) | 
| 80 |  | nn0pzuz 12947 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 1 ∈ ℤ) → (𝑀 + 1) ∈
(ℤ≥‘1)) | 
| 81 | 74, 79, 80 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (𝑀 + 1) ∈
(ℤ≥‘1)) | 
| 82 | 74 | nn0zd 12639 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 83 | 1, 2 | gausslemma2dlem0b 27401 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ∈ ℕ) | 
| 84 | 83 | nnzd 12640 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈ ℤ) | 
| 85 | 1, 4, 2 | gausslemma2dlem0g 27406 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ≤ 𝐻) | 
| 86 |  | eluz2 12884 | . . . . . . . . . . 11
⊢ (𝐻 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑀 ≤ 𝐻)) | 
| 87 | 82, 84, 85, 86 | syl3anbrc 1344 | . . . . . . . . . 10
⊢ (𝜑 → 𝐻 ∈ (ℤ≥‘𝑀)) | 
| 88 |  | fzsplit2 13589 | . . . . . . . . . 10
⊢ (((𝑀 + 1) ∈
(ℤ≥‘1) ∧ 𝐻 ∈ (ℤ≥‘𝑀)) → (1...𝐻) = ((1...𝑀) ∪ ((𝑀 + 1)...𝐻))) | 
| 89 | 81, 87, 88 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (1...𝐻) = ((1...𝑀) ∪ ((𝑀 + 1)...𝐻))) | 
| 90 | 14 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝐻) → 2 ∈ ℤ) | 
| 91 | 68, 90 | zmulcld 12728 | . . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝐻) → (𝑘 · 2) ∈ ℤ) | 
| 92 | 91 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑘 · 2) ∈ ℤ) | 
| 93 | 92 | zcnd 12723 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐻)) → (𝑘 · 2) ∈ ℂ) | 
| 94 | 78, 89, 67, 93 | fprodsplit 16002 | . . . . . . . 8
⊢ (𝜑 → ∏𝑘 ∈ (1...𝐻)(𝑘 · 2) = (∏𝑘 ∈ (1...𝑀)(𝑘 · 2) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) | 
| 95 |  | nnnn0 12533 | . . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℕ0) | 
| 96 | 95 | anim1i 615 | . . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℕ ∧ ¬ 2
∥ 𝑃) → (𝑃 ∈ ℕ0
∧ ¬ 2 ∥ 𝑃)) | 
| 97 | 42, 96 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∈
ℕ0 ∧ ¬ 2 ∥ 𝑃)) | 
| 98 |  | nn0oddm1d2 16422 | . . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℕ0
→ (¬ 2 ∥ 𝑃
↔ ((𝑃 − 1) / 2)
∈ ℕ0)) | 
| 99 | 98 | biimpa 476 | . . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℕ0
∧ ¬ 2 ∥ 𝑃)
→ ((𝑃 − 1) / 2)
∈ ℕ0) | 
| 100 | 2, 99 | eqeltrid 2845 | . . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℕ0
∧ ¬ 2 ∥ 𝑃)
→ 𝐻 ∈
ℕ0) | 
| 101 | 1, 97, 100 | 3syl 18 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ∈
ℕ0) | 
| 102 |  | fprodfac 16009 | . . . . . . . . . . . 12
⊢ (𝐻 ∈ ℕ0
→ (!‘𝐻) =
∏𝑘 ∈ (1...𝐻)𝑘) | 
| 103 | 101, 102 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (!‘𝐻) = ∏𝑘 ∈ (1...𝐻)𝑘) | 
| 104 | 103 | eqcomd 2743 | . . . . . . . . . 10
⊢ (𝜑 → ∏𝑘 ∈ (1...𝐻)𝑘 = (!‘𝐻)) | 
| 105 |  | fzfi 14013 | . . . . . . . . . . . 12
⊢
(1...𝐻) ∈
Fin | 
| 106 | 105, 71 | pm3.2i 470 | . . . . . . . . . . 11
⊢
((1...𝐻) ∈ Fin
∧ 2 ∈ ℂ) | 
| 107 |  | fprodconst 16014 | . . . . . . . . . . 11
⊢
(((1...𝐻) ∈ Fin
∧ 2 ∈ ℂ) → ∏𝑘 ∈ (1...𝐻)2 = (2↑(♯‘(1...𝐻)))) | 
| 108 | 106, 107 | mp1i 13 | . . . . . . . . . 10
⊢ (𝜑 → ∏𝑘 ∈ (1...𝐻)2 = (2↑(♯‘(1...𝐻)))) | 
| 109 | 104, 108 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝜑 → (∏𝑘 ∈ (1...𝐻)𝑘 · ∏𝑘 ∈ (1...𝐻)2) = ((!‘𝐻) · (2↑(♯‘(1...𝐻))))) | 
| 110 |  | hashfz1 14385 | . . . . . . . . . . . 12
⊢ (𝐻 ∈ ℕ0
→ (♯‘(1...𝐻)) = 𝐻) | 
| 111 | 101, 110 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (♯‘(1...𝐻)) = 𝐻) | 
| 112 | 111 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝜑 →
(2↑(♯‘(1...𝐻))) = (2↑𝐻)) | 
| 113 | 112 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝜑 → ((!‘𝐻) ·
(2↑(♯‘(1...𝐻)))) = ((!‘𝐻) · (2↑𝐻))) | 
| 114 | 101 | faccld 14323 | . . . . . . . . . . 11
⊢ (𝜑 → (!‘𝐻) ∈ ℕ) | 
| 115 | 114 | nncnd 12282 | . . . . . . . . . 10
⊢ (𝜑 → (!‘𝐻) ∈ ℂ) | 
| 116 |  | 2nn0 12543 | . . . . . . . . . . 11
⊢ 2 ∈
ℕ0 | 
| 117 |  | nn0expcl 14116 | . . . . . . . . . . . 12
⊢ ((2
∈ ℕ0 ∧ 𝐻 ∈ ℕ0) →
(2↑𝐻) ∈
ℕ0) | 
| 118 | 117 | nn0cnd 12589 | . . . . . . . . . . 11
⊢ ((2
∈ ℕ0 ∧ 𝐻 ∈ ℕ0) →
(2↑𝐻) ∈
ℂ) | 
| 119 | 116, 101,
118 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → (2↑𝐻) ∈ ℂ) | 
| 120 | 115, 119 | mulcomd 11282 | . . . . . . . . 9
⊢ (𝜑 → ((!‘𝐻) · (2↑𝐻)) = ((2↑𝐻) · (!‘𝐻))) | 
| 121 | 109, 113,
120 | 3eqtrd 2781 | . . . . . . . 8
⊢ (𝜑 → (∏𝑘 ∈ (1...𝐻)𝑘 · ∏𝑘 ∈ (1...𝐻)2) = ((2↑𝐻) · (!‘𝐻))) | 
| 122 | 73, 94, 121 | 3eqtr3d 2785 | . . . . . . 7
⊢ (𝜑 → (∏𝑘 ∈ (1...𝑀)(𝑘 · 2) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) = ((2↑𝐻) · (!‘𝐻))) | 
| 123 | 66, 122 | eqtrd 2777 | . . . . . 6
⊢ (𝜑 → (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)) = ((2↑𝐻) · (!‘𝐻))) | 
| 124 | 123 | oveq2d 7447 | . . . . 5
⊢ (𝜑 → ((-1↑𝑁) · (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) = ((-1↑𝑁) · ((2↑𝐻) · (!‘𝐻)))) | 
| 125 | 22 | zcnd 12723 | . . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) ∈ ℂ) | 
| 126 | 56 | recnd 11289 | . . . . . 6
⊢ (𝜑 → (-1↑𝑁) ∈ ℂ) | 
| 127 | 60 | zcnd 12723 | . . . . . 6
⊢ (𝜑 → ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2) ∈ ℂ) | 
| 128 | 125, 126,
127 | mul12d 11470 | . . . . 5
⊢ (𝜑 → (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) = ((-1↑𝑁) · (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2)))) | 
| 129 | 126, 119,
115 | mulassd 11284 | . . . . 5
⊢ (𝜑 → (((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) = ((-1↑𝑁) · ((2↑𝐻) · (!‘𝐻)))) | 
| 130 | 124, 128,
129 | 3eqtr4d 2787 | . . . 4
⊢ (𝜑 → (∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) = (((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻))) | 
| 131 | 130 | oveq1d 7446 | . . 3
⊢ (𝜑 → ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · ((-1↑𝑁) · ∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑘 · 2))) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃)) | 
| 132 | 52, 64, 131 | 3eqtrd 2781 | . 2
⊢ (𝜑 → ((∏𝑘 ∈ (1...𝑀)(𝑅‘𝑘) · (∏𝑘 ∈ ((𝑀 + 1)...𝐻)(𝑅‘𝑘) mod 𝑃)) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃)) | 
| 133 | 6, 48, 132 | 3eqtrd 2781 | 1
⊢ (𝜑 → ((!‘𝐻) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃)) |