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	128	flcld	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to ⌊\frac{M}{2}⌋ \in ℤ$
130	129	peano2zd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to ⌊\frac{M}{2}⌋ + 1 \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		reflcl	$⊢ \frac{M}{2} \in ℝ \to ⌊\frac{M}{2}⌋ \in ℝ$
136	128 135	syl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to ⌊\frac{M}{2}⌋ \in ℝ$
137	134	zred	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to M - n \in ℝ$
138		flle	$⊢ \frac{M}{2} \in ℝ \to ⌊\frac{M}{2}⌋ \leq \frac{M}{2}$
139	128 138	syl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to ⌊\frac{M}{2}⌋ \leq \frac{M}{2}$
140		zre	$⊢ n \in ℤ \to n \in ℝ$
141	140	ad2antrl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to n \in ℝ$
142		simprr	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n + 1 = 1^{st} (z)$
143	121	adantr	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 1^{st} (z) \in (1 \dots M)$
144	142 143	eqeltrd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n + 1 \in (1 \dots M)$
145		elfzle2	$⊢ 2 n + 1 \in (1 \dots M) \to 2 n + 1 \leq M$
146	144 145	syl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n + 1 \leq M$
147		zmulcl	$⊢ (2 \in ℤ \land n \in ℤ) \to 2 n \in ℤ$
148	17 133 147	sylancr	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n \in ℤ$
149		zltp1le	$⊢ (2 n \in ℤ \land M \in ℤ) \to (2 n < M \leftrightarrow 2 n + 1 \leq M)$
150	148 132 149	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)$
151	146 150	mpbird	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n < M$
152		2re	$⊢ 2 \in ℝ$
153	152	a1i	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 \in ℝ$
154		2pos	$⊢ 0 < 2$
155	154	a1i	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 0 < 2$
156		ltmuldiv2	$⊢ (n \in ℝ \land M \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 n < M \leftrightarrow n < \frac{M}{2})$
157	141 127 153 155 156	syl112anc	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to (2 n < M \leftrightarrow n < \frac{M}{2})$
158	151 157	mpbid	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to n < \frac{M}{2}$
159	128	recnd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to \frac{M}{2} \in ℂ$
160	125	nncnd	$⊢ φ \to M \in ℂ$
161	160	ad2antrr	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to M \in ℂ$
162	161	2halvesd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to (\frac{M}{2}) + (\frac{M}{2}) = M$
163	159 159 162	mvlraddd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to \frac{M}{2} = M - (\frac{M}{2})$
164	158 163	breqtrd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to n < M - (\frac{M}{2})$
165	141 127 128 164	ltsub13d	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to \frac{M}{2} < M - n$
166	136 128 137 139 165	lelttrd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to ⌊\frac{M}{2}⌋ < M - n$
167		zltp1le	$⊢ (⌊\frac{M}{2}⌋ \in ℤ \land M - n \in ℤ) \to (⌊\frac{M}{2}⌋ < M - n \leftrightarrow ⌊\frac{M}{2}⌋ + 1 \leq M - n)$
168	129 134 167	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)$
169	166 168	mpbid	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to ⌊\frac{M}{2}⌋ + 1 \leq M - n$
170		2t0e0	$⊢ 2 \cdot 0 = 0$
171		2cn	$⊢ 2 \in ℂ$
172		zcn	$⊢ n \in ℤ \to n \in ℂ$
173	172	ad2antrl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to n \in ℂ$
174		mulcl	$⊢ (2 \in ℂ \land n \in ℂ) \to 2 n \in ℂ$
175	171 173 174	sylancr	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n \in ℂ$
176		pncan	$⊢ (2 n \in ℂ \land 1 \in ℂ) \to 2 n + 1 - 1 = 2 n$
177	175 47 176	sylancl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n + 1 - 1 = 2 n$
178		elfznn	$⊢ 2 n + 1 \in (1 \dots M) \to 2 n + 1 \in ℕ$
179		nnm1nn0	$⊢ 2 n + 1 \in ℕ \to 2 n + 1 - 1 \in ℕ_{0}$
180	144 178 179	3syl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n + 1 - 1 \in ℕ_{0}$
181	177 180	eqeltrrd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n \in ℕ_{0}$
182	181	nn0ge0d	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 0 \leq 2 n$
183	170 182	eqbrtrid	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 \cdot 0 \leq 2 n$
184		0red	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 0 \in ℝ$
185		lemul2	$⊢ (0 \in ℝ \land n \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (0 \leq n \leftrightarrow 2 \cdot 0 \leq 2 n)$
186	184 141 153 155 185	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)$
187	183 186	mpbird	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 0 \leq n$
188	127 141	subge02d	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to (0 \leq n \leftrightarrow M - n \leq M)$
189	187 188	mpbid	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to M - n \leq M$
190	130 132 134 169 189	elfzd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to M - n \in (⌊\frac{M}{2}⌋ + 1 \dots M)$
191	92	ad2antrr	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P \in ℙ$
192		prmnn	$⊢ P \in ℙ \to P \in ℕ$
193	191 192	syl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P \in ℕ$
194	193	nncnd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P \in ℂ$
195		peano2cn	$⊢ 2 n \in ℂ \to 2 n + 1 \in ℂ$
196	175 195	syl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 n + 1 \in ℂ$
197	194 196	nncand	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P - (P - (2 n + 1)) = 2 n + 1$
198		1cnd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 1 \in ℂ$
199	194 175 198	sub32d	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P - 2 n - 1 = P - 1 - 2 n$
200	194 175 198	subsub4d	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P - 2 n - 1 = P - (2 n + 1)$
201		2cnd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 \in ℂ$
202	201 161 173	subdid	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 (M - n) = 2 \cdot M - 2 n$
203	4	oveq2i	$⊢ 2 \cdot M = 2 (\frac{P - 1}{2})$
204	14	nnzd	$⊢ φ \to P \in ℤ$
205	204	ad2antrr	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P \in ℤ$
206		peano2zm	$⊢ P \in ℤ \to P - 1 \in ℤ$
207	205 206	syl	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P - 1 \in ℤ$
208	207	zcnd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P - 1 \in ℂ$
209	76	a1i	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 \neq 0$
210	208 201 209	divcan2d	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 (\frac{P - 1}{2}) = P - 1$
211	203 210	syl5eq	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 2 \cdot M = P - 1$
212	211	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$
213	202 212	eqtr2d	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P - 1 - 2 n = 2 (M - n)$
214	199 200 213	3eqtr3d	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to P - (2 n + 1) = 2 (M - n)$
215	214	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)$
216	197 215 142	3eqtr3rd	$⊢ ((φ \land z \in S) \land (n \in ℤ \land 2 n + 1 = 1^{st} (z))) \to 1^{st} (z) = P - 2 (M - n)$
217		oveq2	$⊢ u = M - n \to 2 u = 2 (M - n)$
218	217	oveq2d	$⊢ u = M - n \to P - 2 u = P - 2 (M - n)$
219	218	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$
220	190 216 219	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$
221	220	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)$
222	124 221	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)$
223	117 222	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))$
224	223	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)\}$
225	84 224	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)\}$
226	225	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)\}\|$
227	6	relopabiv	$⊢ Rel S$
228		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\})$
229	57 227 228	mp2	$⊢ Rel \{z \in S \| 1^{st} (z) = P - 2 u\}$
230		relxp	$⊢ Rel (\{P - 2 u\} \times (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋))$
231	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)\}$
232		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)$
233	231 232	bitri	$⊢ ⟨x, y⟩ \in S \leftrightarrow ((x \in (1 \dots M) \land y \in (1 \dots N)) \land y P < x Q)$
234		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))$
235	24	peano2zd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊(\frac{Q}{P}) 2 u⌋ + 1 \in ℤ$
236	235	zred	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊(\frac{Q}{P}) 2 u⌋ + 1 \in ℝ$
237	236	adantr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to ⌊(\frac{Q}{P}) 2 u⌋ + 1 \in ℝ$
238	13	ad2antrr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to Q \in ℝ$
239		nnre	$⊢ y \in ℕ \to y \in ℝ$
240	239	adantl	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to y \in ℝ$
241		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))$
242	237 238 240 241	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))$
243	13	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q \in ℝ$
244	243	recnd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q \in ℂ$
245	66 244	mulcomd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P Q = Q P$
246	68 244	mulcomd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 u Q = Q 2 u$
247	65	nnne0d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P \neq 0$
248	244 66 247	divcan1d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{Q}{P}) P = Q$
249	248	oveq1d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{Q}{P}) P 2 u = Q 2 u$
250	16	recnd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{Q}{P} \in ℂ$
251	250 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$
252	246 249 251	3eqtr2d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 u Q = (\frac{Q}{P}) 2 u P$
253	245 252	oveq12d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P Q - 2 u Q = Q P - (\frac{Q}{P}) 2 u P$
254	66 68 244	subdird	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (P - 2 u) Q = P Q - 2 u Q$
255	23	recnd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{Q}{P}) 2 u \in ℂ$
256	244 255 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$
257	253 254 256	3eqtr4d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (P - 2 u) Q = (Q - (\frac{Q}{P}) 2 u) P$
258	257	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$
259	258	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)$
260	23	adantr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to (\frac{Q}{P}) 2 u \in ℝ$
261	238 260	resubcld	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to Q - (\frac{Q}{P}) 2 u \in ℝ$
262	65	adantr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to P \in ℕ$
263	262	nnred	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to P \in ℝ$
264	262	nngt0d	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to 0 < P$
265		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)$
266	240 261 263 264 265	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)$
267		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)$
268	240 238 260 267	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)$
269	259 266 268	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)$
270	12	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q \in ℕ$
271	270	nnzd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q \in ℤ$
272		nnz	$⊢ y \in ℕ \to y \in ℤ$
273		zsubcl	$⊢ (Q \in ℤ \land y \in ℤ) \to Q - y \in ℤ$
274	271 272 273	syl2an	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to Q - y \in ℤ$
275		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)$
276	260 274 275	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)$
277	24	adantr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to ⌊(\frac{Q}{P}) 2 u⌋ \in ℤ$
278		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)$
279	277 274 278	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)$
280	269 276 279	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)$
281	5	oveq2i	$⊢ 2 \cdot N = 2 (\frac{Q - 1}{2})$
282		peano2rem	$⊢ Q \in ℝ \to Q - 1 \in ℝ$
283	243 282	syl	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q - 1 \in ℝ$
284	283	recnd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q - 1 \in ℂ$
285		2cnd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \in ℂ$
286	76	a1i	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \neq 0$
287	284 285 286	divcan2d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 (\frac{Q - 1}{2}) = Q - 1$
288	281 287	syl5eq	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N = Q - 1$
289	288	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⌋$
290		1cnd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 1 \in ℂ$
291	24	zcnd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊(\frac{Q}{P}) 2 u⌋ \in ℂ$
292	244 290 291	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$
293	244 291 290	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)$
294	289 292 293	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)$
295	294	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)$
296	295	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))$
297	242 280 296	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⌋)$
298	297	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⌋))$
299		2nn	$⊢ 2 \in ℕ$
300	2 5	gausslemma2dlem0b	$⊢ φ \to N \in ℕ$
301		nnmulcl	$⊢ (2 \in ℕ \land N \in ℕ) \to 2 \cdot N \in ℕ$
302	299 300 301	sylancr	$⊢ φ \to 2 \cdot N \in ℕ$
303	302	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N \in ℕ$
304	303	nnred	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N \in ℝ$
305	300	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to N \in ℕ$
306	305	nnred	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to N \in ℝ$
307	24	zred	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊(\frac{Q}{P}) 2 u⌋ \in ℝ$
308	300	nncnd	$⊢ φ \to N \in ℂ$
309	308	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to N \in ℂ$
310	309	2timesd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N = N + N$
311	309 309 310	mvrladdd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N - N = N$
312	243	rehalfcld	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{Q}{2} \in ℝ$
313	243	ltm1d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q - 1 < Q$
314	152	a1i	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \in ℝ$
315	154	a1i	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 0 < 2$
316		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})$
317	283 243 314 315 316	syl112anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (Q - 1 < Q \leftrightarrow \frac{Q - 1}{2} < \frac{Q}{2})$
318	313 317	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{Q - 1}{2} < \frac{Q}{2}$
319	5 318	eqbrtrid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to N < \frac{Q}{2}$
320	306 312 319	ltled	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to N \leq \frac{Q}{2}$
321	244 285 66 286	div32d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{Q}{2}) P = Q (\frac{P}{2})$
322	126	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to M \in ℝ$
323	322	rehalfcld	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{M}{2} \in ℝ$
324		peano2re	$⊢ ⌊\frac{M}{2}⌋ \in ℝ \to ⌊\frac{M}{2}⌋ + 1 \in ℝ$
325	323 135 324	3syl	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊\frac{M}{2}⌋ + 1 \in ℝ$
326	19	zred	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to u \in ℝ$
327		flltp1	$⊢ \frac{M}{2} \in ℝ \to \frac{M}{2} < ⌊\frac{M}{2}⌋ + 1$
328	323 327	syl	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{M}{2} < ⌊\frac{M}{2}⌋ + 1$
329		elfzle1	$⊢ u \in (⌊\frac{M}{2}⌋ + 1 \dots M) \to ⌊\frac{M}{2}⌋ + 1 \leq u$
330	329	adantl	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊\frac{M}{2}⌋ + 1 \leq u$
331	323 325 326 328 330	ltletrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{M}{2} < u$
332		ltdivmul	$⊢ (M \in ℝ \land u \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (\frac{M}{2} < u \leftrightarrow M < 2 u)$
333	322 326 314 315 332	syl112anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{M}{2} < u \leftrightarrow M < 2 u)$
334	331 333	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to M < 2 u$
335	4 334	eqbrtrrid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{P - 1}{2} < 2 u$
336	65	nnred	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P \in ℝ$
337		peano2rem	$⊢ P \in ℝ \to P - 1 \in ℝ$
338	336 337	syl	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 1 \in ℝ$
339		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)$
340	338 22 314 315 339	syl112anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{P - 1}{2} < 2 u \leftrightarrow P - 1 < 2 2 u)$
341	335 340	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 1 < 2 2 u$
342	204	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P \in ℤ$
343		zmulcl	$⊢ (2 \in ℤ \land 2 u \in ℤ) \to 2 2 u \in ℤ$
344	17 21 343	sylancr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 2 u \in ℤ$
345		zlem1lt	$⊢ (P \in ℤ \land 2 2 u \in ℤ) \to (P \leq 2 2 u \leftrightarrow P - 1 < 2 2 u)$
346	342 344 345	syl2anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (P \leq 2 2 u \leftrightarrow P - 1 < 2 2 u)$
347	341 346	mpbird	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P \leq 2 2 u$
348		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)$
349	336 22 314 315 348	syl112anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{P}{2} \leq 2 u \leftrightarrow P \leq 2 2 u)$
350	347 349	mpbird	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{P}{2} \leq 2 u$
351	336	rehalfcld	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{P}{2} \in ℝ$
352	270	nngt0d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 0 < Q$
353		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)$
354	351 22 243 352 353	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)$
355	350 354	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q (\frac{P}{2}) \leq Q 2 u$
356	321 355	eqbrtrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{Q}{2}) P \leq Q 2 u$
357	243 22	remulcld	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q 2 u \in ℝ$
358	65	nngt0d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 0 < P$
359		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})$
360	312 357 336 358 359	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})$
361	356 360	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{Q}{2} \leq \frac{Q 2 u}{P}$
362	244 68 66 247	div23d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{Q 2 u}{P} = (\frac{Q}{P}) 2 u$
363	361 362	breqtrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{Q}{2} \leq (\frac{Q}{P}) 2 u$
364	306 312 23 320 363	letrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to N \leq (\frac{Q}{P}) 2 u$
365	300	nnzd	$⊢ φ \to N \in ℤ$
366	365	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to N \in ℤ$
367		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⌋)$
368	23 366 367	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⌋)$
369	364 368	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to N \leq ⌊(\frac{Q}{P}) 2 u⌋$
370	311 369	eqbrtrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N - N \leq ⌊(\frac{Q}{P}) 2 u⌋$
371	304 306 307 370	subled	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \leq N$
372	371	adantr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \leq N$
373	303	nnzd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N \in ℤ$
374	373 24	zsubcld	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \in ℤ$
375	374	adantr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \in ℤ$
376	375	zred	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \in ℝ$
377	300	ad2antrr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to N \in ℕ$
378	377	nnred	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land y \in ℕ) \to N \in ℝ$
379		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)$
380	240 376 378 379	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)$
381	372 380	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)$
382	381	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⌋))$
383	298 382	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⌋)$
384	383	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⌋))$
385	384	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⌋))$
386	234 385	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⌋))$
387		simpr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to x = P - 2 u$
388	342 21	zsubcld	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 2 u \in ℤ$
389		elfzle2	$⊢ u \in (⌊\frac{M}{2}⌋ + 1 \dots M) \to u \leq M$
390	389	adantl	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to u \leq M$
391	390 4	breqtrdi	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to u \leq \frac{P - 1}{2}$
392		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})$
393	326 338 314 315 392	syl112anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (2 u \leq P - 1 \leftrightarrow u \leq \frac{P - 1}{2})$
394	391 393	mpbird	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 u \leq P - 1$
395	336	ltm1d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 1 < P$
396	22 338 336 394 395	lelttrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 u < P$
397	22 336	posdifd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (2 u < P \leftrightarrow 0 < P - 2 u)$
398	396 397	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 0 < P - 2 u$
399		elnnz	$⊢ P - 2 u \in ℕ \leftrightarrow (P - 2 u \in ℤ \land 0 < P - 2 u)$
400	388 398 399	sylanbrc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 2 u \in ℕ$
401	66 68 290	sub32d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 2 u - 1 = P - 1 - 2 u$
402	4 4	oveq12i	$⊢ M + M = (\frac{P - 1}{2}) + (\frac{P - 1}{2})$
403	65	nnzd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P \in ℤ$
404	403 206	syl	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 1 \in ℤ$
405	404	zcnd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 1 \in ℂ$
406	405	2halvesd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{P - 1}{2}) + (\frac{P - 1}{2}) = P - 1$
407	402 406	syl5eq	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to M + M = P - 1$
408	407	oveq1d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to M + M - M = P - 1 - M$
409	160	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to M \in ℂ$
410	409 409	pncan2d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to M + M - M = M$
411	408 410	eqtr3d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 1 - M = M$
412	411 334	eqbrtrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 1 - M < 2 u$
413	338 322 22 412	ltsub23d	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 1 - 2 u < M$
414	401 413	eqbrtrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 2 u - 1 < M$
415	125	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to M \in ℕ$
416	415	nnzd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to M \in ℤ$
417		zlem1lt	$⊢ (P - 2 u \in ℤ \land M \in ℤ) \to (P - 2 u \leq M \leftrightarrow P - 2 u - 1 < M)$
418	388 416 417	syl2anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (P - 2 u \leq M \leftrightarrow P - 2 u - 1 < M)$
419	414 418	mpbird	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 2 u \leq M$
420		fznn	$⊢ M \in ℤ \to (P - 2 u \in (1 \dots M) \leftrightarrow (P - 2 u \in ℕ \land P - 2 u \leq M))$
421	416 420	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))$
422	400 419 421	mpbir2and	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to P - 2 u \in (1 \dots M)$
423	422	adantr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to P - 2 u \in (1 \dots M)$
424	387 423	eqeltrd	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to x \in (1 \dots M)$
425	424	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)))$
426	365	ad2antrr	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to N \in ℤ$
427		fznn	$⊢ N \in ℤ \to (y \in (1 \dots N) \leftrightarrow (y \in ℕ \land y \leq N))$
428	426 427	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))$
429	425 428	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))$
430	387	oveq1d	$⊢ ((φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \land x = P - 2 u) \to x Q = (P - 2 u) Q$
431	430	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)$
432	429 431	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))$
433	374	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 ℤ$
434		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⌋))$
435	433 434	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⌋))$
436	386 432 435	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⌋))$
437	233 436	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⌋))$
438	437	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⌋)))$
439		vex	$⊢ x \in V$
440		vex	$⊢ y \in V$
441	439 440	op1std	$⊢ z = ⟨x, y⟩ \to 1^{st} (z) = x$
442	441	eqeq1d	$⊢ z = ⟨x, y⟩ \to (1^{st} (z) = P - 2 u \leftrightarrow x = P - 2 u)$
443	442	elrab	$⊢ ⟨x, y⟩ \in \{z \in S \| 1^{st} (z) = P - 2 u\} \leftrightarrow (⟨x, y⟩ \in S \land x = P - 2 u)$
444	443	biancomi	$⊢ ⟨x, y⟩ \in \{z \in S \| 1^{st} (z) = P - 2 u\} \leftrightarrow (x = P - 2 u \land ⟨x, y⟩ \in S)$
445		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⌋))$
446		velsn	$⊢ x \in \{P - 2 u\} \leftrightarrow x = P - 2 u$
447	446	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⌋))$
448	445 447	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⌋))$
449	438 444 448	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⌋)))$
450	229 230 449	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⌋)$
451	450	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⌋)\|$
452		fzfid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (1 \dots 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋) \in Fin$
453		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⌋)$
454	388 452 453	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⌋)$
455		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⌋)\|$
456	454 455	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⌋)\|$
457		ltmul2	$⊢ (2 u \in ℝ \land P \in ℝ \land (Q \in ℝ \land 0 < Q)) \to (2 u < P \leftrightarrow Q 2 u < Q P)$
458	22 336 243 352 457	syl112anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (2 u < P \leftrightarrow Q 2 u < Q P)$
459	396 458	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to Q 2 u < Q P$
460		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)$
461	357 243 336 358 460	syl112anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{Q 2 u}{P} < Q \leftrightarrow Q 2 u < Q P)$
462	459 461	mpbird	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to \frac{Q 2 u}{P} < Q$
463	362 462	eqbrtrrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to (\frac{Q}{P}) 2 u < Q$
464		fllt	$⊢ ((\frac{Q}{P}) 2 u \in ℝ \land Q \in ℤ) \to ((\frac{Q}{P}) 2 u < Q \leftrightarrow ⌊(\frac{Q}{P}) 2 u⌋ < Q)$
465	23 271 464	syl2anc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ((\frac{Q}{P}) 2 u < Q \leftrightarrow ⌊(\frac{Q}{P}) 2 u⌋ < Q)$
466	463 465	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊(\frac{Q}{P}) 2 u⌋ < Q$
467		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)$
468	24 271 467	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)$
469	466 468	mpbid	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊(\frac{Q}{P}) 2 u⌋ \leq Q - 1$
470	469 288	breqtrrd	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊(\frac{Q}{P}) 2 u⌋ \leq 2 \cdot N$
471		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)$
472	24 373 470 471	syl3anbrc	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N \in ℤ_{\geq ⌊(\frac{Q}{P}) 2 u⌋}$
473		uznn0sub	$⊢ 2 \cdot N \in ℤ_{\geq ⌊(\frac{Q}{P}) 2 u⌋} \to 2 \cdot N - ⌊(\frac{Q}{P}) 2 u⌋ \in ℕ_{0}$
474		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⌋$
475	472 473 474	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⌋$
476	451 456 475	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⌋$
477	476	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⌋)$
478	83 226 477	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)\}\|$
479	302	nncnd	$⊢ φ \to 2 \cdot N \in ℂ$
480	479	adantr	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to 2 \cdot N \in ℂ$
481	11 480 291	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⌋$
482	478 481	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⌋$
483	482	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⌋$
484	25	zcnd	$⊢ φ \to \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋ \in ℂ$
485	11 373	fsumzcl	$⊢ φ \to \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} 2 \cdot N \in ℤ$
486	485	zcnd	$⊢ φ \to \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} 2 \cdot N \in ℂ$
487	484 486	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$
488		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$
489	11 479 488	syl2anc	$⊢ φ \to \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} 2 \cdot N = \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| 2 \cdot N$
490		hashcl	$⊢ (⌊\frac{M}{2}⌋ + 1 \dots M) \in Fin \to \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \in ℕ_{0}$
491	11 490	syl	$⊢ φ \to \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \in ℕ_{0}$
492	491	nn0cnd	$⊢ φ \to \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \in ℂ$
493		2cnd	$⊢ φ \to 2 \in ℂ$
494	492 493 308	mul12d	$⊢ φ \to \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| 2 \cdot N = 2 \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N$
495	489 494	eqtrd	$⊢ φ \to \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} 2 \cdot N = 2 \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N$
496	483 487 495	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$
497	496	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}$
498	17	a1i	$⊢ φ \to 2 \in ℤ$
499	491	nn0zd	$⊢ φ \to \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \in ℤ$
500	499 365	zmulcld	$⊢ φ \to \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N \in ℤ$
501		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}$
502	8 10 498 500 501	syl22anc	$⊢ φ \to {(- 1)}^{2 \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N} = {({-1}^{2})}^{\|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N}$
503		neg1sqe1	$⊢ {(- 1)}^{2} = 1$
504	503	oveq1i	$⊢ {({-1}^{2})}^{\|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N} = 1^{\|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N}$
505		1exp	$⊢ \|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N \in ℤ \to 1^{\|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N} = 1$
506	500 505	syl	$⊢ φ \to 1^{\|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N} = 1$
507	504 506	syl5eq	$⊢ φ \to {({-1}^{2})}^{\|(⌊\frac{M}{2}⌋ + 1 \dots M)\| \cdot N} = 1$
508	497 502 507	3eqtrd	$⊢ φ \to {(- 1)}^{\sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋ + \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} = 1$
509	44 55 508	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)\}\|}$
510		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)\}\|}$
511	8 10 25 42 510	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)\}\|}$
512	509 511	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)\}\|}$
513	26 41 41 43 512	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