gausslemma2dlem5a

	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}⌋$
Assertion	gausslemma2dlem5a	$⊢ φ \to \prod_{k = M + 1}^{H} R (k) \mod P = \prod_{k = M + 1}^{H} -1 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	1 2 3 4	gausslemma2dlem3	$⊢ φ \to \forall k \in (M + 1 \dots H) R (k) = P - k \cdot 2$
6		prodeq2	$⊢ \forall k \in (M + 1 \dots H) R (k) = P - k \cdot 2 \to \prod_{k = M + 1}^{H} R (k) = \prod_{k = M + 1}^{H} (P - k \cdot 2)$
7	6	oveq1d	$⊢ \forall k \in (M + 1 \dots H) R (k) = P - k \cdot 2 \to \prod_{k = M + 1}^{H} R (k) \mod P = \prod_{k = M + 1}^{H} (P - k \cdot 2) \mod P$
8	5 7	syl	$⊢ φ \to \prod_{k = M + 1}^{H} R (k) \mod P = \prod_{k = M + 1}^{H} (P - k \cdot 2) \mod P$
9		eldifi	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℙ$
10		fzfid	$⊢ P \in ℙ \to (M + 1 \dots H) \in Fin$
11		prmz	$⊢ P \in ℙ \to P \in ℤ$
12	11	adantr	$⊢ (P \in ℙ \land k \in (M + 1 \dots H)) \to P \in ℤ$
13		elfzelz	$⊢ k \in (M + 1 \dots H) \to k \in ℤ$
14		2z	$⊢ 2 \in ℤ$
15	14	a1i	$⊢ k \in (M + 1 \dots H) \to 2 \in ℤ$
16	13 15	zmulcld	$⊢ k \in (M + 1 \dots H) \to k \cdot 2 \in ℤ$
17	16	adantl	$⊢ (P \in ℙ \land k \in (M + 1 \dots H)) \to k \cdot 2 \in ℤ$
18	12 17	zsubcld	$⊢ (P \in ℙ \land k \in (M + 1 \dots H)) \to P - k \cdot 2 \in ℤ$
19		neg1z	$⊢ - 1 \in ℤ$
20	19	a1i	$⊢ k \in (M + 1 \dots H) \to - 1 \in ℤ$
21	20 16	zmulcld	$⊢ k \in (M + 1 \dots H) \to -1 k \cdot 2 \in ℤ$
22	21	adantl	$⊢ (P \in ℙ \land k \in (M + 1 \dots H)) \to -1 k \cdot 2 \in ℤ$
23		prmnn	$⊢ P \in ℙ \to P \in ℕ$
24	16	zcnd	$⊢ k \in (M + 1 \dots H) \to k \cdot 2 \in ℂ$
25	24	mulm1d	$⊢ k \in (M + 1 \dots H) \to -1 k \cdot 2 = - k \cdot 2$
26	25	adantl	$⊢ (P \in ℙ \land k \in (M + 1 \dots H)) \to -1 k \cdot 2 = - k \cdot 2$
27	26	oveq1d	$⊢ (P \in ℙ \land k \in (M + 1 \dots H)) \to -1 k \cdot 2 \mod P = (- k \cdot 2) \mod P$
28	16	zred	$⊢ k \in (M + 1 \dots H) \to k \cdot 2 \in ℝ$
29	23	nnrpd	$⊢ P \in ℙ \to P \in ℝ^{+}$
30		negmod	$⊢ (k \cdot 2 \in ℝ \land P \in ℝ^{+}) \to (- k \cdot 2) \mod P = (P - k \cdot 2) \mod P$
31	28 29 30	syl2anr	$⊢ (P \in ℙ \land k \in (M + 1 \dots H)) \to (- k \cdot 2) \mod P = (P - k \cdot 2) \mod P$
32	27 31	eqtr2d	$⊢ (P \in ℙ \land k \in (M + 1 \dots H)) \to (P - k \cdot 2) \mod P = -1 k \cdot 2 \mod P$
33	10 18 22 23 32	fprodmodd	$⊢ P \in ℙ \to \prod_{k = M + 1}^{H} (P - k \cdot 2) \mod P = \prod_{k = M + 1}^{H} -1 k \cdot 2 \mod P$
34	1 9 33	3syl	$⊢ φ \to \prod_{k = M + 1}^{H} (P - k \cdot 2) \mod P = \prod_{k = M + 1}^{H} -1 k \cdot 2 \mod P$
35	8 34	eqtrd	$⊢ φ \to \prod_{k = M + 1}^{H} R (k) \mod P = \prod_{k = M + 1}^{H} -1 k \cdot 2 \mod P$

Metamath Proof Explorer

Theorem gausslemma2dlem5a

Proof