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