lgsquadlem3

	Ref	Expression
Hypotheses	lgseisen.1	$⊢ φ \to P \in (ℙ ∖ \{2\})$
	lgseisen.2	$⊢ φ \to Q \in (ℙ ∖ \{2\})$
	lgseisen.3	$⊢ φ \to P \neq Q$
	lgsquad.4	$⊢ M = \frac{P - 1}{2}$
	lgsquad.5	$⊢ N = \frac{Q - 1}{2}$
	lgsquad.6	$⊢ S = \{⟨x, y⟩ \| ((x \in (1 \dots M) \land y \in (1 \dots N)) \land y P < x Q)\}$
Assertion	lgsquadlem3	$⊢ φ \to (P /_{L} Q) (Q /_{L} P) = {(- 1)}^{M \cdot N}$

Proof

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

Metamath Proof Explorer

Theorem lgsquadlem3

Proof