Metamath Proof Explorer

Theorem gausslemma2dlem6

Description: Lemma 6 for gausslemma2d . (Contributed by AV, 16-Jun-2021)

Ref Expression
Hypotheses gausslemma2d.p ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
gausslemma2d.h ⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
gausslemma2d.r ⊢ 𝑅 = ( 𝑥 ∈ ( 1 ... 𝐻 ) ↦ if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
gausslemma2d.m ⊢ 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
gausslemma2d.n ⊢ 𝑁 = ( 𝐻 − 𝑀 )
Assertion gausslemma2dlem6 ( 𝜑 → ( ( ! ‘ 𝐻 ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) · ( ! ‘ 𝐻 ) ) mod 𝑃 ) )

Proof

Step Hyp Ref Expression
1 gausslemma2d.p ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
2 gausslemma2d.h ⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
3 gausslemma2d.r ⊢ 𝑅 = ( 𝑥 ∈ ( 1 ... 𝐻 ) ↦ if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
4 gausslemma2d.m ⊢ 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
5 gausslemma2d.n ⊢ 𝑁 = ( 𝐻 − 𝑀 )
6 1 2 3 4 gausslemma2dlem4 ⊢ ( 𝜑 → ( ! ‘ 𝐻 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) )
7 6 oveq1d ⊢ ( 𝜑 → ( ( ! ‘ 𝐻 ) mod 𝑃 ) = ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) mod 𝑃 ) )
8 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
9 1 2 3 4 gausslemma2dlem2 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) )
11 rspa ⊢ ( ( ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) )
12 11 expcom ⊢ ( 𝑘 ∈ ( 1 ... 𝑀 ) → ( ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) → ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) ) )
13 12 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) → ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) ) )
14 elfzelz ⊢ ( 𝑘 ∈ ( 1 ... 𝑀 ) → 𝑘 ∈ ℤ )
15 2z ⊢ 2 ∈ ℤ
16 15 a1i ⊢ ( 𝑘 ∈ ( 1 ... 𝑀 ) → 2 ∈ ℤ )
17 14 16 zmulcld ⊢ ( 𝑘 ∈ ( 1 ... 𝑀 ) → ( 𝑘 · 2 ) ∈ ℤ )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑘 · 2 ) ∈ ℤ )
19 eleq1 ⊢ ( ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) → ( ( 𝑅 ‘ 𝑘 ) ∈ ℤ ↔ ( 𝑘 · 2 ) ∈ ℤ ) )
20 18 19 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) → ( 𝑅 ‘ 𝑘 ) ∈ ℤ ) )
21 13 20 syld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑘 · 2 ) → ( 𝑅 ‘ 𝑘 ) ∈ ℤ ) )
22 10 21 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑅 ‘ 𝑘 ) ∈ ℤ )
23 8 22 fprodzcl ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) ∈ ℤ )
24 fzfid ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ... 𝐻 ) ∈ Fin )
25 1 2 3 4 gausslemma2dlem3 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ∀ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) )
27 rspa ⊢ ( ( ∀ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) )
28 27 expcom ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → ( ∀ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) → ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) ) )
29 28 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( ∀ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) → ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) ) )
30 1 gausslemma2dlem0a ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
31 30 nnzd ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
32 elfzelz ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → 𝑘 ∈ ℤ )
33 15 a1i ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → 2 ∈ ℤ )
34 32 33 zmulcld ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → ( 𝑘 · 2 ) ∈ ℤ )
35 zsubcl ⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝑘 · 2 ) ∈ ℤ ) → ( 𝑃 − ( 𝑘 · 2 ) ) ∈ ℤ )
36 31 34 35 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( 𝑃 − ( 𝑘 · 2 ) ) ∈ ℤ )
37 eleq1 ⊢ ( ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) → ( ( 𝑅 ‘ 𝑘 ) ∈ ℤ ↔ ( 𝑃 − ( 𝑘 · 2 ) ) ∈ ℤ ) )
38 36 37 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) → ( 𝑅 ‘ 𝑘 ) ∈ ℤ ) )
39 29 38 syld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( ∀ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) → ( 𝑅 ‘ 𝑘 ) ∈ ℤ ) )
40 26 39 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( 𝑅 ‘ 𝑘 ) ∈ ℤ )
41 24 40 fprodzcl ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ∈ ℤ )
42 41 zred ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ∈ ℝ )
43 nnoddn2prm ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) )
44 nnrp ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℝ+ )
45 44 adantr ⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → 𝑃 ∈ ℝ+ )
46 1 43 45 3syl ⊢ ( 𝜑 → 𝑃 ∈ ℝ+ )
47 modmulmodr ⊢ ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) ∈ ℤ ∧ ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) ) mod 𝑃 ) = ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) mod 𝑃 ) )
48 47 eqcomd ⊢ ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) ∈ ℤ ∧ ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) mod 𝑃 ) = ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) ) mod 𝑃 ) )
49 23 42 46 48 syl3anc ⊢ ( 𝜑 → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) ) mod 𝑃 ) = ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) ) mod 𝑃 ) )
50 1 2 3 4 5 gausslemma2dlem5 ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) mod 𝑃 ) )
51 50 oveq2d ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) mod 𝑃 ) ) )
52 51 oveq1d ⊢ ( 𝜑 → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) ) mod 𝑃 ) = ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) mod 𝑃 ) ) mod 𝑃 ) )
53 neg1rr ⊢ - 1 ∈ ℝ
54 53 a1i ⊢ ( 𝜑 → - 1 ∈ ℝ )
55 1 4 2 5 gausslemma2dlem0h ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
56 54 55 reexpcld ⊢ ( 𝜑 → ( - 1 ↑ 𝑁 ) ∈ ℝ )
57 32 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → 𝑘 ∈ ℤ )
58 15 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → 2 ∈ ℤ )
59 57 58 zmulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( 𝑘 · 2 ) ∈ ℤ )
60 24 59 fprodzcl ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ∈ ℤ )
61 60 zred ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ∈ ℝ )
62 56 61 remulcld ⊢ ( 𝜑 → ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) ∈ ℝ )
63 modmulmodr ⊢ ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) ∈ ℤ ∧ ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) ) mod 𝑃 ) )
64 23 62 46 63 syl3anc ⊢ ( 𝜑 → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) ) mod 𝑃 ) )
65 9 prodeq2d ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) = ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑘 · 2 ) )
66 65 oveq1d ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑘 · 2 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) )
67 fzfid ⊢ ( 𝜑 → ( 1 ... 𝐻 ) ∈ Fin )
68 elfzelz ⊢ ( 𝑘 ∈ ( 1 ... 𝐻 ) → 𝑘 ∈ ℤ )
69 68 zcnd ⊢ ( 𝑘 ∈ ( 1 ... 𝐻 ) → 𝑘 ∈ ℂ )
70 69 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐻 ) ) → 𝑘 ∈ ℂ )
71 2cn ⊢ 2 ∈ ℂ
72 71 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐻 ) ) → 2 ∈ ℂ )
73 67 70 72 fprodmul ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑘 · 2 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 𝑘 · ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 2 ) )
74 1 4 gausslemma2dlem0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
75 74 nn0red ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
76 75 ltp1d ⊢ ( 𝜑 → 𝑀 < ( 𝑀 + 1 ) )
77 fzdisj ⊢ ( 𝑀 < ( 𝑀 + 1 ) → ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝐻 ) ) = ∅ )
78 76 77 syl ⊢ ( 𝜑 → ( ( 1 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝐻 ) ) = ∅ )
79 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
80 nn0pzuz ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 1 ∈ ℤ ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
81 74 79 80 syl2anc ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
82 74 nn0zd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
83 1 2 gausslemma2dlem0b ⊢ ( 𝜑 → 𝐻 ∈ ℕ )
84 83 nnzd ⊢ ( 𝜑 → 𝐻 ∈ ℤ )
85 1 4 2 gausslemma2dlem0g ⊢ ( 𝜑 → 𝑀 ≤ 𝐻 )
86 eluz2 ⊢ ( 𝐻 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ 𝑀 ≤ 𝐻 ) )
87 82 84 85 86 syl3anbrc ⊢ ( 𝜑 → 𝐻 ∈ ( ℤ≥ ‘ 𝑀 ) )
88 fzsplit2 ⊢ ( ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝐻 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 1 ... 𝐻 ) = ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝐻 ) ) )
89 81 87 88 syl2anc ⊢ ( 𝜑 → ( 1 ... 𝐻 ) = ( ( 1 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝐻 ) ) )
90 15 a1i ⊢ ( 𝑘 ∈ ( 1 ... 𝐻 ) → 2 ∈ ℤ )
91 68 90 zmulcld ⊢ ( 𝑘 ∈ ( 1 ... 𝐻 ) → ( 𝑘 · 2 ) ∈ ℤ )
92 91 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐻 ) ) → ( 𝑘 · 2 ) ∈ ℤ )
93 92 zcnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝐻 ) ) → ( 𝑘 · 2 ) ∈ ℂ )
94 78 89 67 93 fprodsplit ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) ( 𝑘 · 2 ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑘 · 2 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) )
95 nnnn0 ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℕ0 )
96 95 anim1i ⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑃 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑃 ) )
97 43 96 syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑃 ) )
98 nn0oddm1d2 ⊢ ( 𝑃 ∈ ℕ0 → ( ¬ 2 ∥ 𝑃 ↔ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 ) )
99 98 biimpa ⊢ ( ( 𝑃 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑃 ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 )
100 2 99 eqeltrid ⊢ ( ( 𝑃 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑃 ) → 𝐻 ∈ ℕ0 )
101 1 97 100 3syl ⊢ ( 𝜑 → 𝐻 ∈ ℕ0 )
102 fprodfac ⊢ ( 𝐻 ∈ ℕ0 → ( ! ‘ 𝐻 ) = ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 𝑘 )
103 101 102 syl ⊢ ( 𝜑 → ( ! ‘ 𝐻 ) = ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 𝑘 )
104 103 eqcomd ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 𝑘 = ( ! ‘ 𝐻 ) )
105 fzfi ⊢ ( 1 ... 𝐻 ) ∈ Fin
106 105 71 pm3.2i ⊢ ( ( 1 ... 𝐻 ) ∈ Fin ∧ 2 ∈ ℂ )
107 fprodconst ⊢ ( ( ( 1 ... 𝐻 ) ∈ Fin ∧ 2 ∈ ℂ ) → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 2 = ( 2 ↑ ( ♯ ‘ ( 1 ... 𝐻 ) ) ) )
108 106 107 mp1i ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 2 = ( 2 ↑ ( ♯ ‘ ( 1 ... 𝐻 ) ) ) )
109 104 108 oveq12d ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 𝑘 · ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 2 ) = ( ( ! ‘ 𝐻 ) · ( 2 ↑ ( ♯ ‘ ( 1 ... 𝐻 ) ) ) ) )
110 hashfz1 ⊢ ( 𝐻 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝐻 ) ) = 𝐻 )
111 101 110 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝐻 ) ) = 𝐻 )
112 111 oveq2d ⊢ ( 𝜑 → ( 2 ↑ ( ♯ ‘ ( 1 ... 𝐻 ) ) ) = ( 2 ↑ 𝐻 ) )
113 112 oveq2d ⊢ ( 𝜑 → ( ( ! ‘ 𝐻 ) · ( 2 ↑ ( ♯ ‘ ( 1 ... 𝐻 ) ) ) ) = ( ( ! ‘ 𝐻 ) · ( 2 ↑ 𝐻 ) ) )
114 101 faccld ⊢ ( 𝜑 → ( ! ‘ 𝐻 ) ∈ ℕ )
115 114 nncnd ⊢ ( 𝜑 → ( ! ‘ 𝐻 ) ∈ ℂ )
116 2nn0 ⊢ 2 ∈ ℕ0
117 nn0expcl ⊢ ( ( 2 ∈ ℕ0 ∧ 𝐻 ∈ ℕ0 ) → ( 2 ↑ 𝐻 ) ∈ ℕ0 )
118 117 nn0cnd ⊢ ( ( 2 ∈ ℕ0 ∧ 𝐻 ∈ ℕ0 ) → ( 2 ↑ 𝐻 ) ∈ ℂ )
119 116 101 118 sylancr ⊢ ( 𝜑 → ( 2 ↑ 𝐻 ) ∈ ℂ )
120 115 119 mulcomd ⊢ ( 𝜑 → ( ( ! ‘ 𝐻 ) · ( 2 ↑ 𝐻 ) ) = ( ( 2 ↑ 𝐻 ) · ( ! ‘ 𝐻 ) ) )
121 109 113 120 3eqtrd ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 𝑘 · ∏ 𝑘 ∈ ( 1 ... 𝐻 ) 2 ) = ( ( 2 ↑ 𝐻 ) · ( ! ‘ 𝐻 ) ) )
122 73 94 121 3eqtr3d ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑘 · 2 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) = ( ( 2 ↑ 𝐻 ) · ( ! ‘ 𝐻 ) ) )
123 66 122 eqtrd ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) = ( ( 2 ↑ 𝐻 ) · ( ! ‘ 𝐻 ) ) )
124 123 oveq2d ⊢ ( 𝜑 → ( ( - 1 ↑ 𝑁 ) · ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( ( 2 ↑ 𝐻 ) · ( ! ‘ 𝐻 ) ) ) )
125 23 zcnd ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) ∈ ℂ )
126 56 recnd ⊢ ( 𝜑 → ( - 1 ↑ 𝑁 ) ∈ ℂ )
127 60 zcnd ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ∈ ℂ )
128 125 126 127 mul12d ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) ) )
129 126 119 115 mulassd ⊢ ( 𝜑 → ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) · ( ! ‘ 𝐻 ) ) = ( ( - 1 ↑ 𝑁 ) · ( ( 2 ↑ 𝐻 ) · ( ! ‘ 𝐻 ) ) ) )
130 124 128 129 3eqtr4d ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) ) = ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) · ( ! ‘ 𝐻 ) ) )
131 130 oveq1d ⊢ ( 𝜑 → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) · ( ! ‘ 𝐻 ) ) mod 𝑃 ) )
132 52 64 131 3eqtrd ⊢ ( 𝜑 → ( ( ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑅 ‘ 𝑘 ) · ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) · ( ! ‘ 𝐻 ) ) mod 𝑃 ) )
133 7 49 132 3eqtrd ⊢ ( 𝜑 → ( ( ! ‘ 𝐻 ) mod 𝑃 ) = ( ( ( ( - 1 ↑ 𝑁 ) · ( 2 ↑ 𝐻 ) ) · ( ! ‘ 𝐻 ) ) mod 𝑃 ) )