lgsquadlem3 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lgsquadlem3		Structured version Visualization version GIF version

Theorem lgsquadlem3 27362

Description: Lemma for lgsquad 27363. (Contributed by Mario Carneiro, 18-Jun-2015.)

**Hypotheses**
Ref	Expression
lgseisen.1	⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
lgseisen.2	⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))
lgseisen.3	⊢ (𝜑 → 𝑃 ≠ 𝑄)
lgsquad.4	⊢ 𝑀 = ((𝑃 − 1) / 2)
lgsquad.5	⊢ 𝑁 = ((𝑄 − 1) / 2)
lgsquad.6	⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}

**Assertion**
Ref	Expression
lgsquadlem3	⊢ (𝜑 → ((𝑃 /_L 𝑄) · (𝑄 /_L 𝑃)) = (-1↑(𝑀 · 𝑁)))

Distinct variable groups: 𝑥,𝑦,𝑃 𝜑,𝑥,𝑦 𝑦,𝑀 𝑥,𝑁,𝑦 𝑥,𝑄,𝑦 𝑥,𝑆 𝑥,𝑀 𝑦,𝑆

Proof of Theorem lgsquadlem3 Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lgseisen.2	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))
2		lgseisen.1	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
3		lgseisen.3	. . . . . 6 ⊢ (𝜑 → 𝑃 ≠ 𝑄)
4	3	necomd 2988	. . . . 5 ⊢ (𝜑 → 𝑄 ≠ 𝑃)
5		lgsquad.5	. . . . 5 ⊢ 𝑁 = ((𝑄 − 1) / 2)
6		lgsquad.4	. . . . 5 ⊢ 𝑀 = ((𝑃 − 1) / 2)
7		eleq1w 2820	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ (1...𝑀) ↔ 𝑧 ∈ (1...𝑀)))
8		eleq1w 2820	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ (1...𝑁) ↔ 𝑤 ∈ (1...𝑁)))
9	7, 8	bi2anan9 639	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑧 ∈ (1...𝑀) ∧ 𝑤 ∈ (1...𝑁))))
10	9	biancomd 463	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀))))
11		oveq1 7368	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑥 · 𝑄) = (𝑧 · 𝑄))
12		oveq1 7368	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (𝑦 · 𝑃) = (𝑤 · 𝑃))
13	11, 12	breqan12d 5102	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 · 𝑄) < (𝑦 · 𝑃) ↔ (𝑧 · 𝑄) < (𝑤 · 𝑃)))
14	10, 13	anbi12d 633	. . . . . . 7 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ↔ ((𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀)) ∧ (𝑧 · 𝑄) < (𝑤 · 𝑃))))
15	14	ancoms 458	. . . . . 6 ⊢ ((𝑦 = 𝑤 ∧ 𝑥 = 𝑧) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ↔ ((𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀)) ∧ (𝑧 · 𝑄) < (𝑤 · 𝑃))))
16	15	cbvopabv 5159	. . . . 5 ⊢ {⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} = {⟨𝑤, 𝑧⟩ ∣ ((𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀)) ∧ (𝑧 · 𝑄) < (𝑤 · 𝑃))}
17	1, 2, 4, 5, 6, 16	lgsquadlem2 27361	. . . 4 ⊢ (𝜑 → (𝑃 /_L 𝑄) = (-1↑(♯‘{⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})))
18		relopabv 5771	. . . . . . . 8 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}
19		fzfid 13929	. . . . . . . . . 10 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
20		fzfid 13929	. . . . . . . . . 10 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
21		xpfi 9224	. . . . . . . . . 10 ⊢ (((1...𝑀) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((1...𝑀) × (1...𝑁)) ∈ Fin)
22	19, 20, 21	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin)
23		opabssxp 5717	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ⊆ ((1...𝑀) × (1...𝑁))
24		ssfi 9101	. . . . . . . . 9 ⊢ ((((1...𝑀) × (1...𝑁)) ∈ Fin ∧ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ⊆ ((1...𝑀) × (1...𝑁))) → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin)
25	22, 23, 24	sylancl 587	. . . . . . . 8 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin)
26		cnven 8974	. . . . . . . 8 ⊢ ((Rel {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∧ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin) → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ ^◡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})
27	18, 25, 26	sylancr 588	. . . . . . 7 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ ^◡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})
28		cnvopab 6095	. . . . . . 7 ⊢ ^◡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} = {⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}
29	27, 28	breqtrdi 5127	. . . . . 6 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ {⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})
30		hasheni 14304	. . . . . 6 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ {⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} → (♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) = (♯‘{⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}))
31	29, 30	syl 17	. . . . 5 ⊢ (𝜑 → (♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) = (♯‘{⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}))
32	31	oveq2d 7377	. . . 4 ⊢ (𝜑 → (-1↑(♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})) = (-1↑(♯‘{⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})))
33	17, 32	eqtr4d 2775	. . 3 ⊢ (𝜑 → (𝑃 /_L 𝑄) = (-1↑(♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})))
34		lgsquad.6	. . . 4 ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}
35	2, 1, 3, 6, 5, 34	lgsquadlem2 27361	. . 3 ⊢ (𝜑 → (𝑄 /_L 𝑃) = (-1↑(♯‘𝑆)))
36	33, 35	oveq12d 7379	. 2 ⊢ (𝜑 → ((𝑃 /_L 𝑄) · (𝑄 /_L 𝑃)) = ((-1↑(♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})) · (-1↑(♯‘𝑆))))
37		neg1cn 12138	. . . 4 ⊢ -1 ∈ ℂ
38	37	a1i 11	. . 3 ⊢ (𝜑 → -1 ∈ ℂ)
39		opabssxp 5717	. . . . . 6 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁))
40	34, 39	eqsstri 3969	. . . . 5 ⊢ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))
41		ssfi 9101	. . . . 5 ⊢ ((((1...𝑀) × (1...𝑁)) ∈ Fin ∧ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin)
42	22, 40, 41	sylancl 587	. . . 4 ⊢ (𝜑 → 𝑆 ∈ Fin)
43		hashcl 14312	. . . 4 ⊢ (𝑆 ∈ Fin → (♯‘𝑆) ∈ ℕ₀)
44	42, 43	syl 17	. . 3 ⊢ (𝜑 → (♯‘𝑆) ∈ ℕ₀)
45		hashcl 14312	. . . 4 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin → (♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) ∈ ℕ₀)
46	25, 45	syl 17	. . 3 ⊢ (𝜑 → (♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) ∈ ℕ₀)
47	38, 44, 46	expaddd 14104	. 2 ⊢ (𝜑 → (-1↑((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆))) = ((-1↑(♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})) · (-1↑(♯‘𝑆))))
48	1	eldifad 3902	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄 ∈ ℙ)
49	48	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈ ℙ)
50		prmnn 16637	. . . . . . . . . . . . . . . 16 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℕ)
51	49, 50	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈ ℕ)
52	1, 5	gausslemma2dlem0b 27337	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℕ)
53	52	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ∈ ℕ)
54	53	nnzd 12544	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ∈ ℤ)
55		prmz 16638	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
56	49, 55	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈ ℤ)
57		peano2zm 12564	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑄 ∈ ℤ → (𝑄 − 1) ∈ ℤ)
58	56, 57	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ ℤ)
59	53	nnred 12183	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ∈ ℝ)
60	58	zred 12627	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ ℝ)
61		prmuz2 16659	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ (ℤ_≥‘2))
62	49, 61	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈ (ℤ_≥‘2))
63		uz2m1nn 12867	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑄 ∈ (ℤ_≥‘2) → (𝑄 − 1) ∈ ℕ)
64	62, 63	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ ℕ)
65	64	nnrpd 12978	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ ℝ⁺)
66		rphalflt 12967	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 − 1) ∈ ℝ⁺ → ((𝑄 − 1) / 2) < (𝑄 − 1))
67	65, 66	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑄 − 1) / 2) < (𝑄 − 1))
68	5, 67	eqbrtrid 5121	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 < (𝑄 − 1))
69	59, 60, 68	ltled 11288	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ≤ (𝑄 − 1))
70		eluz2 12788	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑄 − 1) ∈ (ℤ_≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ (𝑄 − 1) ∈ ℤ ∧ 𝑁 ≤ (𝑄 − 1)))
71	54, 58, 69, 70	syl3anbrc 1345	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ (ℤ_≥‘𝑁))
72		fzss2 13512	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄 − 1) ∈ (ℤ_≥‘𝑁) → (1...𝑁) ⊆ (1...(𝑄 − 1)))
73	71, 72	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (1...𝑁) ⊆ (1...(𝑄 − 1)))
74		simprr 773	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ (1...𝑁))
75	73, 74	sseldd 3923	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ (1...(𝑄 − 1)))
76		fzm1ndvds 16285	. . . . . . . . . . . . . . 15 ⊢ ((𝑄 ∈ ℕ ∧ 𝑦 ∈ (1...(𝑄 − 1))) → ¬ 𝑄 ∥ 𝑦)
77	51, 75, 76	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ 𝑄 ∥ 𝑦)
78	4	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ≠ 𝑃)
79	2	eldifad 3902	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑃 ∈ ℙ)
80	79	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℙ)
81		prmrp 16676	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄 ∈ ℙ ∧ 𝑃 ∈ ℙ) → ((𝑄 gcd 𝑃) = 1 ↔ 𝑄 ≠ 𝑃))
82	49, 80, 81	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑄 gcd 𝑃) = 1 ↔ 𝑄 ≠ 𝑃))
83	78, 82	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 gcd 𝑃) = 1)
84		prmz 16638	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
85	80, 84	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℤ)
86		elfzelz 13472	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℤ)
87	86	ad2antll 730	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ ℤ)
88		coprmdvds 16616	. . . . . . . . . . . . . . . 16 ⊢ ((𝑄 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑄 ∥ (𝑃 · 𝑦) ∧ (𝑄 gcd 𝑃) = 1) → 𝑄 ∥ 𝑦))
89	56, 85, 87, 88	syl3anc 1374	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑄 ∥ (𝑃 · 𝑦) ∧ (𝑄 gcd 𝑃) = 1) → 𝑄 ∥ 𝑦))
90	83, 89	mpan2d 695	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 ∥ (𝑃 · 𝑦) → 𝑄 ∥ 𝑦))
91	77, 90	mtod 198	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ 𝑄 ∥ (𝑃 · 𝑦))
92		prmnn 16637	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
93	80, 92	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℕ)
94	93	nncnd 12184	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℂ)
95		elfznn 13501	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
96	95	ad2antll 730	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ ℕ)
97	96	nncnd 12184	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ ℂ)
98	94, 97	mulcomd 11160	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑃 · 𝑦) = (𝑦 · 𝑃))
99	98	breq2d 5098	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 ∥ (𝑃 · 𝑦) ↔ 𝑄 ∥ (𝑦 · 𝑃)))
100	91, 99	mtbid 324	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ 𝑄 ∥ (𝑦 · 𝑃))
101		elfzelz 13472	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...𝑀) → 𝑥 ∈ ℤ)
102	101	ad2antrl 729	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑥 ∈ ℤ)
103		dvdsmul2 16241	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℤ ∧ 𝑄 ∈ ℤ) → 𝑄 ∥ (𝑥 · 𝑄))
104	102, 56, 103	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∥ (𝑥 · 𝑄))
105		breq2 5090	. . . . . . . . . . . . . 14 ⊢ ((𝑥 · 𝑄) = (𝑦 · 𝑃) → (𝑄 ∥ (𝑥 · 𝑄) ↔ 𝑄 ∥ (𝑦 · 𝑃)))
106	104, 105	syl5ibcom 245	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑥 · 𝑄) = (𝑦 · 𝑃) → 𝑄 ∥ (𝑦 · 𝑃)))
107	106	necon3bd 2947	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (¬ 𝑄 ∥ (𝑦 · 𝑃) → (𝑥 · 𝑄) ≠ (𝑦 · 𝑃)))
108	100, 107	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑥 · 𝑄) ≠ (𝑦 · 𝑃))
109		elfznn 13501	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (1...𝑀) → 𝑥 ∈ ℕ)
110	109	ad2antrl 729	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑥 ∈ ℕ)
111	110, 51	nnmulcld 12224	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑥 · 𝑄) ∈ ℕ)
112	111	nnred 12183	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑥 · 𝑄) ∈ ℝ)
113	96, 93	nnmulcld 12224	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑦 · 𝑃) ∈ ℕ)
114	113	nnred 12183	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑦 · 𝑃) ∈ ℝ)
115	112, 114	lttri2d 11279	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑥 · 𝑄) ≠ (𝑦 · 𝑃) ↔ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
116	108, 115	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
117	116	ex 412	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) → ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
118	117	pm4.71rd 562	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)))))
119		ancom 460	. . . . . . . 8 ⊢ ((((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
120	118, 119	bitr2di 288	. . . . . . 7 ⊢ (𝜑 → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))))
121	120	opabbidv 5152	. . . . . 6 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))})
122		unopab 5166	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}) = {⟨𝑥, 𝑦⟩ ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∨ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
123	34	uneq2i 4106	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
124		andi 1010	. . . . . . . 8 ⊢ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∨ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
125	124	opabbii 5153	. . . . . . 7 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = {⟨𝑥, 𝑦⟩ ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∨ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
126	122, 123, 125	3eqtr4i 2770	. . . . . 6 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
127		df-xp 5631	. . . . . 6 ⊢ ((1...𝑀) × (1...𝑁)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))}
128	121, 126, 127	3eqtr4g 2797	. . . . 5 ⊢ (𝜑 → ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆) = ((1...𝑀) × (1...𝑁)))
129	128	fveq2d 6839	. . . 4 ⊢ (𝜑 → (♯‘({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆)) = (♯‘((1...𝑀) × (1...𝑁))))
130		inopab 5779	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}) = {⟨𝑥, 𝑦⟩ ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∧ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
131	34	ineq2i 4158	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
132		anandi 677	. . . . . . . 8 ⊢ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∧ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
133	132	opabbii 5153	. . . . . . 7 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = {⟨𝑥, 𝑦⟩ ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∧ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
134	130, 131, 133	3eqtr4i 2770	. . . . . 6 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
135		ltnsym2 11239	. . . . . . . . . . . 12 ⊢ (((𝑥 · 𝑄) ∈ ℝ ∧ (𝑦 · 𝑃) ∈ ℝ) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
136	112, 114, 135	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
137	136	ex 412	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
138		imnan 399	. . . . . . . . . 10 ⊢ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ ¬ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
139	137, 138	sylib 218	. . . . . . . . 9 ⊢ (𝜑 → ¬ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
140	139	nexdv 1938	. . . . . . . 8 ⊢ (𝜑 → ¬ ∃𝑦((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
141	140	nexdv 1938	. . . . . . 7 ⊢ (𝜑 → ¬ ∃𝑥∃𝑦((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
142		opabn0 5502	. . . . . . . 8 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} ≠ ∅ ↔ ∃𝑥∃𝑦((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
143	142	necon1bbii 2982	. . . . . . 7 ⊢ (¬ ∃𝑥∃𝑦((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = ∅)
144	141, 143	sylib 218	. . . . . 6 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = ∅)
145	134, 144	eqtrid 2784	. . . . 5 ⊢ (𝜑 → ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = ∅)
146		hashun 14338	. . . . 5 ⊢ (({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin ∧ 𝑆 ∈ Fin ∧ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = ∅) → (♯‘({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆)) = ((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆)))
147	25, 42, 145, 146	syl3anc 1374	. . . 4 ⊢ (𝜑 → (♯‘({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆)) = ((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆)))
148		hashxp 14390	. . . . . 6 ⊢ (((1...𝑀) ∈ Fin ∧ (1...𝑁) ∈ Fin) → (♯‘((1...𝑀) × (1...𝑁))) = ((♯‘(1...𝑀)) · (♯‘(1...𝑁))))
149	19, 20, 148	syl2anc 585	. . . . 5 ⊢ (𝜑 → (♯‘((1...𝑀) × (1...𝑁))) = ((♯‘(1...𝑀)) · (♯‘(1...𝑁))))
150	2, 6	gausslemma2dlem0b 27337	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ)
151	150	nnnn0d 12492	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
152		hashfz1 14302	. . . . . . 7 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(1...𝑀)) = 𝑀)
153	151, 152	syl 17	. . . . . 6 ⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀)
154	52	nnnn0d 12492	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
155		hashfz1 14302	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(1...𝑁)) = 𝑁)
156	154, 155	syl 17	. . . . . 6 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
157	153, 156	oveq12d 7379	. . . . 5 ⊢ (𝜑 → ((♯‘(1...𝑀)) · (♯‘(1...𝑁))) = (𝑀 · 𝑁))
158	149, 157	eqtrd 2772	. . . 4 ⊢ (𝜑 → (♯‘((1...𝑀) × (1...𝑁))) = (𝑀 · 𝑁))
159	129, 147, 158	3eqtr3d 2780	. . 3 ⊢ (𝜑 → ((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆)) = (𝑀 · 𝑁))
160	159	oveq2d 7377	. 2 ⊢ (𝜑 → (-1↑((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆))) = (-1↑(𝑀 · 𝑁)))
161	36, 47, 160	3eqtr2d 2778	1 ⊢ (𝜑 → ((𝑃 /_L 𝑄) · (𝑄 /_L 𝑃)) = (-1↑(𝑀 · 𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ≠ wne 2933 ∖ cdif 3887 ∪ cun 3888 ∩ cin 3889 ⊆ wss 3890 ∅c0 4274 {csn 4568 class class class wbr 5086 {copab 5148 × cxp 5623 ^◡ccnv 5624 Rel wrel 5630 ‘cfv 6493 (class class class)co 7361 ≈ cen 8884 Fincfn 8887 ℂcc 11030 ℝcr 11031 1c1 11033 + caddc 11035 · cmul 11037 < clt 11173 ≤ cle 11174 − cmin 11371 -cneg 11372 / cdiv 11801 ℕcn 12168 2c2 12230 ℕ₀cn0 12431 ℤcz 12518 ℤ_≥cuz 12782 ℝ⁺crp 12936 ...cfz 13455 ↑cexp 14017 ♯chash 14286 ∥ cdvds 16215 gcd cgcd 16457 ℙcprime 16634 /_L clgs 27274

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683 ax-inf2 9556 ax-cnex 11088 ax-resscn 11089 ax-1cn 11090 ax-icn 11091 ax-addcl 11092 ax-addrcl 11093 ax-mulcl 11094 ax-mulrcl 11095 ax-mulcom 11096 ax-addass 11097 ax-mulass 11098 ax-distr 11099 ax-i2m1 11100 ax-1ne0 11101 ax-1rid 11102 ax-rnegex 11103 ax-rrecex 11104 ax-cnre 11105 ax-pre-lttri 11106 ax-pre-lttrn 11107 ax-pre-ltadd 11108 ax-pre-mulgt0 11109 ax-pre-sup 11110 ax-addf 11111 ax-mulf 11112

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-disj 5054 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-se 5579 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-isom 6502 df-riota 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-of 7625 df-om 7812 df-1st 7936 df-2nd 7937 df-supp 8105 df-tpos 8170 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-2o 8400 df-oadd 8403 df-er 8637 df-ec 8639 df-qs 8643 df-map 8769 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-fsupp 9269 df-sup 9349 df-inf 9350 df-oi 9419 df-dju 9819 df-card 9857 df-pnf 11175 df-mnf 11176 df-xr 11177 df-ltxr 11178 df-le 11179 df-sub 11373 df-neg 11374 df-div 11802 df-nn 12169 df-2 12238 df-3 12239 df-4 12240 df-5 12241 df-6 12242 df-7 12243 df-8 12244 df-9 12245 df-n0 12432 df-xnn0 12505 df-z 12519 df-dec 12639 df-uz 12783 df-q 12893 df-rp 12937 df-fz 13456 df-fzo 13603 df-fl 13745 df-mod 13823 df-seq 13958 df-exp 14018 df-hash 14287 df-cj 15055 df-re 15056 df-im 15057 df-sqrt 15191 df-abs 15192 df-clim 15444 df-sum 15643 df-dvds 16216 df-gcd 16458 df-prm 16635 df-phi 16730 df-pc 16802 df-struct 17111 df-sets 17128 df-slot 17146 df-ndx 17158 df-base 17174 df-ress 17195 df-plusg 17227 df-mulr 17228 df-starv 17229 df-sca 17230 df-vsca 17231 df-ip 17232 df-tset 17233 df-ple 17234 df-ds 17236 df-unif 17237 df-0g 17398 df-gsum 17399 df-imas 17466 df-qus 17467 df-mgm 18602 df-sgrp 18681 df-mnd 18697 df-mhm 18745 df-submnd 18746 df-grp 18906 df-minusg 18907 df-sbg 18908 df-mulg 19038 df-subg 19093 df-nsg 19094 df-eqg 19095 df-ghm 19182 df-cntz 19286 df-cmn 19751 df-abl 19752 df-mgp 20116 df-rng 20128 df-ur 20157 df-ring 20210 df-cring 20211 df-oppr 20311 df-dvdsr 20331 df-unit 20332 df-invr 20362 df-dvr 20375 df-rhm 20446 df-nzr 20484 df-subrng 20517 df-subrg 20541 df-rlreg 20665 df-domn 20666 df-idom 20667 df-drng 20702 df-field 20703 df-lmod 20851 df-lss 20921 df-lsp 20961 df-sra 21163 df-rgmod 21164 df-lidl 21201 df-rsp 21202 df-2idl 21243 df-cnfld 21348 df-zring 21440 df-zrh 21496 df-zn 21499 df-lgs 27275

This theorem is referenced by: lgsquad 27363

W3C validator