gausslemma2dlem5

	Ref	Expression
Hypotheses	gausslemma2d.p	$⊢ φ \to P \in (ℙ ∖ \{2\})$
	gausslemma2d.h	$⊢ H = \frac{P - 1}{2}$
	gausslemma2d.r	$⊢ R = (x \in (1 \dots H) ⟼ if (x \cdot 2 < \frac{P}{2}, x \cdot 2, P - x \cdot 2))$
	gausslemma2d.m	$⊢ M = ⌊\frac{P}{4}⌋$
	gausslemma2d.n	$⊢ N = H - M$
Assertion	gausslemma2dlem5	$⊢ φ \to \prod_{k = M + 1}^{H} R (k) \mod P = {(- 1)}^{N} \prod_{k = M + 1}^{H} k \cdot 2 \mod P$

Proof

Step	Hyp	Ref	Expression
1		gausslemma2d.p	$⊢ φ \to P \in (ℙ ∖ \{2\})$
2		gausslemma2d.h	$⊢ H = \frac{P - 1}{2}$
3		gausslemma2d.r	$⊢ R = (x \in (1 \dots H) ⟼ if (x \cdot 2 < \frac{P}{2}, x \cdot 2, P - x \cdot 2))$
4		gausslemma2d.m	$⊢ M = ⌊\frac{P}{4}⌋$
5		gausslemma2d.n	$⊢ N = H - M$
6	1 2 3 4	gausslemma2dlem5a	$⊢ φ \to \prod_{k = M + 1}^{H} R (k) \mod P = \prod_{k = M + 1}^{H} -1 k \cdot 2 \mod P$
7		fzfi	$⊢ (M + 1 \dots H) \in Fin$
8	7	a1i	$⊢ φ \to (M + 1 \dots H) \in Fin$
9		neg1cn	$⊢ - 1 \in ℂ$
10	9	a1i	$⊢ (φ \land k \in (M + 1 \dots H)) \to - 1 \in ℂ$
11		elfzelz	$⊢ k \in (M + 1 \dots H) \to k \in ℤ$
12		2z	$⊢ 2 \in ℤ$
13	12	a1i	$⊢ k \in (M + 1 \dots H) \to 2 \in ℤ$
14	11 13	zmulcld	$⊢ k \in (M + 1 \dots H) \to k \cdot 2 \in ℤ$
15	14	zcnd	$⊢ k \in (M + 1 \dots H) \to k \cdot 2 \in ℂ$
16	15	adantl	$⊢ (φ \land k \in (M + 1 \dots H)) \to k \cdot 2 \in ℂ$
17	8 10 16	fprodmul	$⊢ φ \to \prod_{k = M + 1}^{H} -1 k \cdot 2 = \prod_{k = M + 1}^{H} -1 \prod_{k = M + 1}^{H} k \cdot 2$
18	7 9	pm3.2i	$⊢ ((M + 1 \dots H) \in Fin \land - 1 \in ℂ)$
19		fprodconst	$⊢ ((M + 1 \dots H) \in Fin \land - 1 \in ℂ) \to \prod_{k = M + 1}^{H} -1 = {(- 1)}^{\|(M + 1 \dots H)\|}$
20	18 19	mp1i	$⊢ φ \to \prod_{k = M + 1}^{H} -1 = {(- 1)}^{\|(M + 1 \dots H)\|}$
21		nnoddn2prm	$⊢ P \in (ℙ ∖ \{2\}) \to (P \in ℕ \land \neg 2 ∥ P)$
22		nnre	$⊢ P \in ℕ \to P \in ℝ$
23	22	adantr	$⊢ (P \in ℕ \land \neg 2 ∥ P) \to P \in ℝ$
24	1 21 23	3syl	$⊢ φ \to P \in ℝ$
25		4re	$⊢ 4 \in ℝ$
26	25	a1i	$⊢ φ \to 4 \in ℝ$
27		4ne0	$⊢ 4 \neq 0$
28	27	a1i	$⊢ φ \to 4 \neq 0$
29	24 26 28	redivcld	$⊢ φ \to \frac{P}{4} \in ℝ$
30	29	flcld	$⊢ φ \to ⌊\frac{P}{4}⌋ \in ℤ$
31	4 30	eqeltrid	$⊢ φ \to M \in ℤ$
32	31	peano2zd	$⊢ φ \to M + 1 \in ℤ$
33		nnz	$⊢ P \in ℕ \to P \in ℤ$
34		oddm1d2	$⊢ P \in ℤ \to (\neg 2 ∥ P \leftrightarrow \frac{P - 1}{2} \in ℤ)$
35	33 34	syl	$⊢ P \in ℕ \to (\neg 2 ∥ P \leftrightarrow \frac{P - 1}{2} \in ℤ)$
36	35	biimpa	$⊢ (P \in ℕ \land \neg 2 ∥ P) \to \frac{P - 1}{2} \in ℤ$
37	1 21 36	3syl	$⊢ φ \to \frac{P - 1}{2} \in ℤ$
38	2 37	eqeltrid	$⊢ φ \to H \in ℤ$
39	1 4 2	gausslemma2dlem0f	$⊢ φ \to M + 1 \leq H$
40		eluz2	$⊢ H \in ℤ_{\geq (M + 1)} \leftrightarrow (M + 1 \in ℤ \land H \in ℤ \land M + 1 \leq H)$
41	32 38 39 40	syl3anbrc	$⊢ φ \to H \in ℤ_{\geq (M + 1)}$
42		hashfz	$⊢ H \in ℤ_{\geq (M + 1)} \to \|(M + 1 \dots H)\| = H - (M + 1) + 1$
43	41 42	syl	$⊢ φ \to \|(M + 1 \dots H)\| = H - (M + 1) + 1$
44	38	zcnd	$⊢ φ \to H \in ℂ$
45	31	zcnd	$⊢ φ \to M \in ℂ$
46		1cnd	$⊢ φ \to 1 \in ℂ$
47	44 45 46	nppcan2d	$⊢ φ \to H - (M + 1) + 1 = H - M$
48	47 5	eqtr4di	$⊢ φ \to H - (M + 1) + 1 = N$
49	43 48	eqtrd	$⊢ φ \to \|(M + 1 \dots H)\| = N$
50	49	oveq2d	$⊢ φ \to {(- 1)}^{\|(M + 1 \dots H)\|} = {(- 1)}^{N}$
51	20 50	eqtrd	$⊢ φ \to \prod_{k = M + 1}^{H} -1 = {(- 1)}^{N}$
52	51	oveq1d	$⊢ φ \to \prod_{k = M + 1}^{H} -1 \prod_{k = M + 1}^{H} k \cdot 2 = {(- 1)}^{N} \prod_{k = M + 1}^{H} k \cdot 2$
53	17 52	eqtrd	$⊢ φ \to \prod_{k = M + 1}^{H} -1 k \cdot 2 = {(- 1)}^{N} \prod_{k = M + 1}^{H} k \cdot 2$
54	53	oveq1d	$⊢ φ \to \prod_{k = M + 1}^{H} -1 k \cdot 2 \mod P = {(- 1)}^{N} \prod_{k = M + 1}^{H} k \cdot 2 \mod P$
55	6 54	eqtrd	$⊢ φ \to \prod_{k = M + 1}^{H} R (k) \mod P = {(- 1)}^{N} \prod_{k = M + 1}^{H} k \cdot 2 \mod P$

Metamath Proof Explorer

Theorem gausslemma2dlem5

Proof