Metamath Proof Explorer

Theorem gausslemma2dlem5

Description: Lemma 5 for gausslemma2d . (Contributed by AV, 9-Jul-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 gausslemma2dlem5 ( 𝜑 → ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 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 gausslemma2dlem5a ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) = ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( - 1 · ( 𝑘 · 2 ) ) mod 𝑃 ) )
7 fzfi ⊢ ( ( 𝑀 + 1 ) ... 𝐻 ) ∈ Fin
8 7 a1i ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ... 𝐻 ) ∈ Fin )
9 neg1cn ⊢ - 1 ∈ ℂ
10 9 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → - 1 ∈ ℂ )
11 elfzelz ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → 𝑘 ∈ ℤ )
12 2z ⊢ 2 ∈ ℤ
13 12 a1i ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → 2 ∈ ℤ )
14 11 13 zmulcld ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → ( 𝑘 · 2 ) ∈ ℤ )
15 14 zcnd ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → ( 𝑘 · 2 ) ∈ ℂ )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( 𝑘 · 2 ) ∈ ℂ )
17 8 10 16 fprodmul ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( - 1 · ( 𝑘 · 2 ) ) = ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) - 1 · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) )
18 7 9 pm3.2i ⊢ ( ( ( 𝑀 + 1 ) ... 𝐻 ) ∈ Fin ∧ - 1 ∈ ℂ )
19 fprodconst ⊢ ( ( ( ( 𝑀 + 1 ) ... 𝐻 ) ∈ Fin ∧ - 1 ∈ ℂ ) → ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) - 1 = ( - 1 ↑ ( ♯ ‘ ( ( 𝑀 + 1 ) ... 𝐻 ) ) ) )
20 18 19 mp1i ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) - 1 = ( - 1 ↑ ( ♯ ‘ ( ( 𝑀 + 1 ) ... 𝐻 ) ) ) )
21 nnoddn2prm ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) )
22 nnre ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℝ )
23 22 adantr ⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → 𝑃 ∈ ℝ )
24 1 21 23 3syl ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
25 4re ⊢ 4 ∈ ℝ
26 25 a1i ⊢ ( 𝜑 → 4 ∈ ℝ )
27 4ne0 ⊢ 4 ≠ 0
28 27 a1i ⊢ ( 𝜑 → 4 ≠ 0 )
29 24 26 28 redivcld ⊢ ( 𝜑 → ( 𝑃 / 4 ) ∈ ℝ )
30 29 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℤ )
31 4 30 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
32 31 peano2zd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℤ )
33 nnz ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℤ )
34 oddm1d2 ⊢ ( 𝑃 ∈ ℤ → ( ¬ 2 ∥ 𝑃 ↔ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ) )
35 33 34 syl ⊢ ( 𝑃 ∈ ℕ → ( ¬ 2 ∥ 𝑃 ↔ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ) )
36 35 biimpa ⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ )
37 1 21 36 3syl ⊢ ( 𝜑 → ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ )
38 2 37 eqeltrid ⊢ ( 𝜑 → 𝐻 ∈ ℤ )
39 1 4 2 gausslemma2dlem0f ⊢ ( 𝜑 → ( 𝑀 + 1 ) ≤ 𝐻 )
40 eluz2 ⊢ ( 𝐻 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ↔ ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝐻 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝐻 ) )
41 32 38 39 40 syl3anbrc ⊢ ( 𝜑 → 𝐻 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
42 hashfz ⊢ ( 𝐻 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( ♯ ‘ ( ( 𝑀 + 1 ) ... 𝐻 ) ) = ( ( 𝐻 − ( 𝑀 + 1 ) ) + 1 ) )
43 41 42 syl ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑀 + 1 ) ... 𝐻 ) ) = ( ( 𝐻 − ( 𝑀 + 1 ) ) + 1 ) )
44 38 zcnd ⊢ ( 𝜑 → 𝐻 ∈ ℂ )
45 31 zcnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
46 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
47 44 45 46 nppcan2d ⊢ ( 𝜑 → ( ( 𝐻 − ( 𝑀 + 1 ) ) + 1 ) = ( 𝐻 − 𝑀 ) )
48 47 5 eqtr4di ⊢ ( 𝜑 → ( ( 𝐻 − ( 𝑀 + 1 ) ) + 1 ) = 𝑁 )
49 43 48 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑀 + 1 ) ... 𝐻 ) ) = 𝑁 )
50 49 oveq2d ⊢ ( 𝜑 → ( - 1 ↑ ( ♯ ‘ ( ( 𝑀 + 1 ) ... 𝐻 ) ) ) = ( - 1 ↑ 𝑁 ) )
51 20 50 eqtrd ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) - 1 = ( - 1 ↑ 𝑁 ) )
52 51 oveq1d ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) - 1 · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) = ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) )
53 17 52 eqtrd ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( - 1 · ( 𝑘 · 2 ) ) = ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) )
54 53 oveq1d ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( - 1 · ( 𝑘 · 2 ) ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) mod 𝑃 ) )
55 6 54 eqtrd ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) = ( ( ( - 1 ↑ 𝑁 ) · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑘 · 2 ) ) mod 𝑃 ) )