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