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 𝑃 ) )