lgsquadlem1

Description: Lemma for lgsquad . Count the members of S with odd coordinates. (Contributed by Mario Carneiro, 19-Jun-2015)

	Ref	Expression
Hypotheses	lgseisen.1	$⊢ φ \to P \in (ℙ ∖ \{2\})$
	lgseisen.2	$⊢ φ \to Q \in (ℙ ∖ \{2\})$
	lgseisen.3	$⊢ φ \to P \neq Q$
	lgsquad.4	$⊢ M = \frac{P - 1}{2}$
	lgsquad.5	$⊢ N = \frac{Q - 1}{2}$
	lgsquad.6	$⊢ S = \{⟨x, y⟩ \| ((x \in (1 \dots M) \land y \in (1 \dots N)) \land y P < x Q)\}$
Assertion	lgsquadlem1	$⊢ φ \to {(- 1)}^{\sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋} = {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|}$

Proof

Step	Hyp	Ref	Expression
1		lgseisen.1	$⊢ φ \to P \in (ℙ ∖ \{2\})$
2		lgseisen.2	$⊢ φ \to Q \in (ℙ ∖ \{2\})$
3		lgseisen.3	$⊢ φ \to P \neq Q$
4		lgsquad.4	$⊢ M = \frac{P - 1}{2}$
5		lgsquad.5	$⊢ N = \frac{Q - 1}{2}$
6		lgsquad.6	$⊢ S = \{⟨x, y⟩ \| ((x \in (1 \dots M) \land y \in (1 \dots N)) \land y P < x Q)\}$
7		neg1cn	$⊢ - 1 \in ℂ$
8	7	a1i	$⊢ φ \to - 1 \in ℂ$
9		neg1ne0	$⊢ - 1 \neq 0$
10	9	a1i	$⊢ φ \to - 1 \neq 0$
11		fzfid	$⊢ φ \to (⌊\frac{M}{2}⌋ + 1 \dots M) \in Fin$
12	2	gausslemma2dlem0a	$⊢ φ \to Q \in ℕ$
13	12	nnred	$⊢ φ \to Q \in ℝ$
14	1	gausslemma2dlem0a	$⊢ φ \to P \in ℕ$
15	13 14	nndivred	$⊢ φ \to \frac{Q}{P} \in ℝ$
16	15	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{Q}{P} \in ℝ$
17		2z	$⊢ 2 \in ℤ$
18		elfzelz	$⊢ u \in (⌊\frac{M}{2}⌋ + 1 \dots M) \to u \in ℤ$
19	18	adantl	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to u \in ℤ$
20		zmulcl	$⊢ (2 \in ℤ \land u \in ℤ) \to 2 u \in ℤ$
21	17 19 20	sylancr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 u \in ℤ$
22	21	zred	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 u \in ℝ$
23	16 22	remulcld	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{Q}{P}) 2 u \in ℝ$
24	23	flcld	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊(\frac{Q}{P}) 2 u⌋ \in ℤ$
25	11 24	fsumzcl	$⊢ φ \to \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋ \in ℤ$
26	8 10 25	expclzd	$⊢ φ \to {(- 1)}^{\sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋} \in ℂ$
27		fzfid	$⊢ φ \to (1 \dots M) \in Fin$
28		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
29		xpfi	$⊢ ((1 \dots M) \in Fin \land (1 \dots N) \in Fin) \to (1 \dots M) \times (1 \dots N) \in Fin$
30	27 28 29	syl2anc	$⊢ φ \to (1 \dots M) \times (1 \dots N) \in Fin$
31		opabssxp	$⊢ \{⟨x, y⟩ \| ((x \in (1 \dots M) \land y \in (1 \dots N)) \land y P < x Q)\} \subseteq (1 \dots M) \times (1 \dots N)$
32	6 31	eqsstri	$⊢ S \subseteq (1 \dots M) \times (1 \dots N)$
33		ssfi	$⊢ ((1 \dots M) \times (1 \dots N) \in Fin \land S \subseteq (1 \dots M) \times (1 \dots N)) \to S \in Fin$
34	30 32 33	sylancl	$⊢ φ \to S \in Fin$
35		ssrab2	$⊢ \{z \in S \| \neg 2 ∥ 1^{st} (z)\} \subseteq S$
36		ssfi	$⊢ (S \in Fin \land \{z \in S \| \neg 2 ∥ 1^{st} (z)\} \subseteq S) \to \{z \in S \| \neg 2 ∥ 1^{st} (z)\} \in Fin$
37	34 35 36	sylancl	$⊢ φ \to \{z \in S \| \neg 2 ∥ 1^{st} (z)\} \in Fin$
38		hashcl	$⊢ \{z \in S \| \neg 2 ∥ 1^{st} (z)\} \in Fin \to \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\| \in ℕ_{0}$
39	37 38	syl	$⊢ φ \to \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\| \in ℕ_{0}$
40		expcl	$⊢ (- 1 \in ℂ \land \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\| \in ℕ_{0}) \to {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} \in ℂ$
41	7 39 40	sylancr	$⊢ φ \to {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} \in ℂ$
42	39	nn0zd	$⊢ φ \to \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\| \in ℤ$
43	8 10 42	expne0d	$⊢ φ \to {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} \neq 0$
44	41 43	recidd	$⊢ φ \to {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} (\frac{1}{{(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|}}) = 1$
45		1div1e1	$⊢ \frac{1}{1} = 1$
46	45	negeqi	$⊢ - \frac{1}{1} = - 1$
47		ax-1cn	$⊢ 1 \in ℂ$
48		ax-1ne0	$⊢ 1 \neq 0$
49		divneg2	$⊢ (1 \in ℂ \land 1 \in ℂ \land 1 \neq 0) \to - \frac{1}{1} = \frac{1}{- 1}$
50	47 47 48 49	mp3an	$⊢ - \frac{1}{1} = \frac{1}{- 1}$
51	46 50	eqtr3i	$⊢ - 1 = \frac{1}{- 1}$
52	51	oveq1i	$⊢ {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} = {(\frac{1}{- 1})}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|}$
53	8 10 42	exprecd	$⊢ φ \to {(\frac{1}{- 1})}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} = \frac{1}{{(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|}}$
54	52 53	syl5eq	$⊢ φ \to {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} = \frac{1}{{(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|}}$
55	54	oveq2d	$⊢ φ \to {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} = {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} (\frac{1}{{(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|}})$
56	34	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to S \in Fin$
57		ssrab2	$⊢ \{z \in S \| 1^{st} (z) = P - 2 u\} \subseteq S$
58		ssfi	$⊢ (S \in Fin \land \{z \in S \| 1^{st} (z) = P - 2 u\} \subseteq S) \to \{z \in S \| 1^{st} (z) = P - 2 u\} \in Fin$
59	56 57 58	sylancl	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \{z \in S \| 1^{st} (z) = P - 2 u\} \in Fin$
60		fveqeq2	$⊢ z = v \to (1^{st} (z) = P - 2 u \leftrightarrow 1^{st} (v) = P - 2 u)$
61	60	elrab	$⊢ v \in \{z \in S \| 1^{st} (z) = P - 2 u\} \leftrightarrow (v \in S \land 1^{st} (v) = P - 2 u)$
62	61	simprbi	$⊢ v \in \{z \in S \| 1^{st} (z) = P - 2 u\} \to 1^{st} (v) = P - 2 u$
63	62	ad2antll	$⊢ (φ \land (u \in (⌊\frac{M}{2}⌋ + 1 \dots M) \land v \in \{z \in S \| 1^{st} (z) = P - 2 u\})) \to 1^{st} (v) = P - 2 u$
64	63	oveq2d	$⊢ (φ \land (u \in (⌊\frac{M}{2}⌋ + 1 \dots M) \land v \in \{z \in S \| 1^{st} (z) = P - 2 u\})) \to P - 1^{st} (v) = P - (P - 2 u)$
65	14	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P \in ℕ$
66	65	nncnd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P \in ℂ$
67	66	adantrr	$⊢ (φ \land (u \in (⌊\frac{M}{2}⌋ + 1 \dots M) \land v \in \{z \in S \| 1^{st} (z) = P - 2 u\})) \to P \in ℂ$
68	21	zcnd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 u \in ℂ$
69	68	adantrr	$⊢ (φ \land (u \in (⌊\frac{M}{2}⌋ + 1 \dots M) \land v \in \{z \in S \| 1^{st} (z) = P - 2 u\})) \to 2 u \in ℂ$
70	67 69	nncand	$⊢ (φ \land (u \in (⌊\frac{M}{2}⌋ + 1 \dots M) \land v \in \{z \in S \| 1^{st} (z) = P - 2 u\})) \to P - (P - 2 u) = 2 u$
71	64 70	eqtrd	$⊢ (φ \land (u \in (⌊\frac{M}{2}⌋ + 1 \dots M) \land v \in \{z \in S \| 1^{st} (z) = P - 2 u\})) \to P - 1^{st} (v) = 2 u$
72	71	oveq1d	$⊢ (φ \land (u \in (⌊\frac{M}{2}⌋ + 1 \dots M) \land v \in \{z \in S \| 1^{st} (z) = P - 2 u\})) \to \frac{P - 1^{st} (v)}{2} = \frac{2 u}{2}$
73	19	zcnd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to u \in ℂ$
74	73	adantrr	$⊢ (φ \land (u \in (⌊\frac{M}{2}⌋ + 1 \dots M) \land v \in \{z \in S \| 1^{st} (z) = P - 2 u\})) \to u \in ℂ$
75		2cnd	$⊢ (φ \land (u \in (⌊\frac{M}{2}⌋ + 1 \dots M) \land v \in \{z \in S \| 1^{st} (z) = P - 2 u\})) \to 2 \in ℂ$
76		2ne0	$⊢ 2 \neq 0$
77	76	a1i	$⊢ (φ \land (u \in (⌊\frac{M}{2}⌋ + 1 \dots M) \land v \in \{z \in S \| 1^{st} (z) = P - 2 u\})) \to 2 \neq 0$
78	74 75 77	divcan3d	$⊢ (φ \land (u \in (⌊\frac{M}{2}⌋ + 1 \dots M) \land v \in \{z \in S \| 1^{st} (z) = P - 2 u\})) \to \frac{2 u}{2} = u$
79	72 78	eqtrd	$⊢ (φ \land (u \in (⌊\frac{M}{2}⌋ + 1 \dots M) \land v \in \{z \in S \| 1^{st} (z) = P - 2 u\})) \to \frac{P - 1^{st} (v)}{2} = u$
80	79	ralrimivva	$⊢ φ \to \forall u \in (⌊\frac{M}{2}⌋ + 1 \dots M) \forall v \in \{z \in S \| 1^{st} (z) = P - 2 u\} \frac{P - 1^{st} (v)}{2} = u$
81		invdisj	$⊢ \forall u \in (⌊\frac{M}{2}⌋ + 1 \dots M) \forall v \in \{z \in S \| 1^{st} (z) = P - 2 u\} \frac{P - 1^{st} (v)}{2} = u \to {Disj}_{u = ⌊\frac{M}{2}⌋ + 1}^{M} \{z \in S \| 1^{st} (z) = P - 2 u\}$
82	80 81	syl	$⊢ φ \to {Disj}_{u = ⌊\frac{M}{2}⌋ + 1}^{M} \{z \in S \| 1^{st} (z) = P - 2 u\}$
83	11 59 82	hashiun	$⊢ φ \to \|⋃_{u = ⌊\frac{M}{2}⌋ + 1}^{M} \{z \in S \| 1^{st} (z) = P - 2 u\}\| = \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} \|\{z \in S \| 1^{st} (z) = P - 2 u\}\|$
84		iunrab	$⊢ ⋃_{u = ⌊\frac{M}{2}⌋ + 1}^{M} \{z \in S \| 1^{st} (z) = P - 2 u\} = \{z \in S \| \exists u \in (⌊\frac{M}{2}⌋ + 1 \dots M) 1^{st} (z) = P - 2 u\}$
85		eldifsni	$⊢ P \in (ℙ ∖ \{2\}) \to P \neq 2$
86	1 85	syl	$⊢ φ \to P \neq 2$
87	86	necomd	$⊢ φ \to 2 \neq P$
88	87	neneqd	$⊢ φ \to \neg 2 = P$
89	88	ad2antrr	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \neg 2 = P$
90		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
91	17 90	ax-mp	$⊢ 2 \in ℤ_{\geq 2}$
92	1	eldifad	$⊢ φ \to P \in ℙ$
93	92	ad2antrr	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P \in ℙ$
94		dvdsprm	$⊢ (2 \in ℤ_{\geq 2} \land P \in ℙ) \to (2 ∥ P \leftrightarrow 2 = P)$
95	91 93 94	sylancr	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (2 ∥ P \leftrightarrow 2 = P)$
96	89 95	mtbird	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \neg 2 ∥ P$
97	14	ad2antrr	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P \in ℕ$
98	97	nncnd	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P \in ℂ$
99	21	adantlr	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 u \in ℤ$
100	99	zcnd	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 u \in ℂ$
101	98 100	npcand	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 2 u + 2 u = P$
102	101	breq2d	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (2 ∥ (P - 2 u + 2 u) \leftrightarrow 2 ∥ P)$
103	96 102	mtbird	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \neg 2 ∥ (P - 2 u + 2 u)$
104	18	adantl	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to u \in ℤ$
105		dvdsmul1	$⊢ (2 \in ℤ \land u \in ℤ) \to 2 ∥ 2 u$
106	17 104 105	sylancr	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 ∥ 2 u$
107	17	a1i	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \in ℤ$
108	97	nnzd	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P \in ℤ$
109	108 99	zsubcld	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 2 u \in ℤ$
110		dvds2add	$⊢ (2 \in ℤ \land P - 2 u \in ℤ \land 2 u \in ℤ) \to ((2 ∥ (P - 2 u) \land 2 ∥ 2 u) \to 2 ∥ (P - 2 u + 2 u))$
111	107 109 99 110	syl3anc	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ((2 ∥ (P - 2 u) \land 2 ∥ 2 u) \to 2 ∥ (P - 2 u + 2 u))$
112	106 111	mpan2d	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (2 ∥ (P - 2 u) \to 2 ∥ (P - 2 u + 2 u))$
113	103 112	mtod	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \neg 2 ∥ (P - 2 u)$
114		breq2	$⊢ 1^{st} (z) = P - 2 u \to (2 ∥ 1^{st} (z) \leftrightarrow 2 ∥ (P - 2 u))$
115	114	notbid	$⊢ 1^{st} (z) = P - 2 u \to (\neg 2 ∥ 1^{st} (z) \leftrightarrow \neg 2 ∥ (P - 2 u))$
116	113 115	syl5ibrcom	$⊢ ((φ \land z \in S) \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (1^{st} (z) = P - 2 u \to \neg 2 ∥ 1^{st} (z))$
117	116	rexlimdva	$⊢ (φ \land z \in S) \to (\exists u \in (⌊\frac{M}{2}⌋ + 1 \dots M) 1^{st} (z) = P - 2 u \to \neg 2 ∥ 1^{st} (z))$
118		simpr	$⊢ (φ \land z \in S) \to z \in S$
119	32 118	sseldi	$⊢ (φ \land z \in S) \to z \in ((1 \dots M) \times (1 \dots N))$
120		xp1st	$⊢ z \in ((1 \dots M) \times (1 \dots N)) \to 1^{st} (z) \in (1 \dots M)$
121	119 120	syl	$⊢ (φ \land z \in S) \to 1^{st} (z) \in (1 \dots M)$
122		elfzelz	$⊢ 1^{st} (z) \in (1 \dots M) \to 1^{st} (z) \in ℤ$
123		odd2np1	$⊢ 1^{st} (z) \in ℤ \to (\neg 2 ∥ 1^{st} (z) \leftrightarrow \exists n \in ℤ 2 n + 1 = 1^{st} (z))$
124	121 122 123	3syl	$⊢ (φ \land z \in S) \to (\neg 2 ∥ 1^{st} (z) \leftrightarrow \exists n \in ℤ 2 n + 1 = 1^{st} (z))$
125	1 4	gausslemma2dlem0b	$⊢ φ \to M \in ℕ$
126	125	nnred	$⊢ φ \to M \in ℝ$
127	126	ad2antrr	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to M \in ℝ$
128	127	rehalfcld	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to \frac{M}{2} \in ℝ$
129		reflcl	$⊢ \frac{M}{2} \in ℝ \to ⌊\frac{M}{2}⌋ \in ℝ$
130	128 129	syl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to ⌊\frac{M}{2}⌋ \in ℝ$
131	125	ad2antrr	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to M \in ℕ$
132	131	nnzd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to M \in ℤ$
133		simprl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to n \in ℤ$
134	132 133	zsubcld	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to M - n \in ℤ$
135	134	zred	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to M - n \in ℝ$
136		flle	$⊢ \frac{M}{2} \in ℝ \to ⌊\frac{M}{2}⌋ \leq \frac{M}{2}$
137	128 136	syl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to ⌊\frac{M}{2}⌋ \leq \frac{M}{2}$
138		zre	$⊢ n \in ℤ \to n \in ℝ$
139	138	ad2antrl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to n \in ℝ$
140		simprr	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n + 1 = 1^{st} (z)$
141	121	adantr	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 1^{st} (z) \in (1 \dots M)$
142	140 141	eqeltrd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n + 1 \in (1 \dots M)$
143		elfzle2	$⊢ 2 n + 1 \in (1 \dots M) \to 2 n + 1 \leq M$
144	142 143	syl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n + 1 \leq M$
145		zmulcl	$⊢ (2 \in ℤ \land n \in ℤ) \to 2 n \in ℤ$
146	17 133 145	sylancr	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n \in ℤ$
147		zltp1le	$⊢ (2 n \in ℤ \land M \in ℤ) \to (2 n < M \leftrightarrow 2 n + 1 \leq M)$
148	146 132 147	syl2anc	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to (2 n < M \leftrightarrow 2 n + 1 \leq M)$
149	144 148	mpbird	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n < M$
150		2re	$⊢ 2 \in ℝ$
151	150	a1i	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 \in ℝ$
152		2pos	$⊢ 0 < 2$
153	152	a1i	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 0 < 2$
154		ltmuldiv2	$⊢ (n \in ℝ \land M \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 n < M \leftrightarrow n < \frac{M}{2})$
155	139 127 151 153 154	syl112anc	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to (2 n < M \leftrightarrow n < \frac{M}{2})$
156	149 155	mpbid	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to n < \frac{M}{2}$
157	128	recnd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to \frac{M}{2} \in ℂ$
158	125	nncnd	$⊢ φ \to M \in ℂ$
159	158	ad2antrr	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to M \in ℂ$
160	159	2halvesd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to (\frac{M}{2}) + (\frac{M}{2}) = M$
161	157 157 160	mvlraddd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to \frac{M}{2} = M - (\frac{M}{2})$
162	156 161	breqtrd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to n < M - (\frac{M}{2})$
163	139 127 128 162	ltsub13d	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to \frac{M}{2} < M - n$
164	130 128 135 137 163	lelttrd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to ⌊\frac{M}{2}⌋ < M - n$
165	128	flcld	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to ⌊\frac{M}{2}⌋ \in ℤ$
166		zltp1le	$⊢ (⌊\frac{M}{2}⌋ \in ℤ \land M - n \in ℤ) \to (⌊\frac{M}{2}⌋ < M - n \leftrightarrow ⌊\frac{M}{2}⌋ + 1 \leq M - n)$
167	165 134 166	syl2anc	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to (⌊\frac{M}{2}⌋ < M - n \leftrightarrow ⌊\frac{M}{2}⌋ + 1 \leq M - n)$
168	164 167	mpbid	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to ⌊\frac{M}{2}⌋ + 1 \leq M - n$
169		2t0e0	$⊢ 2 \cdot 0 = 0$
170		2cn	$⊢ 2 \in ℂ$
171		zcn	$⊢ n \in ℤ \to n \in ℂ$
172	171	ad2antrl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to n \in ℂ$
173		mulcl	$⊢ (2 \in ℂ \land n \in ℂ) \to 2 n \in ℂ$
174	170 172 173	sylancr	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n \in ℂ$
175		pncan	$⊢ (2 n \in ℂ \land 1 \in ℂ) \to 2 n + 1 - 1 = 2 n$
176	174 47 175	sylancl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n + 1 - 1 = 2 n$
177		elfznn	$⊢ 2 n + 1 \in (1 \dots M) \to 2 n + 1 \in ℕ$
178		nnm1nn0	$⊢ 2 n + 1 \in ℕ \to 2 n + 1 - 1 \in ℕ_{0}$
179	142 177 178	3syl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n + 1 - 1 \in ℕ_{0}$
180	176 179	eqeltrrd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n \in ℕ_{0}$
181	180	nn0ge0d	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 0 \leq 2 n$
182	169 181	eqbrtrid	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 \cdot 0 \leq 2 n$
183		0red	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 0 \in ℝ$
184		lemul2	$⊢ (0 \in ℝ \land n \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (0 \leq n \leftrightarrow 2 \cdot 0 \leq 2 n)$
185	183 139 151 153 184	syl112anc	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to (0 \leq n \leftrightarrow 2 \cdot 0 \leq 2 n)$
186	182 185	mpbird	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 0 \leq n$
187	127 139	subge02d	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to (0 \leq n \leftrightarrow M - n \leq M)$
188	186 187	mpbid	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to M - n \leq M$
189	165	peano2zd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to ⌊\frac{M}{2}⌋ + 1 \in ℤ$
190		elfz	$⊢ (M - n \in ℤ \land ⌊\frac{M}{2}⌋ + 1 \in ℤ \land M \in ℤ) \to (M - n \in (⌊\frac{M}{2}⌋ + 1 \dots M) \leftrightarrow (⌊\frac{M}{2}⌋ + 1 \leq M - n \land M - n \leq M))$
191	134 189 132 190	syl3anc	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to (M - n \in (⌊\frac{M}{2}⌋ + 1 \dots M) \leftrightarrow (⌊\frac{M}{2}⌋ + 1 \leq M - n \land M - n \leq M))$
192	168 188 191	mpbir2and	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to M - n \in (⌊\frac{M}{2}⌋ + 1 \dots M)$
193	92	ad2antrr	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P \in ℙ$
194		prmnn	$⊢ P \in ℙ \to P \in ℕ$
195	193 194	syl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P \in ℕ$
196	195	nncnd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P \in ℂ$
197		peano2cn	$⊢ 2 n \in ℂ \to 2 n + 1 \in ℂ$
198	174 197	syl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n + 1 \in ℂ$
199	196 198	nncand	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P - (P - (2 n + 1)) = 2 n + 1$
200		1cnd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 1 \in ℂ$
201	196 174 200	sub32d	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P - 2 n - 1 = P - 1 - 2 n$
202	196 174 200	subsub4d	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P - 2 n - 1 = P - (2 n + 1)$
203		2cnd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 \in ℂ$
204	203 159 172	subdid	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 (M - n) = 2 \cdot M - 2 n$
205	4	oveq2i	$⊢ 2 \cdot M = 2 (\frac{P - 1}{2})$
206	14	nnzd	$⊢ φ \to P \in ℤ$
207	206	ad2antrr	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P \in ℤ$
208		peano2zm	$⊢ P \in ℤ \to P - 1 \in ℤ$
209	207 208	syl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P - 1 \in ℤ$
210	209	zcnd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P - 1 \in ℂ$
211	76	a1i	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 \neq 0$
212	210 203 211	divcan2d	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 (\frac{P - 1}{2}) = P - 1$
213	205 212	syl5eq	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 \cdot M = P - 1$
214	213	oveq1d	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 \cdot M - 2 n = P - 1 - 2 n$
215	204 214	eqtr2d	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P - 1 - 2 n = 2 (M - n)$
216	201 202 215	3eqtr3d	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P - (2 n + 1) = 2 (M - n)$
217	216	oveq2d	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P - (P - (2 n + 1)) = P - 2 (M - n)$
218	199 217 140	3eqtr3rd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 1^{st} (z) = P - 2 (M - n)$
219		oveq2	$⊢ u = M - n \to 2 u = 2 (M - n)$
220	219	oveq2d	$⊢ u = M - n \to P - 2 u = P - 2 (M - n)$
221	220	rspceeqv	$⊢ (M - n \in (⌊\frac{M}{2}⌋ + 1 \dots M) \land 1^{st} (z) = P - 2 (M - n)) \to \exists u \in (⌊\frac{M}{2}⌋ + 1 \dots M) 1^{st} (z) = P - 2 u$
222	192 218 221	syl2anc	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to \exists u \in (⌊\frac{M}{2}⌋ + 1 \dots M) 1^{st} (z) = P - 2 u$
223	222	rexlimdvaa	$⊢ (φ \land z \in S) \to (\exists n \in ℤ 2 n + 1 = 1^{st} (z) \to \exists u \in (⌊\frac{M}{2}⌋ + 1 \dots M) 1^{st} (z) = P - 2 u)$
224	124 223	sylbid	$⊢ (φ \land z \in S) \to (\neg 2 ∥ 1^{st} (z) \to \exists u \in (⌊\frac{M}{2}⌋ + 1 \dots M) 1^{st} (z) = P - 2 u)$
225	117 224	impbid	$⊢ (φ \land z \in S) \to (\exists u \in (⌊\frac{M}{2}⌋ + 1 \dots M) 1^{st} (z) = P - 2 u \leftrightarrow \neg 2 ∥ 1^{st} (z))$
226	225	rabbidva	$⊢ φ \to \{z \in S \| \exists u \in (⌊\frac{M}{2}⌋ + 1 \dots M) 1^{st} (z) = P - 2 u\} = \{z \in S \| \neg 2 ∥ 1^{st} (z)\}$
227	84 226	syl5eq	$⊢ φ \to ⋃_{u = ⌊\frac{M}{2}⌋ + 1}^{M} \{z \in S \| 1^{st} (z) = P - 2 u\} = \{z \in S \| \neg 2 ∥ 1^{st} (z)\}$
228	227	fveq2d	$⊢ φ \to \|⋃_{u = ⌊\frac{M}{2}⌋ + 1}^{M} \{z \in S \| 1^{st} (z) = P - 2 u\}\| = \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|$
229	6	relopabi	$⊢ Rel S$
230		relss	$⊢ \{z \in S \| 1^{st} (z) = P - 2 u\} \subseteq S \to (Rel S \to Rel \{z \in S \| 1^{st} (z) = P - 2 u\})$
231	57 229 230	mp2	$⊢ Rel \{z \in S \| 1^{st} (z) = P - 2 u\}$
232		relxp	$⊢ Rel (\{P - 2 u\} \times (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋))$
233	6	eleq2i	$⊢ ⟨x, y⟩ \in S \leftrightarrow ⟨x, y⟩ \in \{⟨x, y⟩ \| ((x \in (1 \dots M) \land y \in (1 \dots N)) \land y P < x Q)\}$
234		opabidw	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| ((x \in (1 \dots M) \land y \in (1 \dots N)) \land y P < x Q)\} \leftrightarrow ((x \in (1 \dots M) \land y \in (1 \dots N)) \land y P < x Q)$
235	233 234	bitri	$⊢ ⟨x, y⟩ \in S \leftrightarrow ((x \in (1 \dots M) \land y \in (1 \dots N)) \land y P < x Q)$
236		anass	$⊢ ((y \in ℕ \land y \leq N) \land y P < (P - 2 u) Q) \leftrightarrow (y \in ℕ \land (y \leq N \land y P < (P - 2 u) Q))$
237	24	peano2zd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊(\frac{Q}{P}) 2 u⌋ + 1 \in ℤ$
238	237	zred	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊(\frac{Q}{P}) 2 u⌋ + 1 \in ℝ$
239	238	adantr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to ⌊(\frac{Q}{P}) 2 u⌋ + 1 \in ℝ$
240	13	ad2antrr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to Q \in ℝ$
241		nnre	$⊢ y \in ℕ \to y \in ℝ$
242	241	adantl	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to y \in ℝ$
243		lesub	$⊢ (⌊(\frac{Q}{P}) 2 u⌋ + 1 \in ℝ \land Q \in ℝ \land y \in ℝ) \to (⌊(\frac{Q}{P}) 2 u⌋ + 1 \leq Q - y \leftrightarrow y \leq Q - (⌊(\frac{Q}{P}) 2 u⌋ + 1))$
244	239 240 242 243	syl3anc	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to (⌊(\frac{Q}{P}) 2 u⌋ + 1 \leq Q - y \leftrightarrow y \leq Q - (⌊(\frac{Q}{P}) 2 u⌋ + 1))$
245	13	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q \in ℝ$
246	245	recnd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q \in ℂ$
247	66 246	mulcomd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P Q = Q P$
248	68 246	mulcomd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 u Q = Q 2 u$
249	65	nnne0d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P \neq 0$
250	246 66 249	divcan1d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{Q}{P}) P = Q$
251	250	oveq1d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{Q}{P}) P 2 u = Q 2 u$
252	16	recnd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{Q}{P} \in ℂ$
253	252 66 68	mul32d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{Q}{P}) P 2 u = (\frac{Q}{P}) 2 u P$
254	248 251 253	3eqtr2d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 u Q = (\frac{Q}{P}) 2 u P$
255	247 254	oveq12d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P Q - 2 u Q = Q P - (\frac{Q}{P}) 2 u P$
256	66 68 246	subdird	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (P - 2 u) Q = P Q - 2 u Q$
257	23	recnd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{Q}{P}) 2 u \in ℂ$
258	246 257 66	subdird	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (Q - (\frac{Q}{P}) 2 u) P = Q P - (\frac{Q}{P}) 2 u P$
259	255 256 258	3eqtr4d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (P - 2 u) Q = (Q - (\frac{Q}{P}) 2 u) P$
260	259	adantr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to (P - 2 u) Q = (Q - (\frac{Q}{P}) 2 u) P$
261	260	breq2d	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to (y P < (P - 2 u) Q \leftrightarrow y P < (Q - (\frac{Q}{P}) 2 u) P)$
262	23	adantr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to (\frac{Q}{P}) 2 u \in ℝ$
263	240 262	resubcld	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to Q - (\frac{Q}{P}) 2 u \in ℝ$
264	65	adantr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to P \in ℕ$
265	264	nnred	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to P \in ℝ$
266	264	nngt0d	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to 0 < P$
267		ltmul1	$⊢ (y \in ℝ \land Q - (\frac{Q}{P}) 2 u \in ℝ \land (P \in ℝ \land 0 < P)) \to (y < Q - (\frac{Q}{P}) 2 u \leftrightarrow y P < (Q - (\frac{Q}{P}) 2 u) P)$
268	242 263 265 266 267	syl112anc	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to (y < Q - (\frac{Q}{P}) 2 u \leftrightarrow y P < (Q - (\frac{Q}{P}) 2 u) P)$
269		ltsub13	$⊢ (y \in ℝ \land Q \in ℝ \land (\frac{Q}{P}) 2 u \in ℝ) \to (y < Q - (\frac{Q}{P}) 2 u \leftrightarrow (\frac{Q}{P}) 2 u < Q - y)$
270	242 240 262 269	syl3anc	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to (y < Q - (\frac{Q}{P}) 2 u \leftrightarrow (\frac{Q}{P}) 2 u < Q - y)$
271	261 268 270	3bitr2d	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to (y P < (P - 2 u) Q \leftrightarrow (\frac{Q}{P}) 2 u < Q - y)$
272	12	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q \in ℕ$
273	272	nnzd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q \in ℤ$
274		nnz	$⊢ y \in ℕ \to y \in ℤ$
275		zsubcl	$⊢ (Q \in ℤ \land y \in ℤ) \to Q - y \in ℤ$
276	273 274 275	syl2an	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to Q - y \in ℤ$
277		fllt	$⊢ ((\frac{Q}{P}) 2 u \in ℝ \land Q - y \in ℤ) \to ((\frac{Q}{P}) 2 u < Q - y \leftrightarrow ⌊(\frac{Q}{P}) 2 u⌋ < Q - y)$
278	262 276 277	syl2anc	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to ((\frac{Q}{P}) 2 u < Q - y \leftrightarrow ⌊(\frac{Q}{P}) 2 u⌋ < Q - y)$
279	24	adantr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to ⌊(\frac{Q}{P}) 2 u⌋ \in ℤ$
280		zltp1le	$⊢ (⌊(\frac{Q}{P}) 2 u⌋ \in ℤ \land Q - y \in ℤ) \to (⌊(\frac{Q}{P}) 2 u⌋ < Q - y \leftrightarrow ⌊(\frac{Q}{P}) 2 u⌋ + 1 \leq Q - y)$
281	279 276 280	syl2anc	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to (⌊(\frac{Q}{P}) 2 u⌋ < Q - y \leftrightarrow ⌊(\frac{Q}{P}) 2 u⌋ + 1 \leq Q - y)$
282	271 278 281	3bitrd	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to (y P < (P - 2 u) Q \leftrightarrow ⌊(\frac{Q}{P}) 2 u⌋ + 1 \leq Q - y)$
283	5	oveq2i	$⊢ 2 \cdot N = 2 (\frac{Q - 1}{2})$
284		peano2rem	$⊢ Q \in ℝ \to Q - 1 \in ℝ$
285	245 284	syl	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q - 1 \in ℝ$
286	285	recnd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q - 1 \in ℂ$
287		2cnd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \in ℂ$
288	76	a1i	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \neq 0$
289	286 287 288	divcan2d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 (\frac{Q - 1}{2}) = Q - 1$
290	283 289	syl5eq	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N = Q - 1$
291	290	oveq1d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ = Q - 1 - ⌊(\frac{Q}{P}) 2 u⌋$
292		1cnd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 1 \in ℂ$
293	24	zcnd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊(\frac{Q}{P}) 2 u⌋ \in ℂ$
294	246 292 293	sub32d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q - 1 - ⌊(\frac{Q}{P}) 2 u⌋ = Q - ⌊(\frac{Q}{P}) 2 u⌋ - 1$
295	246 293 292	subsub4d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q - ⌊(\frac{Q}{P}) 2 u⌋ - 1 = Q - (⌊(\frac{Q}{P}) 2 u⌋ + 1)$
296	291 294 295	3eqtrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ = Q - (⌊(\frac{Q}{P}) 2 u⌋ + 1)$
297	296	adantr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ = Q - (⌊(\frac{Q}{P}) 2 u⌋ + 1)$
298	297	breq2d	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to (y \leq 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \leftrightarrow y \leq Q - (⌊(\frac{Q}{P}) 2 u⌋ + 1))$
299	244 282 298	3bitr4d	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to (y P < (P - 2 u) Q \leftrightarrow y \leq 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)$
300	299	anbi2d	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to ((y \leq N \land y P < (P - 2 u) Q) \leftrightarrow (y \leq N \land y \leq 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋))$
301		2nn	$⊢ 2 \in ℕ$
302	2 5	gausslemma2dlem0b	$⊢ φ \to N \in ℕ$
303		nnmulcl	$⊢ (2 \in ℕ \land N \in ℕ) \to 2 \cdot N \in ℕ$
304	301 302 303	sylancr	$⊢ φ \to 2 \cdot N \in ℕ$
305	304	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N \in ℕ$
306	305	nnred	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N \in ℝ$
307	302	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to N \in ℕ$
308	307	nnred	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to N \in ℝ$
309	24	zred	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊(\frac{Q}{P}) 2 u⌋ \in ℝ$
310	302	nncnd	$⊢ φ \to N \in ℂ$
311	310	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to N \in ℂ$
312	311	2timesd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N = N + N$
313	311 311 312	mvrladdd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N - N = N$
314	245	rehalfcld	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{Q}{2} \in ℝ$
315	245	ltm1d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q - 1 < Q$
316	150	a1i	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \in ℝ$
317	152	a1i	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 0 < 2$
318		ltdiv1	$⊢ (Q - 1 \in ℝ \land Q \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (Q - 1 < Q \leftrightarrow \frac{Q - 1}{2} < \frac{Q}{2})$
319	285 245 316 317 318	syl112anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (Q - 1 < Q \leftrightarrow \frac{Q - 1}{2} < \frac{Q}{2})$
320	315 319	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{Q - 1}{2} < \frac{Q}{2}$
321	5 320	eqbrtrid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to N < \frac{Q}{2}$
322	308 314 321	ltled	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to N \leq \frac{Q}{2}$
323	246 287 66 288	div32d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{Q}{2}) P = Q (\frac{P}{2})$
324	126	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to M \in ℝ$
325	324	rehalfcld	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{M}{2} \in ℝ$
326		peano2re	$⊢ ⌊\frac{M}{2}⌋ \in ℝ \to ⌊\frac{M}{2}⌋ + 1 \in ℝ$
327	325 129 326	3syl	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊\frac{M}{2}⌋ + 1 \in ℝ$
328	19	zred	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to u \in ℝ$
329		flltp1	$⊢ \frac{M}{2} \in ℝ \to \frac{M}{2} < ⌊\frac{M}{2}⌋ + 1$
330	325 329	syl	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{M}{2} < ⌊\frac{M}{2}⌋ + 1$
331		elfzle1	$⊢ u \in (⌊\frac{M}{2}⌋ + 1 \dots M) \to ⌊\frac{M}{2}⌋ + 1 \leq u$
332	331	adantl	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊\frac{M}{2}⌋ + 1 \leq u$
333	325 327 328 330 332	ltletrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{M}{2} < u$
334		ltdivmul	$⊢ (M \in ℝ \land u \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (\frac{M}{2} < u \leftrightarrow M < 2 u)$
335	324 328 316 317 334	syl112anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{M}{2} < u \leftrightarrow M < 2 u)$
336	333 335	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to M < 2 u$
337	4 336	eqbrtrrid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{P - 1}{2} < 2 u$
338	65	nnred	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P \in ℝ$
339		peano2rem	$⊢ P \in ℝ \to P - 1 \in ℝ$
340	338 339	syl	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 1 \in ℝ$
341		ltdivmul	$⊢ (P - 1 \in ℝ \land 2 u \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (\frac{P - 1}{2} < 2 u \leftrightarrow P - 1 < 2 2 u)$
342	340 22 316 317 341	syl112anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{P - 1}{2} < 2 u \leftrightarrow P - 1 < 2 2 u)$
343	337 342	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 1 < 2 2 u$
344	206	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P \in ℤ$
345		zmulcl	$⊢ (2 \in ℤ \land 2 u \in ℤ) \to 2 2 u \in ℤ$
346	17 21 345	sylancr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 2 u \in ℤ$
347		zlem1lt	$⊢ (P \in ℤ \land 2 2 u \in ℤ) \to (P \leq 2 2 u \leftrightarrow P - 1 < 2 2 u)$
348	344 346 347	syl2anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (P \leq 2 2 u \leftrightarrow P - 1 < 2 2 u)$
349	343 348	mpbird	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P \leq 2 2 u$
350		ledivmul	$⊢ (P \in ℝ \land 2 u \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (\frac{P}{2} \leq 2 u \leftrightarrow P \leq 2 2 u)$
351	338 22 316 317 350	syl112anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{P}{2} \leq 2 u \leftrightarrow P \leq 2 2 u)$
352	349 351	mpbird	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{P}{2} \leq 2 u$
353	338	rehalfcld	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{P}{2} \in ℝ$
354	272	nngt0d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 0 < Q$
355		lemul2	$⊢ (\frac{P}{2} \in ℝ \land 2 u \in ℝ \land (Q \in ℝ \land 0 < Q)) \to (\frac{P}{2} \leq 2 u \leftrightarrow Q (\frac{P}{2}) \leq Q 2 u)$
356	353 22 245 354 355	syl112anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{P}{2} \leq 2 u \leftrightarrow Q (\frac{P}{2}) \leq Q 2 u)$
357	352 356	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q (\frac{P}{2}) \leq Q 2 u$
358	323 357	eqbrtrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{Q}{2}) P \leq Q 2 u$
359	245 22	remulcld	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q 2 u \in ℝ$
360	65	nngt0d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 0 < P$
361		lemuldiv	$⊢ (\frac{Q}{2} \in ℝ \land Q 2 u \in ℝ \land (P \in ℝ \land 0 < P)) \to ((\frac{Q}{2}) P \leq Q 2 u \leftrightarrow \frac{Q}{2} \leq \frac{Q 2 u}{P})$
362	314 359 338 360 361	syl112anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ((\frac{Q}{2}) P \leq Q 2 u \leftrightarrow \frac{Q}{2} \leq \frac{Q 2 u}{P})$
363	358 362	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{Q}{2} \leq \frac{Q 2 u}{P}$
364	246 68 66 249	div23d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{Q 2 u}{P} = (\frac{Q}{P}) 2 u$
365	363 364	breqtrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{Q}{2} \leq (\frac{Q}{P}) 2 u$
366	308 314 23 322 365	letrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to N \leq (\frac{Q}{P}) 2 u$
367	302	nnzd	$⊢ φ \to N \in ℤ$
368	367	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to N \in ℤ$
369		flge	$⊢ ((\frac{Q}{P}) 2 u \in ℝ \land N \in ℤ) \to (N \leq (\frac{Q}{P}) 2 u \leftrightarrow N \leq ⌊(\frac{Q}{P}) 2 u⌋)$
370	23 368 369	syl2anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (N \leq (\frac{Q}{P}) 2 u \leftrightarrow N \leq ⌊(\frac{Q}{P}) 2 u⌋)$
371	366 370	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to N \leq ⌊(\frac{Q}{P}) 2 u⌋$
372	313 371	eqbrtrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N - N \leq ⌊(\frac{Q}{P}) 2 u⌋$
373	306 308 309 372	subled	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \leq N$
374	373	adantr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \leq N$
375	305	nnzd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N \in ℤ$
376	375 24	zsubcld	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \in ℤ$
377	376	adantr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \in ℤ$
378	377	zred	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \in ℝ$
379	302	ad2antrr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to N \in ℕ$
380	379	nnred	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to N \in ℝ$
381		letr	$⊢ (y \in ℝ \land 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \in ℝ \land N \in ℝ) \to ((y \leq 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \land 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \leq N) \to y \leq N)$
382	242 378 380 381	syl3anc	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to ((y \leq 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \land 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \leq N) \to y \leq N)$
383	374 382	mpan2d	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to (y \leq 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \to y \leq N)$
384	383	pm4.71rd	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to (y \leq 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \leftrightarrow (y \leq N \land y \leq 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋))$
385	300 384	bitr4d	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to ((y \leq N \land y P < (P - 2 u) Q) \leftrightarrow y \leq 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)$
386	385	pm5.32da	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ((y \in ℕ \land (y \leq N \land y P < (P - 2 u) Q)) \leftrightarrow (y \in ℕ \land y \leq 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋))$
387	386	adantr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to ((y \in ℕ \land (y \leq N \land y P < (P - 2 u) Q)) \leftrightarrow (y \in ℕ \land y \leq 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋))$
388	236 387	syl5bb	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to (((y \in ℕ \land y \leq N) \land y P < (P - 2 u) Q) \leftrightarrow (y \in ℕ \land y \leq 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋))$
389		simpr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to x = P - 2 u$
390	344 21	zsubcld	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 2 u \in ℤ$
391		elfzle2	$⊢ u \in (⌊\frac{M}{2}⌋ + 1 \dots M) \to u \leq M$
392	391	adantl	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to u \leq M$
393	392 4	breqtrdi	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to u \leq \frac{P - 1}{2}$
394		lemuldiv2	$⊢ (u \in ℝ \land P - 1 \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 u \leq P - 1 \leftrightarrow u \leq \frac{P - 1}{2})$
395	328 340 316 317 394	syl112anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (2 u \leq P - 1 \leftrightarrow u \leq \frac{P - 1}{2})$
396	393 395	mpbird	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 u \leq P - 1$
397	338	ltm1d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 1 < P$
398	22 340 338 396 397	lelttrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 u < P$
399	22 338	posdifd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (2 u < P \leftrightarrow 0 < P - 2 u)$
400	398 399	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 0 < P - 2 u$
401		elnnz	$⊢ P - 2 u \in ℕ \leftrightarrow (P - 2 u \in ℤ \land 0 < P - 2 u)$
402	390 400 401	sylanbrc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 2 u \in ℕ$
403	66 68 292	sub32d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 2 u - 1 = P - 1 - 2 u$
404	4 4	oveq12i	$⊢ M + M = (\frac{P - 1}{2}) + (\frac{P - 1}{2})$
405	65	nnzd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P \in ℤ$
406	405 208	syl	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 1 \in ℤ$
407	406	zcnd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 1 \in ℂ$
408	407	2halvesd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{P - 1}{2}) + (\frac{P - 1}{2}) = P - 1$
409	404 408	syl5eq	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to M + M = P - 1$
410	409	oveq1d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to M + M - M = P - 1 - M$
411	158	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to M \in ℂ$
412	411 411	pncan2d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to M + M - M = M$
413	410 412	eqtr3d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 1 - M = M$
414	413 336	eqbrtrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 1 - M < 2 u$
415	340 324 22 414	ltsub23d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 1 - 2 u < M$
416	403 415	eqbrtrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 2 u - 1 < M$
417	125	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to M \in ℕ$
418	417	nnzd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to M \in ℤ$
419		zlem1lt	$⊢ (P - 2 u \in ℤ \land M \in ℤ) \to (P - 2 u \leq M \leftrightarrow P - 2 u - 1 < M)$
420	390 418 419	syl2anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (P - 2 u \leq M \leftrightarrow P - 2 u - 1 < M)$
421	416 420	mpbird	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 2 u \leq M$
422		fznn	$⊢ M \in ℤ \to (P - 2 u \in (1 \dots M) \leftrightarrow (P - 2 u \in ℕ \land P - 2 u \leq M))$
423	418 422	syl	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (P - 2 u \in (1 \dots M) \leftrightarrow (P - 2 u \in ℕ \land P - 2 u \leq M))$
424	402 421 423	mpbir2and	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 2 u \in (1 \dots M)$
425	424	adantr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to P - 2 u \in (1 \dots M)$
426	389 425	eqeltrd	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to x \in (1 \dots M)$
427	426	biantrurd	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to (y \in (1 \dots N) \leftrightarrow (x \in (1 \dots M) \land y \in (1 \dots N)))$
428	367	ad2antrr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to N \in ℤ$
429		fznn	$⊢ N \in ℤ \to (y \in (1 \dots N) \leftrightarrow (y \in ℕ \land y \leq N))$
430	428 429	syl	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to (y \in (1 \dots N) \leftrightarrow (y \in ℕ \land y \leq N))$
431	427 430	bitr3d	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to ((x \in (1 \dots M) \land y \in (1 \dots N)) \leftrightarrow (y \in ℕ \land y \leq N))$
432	389	oveq1d	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to x Q = (P - 2 u) Q$
433	432	breq2d	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to (y P < x Q \leftrightarrow y P < (P - 2 u) Q)$
434	431 433	anbi12d	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to (((x \in (1 \dots M) \land y \in (1 \dots N)) \land y P < x Q) \leftrightarrow ((y \in ℕ \land y \leq N) \land y P < (P - 2 u) Q))$
435	376	adantr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \in ℤ$
436		fznn	$⊢ 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \in ℤ \to (y \in (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋) \leftrightarrow (y \in ℕ \land y \leq 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋))$
437	435 436	syl	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to (y \in (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋) \leftrightarrow (y \in ℕ \land y \leq 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋))$
438	388 434 437	3bitr4d	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to (((x \in (1 \dots M) \land y \in (1 \dots N)) \land y P < x Q) \leftrightarrow y \in (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋))$
439	235 438	syl5bb	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to (⟨x, y⟩ \in S \leftrightarrow y \in (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋))$
440	439	pm5.32da	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ((x = P - 2 u \land ⟨x, y⟩ \in S) \leftrightarrow (x = P - 2 u \land y \in (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)))$
441		vex	$⊢ x \in V$
442		vex	$⊢ y \in V$
443	441 442	op1std	$⊢ z = ⟨x, y⟩ \to 1^{st} (z) = x$
444	443	eqeq1d	$⊢ z = ⟨x, y⟩ \to (1^{st} (z) = P - 2 u \leftrightarrow x = P - 2 u)$
445	444	elrab	$⊢ ⟨x, y⟩ \in \{z \in S \| 1^{st} (z) = P - 2 u\} \leftrightarrow (⟨x, y⟩ \in S \land x = P - 2 u)$
446	445	biancomi	$⊢ ⟨x, y⟩ \in \{z \in S \| 1^{st} (z) = P - 2 u\} \leftrightarrow (x = P - 2 u \land ⟨x, y⟩ \in S)$
447		opelxp	$⊢ ⟨x, y⟩ \in (\{P - 2 u\} \times (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)) \leftrightarrow (x \in \{P - 2 u\} \land y \in (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋))$
448		velsn	$⊢ x \in \{P - 2 u\} \leftrightarrow x = P - 2 u$
449	448	anbi1i	$⊢ (x \in \{P - 2 u\} \land y \in (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)) \leftrightarrow (x = P - 2 u \land y \in (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋))$
450	447 449	bitri	$⊢ ⟨x, y⟩ \in (\{P - 2 u\} \times (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)) \leftrightarrow (x = P - 2 u \land y \in (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋))$
451	440 446 450	3bitr4g	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (⟨x, y⟩ \in \{z \in S \| 1^{st} (z) = P - 2 u\} \leftrightarrow ⟨x, y⟩ \in (\{P - 2 u\} \times (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)))$
452	231 232 451	eqrelrdv	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \{z \in S \| 1^{st} (z) = P - 2 u\} = \{P - 2 u\} \times (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)$
453	452	fveq2d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \|\{z \in S \| 1^{st} (z) = P - 2 u\}\| = \|\{P - 2 u\} \times (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)\|$
454		fzfid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋) \in Fin$
455		xpsnen2g	$⊢ (P - 2 u \in ℤ \land (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋) \in Fin) \to (\{P - 2 u\} \times (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)) \approx (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)$
456	390 454 455	syl2anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\{P - 2 u\} \times (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)) \approx (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)$
457		hasheni	$⊢ (\{P - 2 u\} \times (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)) \approx (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋) \to \|\{P - 2 u\} \times (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)\| = \|(1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)\|$
458	456 457	syl	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \|\{P - 2 u\} \times (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)\| = \|(1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)\|$
459		ltmul2	$⊢ (2 u \in ℝ \land P \in ℝ \land (Q \in ℝ \land 0 < Q)) \to (2 u < P \leftrightarrow Q 2 u < Q P)$
460	22 338 245 354 459	syl112anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (2 u < P \leftrightarrow Q 2 u < Q P)$
461	398 460	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q 2 u < Q P$
462		ltdivmul2	$⊢ (Q 2 u \in ℝ \land Q \in ℝ \land (P \in ℝ \land 0 < P)) \to (\frac{Q 2 u}{P} < Q \leftrightarrow Q 2 u < Q P)$
463	359 245 338 360 462	syl112anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{Q 2 u}{P} < Q \leftrightarrow Q 2 u < Q P)$
464	461 463	mpbird	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{Q 2 u}{P} < Q$
465	364 464	eqbrtrrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{Q}{P}) 2 u < Q$
466		fllt	$⊢ ((\frac{Q}{P}) 2 u \in ℝ \land Q \in ℤ) \to ((\frac{Q}{P}) 2 u < Q \leftrightarrow ⌊(\frac{Q}{P}) 2 u⌋ < Q)$
467	23 273 466	syl2anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ((\frac{Q}{P}) 2 u < Q \leftrightarrow ⌊(\frac{Q}{P}) 2 u⌋ < Q)$
468	465 467	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊(\frac{Q}{P}) 2 u⌋ < Q$
469		zltlem1	$⊢ (⌊(\frac{Q}{P}) 2 u⌋ \in ℤ \land Q \in ℤ) \to (⌊(\frac{Q}{P}) 2 u⌋ < Q \leftrightarrow ⌊(\frac{Q}{P}) 2 u⌋ \leq Q - 1)$
470	24 273 469	syl2anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (⌊(\frac{Q}{P}) 2 u⌋ < Q \leftrightarrow ⌊(\frac{Q}{P}) 2 u⌋ \leq Q - 1)$
471	468 470	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊(\frac{Q}{P}) 2 u⌋ \leq Q - 1$
472	471 290	breqtrrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊(\frac{Q}{P}) 2 u⌋ \leq 2 \cdot N$
473		eluz2	$⊢ 2 \cdot N \in ℤ_{\geq ⌊(\frac{Q}{P}) 2 u⌋} \leftrightarrow (⌊(\frac{Q}{P}) 2 u⌋ \in ℤ \land 2 \cdot N \in ℤ \land ⌊(\frac{Q}{P}) 2 u⌋ \leq 2 \cdot N)$
474	24 375 472 473	syl3anbrc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N \in ℤ_{\geq ⌊(\frac{Q}{P}) 2 u⌋}$
475		uznn0sub	$⊢ 2 \cdot N \in ℤ_{\geq ⌊(\frac{Q}{P}) 2 u⌋} \to 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \in ℕ_{0}$
476		hashfz1	$⊢ 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \in ℕ_{0} \to \|(1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)\| = 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋$
477	474 475 476	3syl	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \|(1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)\| = 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋$
478	453 458 477	3eqtrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \|\{z \in S \| 1^{st} (z) = P - 2 u\}\| = 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋$
479	478	sumeq2dv	$⊢ φ \to \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} \|\{z \in S \| 1^{st} (z) = P - 2 u\}\| = \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} (2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋)$
480	83 228 479	3eqtr3rd	$⊢ φ \to \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} (2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋) = \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|$
481	304	nncnd	$⊢ φ \to 2 \cdot N \in ℂ$
482	481	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N \in ℂ$
483	11 482 293	fsumsub	$⊢ φ \to \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} (2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋) = \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} 2 \cdot N - \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋$
484	480 483	eqtr3d	$⊢ φ \to \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\| = \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} 2 \cdot N - \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋$
485	484	oveq2d	$⊢ φ \to \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋ + \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\| = \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋ + \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} 2 \cdot N - \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋$
486	25	zcnd	$⊢ φ \to \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋ \in ℂ$
487	11 375	fsumzcl	$⊢ φ \to \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} 2 \cdot N \in ℤ$
488	487	zcnd	$⊢ φ \to \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} 2 \cdot N \in ℂ$
489	486 488	pncan3d	$⊢ φ \to \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋ + \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} 2 \cdot N - \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋ = \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} 2 \cdot N$
490		fsumconst	$⊢ ((⌊\frac{M}{2}⌋ + 1 \dots M) \in Fin \land 2 \cdot N \in ℂ) \to \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} 2 \cdot N = \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| 2 \cdot N$
491	11 481 490	syl2anc	$⊢ φ \to \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} 2 \cdot N = \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| 2 \cdot N$
492		hashcl	$⊢ (⌊\frac{M}{2}⌋ + 1 \dots M) \in Fin \to \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \in ℕ_{0}$
493	11 492	syl	$⊢ φ \to \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \in ℕ_{0}$
494	493	nn0cnd	$⊢ φ \to \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \in ℂ$
495		2cnd	$⊢ φ \to 2 \in ℂ$
496	494 495 310	mul12d	$⊢ φ \to \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| 2 \cdot N = 2 \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N$
497	491 496	eqtrd	$⊢ φ \to \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} 2 \cdot N = 2 \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N$
498	485 489 497	3eqtrd	$⊢ φ \to \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋ + \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\| = 2 \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N$
499	498	oveq2d	$⊢ φ \to {(- 1)}^{\sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋ + \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} = {(- 1)}^{2 \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N}$
500	17	a1i	$⊢ φ \to 2 \in ℤ$
501	493	nn0zd	$⊢ φ \to \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \in ℤ$
502	501 367	zmulcld	$⊢ φ \to \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N \in ℤ$
503		expmulz	$⊢ ((- 1 \in ℂ \land - 1 \neq 0) \land (2 \in ℤ \land \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N \in ℤ)) \to {(- 1)}^{2 \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N} = {({-1}^{2})}^{\|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N}$
504	8 10 500 502 503	syl22anc	$⊢ φ \to {(- 1)}^{2 \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N} = {({-1}^{2})}^{\|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N}$
505		neg1sqe1	$⊢ {(- 1)}^{2} = 1$
506	505	oveq1i	$⊢ {({-1}^{2})}^{\|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N} = 1^{\|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N}$
507		1exp	$⊢ \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N \in ℤ \to 1^{\|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N} = 1$
508	502 507	syl	$⊢ φ \to 1^{\|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N} = 1$
509	506 508	syl5eq	$⊢ φ \to {({-1}^{2})}^{\|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N} = 1$
510	499 504 509	3eqtrd	$⊢ φ \to {(- 1)}^{\sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋ + \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} = 1$
511	44 55 510	3eqtr4d	$⊢ φ \to {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} = {(- 1)}^{\sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋ + \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|}$
512		expaddz	$⊢ ((- 1 \in ℂ \land - 1 \neq 0) \land (\sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋ \in ℤ \land \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\| \in ℤ)) \to {(- 1)}^{\sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋ + \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} = {(- 1)}^{\sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋} {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|}$
513	8 10 25 42 512	syl22anc	$⊢ φ \to {(- 1)}^{\sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋ + \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} = {(- 1)}^{\sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋} {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|}$
514	511 513	eqtr2d	$⊢ φ \to {(- 1)}^{\sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋} {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} = {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|}$
515	26 41 41 43 514	mulcan2ad	$⊢ φ \to {(- 1)}^{\sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋} = {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|}$

Metamath Proof Explorer

Theorem lgsquadlem1

Proof