gausslemma2dlem6

	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	gausslemma2dlem6	$⊢ φ \to H! \mod P = {(- 1)}^{N} 2^{H} H! \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	gausslemma2dlem4	$⊢ φ \to H! = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k)$
7	6	oveq1d	$⊢ φ \to H! \mod P = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k) \mod P$
8		fzfid	$⊢ φ \to (1 \dots M) \in Fin$
9	1 2 3 4	gausslemma2dlem2	$⊢ φ \to \forall k \in (1 \dots M) R (k) = k \cdot 2$
10	9	adantr	$⊢ (φ \land k \in (1 \dots M)) \to \forall k \in (1 \dots M) R (k) = k \cdot 2$
11		rspa	$⊢ (\forall k \in (1 \dots M) R (k) = k \cdot 2 \land k \in (1 \dots M)) \to R (k) = k \cdot 2$
12	11	expcom	$⊢ k \in (1 \dots M) \to (\forall k \in (1 \dots M) R (k) = k \cdot 2 \to R (k) = k \cdot 2)$
13	12	adantl	$⊢ (φ \land k \in (1 \dots M)) \to (\forall k \in (1 \dots M) R (k) = k \cdot 2 \to R (k) = k \cdot 2)$
14		elfzelz	$⊢ k \in (1 \dots M) \to k \in ℤ$
15		2z	$⊢ 2 \in ℤ$
16	15	a1i	$⊢ k \in (1 \dots M) \to 2 \in ℤ$
17	14 16	zmulcld	$⊢ k \in (1 \dots M) \to k \cdot 2 \in ℤ$
18	17	adantl	$⊢ (φ \land k \in (1 \dots M)) \to k \cdot 2 \in ℤ$
19		eleq1	$⊢ R (k) = k \cdot 2 \to (R (k) \in ℤ \leftrightarrow k \cdot 2 \in ℤ)$
20	18 19	syl5ibrcom	$⊢ (φ \land k \in (1 \dots M)) \to (R (k) = k \cdot 2 \to R (k) \in ℤ)$
21	13 20	syld	$⊢ (φ \land k \in (1 \dots M)) \to (\forall k \in (1 \dots M) R (k) = k \cdot 2 \to R (k) \in ℤ)$
22	10 21	mpd	$⊢ (φ \land k \in (1 \dots M)) \to R (k) \in ℤ$
23	8 22	fprodzcl	$⊢ φ \to \prod_{k = 1}^{M} R (k) \in ℤ$
24		fzfid	$⊢ φ \to (M + 1 \dots H) \in Fin$
25	1 2 3 4	gausslemma2dlem3	$⊢ φ \to \forall k \in (M + 1 \dots H) R (k) = P - k \cdot 2$
26	25	adantr	$⊢ (φ \land k \in (M + 1 \dots H)) \to \forall k \in (M + 1 \dots H) R (k) = P - k \cdot 2$
27		rspa	$⊢ (\forall k \in (M + 1 \dots H) R (k) = P - k \cdot 2 \land k \in (M + 1 \dots H)) \to R (k) = P - k \cdot 2$
28	27	expcom	$⊢ k \in (M + 1 \dots H) \to (\forall k \in (M + 1 \dots H) R (k) = P - k \cdot 2 \to R (k) = P - k \cdot 2)$
29	28	adantl	$⊢ (φ \land k \in (M + 1 \dots H)) \to (\forall k \in (M + 1 \dots H) R (k) = P - k \cdot 2 \to R (k) = P - k \cdot 2)$
30	1	gausslemma2dlem0a	$⊢ φ \to P \in ℕ$
31	30	nnzd	$⊢ φ \to P \in ℤ$
32		elfzelz	$⊢ k \in (M + 1 \dots H) \to k \in ℤ$
33	15	a1i	$⊢ k \in (M + 1 \dots H) \to 2 \in ℤ$
34	32 33	zmulcld	$⊢ k \in (M + 1 \dots H) \to k \cdot 2 \in ℤ$
35		zsubcl	$⊢ (P \in ℤ \land k \cdot 2 \in ℤ) \to P - k \cdot 2 \in ℤ$
36	31 34 35	syl2an	$⊢ (φ \land k \in (M + 1 \dots H)) \to P - k \cdot 2 \in ℤ$
37		eleq1	$⊢ R (k) = P - k \cdot 2 \to (R (k) \in ℤ \leftrightarrow P - k \cdot 2 \in ℤ)$
38	36 37	syl5ibrcom	$⊢ (φ \land k \in (M + 1 \dots H)) \to (R (k) = P - k \cdot 2 \to R (k) \in ℤ)$
39	29 38	syld	$⊢ (φ \land k \in (M + 1 \dots H)) \to (\forall k \in (M + 1 \dots H) R (k) = P - k \cdot 2 \to R (k) \in ℤ)$
40	26 39	mpd	$⊢ (φ \land k \in (M + 1 \dots H)) \to R (k) \in ℤ$
41	24 40	fprodzcl	$⊢ φ \to \prod_{k = M + 1}^{H} R (k) \in ℤ$
42	41	zred	$⊢ φ \to \prod_{k = M + 1}^{H} R (k) \in ℝ$
43		nnoddn2prm	$⊢ P \in (ℙ ∖ \{2\}) \to (P \in ℕ \land \neg 2 ∥ P)$
44		nnrp	$⊢ P \in ℕ \to P \in ℝ^{+}$
45	44	adantr	$⊢ (P \in ℕ \land \neg 2 ∥ P) \to P \in ℝ^{+}$
46	1 43 45	3syl	$⊢ φ \to P \in ℝ^{+}$
47		modmulmodr	$⊢ (\prod_{k = 1}^{M} R (k) \in ℤ \land \prod_{k = M + 1}^{H} R (k) \in ℝ \land P \in ℝ^{+}) \to \prod_{k = 1}^{M} R (k) (\prod_{k = M + 1}^{H} R (k) \mod P) \mod P = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k) \mod P$
48	47	eqcomd	$⊢ (\prod_{k = 1}^{M} R (k) \in ℤ \land \prod_{k = M + 1}^{H} R (k) \in ℝ \land P \in ℝ^{+}) \to \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k) \mod P = \prod_{k = 1}^{M} R (k) (\prod_{k = M + 1}^{H} R (k) \mod P) \mod P$
49	23 42 46 48	syl3anc	$⊢ φ \to \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k) \mod P = \prod_{k = 1}^{M} R (k) (\prod_{k = M + 1}^{H} R (k) \mod P) \mod P$
50	1 2 3 4 5	gausslemma2dlem5	$⊢ φ \to \prod_{k = M + 1}^{H} R (k) \mod P = {(- 1)}^{N} \prod_{k = M + 1}^{H} k \cdot 2 \mod P$
51	50	oveq2d	$⊢ φ \to \prod_{k = 1}^{M} R (k) (\prod_{k = M + 1}^{H} R (k) \mod P) = \prod_{k = 1}^{M} R (k) ({(- 1)}^{N} \prod_{k = M + 1}^{H} k \cdot 2 \mod P)$
52	51	oveq1d	$⊢ φ \to \prod_{k = 1}^{M} R (k) (\prod_{k = M + 1}^{H} R (k) \mod P) \mod P = \prod_{k = 1}^{M} R (k) ({(- 1)}^{N} \prod_{k = M + 1}^{H} k \cdot 2 \mod P) \mod P$
53		neg1rr	$⊢ - 1 \in ℝ$
54	53	a1i	$⊢ φ \to - 1 \in ℝ$
55	1 4 2 5	gausslemma2dlem0h	$⊢ φ \to N \in ℕ_{0}$
56	54 55	reexpcld	$⊢ φ \to {(- 1)}^{N} \in ℝ$
57	32	adantl	$⊢ (φ \land k \in (M + 1 \dots H)) \to k \in ℤ$
58	15	a1i	$⊢ (φ \land k \in (M + 1 \dots H)) \to 2 \in ℤ$
59	57 58	zmulcld	$⊢ (φ \land k \in (M + 1 \dots H)) \to k \cdot 2 \in ℤ$
60	24 59	fprodzcl	$⊢ φ \to \prod_{k = M + 1}^{H} k \cdot 2 \in ℤ$
61	60	zred	$⊢ φ \to \prod_{k = M + 1}^{H} k \cdot 2 \in ℝ$
62	56 61	remulcld	$⊢ φ \to {(- 1)}^{N} \prod_{k = M + 1}^{H} k \cdot 2 \in ℝ$
63		modmulmodr	$⊢ (\prod_{k = 1}^{M} R (k) \in ℤ \land {(- 1)}^{N} \prod_{k = M + 1}^{H} k \cdot 2 \in ℝ \land P \in ℝ^{+}) \to \prod_{k = 1}^{M} R (k) ({(- 1)}^{N} \prod_{k = M + 1}^{H} k \cdot 2 \mod P) \mod P = \prod_{k = 1}^{M} R (k) {(- 1)}^{N} \prod_{k = M + 1}^{H} k \cdot 2 \mod P$
64	23 62 46 63	syl3anc	$⊢ φ \to \prod_{k = 1}^{M} R (k) ({(- 1)}^{N} \prod_{k = M + 1}^{H} k \cdot 2 \mod P) \mod P = \prod_{k = 1}^{M} R (k) {(- 1)}^{N} \prod_{k = M + 1}^{H} k \cdot 2 \mod P$
65	9	prodeq2d	$⊢ φ \to \prod_{k = 1}^{M} R (k) = \prod_{k = 1}^{M} k \cdot 2$
66	65	oveq1d	$⊢ φ \to \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} k \cdot 2 = \prod_{k = 1}^{M} k \cdot 2 \prod_{k = M + 1}^{H} k \cdot 2$
67		fzfid	$⊢ φ \to (1 \dots H) \in Fin$
68		elfzelz	$⊢ k \in (1 \dots H) \to k \in ℤ$
69	68	zcnd	$⊢ k \in (1 \dots H) \to k \in ℂ$
70	69	adantl	$⊢ (φ \land k \in (1 \dots H)) \to k \in ℂ$
71		2cn	$⊢ 2 \in ℂ$
72	71	a1i	$⊢ (φ \land k \in (1 \dots H)) \to 2 \in ℂ$
73	67 70 72	fprodmul	$⊢ φ \to \prod_{k = 1}^{H} k \cdot 2 = \prod_{k = 1}^{H} k \prod_{k = 1}^{H} 2$
74	1 4	gausslemma2dlem0d	$⊢ φ \to M \in ℕ_{0}$
75	74	nn0red	$⊢ φ \to M \in ℝ$
76	75	ltp1d	$⊢ φ \to M < M + 1$
77		fzdisj	$⊢ M < M + 1 \to (1 \dots M) \cap (M + 1 \dots H) = \emptyset$
78	76 77	syl	$⊢ φ \to (1 \dots M) \cap (M + 1 \dots H) = \emptyset$
79		1zzd	$⊢ φ \to 1 \in ℤ$
80		nn0pzuz	$⊢ (M \in ℕ_{0} \land 1 \in ℤ) \to M + 1 \in ℤ_{\geq 1}$
81	74 79 80	syl2anc	$⊢ φ \to M + 1 \in ℤ_{\geq 1}$
82	74	nn0zd	$⊢ φ \to M \in ℤ$
83	1 2	gausslemma2dlem0b	$⊢ φ \to H \in ℕ$
84	83	nnzd	$⊢ φ \to H \in ℤ$
85	1 4 2	gausslemma2dlem0g	$⊢ φ \to M \leq H$
86		eluz2	$⊢ H \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land H \in ℤ \land M \leq H)$
87	82 84 85 86	syl3anbrc	$⊢ φ \to H \in ℤ_{\geq M}$
88		fzsplit2	$⊢ (M + 1 \in ℤ_{\geq 1} \land H \in ℤ_{\geq M}) \to (1 \dots H) = (1 \dots M) \cup (M + 1 \dots H)$
89	81 87 88	syl2anc	$⊢ φ \to (1 \dots H) = (1 \dots M) \cup (M + 1 \dots H)$
90	15	a1i	$⊢ k \in (1 \dots H) \to 2 \in ℤ$
91	68 90	zmulcld	$⊢ k \in (1 \dots H) \to k \cdot 2 \in ℤ$
92	91	adantl	$⊢ (φ \land k \in (1 \dots H)) \to k \cdot 2 \in ℤ$
93	92	zcnd	$⊢ (φ \land k \in (1 \dots H)) \to k \cdot 2 \in ℂ$
94	78 89 67 93	fprodsplit	$⊢ φ \to \prod_{k = 1}^{H} k \cdot 2 = \prod_{k = 1}^{M} k \cdot 2 \prod_{k = M + 1}^{H} k \cdot 2$
95		nnnn0	$⊢ P \in ℕ \to P \in ℕ_{0}$
96	95	anim1i	$⊢ (P \in ℕ \land \neg 2 ∥ P) \to (P \in ℕ_{0} \land \neg 2 ∥ P)$
97	43 96	syl	$⊢ P \in (ℙ ∖ \{2\}) \to (P \in ℕ_{0} \land \neg 2 ∥ P)$
98		nn0oddm1d2	$⊢ P \in ℕ_{0} \to (\neg 2 ∥ P \leftrightarrow \frac{P - 1}{2} \in ℕ_{0})$
99	98	biimpa	$⊢ (P \in ℕ_{0} \land \neg 2 ∥ P) \to \frac{P - 1}{2} \in ℕ_{0}$
100	2 99	eqeltrid	$⊢ (P \in ℕ_{0} \land \neg 2 ∥ P) \to H \in ℕ_{0}$
101	1 97 100	3syl	$⊢ φ \to H \in ℕ_{0}$
102		fprodfac	$⊢ H \in ℕ_{0} \to H! = \prod_{k = 1}^{H} k$
103	101 102	syl	$⊢ φ \to H! = \prod_{k = 1}^{H} k$
104	103	eqcomd	$⊢ φ \to \prod_{k = 1}^{H} k = H!$
105		fzfi	$⊢ (1 \dots H) \in Fin$
106	105 71	pm3.2i	$⊢ ((1 \dots H) \in Fin \land 2 \in ℂ)$
107		fprodconst	$⊢ ((1 \dots H) \in Fin \land 2 \in ℂ) \to \prod_{k = 1}^{H} 2 = 2^{\|(1 \dots H)\|}$
108	106 107	mp1i	$⊢ φ \to \prod_{k = 1}^{H} 2 = 2^{\|(1 \dots H)\|}$
109	104 108	oveq12d	$⊢ φ \to \prod_{k = 1}^{H} k \prod_{k = 1}^{H} 2 = H! 2^{\|(1 \dots H)\|}$
110		hashfz1	$⊢ H \in ℕ_{0} \to \|(1 \dots H)\| = H$
111	101 110	syl	$⊢ φ \to \|(1 \dots H)\| = H$
112	111	oveq2d	$⊢ φ \to 2^{\|(1 \dots H)\|} = 2^{H}$
113	112	oveq2d	$⊢ φ \to H! 2^{\|(1 \dots H)\|} = H! 2^{H}$
114	101	faccld	$⊢ φ \to H! \in ℕ$
115	114	nncnd	$⊢ φ \to H! \in ℂ$
116		2nn0	$⊢ 2 \in ℕ_{0}$
117		nn0expcl	$⊢ (2 \in ℕ_{0} \land H \in ℕ_{0}) \to 2^{H} \in ℕ_{0}$
118	117	nn0cnd	$⊢ (2 \in ℕ_{0} \land H \in ℕ_{0}) \to 2^{H} \in ℂ$
119	116 101 118	sylancr	$⊢ φ \to 2^{H} \in ℂ$
120	115 119	mulcomd	$⊢ φ \to H! 2^{H} = 2^{H} H!$
121	109 113 120	3eqtrd	$⊢ φ \to \prod_{k = 1}^{H} k \prod_{k = 1}^{H} 2 = 2^{H} H!$
122	73 94 121	3eqtr3d	$⊢ φ \to \prod_{k = 1}^{M} k \cdot 2 \prod_{k = M + 1}^{H} k \cdot 2 = 2^{H} H!$
123	66 122	eqtrd	$⊢ φ \to \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} k \cdot 2 = 2^{H} H!$
124	123	oveq2d	$⊢ φ \to {(- 1)}^{N} \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} k \cdot 2 = {(- 1)}^{N} 2^{H} H!$
125	23	zcnd	$⊢ φ \to \prod_{k = 1}^{M} R (k) \in ℂ$
126	56	recnd	$⊢ φ \to {(- 1)}^{N} \in ℂ$
127	60	zcnd	$⊢ φ \to \prod_{k = M + 1}^{H} k \cdot 2 \in ℂ$
128	125 126 127	mul12d	$⊢ φ \to \prod_{k = 1}^{M} R (k) {(- 1)}^{N} \prod_{k = M + 1}^{H} k \cdot 2 = {(- 1)}^{N} \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} k \cdot 2$
129	126 119 115	mulassd	$⊢ φ \to {(- 1)}^{N} 2^{H} H! = {(- 1)}^{N} 2^{H} H!$
130	124 128 129	3eqtr4d	$⊢ φ \to \prod_{k = 1}^{M} R (k) {(- 1)}^{N} \prod_{k = M + 1}^{H} k \cdot 2 = {(- 1)}^{N} 2^{H} H!$
131	130	oveq1d	$⊢ φ \to \prod_{k = 1}^{M} R (k) {(- 1)}^{N} \prod_{k = M + 1}^{H} k \cdot 2 \mod P = {(- 1)}^{N} 2^{H} H! \mod P$
132	52 64 131	3eqtrd	$⊢ φ \to \prod_{k = 1}^{M} R (k) (\prod_{k = M + 1}^{H} R (k) \mod P) \mod P = {(- 1)}^{N} 2^{H} H! \mod P$
133	7 49 132	3eqtrd	$⊢ φ \to H! \mod P = {(- 1)}^{N} 2^{H} H! \mod P$

Metamath Proof Explorer

Theorem gausslemma2dlem6

Proof