# Metamath Proof Explorer

Description: Lemma for lgsquad . Count the members of S with odd coordinates. (Contributed by Mario Carneiro, 19-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 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|}$

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