# Metamath Proof Explorer

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 ${⊢}{\phi }\to {P}\in \left(ℙ\setminus \left\{2\right\}\right)$
lgseisen.2 ${⊢}{\phi }\to {Q}\in \left(ℙ\setminus \left\{2\right\}\right)$
lgseisen.3 ${⊢}{\phi }\to {P}\ne {Q}$
lgsquad.4 ${⊢}{M}=\frac{{P}-1}{2}$
lgsquad.5 ${⊢}{N}=\frac{{Q}-1}{2}$
lgsquad.6 ${⊢}{S}=\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {y}{P}<{x}{Q}\right)\right\}$
Assertion lgsquadlem2 ${⊢}{\phi }\to {Q}{/}_{L}{P}={\left(-1\right)}^{\left|{S}\right|}$

### Proof

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