lgsquadlem2

Description: Lemma for lgsquad . Count the members of S with even coordinates, and combine with lgsquadlem1 to get the total count of lattice points in S (up to parity). (Contributed by Mario Carneiro, 18-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	lgsquadlem2	$⊢ φ \to Q /_{L} P = {(- 1)}^{\|S\|}$

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	1 2 3	lgseisen	$⊢ φ \to Q /_{L} P = {(- 1)}^{\sum_{u = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 u⌋}$
8	4	oveq2i	$⊢ (1 \dots M) = (1 \dots \frac{P - 1}{2})$
9	8	sumeq1i	$⊢ \sum_{u = 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋ = \sum_{u = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 u⌋$
10	1 4	gausslemma2dlem0b	$⊢ φ \to M \in ℕ$
11	10	nnred	$⊢ φ \to M \in ℝ$
12	11	rehalfcld	$⊢ φ \to \frac{M}{2} \in ℝ$
13	12	flcld	$⊢ φ \to ⌊\frac{M}{2}⌋ \in ℤ$
14	13	zred	$⊢ φ \to ⌊\frac{M}{2}⌋ \in ℝ$
15	14	ltp1d	$⊢ φ \to ⌊\frac{M}{2}⌋ < ⌊\frac{M}{2}⌋ + 1$
16		fzdisj	$⊢ ⌊\frac{M}{2}⌋ < ⌊\frac{M}{2}⌋ + 1 \to (1 \dots ⌊\frac{M}{2}⌋) \cap (⌊\frac{M}{2}⌋ + 1 \dots M) = \emptyset$
17	15 16	syl	$⊢ φ \to (1 \dots ⌊\frac{M}{2}⌋) \cap (⌊\frac{M}{2}⌋ + 1 \dots M) = \emptyset$
18	10	nnrpd	$⊢ φ \to M \in ℝ^{+}$
19	18	rphalfcld	$⊢ φ \to \frac{M}{2} \in ℝ^{+}$
20	19	rpge0d	$⊢ φ \to 0 \leq \frac{M}{2}$
21		flge0nn0	$⊢ (\frac{M}{2} \in ℝ \land 0 \leq \frac{M}{2}) \to ⌊\frac{M}{2}⌋ \in ℕ_{0}$
22	12 20 21	syl2anc	$⊢ φ \to ⌊\frac{M}{2}⌋ \in ℕ_{0}$
23	10	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
24		rphalflt	$⊢ M \in ℝ^{+} \to \frac{M}{2} < M$
25	18 24	syl	$⊢ φ \to \frac{M}{2} < M$
26	10	nnzd	$⊢ φ \to M \in ℤ$
27		fllt	$⊢ (\frac{M}{2} \in ℝ \land M \in ℤ) \to (\frac{M}{2} < M \leftrightarrow ⌊\frac{M}{2}⌋ < M)$
28	12 26 27	syl2anc	$⊢ φ \to (\frac{M}{2} < M \leftrightarrow ⌊\frac{M}{2}⌋ < M)$
29	25 28	mpbid	$⊢ φ \to ⌊\frac{M}{2}⌋ < M$
30	14 11 29	ltled	$⊢ φ \to ⌊\frac{M}{2}⌋ \leq M$
31		elfz2nn0	$⊢ ⌊\frac{M}{2}⌋ \in (0 \dots M) \leftrightarrow (⌊\frac{M}{2}⌋ \in ℕ_{0} \land M \in ℕ_{0} \land ⌊\frac{M}{2}⌋ \leq M)$
32	22 23 30 31	syl3anbrc	$⊢ φ \to ⌊\frac{M}{2}⌋ \in (0 \dots M)$
33		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
34	23 33	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
35		elfzp12	$⊢ M \in ℤ_{\geq 0} \to (⌊\frac{M}{2}⌋ \in (0 \dots M) \leftrightarrow (⌊\frac{M}{2}⌋ = 0 \lor ⌊\frac{M}{2}⌋ \in (0 + 1 \dots M)))$
36	34 35	syl	$⊢ φ \to (⌊\frac{M}{2}⌋ \in (0 \dots M) \leftrightarrow (⌊\frac{M}{2}⌋ = 0 \lor ⌊\frac{M}{2}⌋ \in (0 + 1 \dots M)))$
37	32 36	mpbid	$⊢ φ \to (⌊\frac{M}{2}⌋ = 0 \lor ⌊\frac{M}{2}⌋ \in (0 + 1 \dots M))$
38		un0	$⊢ (1 \dots M) \cup \emptyset = (1 \dots M)$
39		uncom	$⊢ (1 \dots M) \cup \emptyset = \emptyset \cup (1 \dots M)$
40	38 39	eqtr3i	$⊢ (1 \dots M) = \emptyset \cup (1 \dots M)$
41		oveq2	$⊢ ⌊\frac{M}{2}⌋ = 0 \to (1 \dots ⌊\frac{M}{2}⌋) = (1 \dots 0)$
42		fz10	$⊢ (1 \dots 0) = \emptyset$
43	41 42	eqtrdi	$⊢ ⌊\frac{M}{2}⌋ = 0 \to (1 \dots ⌊\frac{M}{2}⌋) = \emptyset$
44		oveq1	$⊢ ⌊\frac{M}{2}⌋ = 0 \to ⌊\frac{M}{2}⌋ + 1 = 0 + 1$
45		0p1e1	$⊢ 0 + 1 = 1$
46	44 45	eqtrdi	$⊢ ⌊\frac{M}{2}⌋ = 0 \to ⌊\frac{M}{2}⌋ + 1 = 1$
47	46	oveq1d	$⊢ ⌊\frac{M}{2}⌋ = 0 \to (⌊\frac{M}{2}⌋ + 1 \dots M) = (1 \dots M)$
48	43 47	uneq12d	$⊢ ⌊\frac{M}{2}⌋ = 0 \to (1 \dots ⌊\frac{M}{2}⌋) \cup (⌊\frac{M}{2}⌋ + 1 \dots M) = \emptyset \cup (1 \dots M)$
49	40 48	eqtr4id	$⊢ ⌊\frac{M}{2}⌋ = 0 \to (1 \dots M) = (1 \dots ⌊\frac{M}{2}⌋) \cup (⌊\frac{M}{2}⌋ + 1 \dots M)$
50		fzsplit	$⊢ ⌊\frac{M}{2}⌋ \in (1 \dots M) \to (1 \dots M) = (1 \dots ⌊\frac{M}{2}⌋) \cup (⌊\frac{M}{2}⌋ + 1 \dots M)$
51	45	oveq1i	$⊢ (0 + 1 \dots M) = (1 \dots M)$
52	50 51	eleq2s	$⊢ ⌊\frac{M}{2}⌋ \in (0 + 1 \dots M) \to (1 \dots M) = (1 \dots ⌊\frac{M}{2}⌋) \cup (⌊\frac{M}{2}⌋ + 1 \dots M)$
53	49 52	jaoi	$⊢ (⌊\frac{M}{2}⌋ = 0 \lor ⌊\frac{M}{2}⌋ \in (0 + 1 \dots M)) \to (1 \dots M) = (1 \dots ⌊\frac{M}{2}⌋) \cup (⌊\frac{M}{2}⌋ + 1 \dots M)$
54	37 53	syl	$⊢ φ \to (1 \dots M) = (1 \dots ⌊\frac{M}{2}⌋) \cup (⌊\frac{M}{2}⌋ + 1 \dots M)$
55		fzfid	$⊢ φ \to (1 \dots M) \in Fin$
56	2	gausslemma2dlem0a	$⊢ φ \to Q \in ℕ$
57	56	nnred	$⊢ φ \to Q \in ℝ$
58	1	gausslemma2dlem0a	$⊢ φ \to P \in ℕ$
59	57 58	nndivred	$⊢ φ \to \frac{Q}{P} \in ℝ$
60	59	adantr	$⊢ (φ \land u \in (1 \dots M)) \to \frac{Q}{P} \in ℝ$
61		2nn	$⊢ 2 \in ℕ$
62		elfznn	$⊢ u \in (1 \dots M) \to u \in ℕ$
63	62	adantl	$⊢ (φ \land u \in (1 \dots M)) \to u \in ℕ$
64		nnmulcl	$⊢ (2 \in ℕ \land u \in ℕ) \to 2 u \in ℕ$
65	61 63 64	sylancr	$⊢ (φ \land u \in (1 \dots M)) \to 2 u \in ℕ$
66	65	nnred	$⊢ (φ \land u \in (1 \dots M)) \to 2 u \in ℝ$
67	60 66	remulcld	$⊢ (φ \land u \in (1 \dots M)) \to (\frac{Q}{P}) 2 u \in ℝ$
68	56	nnrpd	$⊢ φ \to Q \in ℝ^{+}$
69	58	nnrpd	$⊢ φ \to P \in ℝ^{+}$
70	68 69	rpdivcld	$⊢ φ \to \frac{Q}{P} \in ℝ^{+}$
71	70	adantr	$⊢ (φ \land u \in (1 \dots M)) \to \frac{Q}{P} \in ℝ^{+}$
72	65	nnrpd	$⊢ (φ \land u \in (1 \dots M)) \to 2 u \in ℝ^{+}$
73	71 72	rpmulcld	$⊢ (φ \land u \in (1 \dots M)) \to (\frac{Q}{P}) 2 u \in ℝ^{+}$
74	73	rpge0d	$⊢ (φ \land u \in (1 \dots M)) \to 0 \leq (\frac{Q}{P}) 2 u$
75		flge0nn0	$⊢ ((\frac{Q}{P}) 2 u \in ℝ \land 0 \leq (\frac{Q}{P}) 2 u) \to ⌊(\frac{Q}{P}) 2 u⌋ \in ℕ_{0}$
76	67 74 75	syl2anc	$⊢ (φ \land u \in (1 \dots M)) \to ⌊(\frac{Q}{P}) 2 u⌋ \in ℕ_{0}$
77	76	nn0cnd	$⊢ (φ \land u \in (1 \dots M)) \to ⌊(\frac{Q}{P}) 2 u⌋ \in ℂ$
78	17 54 55 77	fsumsplit	$⊢ φ \to \sum_{u = 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋ = \sum_{u = 1}^{⌊\frac{M}{2}⌋} ⌊(\frac{Q}{P}) 2 u⌋ + \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋$
79	9 78	eqtr3id	$⊢ φ \to \sum_{u = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 u⌋ = \sum_{u = 1}^{⌊\frac{M}{2}⌋} ⌊(\frac{Q}{P}) 2 u⌋ + \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋$
80	79	oveq2d	$⊢ φ \to {(- 1)}^{\sum_{u = 1}^{\frac{P - 1}{2}} ⌊(\frac{Q}{P}) 2 u⌋} = {(- 1)}^{\sum_{u = 1}^{⌊\frac{M}{2}⌋} ⌊(\frac{Q}{P}) 2 u⌋ + \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋}$
81		neg1cn	$⊢ - 1 \in ℂ$
82	81	a1i	$⊢ φ \to - 1 \in ℂ$
83		fzfid	$⊢ φ \to (⌊\frac{M}{2}⌋ + 1 \dots M) \in Fin$
84		ssun2	$⊢ (⌊\frac{M}{2}⌋ + 1 \dots M) \subseteq (1 \dots ⌊\frac{M}{2}⌋) \cup (⌊\frac{M}{2}⌋ + 1 \dots M)$
85	84 54	sseqtrrid	$⊢ φ \to (⌊\frac{M}{2}⌋ + 1 \dots M) \subseteq (1 \dots M)$
86	85	sselda	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to u \in (1 \dots M)$
87	86 76	syldan	$⊢ (φ \land u \in (⌊\frac{M}{2}⌋ + 1 \dots M)) \to ⌊(\frac{Q}{P}) 2 u⌋ \in ℕ_{0}$
88	83 87	fsumnn0cl	$⊢ φ \to \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋ \in ℕ_{0}$
89		fzfid	$⊢ φ \to (1 \dots ⌊\frac{M}{2}⌋) \in Fin$
90		ssun1	$⊢ (1 \dots ⌊\frac{M}{2}⌋) \subseteq (1 \dots ⌊\frac{M}{2}⌋) \cup (⌊\frac{M}{2}⌋ + 1 \dots M)$
91	90 54	sseqtrrid	$⊢ φ \to (1 \dots ⌊\frac{M}{2}⌋) \subseteq (1 \dots M)$
92	91	sselda	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to u \in (1 \dots M)$
93	92 76	syldan	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to ⌊(\frac{Q}{P}) 2 u⌋ \in ℕ_{0}$
94	89 93	fsumnn0cl	$⊢ φ \to \sum_{u = 1}^{⌊\frac{M}{2}⌋} ⌊(\frac{Q}{P}) 2 u⌋ \in ℕ_{0}$
95	82 88 94	expaddd	$⊢ φ \to {(- 1)}^{\sum_{u = 1}^{⌊\frac{M}{2}⌋} ⌊(\frac{Q}{P}) 2 u⌋ + \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋} = {(- 1)}^{\sum_{u = 1}^{⌊\frac{M}{2}⌋} ⌊(\frac{Q}{P}) 2 u⌋} {(- 1)}^{\sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋}$
96		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
97		xpfi	$⊢ ((1 \dots M) \in Fin \land (1 \dots N) \in Fin) \to (1 \dots M) \times (1 \dots N) \in Fin$
98	55 96 97	syl2anc	$⊢ φ \to (1 \dots M) \times (1 \dots N) \in Fin$
99		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)$
100	6 99	eqsstri	$⊢ S \subseteq (1 \dots M) \times (1 \dots N)$
101		ssfi	$⊢ ((1 \dots M) \times (1 \dots N) \in Fin \land S \subseteq (1 \dots M) \times (1 \dots N)) \to S \in Fin$
102	98 100 101	sylancl	$⊢ φ \to S \in Fin$
103		ssrab2	$⊢ \{z \in S \| \neg 2 ∥ 1^{st} (z)\} \subseteq S$
104		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$
105	102 103 104	sylancl	$⊢ φ \to \{z \in S \| \neg 2 ∥ 1^{st} (z)\} \in Fin$
106		hashcl	$⊢ \{z \in S \| \neg 2 ∥ 1^{st} (z)\} \in Fin \to \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\| \in ℕ_{0}$
107	105 106	syl	$⊢ φ \to \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\| \in ℕ_{0}$
108		ssrab2	$⊢ \{z \in S \| 2 ∥ 1^{st} (z)\} \subseteq S$
109		ssfi	$⊢ (S \in Fin \land \{z \in S \| 2 ∥ 1^{st} (z)\} \subseteq S) \to \{z \in S \| 2 ∥ 1^{st} (z)\} \in Fin$
110	102 108 109	sylancl	$⊢ φ \to \{z \in S \| 2 ∥ 1^{st} (z)\} \in Fin$
111		hashcl	$⊢ \{z \in S \| 2 ∥ 1^{st} (z)\} \in Fin \to \|\{z \in S \| 2 ∥ 1^{st} (z)\}\| \in ℕ_{0}$
112	110 111	syl	$⊢ φ \to \|\{z \in S \| 2 ∥ 1^{st} (z)\}\| \in ℕ_{0}$
113	82 107 112	expaddd	$⊢ φ \to {(- 1)}^{\|\{z \in S \| 2 ∥ 1^{st} (z)\}\| + \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} = {(- 1)}^{\|\{z \in S \| 2 ∥ 1^{st} (z)\}\|} {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|}$
114	92 65	syldan	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to 2 u \in ℕ$
115		fzfid	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to (1 \dots ⌊(\frac{Q}{P}) 2 u⌋) \in Fin$
116		xpsnen2g	$⊢ (2 u \in ℕ \land (1 \dots ⌊(\frac{Q}{P}) 2 u⌋) \in Fin) \to (\{2 u\} \times (1 \dots ⌊(\frac{Q}{P}) 2 u⌋)) \approx (1 \dots ⌊(\frac{Q}{P}) 2 u⌋)$
117	114 115 116	syl2anc	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to (\{2 u\} \times (1 \dots ⌊(\frac{Q}{P}) 2 u⌋)) \approx (1 \dots ⌊(\frac{Q}{P}) 2 u⌋)$
118		hasheni	$⊢ (\{2 u\} \times (1 \dots ⌊(\frac{Q}{P}) 2 u⌋)) \approx (1 \dots ⌊(\frac{Q}{P}) 2 u⌋) \to \|\{2 u\} \times (1 \dots ⌊(\frac{Q}{P}) 2 u⌋)\| = \|(1 \dots ⌊(\frac{Q}{P}) 2 u⌋)\|$
119	117 118	syl	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to \|\{2 u\} \times (1 \dots ⌊(\frac{Q}{P}) 2 u⌋)\| = \|(1 \dots ⌊(\frac{Q}{P}) 2 u⌋)\|$
120		ssrab2	$⊢ \{z \in S \| 2 u = 1^{st} (z)\} \subseteq S$
121	6	relopabiv	$⊢ Rel S$
122		relss	$⊢ \{z \in S \| 2 u = 1^{st} (z)\} \subseteq S \to (Rel S \to Rel \{z \in S \| 2 u = 1^{st} (z)\})$
123	120 121 122	mp2	$⊢ Rel \{z \in S \| 2 u = 1^{st} (z)\}$
124		relxp	$⊢ Rel (\{2 u\} \times (1 \dots ⌊(\frac{Q}{P}) 2 u⌋))$
125	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)\}$
126		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)$
127	125 126	bitri	$⊢ ⟨x, y⟩ \in S \leftrightarrow ((x \in (1 \dots M) \land y \in (1 \dots N)) \land y P < x Q)$
128		anass	$⊢ ((y \in ℕ \land y \leq N) \land y P < Q 2 u) \leftrightarrow (y \in ℕ \land (y \leq N \land y P < Q 2 u))$
129	114	adantr	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to 2 u \in ℕ$
130	129	nnred	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to 2 u \in ℝ$
131	58	ad2antrr	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to P \in ℕ$
132	131	nnred	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to P \in ℝ$
133	132	rehalfcld	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to \frac{P}{2} \in ℝ$
134	11	adantr	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to M \in ℝ$
135	134	adantr	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to M \in ℝ$
136		elfzle2	$⊢ u \in (1 \dots ⌊\frac{M}{2}⌋) \to u \leq ⌊\frac{M}{2}⌋$
137	136	adantl	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to u \leq ⌊\frac{M}{2}⌋$
138	134	rehalfcld	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to \frac{M}{2} \in ℝ$
139		elfzelz	$⊢ u \in (1 \dots ⌊\frac{M}{2}⌋) \to u \in ℤ$
140	139	adantl	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to u \in ℤ$
141		flge	$⊢ (\frac{M}{2} \in ℝ \land u \in ℤ) \to (u \leq \frac{M}{2} \leftrightarrow u \leq ⌊\frac{M}{2}⌋)$
142	138 140 141	syl2anc	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to (u \leq \frac{M}{2} \leftrightarrow u \leq ⌊\frac{M}{2}⌋)$
143	137 142	mpbird	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to u \leq \frac{M}{2}$
144		elfznn	$⊢ u \in (1 \dots ⌊\frac{M}{2}⌋) \to u \in ℕ$
145	144	adantl	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to u \in ℕ$
146	145	nnred	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to u \in ℝ$
147		2re	$⊢ 2 \in ℝ$
148	147	a1i	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to 2 \in ℝ$
149		2pos	$⊢ 0 < 2$
150	149	a1i	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to 0 < 2$
151		lemuldiv2	$⊢ (u \in ℝ \land M \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 u \leq M \leftrightarrow u \leq \frac{M}{2})$
152	146 134 148 150 151	syl112anc	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to (2 u \leq M \leftrightarrow u \leq \frac{M}{2})$
153	143 152	mpbird	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to 2 u \leq M$
154	153	adantr	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to 2 u \leq M$
155	132	ltm1d	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to P - 1 < P$
156		peano2rem	$⊢ P \in ℝ \to P - 1 \in ℝ$
157	132 156	syl	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to P - 1 \in ℝ$
158	147	a1i	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to 2 \in ℝ$
159	149	a1i	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to 0 < 2$
160		ltdiv1	$⊢ (P - 1 \in ℝ \land P \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (P - 1 < P \leftrightarrow \frac{P - 1}{2} < \frac{P}{2})$
161	157 132 158 159 160	syl112anc	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (P - 1 < P \leftrightarrow \frac{P - 1}{2} < \frac{P}{2})$
162	155 161	mpbid	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to \frac{P - 1}{2} < \frac{P}{2}$
163	4 162	eqbrtrid	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to M < \frac{P}{2}$
164	130 135 133 154 163	lelttrd	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to 2 u < \frac{P}{2}$
165	131	nnrpd	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to P \in ℝ^{+}$
166		rphalflt	$⊢ P \in ℝ^{+} \to \frac{P}{2} < P$
167	165 166	syl	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to \frac{P}{2} < P$
168	130 133 132 164 167	lttrd	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to 2 u < P$
169	130 132	ltnled	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (2 u < P \leftrightarrow \neg P \leq 2 u)$
170	168 169	mpbid	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to \neg P \leq 2 u$
171	1	eldifad	$⊢ φ \to P \in ℙ$
172	171	ad2antrr	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to P \in ℙ$
173		prmz	$⊢ P \in ℙ \to P \in ℤ$
174	172 173	syl	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to P \in ℤ$
175		dvdsle	$⊢ (P \in ℤ \land 2 u \in ℕ) \to (P ∥ 2 u \to P \leq 2 u)$
176	174 129 175	syl2anc	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (P ∥ 2 u \to P \leq 2 u)$
177	170 176	mtod	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to \neg P ∥ 2 u$
178	2	eldifad	$⊢ φ \to Q \in ℙ$
179		prmrp	$⊢ (P \in ℙ \land Q \in ℙ) \to (P \gcd Q = 1 \leftrightarrow P \neq Q)$
180	171 178 179	syl2anc	$⊢ φ \to (P \gcd Q = 1 \leftrightarrow P \neq Q)$
181	3 180	mpbird	$⊢ φ \to P \gcd Q = 1$
182	181	ad2antrr	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to P \gcd Q = 1$
183	178	ad2antrr	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to Q \in ℙ$
184		prmz	$⊢ Q \in ℙ \to Q \in ℤ$
185	183 184	syl	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to Q \in ℤ$
186	129	nnzd	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to 2 u \in ℤ$
187		coprmdvds	$⊢ (P \in ℤ \land Q \in ℤ \land 2 u \in ℤ) \to ((P ∥ Q 2 u \land P \gcd Q = 1) \to P ∥ 2 u)$
188	174 185 186 187	syl3anc	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to ((P ∥ Q 2 u \land P \gcd Q = 1) \to P ∥ 2 u)$
189	182 188	mpan2d	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (P ∥ Q 2 u \to P ∥ 2 u)$
190	177 189	mtod	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to \neg P ∥ Q 2 u$
191		nnz	$⊢ y \in ℕ \to y \in ℤ$
192	191	adantl	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to y \in ℤ$
193		dvdsmul2	$⊢ (y \in ℤ \land P \in ℤ) \to P ∥ y P$
194	192 174 193	syl2anc	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to P ∥ y P$
195		breq2	$⊢ Q 2 u = y P \to (P ∥ Q 2 u \leftrightarrow P ∥ y P)$
196	194 195	syl5ibrcom	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (Q 2 u = y P \to P ∥ Q 2 u)$
197	196	necon3bd	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (\neg P ∥ Q 2 u \to Q 2 u \neq y P)$
198	190 197	mpd	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to Q 2 u \neq y P$
199		simpr	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to y \in ℕ$
200	199 131	nnmulcld	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to y P \in ℕ$
201	200	nnred	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to y P \in ℝ$
202	56	adantr	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to Q \in ℕ$
203	202 114	nnmulcld	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to Q 2 u \in ℕ$
204	203	adantr	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to Q 2 u \in ℕ$
205	204	nnred	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to Q 2 u \in ℝ$
206	201 205	ltlend	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (y P < Q 2 u \leftrightarrow (y P \leq Q 2 u \land Q 2 u \neq y P))$
207	198 206	mpbiran2d	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (y P < Q 2 u \leftrightarrow y P \leq Q 2 u)$
208		nnre	$⊢ y \in ℕ \to y \in ℝ$
209	208	adantl	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to y \in ℝ$
210	131	nngt0d	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to 0 < P$
211		lemuldiv	$⊢ (y \in ℝ \land Q 2 u \in ℝ \land (P \in ℝ \land 0 < P)) \to (y P \leq Q 2 u \leftrightarrow y \leq \frac{Q 2 u}{P})$
212	209 205 132 210 211	syl112anc	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (y P \leq Q 2 u \leftrightarrow y \leq \frac{Q 2 u}{P})$
213	202	adantr	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to Q \in ℕ$
214	213	nncnd	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to Q \in ℂ$
215	129	nncnd	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to 2 u \in ℂ$
216	131	nncnd	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to P \in ℂ$
217	131	nnne0d	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to P \neq 0$
218	214 215 216 217	div23d	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to \frac{Q 2 u}{P} = (\frac{Q}{P}) 2 u$
219	218	breq2d	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (y \leq \frac{Q 2 u}{P} \leftrightarrow y \leq (\frac{Q}{P}) 2 u)$
220	207 212 219	3bitrd	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (y P < Q 2 u \leftrightarrow y \leq (\frac{Q}{P}) 2 u)$
221	213	nnred	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to Q \in ℝ$
222	213	nngt0d	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to 0 < Q$
223		ltmul2	$⊢ (2 u \in ℝ \land \frac{P}{2} \in ℝ \land (Q \in ℝ \land 0 < Q)) \to (2 u < \frac{P}{2} \leftrightarrow Q 2 u < Q (\frac{P}{2}))$
224	130 133 221 222 223	syl112anc	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (2 u < \frac{P}{2} \leftrightarrow Q 2 u < Q (\frac{P}{2}))$
225	164 224	mpbid	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to Q 2 u < Q (\frac{P}{2})$
226		2cnd	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to 2 \in ℂ$
227		2ne0	$⊢ 2 \neq 0$
228	227	a1i	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to 2 \neq 0$
229		divass	$⊢ (Q \in ℂ \land P \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to \frac{Q P}{2} = Q (\frac{P}{2})$
230		div23	$⊢ (Q \in ℂ \land P \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to \frac{Q P}{2} = (\frac{Q}{2}) P$
231	229 230	eqtr3d	$⊢ (Q \in ℂ \land P \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to Q (\frac{P}{2}) = (\frac{Q}{2}) P$
232	214 216 226 228 231	syl112anc	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to Q (\frac{P}{2}) = (\frac{Q}{2}) P$
233	225 232	breqtrd	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to Q 2 u < (\frac{Q}{2}) P$
234	221	rehalfcld	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to \frac{Q}{2} \in ℝ$
235	234 132	remulcld	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (\frac{Q}{2}) P \in ℝ$
236		lttr	$⊢ (y P \in ℝ \land Q 2 u \in ℝ \land (\frac{Q}{2}) P \in ℝ) \to ((y P < Q 2 u \land Q 2 u < (\frac{Q}{2}) P) \to y P < (\frac{Q}{2}) P)$
237	201 205 235 236	syl3anc	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to ((y P < Q 2 u \land Q 2 u < (\frac{Q}{2}) P) \to y P < (\frac{Q}{2}) P)$
238	233 237	mpan2d	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (y P < Q 2 u \to y P < (\frac{Q}{2}) P)$
239		ltmul1	$⊢ (y \in ℝ \land \frac{Q}{2} \in ℝ \land (P \in ℝ \land 0 < P)) \to (y < \frac{Q}{2} \leftrightarrow y P < (\frac{Q}{2}) P)$
240	209 234 132 210 239	syl112anc	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (y < \frac{Q}{2} \leftrightarrow y P < (\frac{Q}{2}) P)$
241	238 240	sylibrd	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (y P < Q 2 u \to y < \frac{Q}{2})$
242		peano2rem	$⊢ Q \in ℝ \to Q - 1 \in ℝ$
243	221 242	syl	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to Q - 1 \in ℝ$
244	243	recnd	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to Q - 1 \in ℂ$
245	214 244 226 228	divsubdird	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to \frac{Q - (Q - 1)}{2} = (\frac{Q}{2}) - (\frac{Q - 1}{2})$
246	5	oveq2i	$⊢ (\frac{Q}{2}) - N = (\frac{Q}{2}) - (\frac{Q - 1}{2})$
247	245 246	eqtr4di	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to \frac{Q - (Q - 1)}{2} = (\frac{Q}{2}) - N$
248		ax-1cn	$⊢ 1 \in ℂ$
249		nncan	$⊢ (Q \in ℂ \land 1 \in ℂ) \to Q - (Q - 1) = 1$
250	214 248 249	sylancl	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to Q - (Q - 1) = 1$
251	250	oveq1d	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to \frac{Q - (Q - 1)}{2} = \frac{1}{2}$
252		halflt1	$⊢ \frac{1}{2} < 1$
253	251 252	eqbrtrdi	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to \frac{Q - (Q - 1)}{2} < 1$
254	247 253	eqbrtrrd	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (\frac{Q}{2}) - N < 1$
255	2 5	gausslemma2dlem0b	$⊢ φ \to N \in ℕ$
256	255	ad2antrr	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to N \in ℕ$
257	256	nnred	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to N \in ℝ$
258		1red	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to 1 \in ℝ$
259	234 257 258	ltsubadd2d	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to ((\frac{Q}{2}) - N < 1 \leftrightarrow \frac{Q}{2} < N + 1)$
260	254 259	mpbid	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to \frac{Q}{2} < N + 1$
261		peano2re	$⊢ N \in ℝ \to N + 1 \in ℝ$
262	257 261	syl	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to N + 1 \in ℝ$
263		lttr	$⊢ (y \in ℝ \land \frac{Q}{2} \in ℝ \land N + 1 \in ℝ) \to ((y < \frac{Q}{2} \land \frac{Q}{2} < N + 1) \to y < N + 1)$
264	209 234 262 263	syl3anc	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to ((y < \frac{Q}{2} \land \frac{Q}{2} < N + 1) \to y < N + 1)$
265	260 264	mpan2d	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (y < \frac{Q}{2} \to y < N + 1)$
266	241 265	syld	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (y P < Q 2 u \to y < N + 1)$
267		nnleltp1	$⊢ (y \in ℕ \land N \in ℕ) \to (y \leq N \leftrightarrow y < N + 1)$
268	199 256 267	syl2anc	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (y \leq N \leftrightarrow y < N + 1)$
269	266 268	sylibrd	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (y P < Q 2 u \to y \leq N)$
270	269	pm4.71rd	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (y P < Q 2 u \leftrightarrow (y \leq N \land y P < Q 2 u))$
271	92 67	syldan	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to (\frac{Q}{P}) 2 u \in ℝ$
272		flge	$⊢ ((\frac{Q}{P}) 2 u \in ℝ \land y \in ℤ) \to (y \leq (\frac{Q}{P}) 2 u \leftrightarrow y \leq ⌊(\frac{Q}{P}) 2 u⌋)$
273	271 191 272	syl2an	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to (y \leq (\frac{Q}{P}) 2 u \leftrightarrow y \leq ⌊(\frac{Q}{P}) 2 u⌋)$
274	220 270 273	3bitr3d	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land y \in ℕ) \to ((y \leq N \land y P < Q 2 u) \leftrightarrow y \leq ⌊(\frac{Q}{P}) 2 u⌋)$
275	274	pm5.32da	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to ((y \in ℕ \land (y \leq N \land y P < Q 2 u)) \leftrightarrow (y \in ℕ \land y \leq ⌊(\frac{Q}{P}) 2 u⌋))$
276	128 275	bitrid	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to (((y \in ℕ \land y \leq N) \land y P < Q 2 u) \leftrightarrow (y \in ℕ \land y \leq ⌊(\frac{Q}{P}) 2 u⌋))$
277	276	adantr	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land x = 2 u) \to (((y \in ℕ \land y \leq N) \land y P < Q 2 u) \leftrightarrow (y \in ℕ \land y \leq ⌊(\frac{Q}{P}) 2 u⌋))$
278		simpr	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land x = 2 u) \to x = 2 u$
279		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
280	114 279	eleqtrdi	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to 2 u \in ℤ_{\geq 1}$
281	26	adantr	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to M \in ℤ$
282		elfz5	$⊢ (2 u \in ℤ_{\geq 1} \land M \in ℤ) \to (2 u \in (1 \dots M) \leftrightarrow 2 u \leq M)$
283	280 281 282	syl2anc	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to (2 u \in (1 \dots M) \leftrightarrow 2 u \leq M)$
284	153 283	mpbird	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to 2 u \in (1 \dots M)$
285	284	adantr	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land x = 2 u) \to 2 u \in (1 \dots M)$
286	278 285	eqeltrd	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land x = 2 u) \to x \in (1 \dots M)$
287	286	biantrurd	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land x = 2 u) \to (y \in (1 \dots N) \leftrightarrow (x \in (1 \dots M) \land y \in (1 \dots N)))$
288	255	nnzd	$⊢ φ \to N \in ℤ$
289	288	ad2antrr	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land x = 2 u) \to N \in ℤ$
290		fznn	$⊢ N \in ℤ \to (y \in (1 \dots N) \leftrightarrow (y \in ℕ \land y \leq N))$
291	289 290	syl	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land x = 2 u) \to (y \in (1 \dots N) \leftrightarrow (y \in ℕ \land y \leq N))$
292	287 291	bitr3d	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land x = 2 u) \to ((x \in (1 \dots M) \land y \in (1 \dots N)) \leftrightarrow (y \in ℕ \land y \leq N))$
293		oveq1	$⊢ x = 2 u \to x Q = 2 u Q$
294	114	nncnd	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to 2 u \in ℂ$
295	202	nncnd	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to Q \in ℂ$
296	294 295	mulcomd	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to 2 u Q = Q 2 u$
297	293 296	sylan9eqr	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land x = 2 u) \to x Q = Q 2 u$
298	297	breq2d	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land x = 2 u) \to (y P < x Q \leftrightarrow y P < Q 2 u)$
299	292 298	anbi12d	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land x = 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 < Q 2 u))$
300	271	flcld	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to ⌊(\frac{Q}{P}) 2 u⌋ \in ℤ$
301		fznn	$⊢ ⌊(\frac{Q}{P}) 2 u⌋ \in ℤ \to (y \in (1 \dots ⌊(\frac{Q}{P}) 2 u⌋) \leftrightarrow (y \in ℕ \land y \leq ⌊(\frac{Q}{P}) 2 u⌋))$
302	300 301	syl	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to (y \in (1 \dots ⌊(\frac{Q}{P}) 2 u⌋) \leftrightarrow (y \in ℕ \land y \leq ⌊(\frac{Q}{P}) 2 u⌋))$
303	302	adantr	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land x = 2 u) \to (y \in (1 \dots ⌊(\frac{Q}{P}) 2 u⌋) \leftrightarrow (y \in ℕ \land y \leq ⌊(\frac{Q}{P}) 2 u⌋))$
304	277 299 303	3bitr4d	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land x = 2 u) \to (((x \in (1 \dots M) \land y \in (1 \dots N)) \land y P < x Q) \leftrightarrow y \in (1 \dots ⌊(\frac{Q}{P}) 2 u⌋))$
305	127 304	bitrid	$⊢ ((φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \land x = 2 u) \to (⟨x, y⟩ \in S \leftrightarrow y \in (1 \dots ⌊(\frac{Q}{P}) 2 u⌋))$
306	305	pm5.32da	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to ((x = 2 u \land ⟨x, y⟩ \in S) \leftrightarrow (x = 2 u \land y \in (1 \dots ⌊(\frac{Q}{P}) 2 u⌋)))$
307		vex	$⊢ x \in V$
308		vex	$⊢ y \in V$
309	307 308	op1std	$⊢ z = ⟨x, y⟩ \to 1^{st} (z) = x$
310	309	eqeq2d	$⊢ z = ⟨x, y⟩ \to (2 u = 1^{st} (z) \leftrightarrow 2 u = x)$
311		eqcom	$⊢ 2 u = x \leftrightarrow x = 2 u$
312	310 311	bitrdi	$⊢ z = ⟨x, y⟩ \to (2 u = 1^{st} (z) \leftrightarrow x = 2 u)$
313	312	elrab	$⊢ ⟨x, y⟩ \in \{z \in S \| 2 u = 1^{st} (z)\} \leftrightarrow (⟨x, y⟩ \in S \land x = 2 u)$
314	313	biancomi	$⊢ ⟨x, y⟩ \in \{z \in S \| 2 u = 1^{st} (z)\} \leftrightarrow (x = 2 u \land ⟨x, y⟩ \in S)$
315		opelxp	$⊢ ⟨x, y⟩ \in (\{2 u\} \times (1 \dots ⌊(\frac{Q}{P}) 2 u⌋)) \leftrightarrow (x \in \{2 u\} \land y \in (1 \dots ⌊(\frac{Q}{P}) 2 u⌋))$
316		velsn	$⊢ x \in \{2 u\} \leftrightarrow x = 2 u$
317	316	anbi1i	$⊢ (x \in \{2 u\} \land y \in (1 \dots ⌊(\frac{Q}{P}) 2 u⌋)) \leftrightarrow (x = 2 u \land y \in (1 \dots ⌊(\frac{Q}{P}) 2 u⌋))$
318	315 317	bitri	$⊢ ⟨x, y⟩ \in (\{2 u\} \times (1 \dots ⌊(\frac{Q}{P}) 2 u⌋)) \leftrightarrow (x = 2 u \land y \in (1 \dots ⌊(\frac{Q}{P}) 2 u⌋))$
319	306 314 318	3bitr4g	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to (⟨x, y⟩ \in \{z \in S \| 2 u = 1^{st} (z)\} \leftrightarrow ⟨x, y⟩ \in (\{2 u\} \times (1 \dots ⌊(\frac{Q}{P}) 2 u⌋)))$
320	123 124 319	eqrelrdv	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to \{z \in S \| 2 u = 1^{st} (z)\} = \{2 u\} \times (1 \dots ⌊(\frac{Q}{P}) 2 u⌋)$
321	320	eqcomd	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to \{2 u\} \times (1 \dots ⌊(\frac{Q}{P}) 2 u⌋) = \{z \in S \| 2 u = 1^{st} (z)\}$
322	321	fveq2d	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to \|\{2 u\} \times (1 \dots ⌊(\frac{Q}{P}) 2 u⌋)\| = \|\{z \in S \| 2 u = 1^{st} (z)\}\|$
323		hashfz1	$⊢ ⌊(\frac{Q}{P}) 2 u⌋ \in ℕ_{0} \to \|(1 \dots ⌊(\frac{Q}{P}) 2 u⌋)\| = ⌊(\frac{Q}{P}) 2 u⌋$
324	93 323	syl	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to \|(1 \dots ⌊(\frac{Q}{P}) 2 u⌋)\| = ⌊(\frac{Q}{P}) 2 u⌋$
325	119 322 324	3eqtr3rd	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to ⌊(\frac{Q}{P}) 2 u⌋ = \|\{z \in S \| 2 u = 1^{st} (z)\}\|$
326	325	sumeq2dv	$⊢ φ \to \sum_{u = 1}^{⌊\frac{M}{2}⌋} ⌊(\frac{Q}{P}) 2 u⌋ = \sum_{u = 1}^{⌊\frac{M}{2}⌋} \|\{z \in S \| 2 u = 1^{st} (z)\}\|$
327	102	adantr	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to S \in Fin$
328		ssfi	$⊢ (S \in Fin \land \{z \in S \| 2 u = 1^{st} (z)\} \subseteq S) \to \{z \in S \| 2 u = 1^{st} (z)\} \in Fin$
329	327 120 328	sylancl	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to \{z \in S \| 2 u = 1^{st} (z)\} \in Fin$
330		fveq2	$⊢ z = v \to 1^{st} (z) = 1^{st} (v)$
331	330	eqeq2d	$⊢ z = v \to (2 u = 1^{st} (z) \leftrightarrow 2 u = 1^{st} (v))$
332	331	elrab	$⊢ v \in \{z \in S \| 2 u = 1^{st} (z)\} \leftrightarrow (v \in S \land 2 u = 1^{st} (v))$
333	332	simprbi	$⊢ v \in \{z \in S \| 2 u = 1^{st} (z)\} \to 2 u = 1^{st} (v)$
334	333	ad2antll	$⊢ (φ \land (u \in (1 \dots ⌊\frac{M}{2}⌋) \land v \in \{z \in S \| 2 u = 1^{st} (z)\})) \to 2 u = 1^{st} (v)$
335	334	oveq1d	$⊢ (φ \land (u \in (1 \dots ⌊\frac{M}{2}⌋) \land v \in \{z \in S \| 2 u = 1^{st} (z)\})) \to \frac{2 u}{2} = \frac{1^{st} (v)}{2}$
336	145	nncnd	$⊢ (φ \land u \in (1 \dots ⌊\frac{M}{2}⌋)) \to u \in ℂ$
337	336	adantrr	$⊢ (φ \land (u \in (1 \dots ⌊\frac{M}{2}⌋) \land v \in \{z \in S \| 2 u = 1^{st} (z)\})) \to u \in ℂ$
338		2cnd	$⊢ (φ \land (u \in (1 \dots ⌊\frac{M}{2}⌋) \land v \in \{z \in S \| 2 u = 1^{st} (z)\})) \to 2 \in ℂ$
339	227	a1i	$⊢ (φ \land (u \in (1 \dots ⌊\frac{M}{2}⌋) \land v \in \{z \in S \| 2 u = 1^{st} (z)\})) \to 2 \neq 0$
340	337 338 339	divcan3d	$⊢ (φ \land (u \in (1 \dots ⌊\frac{M}{2}⌋) \land v \in \{z \in S \| 2 u = 1^{st} (z)\})) \to \frac{2 u}{2} = u$
341	335 340	eqtr3d	$⊢ (φ \land (u \in (1 \dots ⌊\frac{M}{2}⌋) \land v \in \{z \in S \| 2 u = 1^{st} (z)\})) \to \frac{1^{st} (v)}{2} = u$
342	341	ralrimivva	$⊢ φ \to \forall u \in (1 \dots ⌊\frac{M}{2}⌋) \forall v \in \{z \in S \| 2 u = 1^{st} (z)\} \frac{1^{st} (v)}{2} = u$
343		invdisj	$⊢ \forall u \in (1 \dots ⌊\frac{M}{2}⌋) \forall v \in \{z \in S \| 2 u = 1^{st} (z)\} \frac{1^{st} (v)}{2} = u \to {Disj}_{u = 1}^{⌊\frac{M}{2}⌋} \{z \in S \| 2 u = 1^{st} (z)\}$
344	342 343	syl	$⊢ φ \to {Disj}_{u = 1}^{⌊\frac{M}{2}⌋} \{z \in S \| 2 u = 1^{st} (z)\}$
345	89 329 344	hashiun	$⊢ φ \to \|⋃_{u = 1}^{⌊\frac{M}{2}⌋} \{z \in S \| 2 u = 1^{st} (z)\}\| = \sum_{u = 1}^{⌊\frac{M}{2}⌋} \|\{z \in S \| 2 u = 1^{st} (z)\}\|$
346		iunrab	$⊢ ⋃_{u = 1}^{⌊\frac{M}{2}⌋} \{z \in S \| 2 u = 1^{st} (z)\} = \{z \in S \| \exists u \in (1 \dots ⌊\frac{M}{2}⌋) 2 u = 1^{st} (z)\}$
347		2cn	$⊢ 2 \in ℂ$
348		zcn	$⊢ u \in ℤ \to u \in ℂ$
349	348	adantl	$⊢ ((φ \land z \in S) \land u \in ℤ) \to u \in ℂ$
350		mulcom	$⊢ (2 \in ℂ \land u \in ℂ) \to 2 u = u \cdot 2$
351	347 349 350	sylancr	$⊢ ((φ \land z \in S) \land u \in ℤ) \to 2 u = u \cdot 2$
352	351	eqeq1d	$⊢ ((φ \land z \in S) \land u \in ℤ) \to (2 u = 1^{st} (z) \leftrightarrow u \cdot 2 = 1^{st} (z))$
353	352	rexbidva	$⊢ (φ \land z \in S) \to (\exists u \in ℤ 2 u = 1^{st} (z) \leftrightarrow \exists u \in ℤ u \cdot 2 = 1^{st} (z))$
354	139	anim1i	$⊢ (u \in (1 \dots ⌊\frac{M}{2}⌋) \land 2 u = 1^{st} (z)) \to (u \in ℤ \land 2 u = 1^{st} (z))$
355	354	reximi2	$⊢ \exists u \in (1 \dots ⌊\frac{M}{2}⌋) 2 u = 1^{st} (z) \to \exists u \in ℤ 2 u = 1^{st} (z)$
356		simprr	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to 2 u = 1^{st} (z)$
357		simpr	$⊢ (φ \land z \in S) \to z \in S$
358	100 357	sselid	$⊢ (φ \land z \in S) \to z \in ((1 \dots M) \times (1 \dots N))$
359		xp1st	$⊢ z \in ((1 \dots M) \times (1 \dots N)) \to 1^{st} (z) \in (1 \dots M)$
360	358 359	syl	$⊢ (φ \land z \in S) \to 1^{st} (z) \in (1 \dots M)$
361	360	adantr	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to 1^{st} (z) \in (1 \dots M)$
362		elfzle2	$⊢ 1^{st} (z) \in (1 \dots M) \to 1^{st} (z) \leq M$
363	361 362	syl	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to 1^{st} (z) \leq M$
364	356 363	eqbrtrd	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to 2 u \leq M$
365		zre	$⊢ u \in ℤ \to u \in ℝ$
366	365	ad2antrl	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to u \in ℝ$
367	11	ad2antrr	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to M \in ℝ$
368	147	a1i	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to 2 \in ℝ$
369	149	a1i	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to 0 < 2$
370	366 367 368 369 151	syl112anc	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to (2 u \leq M \leftrightarrow u \leq \frac{M}{2})$
371	364 370	mpbid	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to u \leq \frac{M}{2}$
372	12	ad2antrr	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to \frac{M}{2} \in ℝ$
373		simprl	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to u \in ℤ$
374	372 373 141	syl2anc	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to (u \leq \frac{M}{2} \leftrightarrow u \leq ⌊\frac{M}{2}⌋)$
375	371 374	mpbid	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to u \leq ⌊\frac{M}{2}⌋$
376		2t0e0	$⊢ 2 \cdot 0 = 0$
377		elfznn	$⊢ 1^{st} (z) \in (1 \dots M) \to 1^{st} (z) \in ℕ$
378	361 377	syl	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to 1^{st} (z) \in ℕ$
379	356 378	eqeltrd	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to 2 u \in ℕ$
380	379	nngt0d	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to 0 < 2 u$
381	376 380	eqbrtrid	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to 2 \cdot 0 < 2 u$
382		0red	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to 0 \in ℝ$
383		ltmul2	$⊢ (0 \in ℝ \land u \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (0 < u \leftrightarrow 2 \cdot 0 < 2 u)$
384	382 366 368 369 383	syl112anc	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to (0 < u \leftrightarrow 2 \cdot 0 < 2 u)$
385	381 384	mpbird	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to 0 < u$
386		elnnz	$⊢ u \in ℕ \leftrightarrow (u \in ℤ \land 0 < u)$
387	373 385 386	sylanbrc	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to u \in ℕ$
388	387 279	eleqtrdi	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to u \in ℤ_{\geq 1}$
389	13	ad2antrr	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to ⌊\frac{M}{2}⌋ \in ℤ$
390		elfz5	$⊢ (u \in ℤ_{\geq 1} \land ⌊\frac{M}{2}⌋ \in ℤ) \to (u \in (1 \dots ⌊\frac{M}{2}⌋) \leftrightarrow u \leq ⌊\frac{M}{2}⌋)$
391	388 389 390	syl2anc	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to (u \in (1 \dots ⌊\frac{M}{2}⌋) \leftrightarrow u \leq ⌊\frac{M}{2}⌋)$
392	375 391	mpbird	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to u \in (1 \dots ⌊\frac{M}{2}⌋)$
393	392 356	jca	$⊢ ((φ \land z \in S) \land (u \in ℤ \land 2 u = 1^{st} (z))) \to (u \in (1 \dots ⌊\frac{M}{2}⌋) \land 2 u = 1^{st} (z))$
394	393	ex	$⊢ (φ \land z \in S) \to ((u \in ℤ \land 2 u = 1^{st} (z)) \to (u \in (1 \dots ⌊\frac{M}{2}⌋) \land 2 u = 1^{st} (z)))$
395	394	reximdv2	$⊢ (φ \land z \in S) \to (\exists u \in ℤ 2 u = 1^{st} (z) \to \exists u \in (1 \dots ⌊\frac{M}{2}⌋) 2 u = 1^{st} (z))$
396	355 395	impbid2	$⊢ (φ \land z \in S) \to (\exists u \in (1 \dots ⌊\frac{M}{2}⌋) 2 u = 1^{st} (z) \leftrightarrow \exists u \in ℤ 2 u = 1^{st} (z))$
397		2z	$⊢ 2 \in ℤ$
398	360	elfzelzd	$⊢ (φ \land z \in S) \to 1^{st} (z) \in ℤ$
399		divides	$⊢ (2 \in ℤ \land 1^{st} (z) \in ℤ) \to (2 ∥ 1^{st} (z) \leftrightarrow \exists u \in ℤ u \cdot 2 = 1^{st} (z))$
400	397 398 399	sylancr	$⊢ (φ \land z \in S) \to (2 ∥ 1^{st} (z) \leftrightarrow \exists u \in ℤ u \cdot 2 = 1^{st} (z))$
401	353 396 400	3bitr4d	$⊢ (φ \land z \in S) \to (\exists u \in (1 \dots ⌊\frac{M}{2}⌋) 2 u = 1^{st} (z) \leftrightarrow 2 ∥ 1^{st} (z))$
402	401	rabbidva	$⊢ φ \to \{z \in S \| \exists u \in (1 \dots ⌊\frac{M}{2}⌋) 2 u = 1^{st} (z)\} = \{z \in S \| 2 ∥ 1^{st} (z)\}$
403	346 402	eqtrid	$⊢ φ \to ⋃_{u = 1}^{⌊\frac{M}{2}⌋} \{z \in S \| 2 u = 1^{st} (z)\} = \{z \in S \| 2 ∥ 1^{st} (z)\}$
404	403	fveq2d	$⊢ φ \to \|⋃_{u = 1}^{⌊\frac{M}{2}⌋} \{z \in S \| 2 u = 1^{st} (z)\}\| = \|\{z \in S \| 2 ∥ 1^{st} (z)\}\|$
405	326 345 404	3eqtr2d	$⊢ φ \to \sum_{u = 1}^{⌊\frac{M}{2}⌋} ⌊(\frac{Q}{P}) 2 u⌋ = \|\{z \in S \| 2 ∥ 1^{st} (z)\}\|$
406	405	oveq2d	$⊢ φ \to {(- 1)}^{\sum_{u = 1}^{⌊\frac{M}{2}⌋} ⌊(\frac{Q}{P}) 2 u⌋} = {(- 1)}^{\|\{z \in S \| 2 ∥ 1^{st} (z)\}\|}$
407	1 2 3 4 5 6	lgsquadlem1	$⊢ φ \to {(- 1)}^{\sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋} = {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|}$
408	406 407	oveq12d	$⊢ φ \to {(- 1)}^{\sum_{u = 1}^{⌊\frac{M}{2}⌋} ⌊(\frac{Q}{P}) 2 u⌋} {(- 1)}^{\sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋} = {(- 1)}^{\|\{z \in S \| 2 ∥ 1^{st} (z)\}\|} {(- 1)}^{\|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|}$
409	113 408	eqtr4d	$⊢ φ \to {(- 1)}^{\|\{z \in S \| 2 ∥ 1^{st} (z)\}\| + \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} = {(- 1)}^{\sum_{u = 1}^{⌊\frac{M}{2}⌋} ⌊(\frac{Q}{P}) 2 u⌋} {(- 1)}^{\sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋}$
410		inrab	$⊢ \{z \in S \| 2 ∥ 1^{st} (z)\} \cap \{z \in S \| \neg 2 ∥ 1^{st} (z)\} = \{z \in S \| (2 ∥ 1^{st} (z) \land \neg 2 ∥ 1^{st} (z))\}$
411		pm3.24	$⊢ \neg (2 ∥ 1^{st} (z) \land \neg 2 ∥ 1^{st} (z))$
412	411	a1i	$⊢ φ \to \neg (2 ∥ 1^{st} (z) \land \neg 2 ∥ 1^{st} (z))$
413	412	ralrimivw	$⊢ φ \to \forall z \in S \neg (2 ∥ 1^{st} (z) \land \neg 2 ∥ 1^{st} (z))$
414		rabeq0	$⊢ \{z \in S \| (2 ∥ 1^{st} (z) \land \neg 2 ∥ 1^{st} (z))\} = \emptyset \leftrightarrow \forall z \in S \neg (2 ∥ 1^{st} (z) \land \neg 2 ∥ 1^{st} (z))$
415	413 414	sylibr	$⊢ φ \to \{z \in S \| (2 ∥ 1^{st} (z) \land \neg 2 ∥ 1^{st} (z))\} = \emptyset$
416	410 415	eqtrid	$⊢ φ \to \{z \in S \| 2 ∥ 1^{st} (z)\} \cap \{z \in S \| \neg 2 ∥ 1^{st} (z)\} = \emptyset$
417		hashun	$⊢ (\{z \in S \| 2 ∥ 1^{st} (z)\} \in Fin \land \{z \in S \| \neg 2 ∥ 1^{st} (z)\} \in Fin \land \{z \in S \| 2 ∥ 1^{st} (z)\} \cap \{z \in S \| \neg 2 ∥ 1^{st} (z)\} = \emptyset) \to \|\{z \in S \| 2 ∥ 1^{st} (z)\} \cup \{z \in S \| \neg 2 ∥ 1^{st} (z)\}\| = \|\{z \in S \| 2 ∥ 1^{st} (z)\}\| + \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|$
418	110 105 416 417	syl3anc	$⊢ φ \to \|\{z \in S \| 2 ∥ 1^{st} (z)\} \cup \{z \in S \| \neg 2 ∥ 1^{st} (z)\}\| = \|\{z \in S \| 2 ∥ 1^{st} (z)\}\| + \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|$
419		unrab	$⊢ \{z \in S \| 2 ∥ 1^{st} (z)\} \cup \{z \in S \| \neg 2 ∥ 1^{st} (z)\} = \{z \in S \| (2 ∥ 1^{st} (z) \lor \neg 2 ∥ 1^{st} (z))\}$
420		exmid	$⊢ (2 ∥ 1^{st} (z) \lor \neg 2 ∥ 1^{st} (z))$
421	420	rgenw	$⊢ \forall z \in S (2 ∥ 1^{st} (z) \lor \neg 2 ∥ 1^{st} (z))$
422		rabid2	$⊢ S = \{z \in S \| (2 ∥ 1^{st} (z) \lor \neg 2 ∥ 1^{st} (z))\} \leftrightarrow \forall z \in S (2 ∥ 1^{st} (z) \lor \neg 2 ∥ 1^{st} (z))$
423	421 422	mpbir	$⊢ S = \{z \in S \| (2 ∥ 1^{st} (z) \lor \neg 2 ∥ 1^{st} (z))\}$
424	419 423	eqtr4i	$⊢ \{z \in S \| 2 ∥ 1^{st} (z)\} \cup \{z \in S \| \neg 2 ∥ 1^{st} (z)\} = S$
425	424	fveq2i	$⊢ \|\{z \in S \| 2 ∥ 1^{st} (z)\} \cup \{z \in S \| \neg 2 ∥ 1^{st} (z)\}\| = \|S\|$
426	418 425	eqtr3di	$⊢ φ \to \|\{z \in S \| 2 ∥ 1^{st} (z)\}\| + \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\| = \|S\|$
427	426	oveq2d	$⊢ φ \to {(- 1)}^{\|\{z \in S \| 2 ∥ 1^{st} (z)\}\| + \|\{z \in S \| \neg 2 ∥ 1^{st} (z)\}\|} = {(- 1)}^{\|S\|}$
428	95 409 427	3eqtr2d	$⊢ φ \to {(- 1)}^{\sum_{u = 1}^{⌊\frac{M}{2}⌋} ⌊(\frac{Q}{P}) 2 u⌋ + \sum_{u = ⌊\frac{M}{2}⌋ + 1}^{M} ⌊(\frac{Q}{P}) 2 u⌋} = {(- 1)}^{\|S\|}$
429	7 80 428	3eqtrd	$⊢ φ \to Q /_{L} P = {(- 1)}^{\|S\|}$

Metamath Proof Explorer

Theorem lgsquadlem2

Proof