Metamath Proof Explorer

Theorem gausslemma2dlem5a

Description: Lemma for gausslemma2dlem5 . (Contributed by AV, 8-Jul-2021)

Ref Expression
Hypotheses gausslemma2d.p ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
gausslemma2d.h ⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
gausslemma2d.r ⊢ 𝑅 = ( 𝑥 ∈ ( 1 ... 𝐻 ) ↦ if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
gausslemma2d.m ⊢ 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
Assertion gausslemma2dlem5a ( 𝜑 → ( ∏ 𝑘 ∈ ( ( 𝑀 + 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 1 2 3 4 gausslemma2dlem3 ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) )
6 prodeq2 ⊢ ( ∀ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) → ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑃 − ( 𝑘 · 2 ) ) )
7 6 oveq1d ⊢ ( ∀ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) = ( 𝑃 − ( 𝑘 · 2 ) ) → ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) = ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑃 − ( 𝑘 · 2 ) ) mod 𝑃 ) )
8 5 7 syl ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) = ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑃 − ( 𝑘 · 2 ) ) mod 𝑃 ) )
9 eldifi ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ )
10 fzfid ⊢ ( 𝑃 ∈ ℙ → ( ( 𝑀 + 1 ) ... 𝐻 ) ∈ Fin )
11 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
12 11 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → 𝑃 ∈ ℤ )
13 elfzelz ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → 𝑘 ∈ ℤ )
14 2z ⊢ 2 ∈ ℤ
15 14 a1i ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → 2 ∈ ℤ )
16 13 15 zmulcld ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → ( 𝑘 · 2 ) ∈ ℤ )
17 16 adantl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( 𝑘 · 2 ) ∈ ℤ )
18 12 17 zsubcld ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( 𝑃 − ( 𝑘 · 2 ) ) ∈ ℤ )
19 neg1z ⊢ - 1 ∈ ℤ
20 19 a1i ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → - 1 ∈ ℤ )
21 20 16 zmulcld ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → ( - 1 · ( 𝑘 · 2 ) ) ∈ ℤ )
22 21 adantl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( - 1 · ( 𝑘 · 2 ) ) ∈ ℤ )
23 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
24 16 zcnd ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → ( 𝑘 · 2 ) ∈ ℂ )
25 24 mulm1d ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → ( - 1 · ( 𝑘 · 2 ) ) = - ( 𝑘 · 2 ) )
26 25 adantl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( - 1 · ( 𝑘 · 2 ) ) = - ( 𝑘 · 2 ) )
27 26 oveq1d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( ( - 1 · ( 𝑘 · 2 ) ) mod 𝑃 ) = ( - ( 𝑘 · 2 ) mod 𝑃 ) )
28 16 zred ⊢ ( 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) → ( 𝑘 · 2 ) ∈ ℝ )
29 23 nnrpd ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℝ+ )
30 negmod ⊢ ( ( ( 𝑘 · 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( - ( 𝑘 · 2 ) mod 𝑃 ) = ( ( 𝑃 − ( 𝑘 · 2 ) ) mod 𝑃 ) )
31 28 29 30 syl2anr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( - ( 𝑘 · 2 ) mod 𝑃 ) = ( ( 𝑃 − ( 𝑘 · 2 ) ) mod 𝑃 ) )
32 27 31 eqtr2d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ) → ( ( 𝑃 − ( 𝑘 · 2 ) ) mod 𝑃 ) = ( ( - 1 · ( 𝑘 · 2 ) ) mod 𝑃 ) )
33 10 18 22 23 32 fprodmodd ⊢ ( 𝑃 ∈ ℙ → ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑃 − ( 𝑘 · 2 ) ) mod 𝑃 ) = ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( - 1 · ( 𝑘 · 2 ) ) mod 𝑃 ) )
34 1 9 33 3syl ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑃 − ( 𝑘 · 2 ) ) mod 𝑃 ) = ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( - 1 · ( 𝑘 · 2 ) ) mod 𝑃 ) )
35 8 34 eqtrd ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( 𝑅 ‘ 𝑘 ) mod 𝑃 ) = ( ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝐻 ) ( - 1 · ( 𝑘 · 2 ) ) mod 𝑃 ) )