gausslemma2dlem4

	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	gausslemma2dlem4	$⊢ φ \to H! = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k)$

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	gausslemma2dlem1	$⊢ φ \to H! = \prod_{k = 1}^{H} R (k)$
6		eldif	$⊢ P \in (ℙ ∖ \{2\}) \leftrightarrow (P \in ℙ \land \neg P \in \{2\})$
7		prm23ge5	$⊢ P \in ℙ \to (P = 2 \lor P = 3 \lor P \in ℤ_{\geq 5})$
8		eleq1	$⊢ P = 2 \to (P \in \{2\} \leftrightarrow 2 \in \{2\})$
9	8	notbid	$⊢ P = 2 \to (\neg P \in \{2\} \leftrightarrow \neg 2 \in \{2\})$
10		2ex	$⊢ 2 \in V$
11	10	snid	$⊢ 2 \in \{2\}$
12	11	2a1i	$⊢ P = 2 \to (\prod_{k = 1}^{H} R (k) \neq \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k) \to 2 \in \{2\})$
13	12	necon1bd	$⊢ P = 2 \to (\neg 2 \in \{2\} \to \prod_{k = 1}^{H} R (k) = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k))$
14	13	a1dd	$⊢ P = 2 \to (\neg 2 \in \{2\} \to (φ \to \prod_{k = 1}^{H} R (k) = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k)))$
15	9 14	sylbid	$⊢ P = 2 \to (\neg P \in \{2\} \to (φ \to \prod_{k = 1}^{H} R (k) = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k)))$
16		3lt4	$⊢ 3 < 4$
17		breq1	$⊢ P = 3 \to (P < 4 \leftrightarrow 3 < 4)$
18	16 17	mpbiri	$⊢ P = 3 \to P < 4$
19		3nn0	$⊢ 3 \in ℕ_{0}$
20		eleq1	$⊢ P = 3 \to (P \in ℕ_{0} \leftrightarrow 3 \in ℕ_{0})$
21	19 20	mpbiri	$⊢ P = 3 \to P \in ℕ_{0}$
22		4nn	$⊢ 4 \in ℕ$
23		divfl0	$⊢ (P \in ℕ_{0} \land 4 \in ℕ) \to (P < 4 \leftrightarrow ⌊\frac{P}{4}⌋ = 0)$
24	21 22 23	sylancl	$⊢ P = 3 \to (P < 4 \leftrightarrow ⌊\frac{P}{4}⌋ = 0)$
25	18 24	mpbid	$⊢ P = 3 \to ⌊\frac{P}{4}⌋ = 0$
26	4 25	eqtrid	$⊢ P = 3 \to M = 0$
27		oveq2	$⊢ M = 0 \to (1 \dots M) = (1 \dots 0)$
28	27	adantr	$⊢ (M = 0 \land φ) \to (1 \dots M) = (1 \dots 0)$
29		fz10	$⊢ (1 \dots 0) = \emptyset$
30	28 29	eqtrdi	$⊢ (M = 0 \land φ) \to (1 \dots M) = \emptyset$
31	30	prodeq1d	$⊢ (M = 0 \land φ) \to \prod_{k = 1}^{M} R (k) = \prod_{k \in \emptyset} R (k)$
32		prod0	$⊢ \prod_{k \in \emptyset} R (k) = 1$
33	31 32	eqtrdi	$⊢ (M = 0 \land φ) \to \prod_{k = 1}^{M} R (k) = 1$
34		oveq1	$⊢ M = 0 \to M + 1 = 0 + 1$
35	34	adantr	$⊢ (M = 0 \land φ) \to M + 1 = 0 + 1$
36		0p1e1	$⊢ 0 + 1 = 1$
37	35 36	eqtrdi	$⊢ (M = 0 \land φ) \to M + 1 = 1$
38	37	oveq1d	$⊢ (M = 0 \land φ) \to (M + 1 \dots H) = (1 \dots H)$
39	38	prodeq1d	$⊢ (M = 0 \land φ) \to \prod_{k = M + 1}^{H} R (k) = \prod_{k = 1}^{H} R (k)$
40	33 39	oveq12d	$⊢ (M = 0 \land φ) \to \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k) = 1 \prod_{k = 1}^{H} R (k)$
41		fzfid	$⊢ (M = 0 \land φ) \to (1 \dots H) \in Fin$
42		oveq1	$⊢ x = k \to x \cdot 2 = k \cdot 2$
43	42	breq1d	$⊢ x = k \to (x \cdot 2 < \frac{P}{2} \leftrightarrow k \cdot 2 < \frac{P}{2})$
44	42	oveq2d	$⊢ x = k \to P - x \cdot 2 = P - k \cdot 2$
45	43 42 44	ifbieq12d	$⊢ x = k \to if (x \cdot 2 < \frac{P}{2}, x \cdot 2, P - x \cdot 2) = if (k \cdot 2 < \frac{P}{2}, k \cdot 2, P - k \cdot 2)$
46		simpr	$⊢ (φ \land k \in (1 \dots H)) \to k \in (1 \dots H)$
47		elfzelz	$⊢ k \in (1 \dots H) \to k \in ℤ$
48	47	zcnd	$⊢ k \in (1 \dots H) \to k \in ℂ$
49		2cnd	$⊢ k \in (1 \dots H) \to 2 \in ℂ$
50	48 49	mulcld	$⊢ k \in (1 \dots H) \to k \cdot 2 \in ℂ$
51	50	adantl	$⊢ (φ \land k \in (1 \dots H)) \to k \cdot 2 \in ℂ$
52		eldifi	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℙ$
53		prmz	$⊢ P \in ℙ \to P \in ℤ$
54	53	zcnd	$⊢ P \in ℙ \to P \in ℂ$
55	1 52 54	3syl	$⊢ φ \to P \in ℂ$
56	55	adantr	$⊢ (φ \land k \in (1 \dots H)) \to P \in ℂ$
57	56 51	subcld	$⊢ (φ \land k \in (1 \dots H)) \to P - k \cdot 2 \in ℂ$
58	51 57	ifcld	$⊢ (φ \land k \in (1 \dots H)) \to if (k \cdot 2 < \frac{P}{2}, k \cdot 2, P - k \cdot 2) \in ℂ$
59	3 45 46 58	fvmptd3	$⊢ (φ \land k \in (1 \dots H)) \to R (k) = if (k \cdot 2 < \frac{P}{2}, k \cdot 2, P - k \cdot 2)$
60	59 58	eqeltrd	$⊢ (φ \land k \in (1 \dots H)) \to R (k) \in ℂ$
61	60	adantll	$⊢ ((M = 0 \land φ) \land k \in (1 \dots H)) \to R (k) \in ℂ$
62	41 61	fprodcl	$⊢ (M = 0 \land φ) \to \prod_{k = 1}^{H} R (k) \in ℂ$
63	62	mullidd	$⊢ (M = 0 \land φ) \to 1 \prod_{k = 1}^{H} R (k) = \prod_{k = 1}^{H} R (k)$
64	40 63	eqtr2d	$⊢ (M = 0 \land φ) \to \prod_{k = 1}^{H} R (k) = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k)$
65	64	ex	$⊢ M = 0 \to (φ \to \prod_{k = 1}^{H} R (k) = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k))$
66	26 65	syl	$⊢ P = 3 \to (φ \to \prod_{k = 1}^{H} R (k) = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k))$
67	66	a1d	$⊢ P = 3 \to (\neg P \in \{2\} \to (φ \to \prod_{k = 1}^{H} R (k) = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k)))$
68	1 4	gausslemma2dlem0d	$⊢ φ \to M \in ℕ_{0}$
69	68	nn0red	$⊢ φ \to M \in ℝ$
70	69	ltp1d	$⊢ φ \to M < M + 1$
71		fzdisj	$⊢ M < M + 1 \to (1 \dots M) \cap (M + 1 \dots H) = \emptyset$
72	70 71	syl	$⊢ φ \to (1 \dots M) \cap (M + 1 \dots H) = \emptyset$
73	72	adantl	$⊢ (P \in ℤ_{\geq 5} \land φ) \to (1 \dots M) \cap (M + 1 \dots H) = \emptyset$
74		eluzelre	$⊢ P \in ℤ_{\geq 5} \to P \in ℝ$
75		4re	$⊢ 4 \in ℝ$
76	75	a1i	$⊢ P \in ℤ_{\geq 5} \to 4 \in ℝ$
77		4ne0	$⊢ 4 \neq 0$
78	77	a1i	$⊢ P \in ℤ_{\geq 5} \to 4 \neq 0$
79	74 76 78	redivcld	$⊢ P \in ℤ_{\geq 5} \to \frac{P}{4} \in ℝ$
80	79	flcld	$⊢ P \in ℤ_{\geq 5} \to ⌊\frac{P}{4}⌋ \in ℤ$
81		nnrp	$⊢ 4 \in ℕ \to 4 \in ℝ^{+}$
82	22 81	ax-mp	$⊢ 4 \in ℝ^{+}$
83		eluz2	$⊢ P \in ℤ_{\geq 5} \leftrightarrow (5 \in ℤ \land P \in ℤ \land 5 \leq P)$
84		4lt5	$⊢ 4 < 5$
85		5re	$⊢ 5 \in ℝ$
86	85	a1i	$⊢ (5 \in ℤ \land P \in ℤ) \to 5 \in ℝ$
87		zre	$⊢ P \in ℤ \to P \in ℝ$
88	87	adantl	$⊢ (5 \in ℤ \land P \in ℤ) \to P \in ℝ$
89		ltleletr	$⊢ (4 \in ℝ \land 5 \in ℝ \land P \in ℝ) \to ((4 < 5 \land 5 \leq P) \to 4 \leq P)$
90	75 86 88 89	mp3an2i	$⊢ (5 \in ℤ \land P \in ℤ) \to ((4 < 5 \land 5 \leq P) \to 4 \leq P)$
91	84 90	mpani	$⊢ (5 \in ℤ \land P \in ℤ) \to (5 \leq P \to 4 \leq P)$
92	91	3impia	$⊢ (5 \in ℤ \land P \in ℤ \land 5 \leq P) \to 4 \leq P$
93	83 92	sylbi	$⊢ P \in ℤ_{\geq 5} \to 4 \leq P$
94		divge1	$⊢ (4 \in ℝ^{+} \land P \in ℝ \land 4 \leq P) \to 1 \leq \frac{P}{4}$
95	82 74 93 94	mp3an2i	$⊢ P \in ℤ_{\geq 5} \to 1 \leq \frac{P}{4}$
96		1zzd	$⊢ P \in ℤ_{\geq 5} \to 1 \in ℤ$
97		flge	$⊢ (\frac{P}{4} \in ℝ \land 1 \in ℤ) \to (1 \leq \frac{P}{4} \leftrightarrow 1 \leq ⌊\frac{P}{4}⌋)$
98	79 96 97	syl2anc	$⊢ P \in ℤ_{\geq 5} \to (1 \leq \frac{P}{4} \leftrightarrow 1 \leq ⌊\frac{P}{4}⌋)$
99	95 98	mpbid	$⊢ P \in ℤ_{\geq 5} \to 1 \leq ⌊\frac{P}{4}⌋$
100		elnnz1	$⊢ ⌊\frac{P}{4}⌋ \in ℕ \leftrightarrow (⌊\frac{P}{4}⌋ \in ℤ \land 1 \leq ⌊\frac{P}{4}⌋)$
101	80 99 100	sylanbrc	$⊢ P \in ℤ_{\geq 5} \to ⌊\frac{P}{4}⌋ \in ℕ$
102	101	adantl	$⊢ (P \in (ℙ ∖ \{2\}) \land P \in ℤ_{\geq 5}) \to ⌊\frac{P}{4}⌋ \in ℕ$
103		oddprm	$⊢ P \in (ℙ ∖ \{2\}) \to \frac{P - 1}{2} \in ℕ$
104	103	adantr	$⊢ (P \in (ℙ ∖ \{2\}) \land P \in ℤ_{\geq 5}) \to \frac{P - 1}{2} \in ℕ$
105		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
106	52 105	syl	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℤ_{\geq 2}$
107	106	adantr	$⊢ (P \in (ℙ ∖ \{2\}) \land P \in ℤ_{\geq 5}) \to P \in ℤ_{\geq 2}$
108		fldiv4lem1div2uz2	$⊢ P \in ℤ_{\geq 2} \to ⌊\frac{P}{4}⌋ \leq \frac{P - 1}{2}$
109	107 108	syl	$⊢ (P \in (ℙ ∖ \{2\}) \land P \in ℤ_{\geq 5}) \to ⌊\frac{P}{4}⌋ \leq \frac{P - 1}{2}$
110	102 104 109	3jca	$⊢ (P \in (ℙ ∖ \{2\}) \land P \in ℤ_{\geq 5}) \to (⌊\frac{P}{4}⌋ \in ℕ \land \frac{P - 1}{2} \in ℕ \land ⌊\frac{P}{4}⌋ \leq \frac{P - 1}{2})$
111	110	ex	$⊢ P \in (ℙ ∖ \{2\}) \to (P \in ℤ_{\geq 5} \to (⌊\frac{P}{4}⌋ \in ℕ \land \frac{P - 1}{2} \in ℕ \land ⌊\frac{P}{4}⌋ \leq \frac{P - 1}{2}))$
112	1 111	syl	$⊢ φ \to (P \in ℤ_{\geq 5} \to (⌊\frac{P}{4}⌋ \in ℕ \land \frac{P - 1}{2} \in ℕ \land ⌊\frac{P}{4}⌋ \leq \frac{P - 1}{2}))$
113	112	impcom	$⊢ (P \in ℤ_{\geq 5} \land φ) \to (⌊\frac{P}{4}⌋ \in ℕ \land \frac{P - 1}{2} \in ℕ \land ⌊\frac{P}{4}⌋ \leq \frac{P - 1}{2})$
114	2	oveq2i	$⊢ (1 \dots H) = (1 \dots \frac{P - 1}{2})$
115	4 114	eleq12i	$⊢ M \in (1 \dots H) \leftrightarrow ⌊\frac{P}{4}⌋ \in (1 \dots \frac{P - 1}{2})$
116		elfz1b	$⊢ ⌊\frac{P}{4}⌋ \in (1 \dots \frac{P - 1}{2}) \leftrightarrow (⌊\frac{P}{4}⌋ \in ℕ \land \frac{P - 1}{2} \in ℕ \land ⌊\frac{P}{4}⌋ \leq \frac{P - 1}{2})$
117	115 116	bitri	$⊢ M \in (1 \dots H) \leftrightarrow (⌊\frac{P}{4}⌋ \in ℕ \land \frac{P - 1}{2} \in ℕ \land ⌊\frac{P}{4}⌋ \leq \frac{P - 1}{2})$
118	113 117	sylibr	$⊢ (P \in ℤ_{\geq 5} \land φ) \to M \in (1 \dots H)$
119		fzsplit	$⊢ M \in (1 \dots H) \to (1 \dots H) = (1 \dots M) \cup (M + 1 \dots H)$
120	118 119	syl	$⊢ (P \in ℤ_{\geq 5} \land φ) \to (1 \dots H) = (1 \dots M) \cup (M + 1 \dots H)$
121		fzfid	$⊢ (P \in ℤ_{\geq 5} \land φ) \to (1 \dots H) \in Fin$
122	60	adantll	$⊢ ((P \in ℤ_{\geq 5} \land φ) \land k \in (1 \dots H)) \to R (k) \in ℂ$
123	73 120 121 122	fprodsplit	$⊢ (P \in ℤ_{\geq 5} \land φ) \to \prod_{k = 1}^{H} R (k) = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k)$
124	123	ex	$⊢ P \in ℤ_{\geq 5} \to (φ \to \prod_{k = 1}^{H} R (k) = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k))$
125	124	a1d	$⊢ P \in ℤ_{\geq 5} \to (\neg P \in \{2\} \to (φ \to \prod_{k = 1}^{H} R (k) = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k)))$
126	15 67 125	3jaoi	$⊢ (P = 2 \lor P = 3 \lor P \in ℤ_{\geq 5}) \to (\neg P \in \{2\} \to (φ \to \prod_{k = 1}^{H} R (k) = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k)))$
127	7 126	syl	$⊢ P \in ℙ \to (\neg P \in \{2\} \to (φ \to \prod_{k = 1}^{H} R (k) = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k)))$
128	127	imp	$⊢ (P \in ℙ \land \neg P \in \{2\}) \to (φ \to \prod_{k = 1}^{H} R (k) = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k))$
129	6 128	sylbi	$⊢ P \in (ℙ ∖ \{2\}) \to (φ \to \prod_{k = 1}^{H} R (k) = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k))$
130	1 129	mpcom	$⊢ φ \to \prod_{k = 1}^{H} R (k) = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k)$
131	5 130	eqtrd	$⊢ φ \to H! = \prod_{k = 1}^{M} R (k) \prod_{k = M + 1}^{H} R (k)$

Metamath Proof Explorer

Theorem gausslemma2dlem4

Proof