# Metamath Proof Explorer

Description: Lemma for lgsquad . (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 lgsquadlem3 ${⊢}{\phi }\to \left({P}{/}_{L}{Q}\right)\left({Q}{/}_{L}{P}\right)={\left(-1\right)}^{{M}\cdot {N}}$

### 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 3 necomd ${⊢}{\phi }\to {Q}\ne {P}$
8 eleq1w ${⊢}{x}={z}\to \left({x}\in \left(1\dots {M}\right)↔{z}\in \left(1\dots {M}\right)\right)$
9 eleq1w ${⊢}{y}={w}\to \left({y}\in \left(1\dots {N}\right)↔{w}\in \left(1\dots {N}\right)\right)$
10 8 9 bi2anan9 ${⊢}\left({x}={z}\wedge {y}={w}\right)\to \left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)↔\left({z}\in \left(1\dots {M}\right)\wedge {w}\in \left(1\dots {N}\right)\right)\right)$
11 10 biancomd ${⊢}\left({x}={z}\wedge {y}={w}\right)\to \left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)↔\left({w}\in \left(1\dots {N}\right)\wedge {z}\in \left(1\dots {M}\right)\right)\right)$
12 oveq1 ${⊢}{x}={z}\to {x}{Q}={z}{Q}$
13 oveq1 ${⊢}{y}={w}\to {y}{P}={w}{P}$
14 12 13 breqan12d ${⊢}\left({x}={z}\wedge {y}={w}\right)\to \left({x}{Q}<{y}{P}↔{z}{Q}<{w}{P}\right)$
15 11 14 anbi12d ${⊢}\left({x}={z}\wedge {y}={w}\right)\to \left(\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)↔\left(\left({w}\in \left(1\dots {N}\right)\wedge {z}\in \left(1\dots {M}\right)\right)\wedge {z}{Q}<{w}{P}\right)\right)$
16 15 ancoms ${⊢}\left({y}={w}\wedge {x}={z}\right)\to \left(\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)↔\left(\left({w}\in \left(1\dots {N}\right)\wedge {z}\in \left(1\dots {M}\right)\right)\wedge {z}{Q}<{w}{P}\right)\right)$
17 16 cbvopabv ${⊢}\left\{⟨{y},{x}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}=\left\{⟨{w},{z}⟩|\left(\left({w}\in \left(1\dots {N}\right)\wedge {z}\in \left(1\dots {M}\right)\right)\wedge {z}{Q}<{w}{P}\right)\right\}$
18 2 1 7 5 4 17 lgsquadlem2 ${⊢}{\phi }\to {P}{/}_{L}{Q}={\left(-1\right)}^{\left|\left\{⟨{y},{x}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\right|}$
19 relopab ${⊢}\mathrm{Rel}\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}$
20 fzfid ${⊢}{\phi }\to \left(1\dots {M}\right)\in \mathrm{Fin}$
21 fzfid ${⊢}{\phi }\to \left(1\dots {N}\right)\in \mathrm{Fin}$
22 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}$
23 20 21 22 syl2anc ${⊢}{\phi }\to \left(1\dots {M}\right)×\left(1\dots {N}\right)\in \mathrm{Fin}$
24 opabssxp ${⊢}\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\subseteq \left(1\dots {M}\right)×\left(1\dots {N}\right)$
25 ssfi ${⊢}\left(\left(1\dots {M}\right)×\left(1\dots {N}\right)\in \mathrm{Fin}\wedge \left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\subseteq \left(1\dots {M}\right)×\left(1\dots {N}\right)\right)\to \left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\in \mathrm{Fin}$
26 23 24 25 sylancl ${⊢}{\phi }\to \left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\in \mathrm{Fin}$
27 cnven ${⊢}\left(\mathrm{Rel}\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\wedge \left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\in \mathrm{Fin}\right)\to \left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\approx {\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}}^{-1}$
28 19 26 27 sylancr ${⊢}{\phi }\to \left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\approx {\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}}^{-1}$
29 cnvopab ${⊢}{\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}}^{-1}=\left\{⟨{y},{x}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}$
30 28 29 breqtrdi ${⊢}{\phi }\to \left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\approx \left\{⟨{y},{x}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}$
31 hasheni ${⊢}\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\approx \left\{⟨{y},{x}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\to \left|\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\right|=\left|\left\{⟨{y},{x}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\right|$
32 30 31 syl ${⊢}{\phi }\to \left|\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\right|=\left|\left\{⟨{y},{x}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\right|$
33 32 oveq2d ${⊢}{\phi }\to {\left(-1\right)}^{\left|\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\right|}={\left(-1\right)}^{\left|\left\{⟨{y},{x}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\right|}$
34 18 33 eqtr4d ${⊢}{\phi }\to {P}{/}_{L}{Q}={\left(-1\right)}^{\left|\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\right|}$
35 1 2 3 4 5 6 lgsquadlem2 ${⊢}{\phi }\to {Q}{/}_{L}{P}={\left(-1\right)}^{\left|{S}\right|}$
36 34 35 oveq12d ${⊢}{\phi }\to \left({P}{/}_{L}{Q}\right)\left({Q}{/}_{L}{P}\right)={\left(-1\right)}^{\left|\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\right|}{\left(-1\right)}^{\left|{S}\right|}$
37 neg1cn ${⊢}-1\in ℂ$
38 37 a1i ${⊢}{\phi }\to -1\in ℂ$
39 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)$
40 6 39 eqsstri ${⊢}{S}\subseteq \left(1\dots {M}\right)×\left(1\dots {N}\right)$
41 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}$
42 23 40 41 sylancl ${⊢}{\phi }\to {S}\in \mathrm{Fin}$
43 hashcl ${⊢}{S}\in \mathrm{Fin}\to \left|{S}\right|\in {ℕ}_{0}$
44 42 43 syl ${⊢}{\phi }\to \left|{S}\right|\in {ℕ}_{0}$
45 hashcl ${⊢}\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\in \mathrm{Fin}\to \left|\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\right|\in {ℕ}_{0}$
46 26 45 syl ${⊢}{\phi }\to \left|\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\right|\in {ℕ}_{0}$
47 38 44 46 expaddd ${⊢}{\phi }\to {\left(-1\right)}^{\left|\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\right|+\left|{S}\right|}={\left(-1\right)}^{\left|\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\right|}{\left(-1\right)}^{\left|{S}\right|}$
48 2 eldifad ${⊢}{\phi }\to {Q}\in ℙ$
49 48 adantr ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {Q}\in ℙ$
50 prmnn ${⊢}{Q}\in ℙ\to {Q}\in ℕ$
51 49 50 syl ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {Q}\in ℕ$
52 2 5 gausslemma2dlem0b ${⊢}{\phi }\to {N}\in ℕ$
53 52 adantr ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {N}\in ℕ$
54 53 nnzd ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {N}\in ℤ$
55 prmz ${⊢}{Q}\in ℙ\to {Q}\in ℤ$
56 49 55 syl ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {Q}\in ℤ$
57 peano2zm ${⊢}{Q}\in ℤ\to {Q}-1\in ℤ$
58 56 57 syl ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {Q}-1\in ℤ$
59 53 nnred ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {N}\in ℝ$
60 58 zred ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {Q}-1\in ℝ$
61 prmuz2 ${⊢}{Q}\in ℙ\to {Q}\in {ℤ}_{\ge 2}$
62 49 61 syl ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {Q}\in {ℤ}_{\ge 2}$
63 uz2m1nn ${⊢}{Q}\in {ℤ}_{\ge 2}\to {Q}-1\in ℕ$
64 62 63 syl ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {Q}-1\in ℕ$
65 64 nnrpd ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {Q}-1\in {ℝ}^{+}$
66 rphalflt ${⊢}{Q}-1\in {ℝ}^{+}\to \frac{{Q}-1}{2}<{Q}-1$
67 65 66 syl ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to \frac{{Q}-1}{2}<{Q}-1$
68 5 67 eqbrtrid ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {N}<{Q}-1$
69 59 60 68 ltled ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {N}\le {Q}-1$
70 eluz2 ${⊢}{Q}-1\in {ℤ}_{\ge {N}}↔\left({N}\in ℤ\wedge {Q}-1\in ℤ\wedge {N}\le {Q}-1\right)$
71 54 58 69 70 syl3anbrc ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {Q}-1\in {ℤ}_{\ge {N}}$
72 fzss2 ${⊢}{Q}-1\in {ℤ}_{\ge {N}}\to \left(1\dots {N}\right)\subseteq \left(1\dots {Q}-1\right)$
73 71 72 syl ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to \left(1\dots {N}\right)\subseteq \left(1\dots {Q}-1\right)$
74 simprr ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {y}\in \left(1\dots {N}\right)$
75 73 74 sseldd ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {y}\in \left(1\dots {Q}-1\right)$
76 fzm1ndvds ${⊢}\left({Q}\in ℕ\wedge {y}\in \left(1\dots {Q}-1\right)\right)\to ¬{Q}\parallel {y}$
77 51 75 76 syl2anc ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to ¬{Q}\parallel {y}$
78 7 adantr ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {Q}\ne {P}$
79 1 eldifad ${⊢}{\phi }\to {P}\in ℙ$
80 79 adantr ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {P}\in ℙ$
81 prmrp ${⊢}\left({Q}\in ℙ\wedge {P}\in ℙ\right)\to \left({Q}\mathrm{gcd}{P}=1↔{Q}\ne {P}\right)$
82 49 80 81 syl2anc ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to \left({Q}\mathrm{gcd}{P}=1↔{Q}\ne {P}\right)$
83 78 82 mpbird ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {Q}\mathrm{gcd}{P}=1$
84 prmz ${⊢}{P}\in ℙ\to {P}\in ℤ$
85 80 84 syl ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {P}\in ℤ$
86 elfzelz ${⊢}{y}\in \left(1\dots {N}\right)\to {y}\in ℤ$
87 86 ad2antll ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {y}\in ℤ$
88 coprmdvds ${⊢}\left({Q}\in ℤ\wedge {P}\in ℤ\wedge {y}\in ℤ\right)\to \left(\left({Q}\parallel {P}{y}\wedge {Q}\mathrm{gcd}{P}=1\right)\to {Q}\parallel {y}\right)$
89 56 85 87 88 syl3anc ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to \left(\left({Q}\parallel {P}{y}\wedge {Q}\mathrm{gcd}{P}=1\right)\to {Q}\parallel {y}\right)$
90 83 89 mpan2d ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to \left({Q}\parallel {P}{y}\to {Q}\parallel {y}\right)$
91 77 90 mtod ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to ¬{Q}\parallel {P}{y}$
92 prmnn ${⊢}{P}\in ℙ\to {P}\in ℕ$
93 80 92 syl ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {P}\in ℕ$
94 93 nncnd ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {P}\in ℂ$
95 elfznn ${⊢}{y}\in \left(1\dots {N}\right)\to {y}\in ℕ$
96 95 ad2antll ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {y}\in ℕ$
97 96 nncnd ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {y}\in ℂ$
98 94 97 mulcomd ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {P}{y}={y}{P}$
99 98 breq2d ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to \left({Q}\parallel {P}{y}↔{Q}\parallel {y}{P}\right)$
100 91 99 mtbid ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to ¬{Q}\parallel {y}{P}$
101 elfzelz ${⊢}{x}\in \left(1\dots {M}\right)\to {x}\in ℤ$
102 101 ad2antrl ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {x}\in ℤ$
103 dvdsmul2 ${⊢}\left({x}\in ℤ\wedge {Q}\in ℤ\right)\to {Q}\parallel {x}{Q}$
104 102 56 103 syl2anc ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {Q}\parallel {x}{Q}$
105 breq2 ${⊢}{x}{Q}={y}{P}\to \left({Q}\parallel {x}{Q}↔{Q}\parallel {y}{P}\right)$
106 104 105 syl5ibcom ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to \left({x}{Q}={y}{P}\to {Q}\parallel {y}{P}\right)$
107 106 necon3bd ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to \left(¬{Q}\parallel {y}{P}\to {x}{Q}\ne {y}{P}\right)$
108 100 107 mpd ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {x}{Q}\ne {y}{P}$
109 elfznn ${⊢}{x}\in \left(1\dots {M}\right)\to {x}\in ℕ$
110 109 ad2antrl ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {x}\in ℕ$
111 110 51 nnmulcld ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {x}{Q}\in ℕ$
112 111 nnred ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {x}{Q}\in ℝ$
113 96 93 nnmulcld ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {y}{P}\in ℕ$
114 113 nnred ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to {y}{P}\in ℝ$
115 112 114 lttri2d ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to \left({x}{Q}\ne {y}{P}↔\left({x}{Q}<{y}{P}\vee {y}{P}<{x}{Q}\right)\right)$
116 108 115 mpbid ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to \left({x}{Q}<{y}{P}\vee {y}{P}<{x}{Q}\right)$
117 116 ex ${⊢}{\phi }\to \left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\to \left({x}{Q}<{y}{P}\vee {y}{P}<{x}{Q}\right)\right)$
118 117 pm4.71rd ${⊢}{\phi }\to \left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)↔\left(\left({x}{Q}<{y}{P}\vee {y}{P}<{x}{Q}\right)\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\right)$
119 ancom ${⊢}\left(\left({x}{Q}<{y}{P}\vee {y}{P}<{x}{Q}\right)\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)↔\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge \left({x}{Q}<{y}{P}\vee {y}{P}<{x}{Q}\right)\right)$
120 118 119 syl6rbb ${⊢}{\phi }\to \left(\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge \left({x}{Q}<{y}{P}\vee {y}{P}<{x}{Q}\right)\right)↔\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)$
121 120 opabbidv ${⊢}{\phi }\to \left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge \left({x}{Q}<{y}{P}\vee {y}{P}<{x}{Q}\right)\right)\right\}=\left\{⟨{x},{y}⟩|\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right\}$
122 unopab ${⊢}\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\cup \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\{⟨{x},{y}⟩|\left(\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\vee \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)\right\}$
123 6 uneq2i ${⊢}\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\cup {S}=\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\cup \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\}$
124 andi ${⊢}\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge \left({x}{Q}<{y}{P}\vee {y}{P}<{x}{Q}\right)\right)↔\left(\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\vee \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)$
125 124 opabbii ${⊢}\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge \left({x}{Q}<{y}{P}\vee {y}{P}<{x}{Q}\right)\right)\right\}=\left\{⟨{x},{y}⟩|\left(\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\vee \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)\right\}$
126 122 123 125 3eqtr4i ${⊢}\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\cup {S}=\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge \left({x}{Q}<{y}{P}\vee {y}{P}<{x}{Q}\right)\right)\right\}$
127 df-xp ${⊢}\left(1\dots {M}\right)×\left(1\dots {N}\right)=\left\{⟨{x},{y}⟩|\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right\}$
128 121 126 127 3eqtr4g ${⊢}{\phi }\to \left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\cup {S}=\left(1\dots {M}\right)×\left(1\dots {N}\right)$
129 128 fveq2d ${⊢}{\phi }\to \left|\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\cup {S}\right|=\left|\left(1\dots {M}\right)×\left(1\dots {N}\right)\right|$
130 inopab ${⊢}\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\cap \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\{⟨{x},{y}⟩|\left(\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\wedge \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)\right\}$
131 6 ineq2i ${⊢}\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\cap {S}=\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\cap \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\}$
132 anandi ${⊢}\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge \left({x}{Q}<{y}{P}\wedge {y}{P}<{x}{Q}\right)\right)↔\left(\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\wedge \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)$
133 132 opabbii ${⊢}\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge \left({x}{Q}<{y}{P}\wedge {y}{P}<{x}{Q}\right)\right)\right\}=\left\{⟨{x},{y}⟩|\left(\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\wedge \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)\right\}$
134 130 131 133 3eqtr4i ${⊢}\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\cap {S}=\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge \left({x}{Q}<{y}{P}\wedge {y}{P}<{x}{Q}\right)\right)\right\}$
135 ltnsym2 ${⊢}\left({x}{Q}\in ℝ\wedge {y}{P}\in ℝ\right)\to ¬\left({x}{Q}<{y}{P}\wedge {y}{P}<{x}{Q}\right)$
136 112 114 135 syl2anc ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\right)\to ¬\left({x}{Q}<{y}{P}\wedge {y}{P}<{x}{Q}\right)$
137 136 ex ${⊢}{\phi }\to \left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\to ¬\left({x}{Q}<{y}{P}\wedge {y}{P}<{x}{Q}\right)\right)$
138 imnan ${⊢}\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\to ¬\left({x}{Q}<{y}{P}\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 \left({x}{Q}<{y}{P}\wedge {y}{P}<{x}{Q}\right)\right)$
139 137 138 sylib ${⊢}{\phi }\to ¬\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge \left({x}{Q}<{y}{P}\wedge {y}{P}<{x}{Q}\right)\right)$
140 139 nexdv ${⊢}{\phi }\to ¬\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge \left({x}{Q}<{y}{P}\wedge {y}{P}<{x}{Q}\right)\right)$
141 140 nexdv ${⊢}{\phi }\to ¬\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge \left({x}{Q}<{y}{P}\wedge {y}{P}<{x}{Q}\right)\right)$
142 opabn0 ${⊢}\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge \left({x}{Q}<{y}{P}\wedge {y}{P}<{x}{Q}\right)\right)\right\}\ne \varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge \left({x}{Q}<{y}{P}\wedge {y}{P}<{x}{Q}\right)\right)$
143 142 necon1bbii ${⊢}¬\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge \left({x}{Q}<{y}{P}\wedge {y}{P}<{x}{Q}\right)\right)↔\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge \left({x}{Q}<{y}{P}\wedge {y}{P}<{x}{Q}\right)\right)\right\}=\varnothing$
144 141 143 sylib ${⊢}{\phi }\to \left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge \left({x}{Q}<{y}{P}\wedge {y}{P}<{x}{Q}\right)\right)\right\}=\varnothing$
145 134 144 syl5eq ${⊢}{\phi }\to \left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\cap {S}=\varnothing$
146 hashun ${⊢}\left(\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\in \mathrm{Fin}\wedge {S}\in \mathrm{Fin}\wedge \left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\cap {S}=\varnothing \right)\to \left|\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\cup {S}\right|=\left|\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\right|+\left|{S}\right|$
147 26 42 145 146 syl3anc ${⊢}{\phi }\to \left|\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\cup {S}\right|=\left|\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\right|+\left|{S}\right|$
148 hashxp ${⊢}\left(\left(1\dots {M}\right)\in \mathrm{Fin}\wedge \left(1\dots {N}\right)\in \mathrm{Fin}\right)\to \left|\left(1\dots {M}\right)×\left(1\dots {N}\right)\right|=\left|\left(1\dots {M}\right)\right|\left|\left(1\dots {N}\right)\right|$
149 20 21 148 syl2anc ${⊢}{\phi }\to \left|\left(1\dots {M}\right)×\left(1\dots {N}\right)\right|=\left|\left(1\dots {M}\right)\right|\left|\left(1\dots {N}\right)\right|$
150 1 4 gausslemma2dlem0b ${⊢}{\phi }\to {M}\in ℕ$
151 150 nnnn0d ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
152 hashfz1 ${⊢}{M}\in {ℕ}_{0}\to \left|\left(1\dots {M}\right)\right|={M}$
153 151 152 syl ${⊢}{\phi }\to \left|\left(1\dots {M}\right)\right|={M}$
154 52 nnnn0d ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
155 hashfz1 ${⊢}{N}\in {ℕ}_{0}\to \left|\left(1\dots {N}\right)\right|={N}$
156 154 155 syl ${⊢}{\phi }\to \left|\left(1\dots {N}\right)\right|={N}$
157 153 156 oveq12d ${⊢}{\phi }\to \left|\left(1\dots {M}\right)\right|\left|\left(1\dots {N}\right)\right|={M}\cdot {N}$
158 149 157 eqtrd ${⊢}{\phi }\to \left|\left(1\dots {M}\right)×\left(1\dots {N}\right)\right|={M}\cdot {N}$
159 129 147 158 3eqtr3d ${⊢}{\phi }\to \left|\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\right|+\left|{S}\right|={M}\cdot {N}$
160 159 oveq2d ${⊢}{\phi }\to {\left(-1\right)}^{\left|\left\{⟨{x},{y}⟩|\left(\left({x}\in \left(1\dots {M}\right)\wedge {y}\in \left(1\dots {N}\right)\right)\wedge {x}{Q}<{y}{P}\right)\right\}\right|+\left|{S}\right|}={\left(-1\right)}^{{M}\cdot {N}}$
161 36 47 160 3eqtr2d ${⊢}{\phi }\to \left({P}{/}_{L}{Q}\right)\left({Q}{/}_{L}{P}\right)={\left(-1\right)}^{{M}\cdot {N}}$