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 27504

Description: Lemma for lgsquad 27505. (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 3015	. . . . 5 ⊢ (𝜑 → 𝑄 ≠ 𝑃)
5		lgsquad.5	. . . . 5 ⊢ 𝑁 = ((𝑄 − 1) / 2)
6		lgsquad.4	. . . . 5 ⊢ 𝑀 = ((𝑃 − 1) / 2)
7		eleq1w 2848	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ (1...𝑀) ↔ 𝑧 ∈ (1...𝑀)))
8		eleq1w 2848	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ (1...𝑁) ↔ 𝑤 ∈ (1...𝑁)))
9	7, 8	bi2anan9 649	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑧 ∈ (1...𝑀) ∧ 𝑤 ∈ (1...𝑁))))
10	9	biancomd 468	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀))))
11		oveq1 7407	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑥 · 𝑄) = (𝑧 · 𝑄))
12		oveq1 7407	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (𝑦 · 𝑃) = (𝑤 · 𝑃))
13	11, 12	breqan12d 5121	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 · 𝑄) < (𝑦 · 𝑃) ↔ (𝑧 · 𝑄) < (𝑤 · 𝑃)))
14	10, 13	anbi12d 643	. . . . . . 7 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ↔ ((𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀)) ∧ (𝑧 · 𝑄) < (𝑤 · 𝑃))))
15	14	ancoms 463	. . . . . 6 ⊢ ((𝑦 = 𝑤 ∧ 𝑥 = 𝑧) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ↔ ((𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀)) ∧ (𝑧 · 𝑄) < (𝑤 · 𝑃))))
16	15	cbvopabv 5178	. . . . 5 ⊢ {⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} = {⟨𝑤, 𝑧⟩ ∣ ((𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀)) ∧ (𝑧 · 𝑄) < (𝑤 · 𝑃))}
17	1, 2, 4, 5, 6, 16	lgsquadlem2 27503	. . . 4 ⊢ (𝜑 → (𝑃 /_L 𝑄) = (-1↑(♯‘{⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})))
18		relopabv 5799	. . . . . . . 8 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}
19		fzfid 14000	. . . . . . . . . 10 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
20		fzfid 14000	. . . . . . . . . 10 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
21		xpfi 9267	. . . . . . . . . 10 ⊢ (((1...𝑀) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((1...𝑀) × (1...𝑁)) ∈ Fin)
22	19, 20, 21	syl2anc 595	. . . . . . . . 9 ⊢ (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin)
23		opabssxp 5744	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ⊆ ((1...𝑀) × (1...𝑁))
24		ssfi 9145	. . . . . . . . 9 ⊢ ((((1...𝑀) × (1...𝑁)) ∈ Fin ∧ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ⊆ ((1...𝑀) × (1...𝑁))) → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin)
25	22, 23, 24	sylancl 597	. . . . . . . 8 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin)
26		cnven 9018	. . . . . . . 8 ⊢ ((Rel {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∧ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin) → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ ^◡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})
27	18, 25, 26	sylancr 598	. . . . . . 7 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ ^◡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})
28		cnvopab 6128	. . . . . . 7 ⊢ ^◡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} = {⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}
29	27, 28	breqtrdi 5146	. . . . . 6 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ {⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})
30		hasheni 14375	. . . . . 6 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ {⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} → (♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) = (♯‘{⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}))
31	29, 30	syl 18	. . . . 5 ⊢ (𝜑 → (♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) = (♯‘{⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}))
32	31	oveq2d 7416	. . . 4 ⊢ (𝜑 → (-1↑(♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})) = (-1↑(♯‘{⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})))
33	17, 32	eqtr4d 2803	. . 3 ⊢ (𝜑 → (𝑃 /_L 𝑄) = (-1↑(♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})))
34		lgsquad.6	. . . 4 ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}
35	2, 1, 3, 6, 5, 34	lgsquadlem2 27503	. . 3 ⊢ (𝜑 → (𝑄 /_L 𝑃) = (-1↑(♯‘𝑆)))
36	33, 35	oveq12d 7418	. 2 ⊢ (𝜑 → ((𝑃 /_L 𝑄) · (𝑄 /_L 𝑃)) = ((-1↑(♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})) · (-1↑(♯‘𝑆))))
37		neg1cn 12194	. . . 4 ⊢ -1 ∈ ℂ
38	37	a1i 11	. . 3 ⊢ (𝜑 → -1 ∈ ℂ)
39		opabssxp 5744	. . . . . 6 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁))
40	34, 39	eqsstri 3985	. . . . 5 ⊢ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))
41		ssfi 9145	. . . . 5 ⊢ ((((1...𝑀) × (1...𝑁)) ∈ Fin ∧ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin)
42	22, 40, 41	sylancl 597	. . . 4 ⊢ (𝜑 → 𝑆 ∈ Fin)
43		hashcl 14383	. . . 4 ⊢ (𝑆 ∈ Fin → (♯‘𝑆) ∈ ℕ₀)
44	42, 43	syl 18	. . 3 ⊢ (𝜑 → (♯‘𝑆) ∈ ℕ₀)
45		hashcl 14383	. . . 4 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin → (♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) ∈ ℕ₀)
46	25, 45	syl 18	. . 3 ⊢ (𝜑 → (♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) ∈ ℕ₀)
47	38, 44, 46	expaddd 14175	. 2 ⊢ (𝜑 → (-1↑((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆))) = ((-1↑(♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})) · (-1↑(♯‘𝑆))))
48	1	eldifad 3919	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄 ∈ ℙ)
49	48	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈ ℙ)
50		prmnn 16722	. . . . . . . . . . . . . . . 16 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℕ)
51	49, 50	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈ ℕ)
52	1, 5	gausslemma2dlem0b 27479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℕ)
53	52	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ∈ ℕ)
54	53	nnzd 12608	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ∈ ℤ)
55		prmz 16723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
56	49, 55	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈ ℤ)
57		peano2zm 12628	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑄 ∈ ℤ → (𝑄 − 1) ∈ ℤ)
58	56, 57	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ ℤ)
59	53	nnred 12239	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ∈ ℝ)
60	58	zred 12691	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ ℝ)
61		prmuz2 16744	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ (ℤ_≥‘2))
62	49, 61	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈ (ℤ_≥‘2))
63		uz2m1nn 12938	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑄 ∈ (ℤ_≥‘2) → (𝑄 − 1) ∈ ℕ)
64	62, 63	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ ℕ)
65	64	nnrpd 13049	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ ℝ⁺)
66		rphalflt 13038	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 − 1) ∈ ℝ⁺ → ((𝑄 − 1) / 2) < (𝑄 − 1))
67	65, 66	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑄 − 1) / 2) < (𝑄 − 1))
68	5, 67	eqbrtrid 5140	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 < (𝑄 − 1))
69	59, 60, 68	ltled 11346	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ≤ (𝑄 − 1))
70		eluz2 12859	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑄 − 1) ∈ (ℤ_≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ (𝑄 − 1) ∈ ℤ ∧ 𝑁 ≤ (𝑄 − 1)))
71	54, 58, 69, 70	syl3anbrc 1360	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ (ℤ_≥‘𝑁))
72		fzss2 13583	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄 − 1) ∈ (ℤ_≥‘𝑁) → (1...𝑁) ⊆ (1...(𝑄 − 1)))
73	71, 72	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (1...𝑁) ⊆ (1...(𝑄 − 1)))
74		simprr 784	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ (1...𝑁))
75	73, 74	sseldd 3940	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ (1...(𝑄 − 1)))
76		fzm1ndvds 16370	. . . . . . . . . . . . . . 15 ⊢ ((𝑄 ∈ ℕ ∧ 𝑦 ∈ (1...(𝑄 − 1))) → ¬ 𝑄 ∥ 𝑦)
77	51, 75, 76	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ 𝑄 ∥ 𝑦)
78	4	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ≠ 𝑃)
79	2	eldifad 3919	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑃 ∈ ℙ)
80	79	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℙ)
81		prmrp 16761	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄 ∈ ℙ ∧ 𝑃 ∈ ℙ) → ((𝑄 gcd 𝑃) = 1 ↔ 𝑄 ≠ 𝑃))
82	49, 80, 81	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑄 gcd 𝑃) = 1 ↔ 𝑄 ≠ 𝑃))
83	78, 82	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 gcd 𝑃) = 1)
84		prmz 16723	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
85	80, 84	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℤ)
86		elfzelz 13543	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℤ)
87	86	ad2antll 741	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ ℤ)
88		coprmdvds 16701	. . . . . . . . . . . . . . . 16 ⊢ ((𝑄 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑄 ∥ (𝑃 · 𝑦) ∧ (𝑄 gcd 𝑃) = 1) → 𝑄 ∥ 𝑦))
89	56, 85, 87, 88	syl3anc 1394	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑄 ∥ (𝑃 · 𝑦) ∧ (𝑄 gcd 𝑃) = 1) → 𝑄 ∥ 𝑦))
90	83, 89	mpan2d 706	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 ∥ (𝑃 · 𝑦) → 𝑄 ∥ 𝑦))
91	77, 90	mtod 201	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ 𝑄 ∥ (𝑃 · 𝑦))
92		prmnn 16722	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
93	80, 92	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℕ)
94	93	nncnd 12240	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℂ)
95		elfznn 13572	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
96	95	ad2antll 741	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ ℕ)
97	96	nncnd 12240	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ ℂ)
98	94, 97	mulcomd 11218	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑃 · 𝑦) = (𝑦 · 𝑃))
99	98	breq2d 5117	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 ∥ (𝑃 · 𝑦) ↔ 𝑄 ∥ (𝑦 · 𝑃)))
100	91, 99	mtbid 327	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ 𝑄 ∥ (𝑦 · 𝑃))
101		elfzelz 13543	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...𝑀) → 𝑥 ∈ ℤ)
102	101	ad2antrl 740	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑥 ∈ ℤ)
103		dvdsmul2 16326	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℤ ∧ 𝑄 ∈ ℤ) → 𝑄 ∥ (𝑥 · 𝑄))
104	102, 56, 103	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∥ (𝑥 · 𝑄))
105		breq2 5109	. . . . . . . . . . . . . 14 ⊢ ((𝑥 · 𝑄) = (𝑦 · 𝑃) → (𝑄 ∥ (𝑥 · 𝑄) ↔ 𝑄 ∥ (𝑦 · 𝑃)))
106	104, 105	syl5ibcom 248	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑥 · 𝑄) = (𝑦 · 𝑃) → 𝑄 ∥ (𝑦 · 𝑃)))
107	106	necon3bd 2974	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (¬ 𝑄 ∥ (𝑦 · 𝑃) → (𝑥 · 𝑄) ≠ (𝑦 · 𝑃)))
108	100, 107	mpd 16	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑥 · 𝑄) ≠ (𝑦 · 𝑃))
109		elfznn 13572	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (1...𝑀) → 𝑥 ∈ ℕ)
110	109	ad2antrl 740	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑥 ∈ ℕ)
111	110, 51	nnmulcld 12280	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑥 · 𝑄) ∈ ℕ)
112	111	nnred 12239	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑥 · 𝑄) ∈ ℝ)
113	96, 93	nnmulcld 12280	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑦 · 𝑃) ∈ ℕ)
114	113	nnred 12239	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑦 · 𝑃) ∈ ℝ)
115	112, 114	lttri2d 11337	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑥 · 𝑄) ≠ (𝑦 · 𝑃) ↔ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
116	108, 115	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
117	116	ex 417	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) → ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
118	117	pm4.71rd 571	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)))))
119		ancom 465	. . . . . . . 8 ⊢ ((((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
120	118, 119	bitr2di 291	. . . . . . 7 ⊢ (𝜑 → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))))
121	120	opabbidv 5171	. . . . . 6 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))})
122		unopab 5185	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}) = {⟨𝑥, 𝑦⟩ ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∨ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
123	34	uneq2i 4121	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
124		andi 1023	. . . . . . . 8 ⊢ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∨ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
125	124	opabbii 5172	. . . . . . 7 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = {⟨𝑥, 𝑦⟩ ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∨ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
126	122, 123, 125	3eqtr4i 2798	. . . . . 6 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
127		df-xp 5658	. . . . . 6 ⊢ ((1...𝑀) × (1...𝑁)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))}
128	121, 126, 127	3eqtr4g 2825	. . . . 5 ⊢ (𝜑 → ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆) = ((1...𝑀) × (1...𝑁)))
129	128	fveq2d 6875	. . . 4 ⊢ (𝜑 → (♯‘({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆)) = (♯‘((1...𝑀) × (1...𝑁))))
130		inopab 5807	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}) = {⟨𝑥, 𝑦⟩ ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∧ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
131	34	ineq2i 4172	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
132		anandi 688	. . . . . . . 8 ⊢ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∧ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
133	132	opabbii 5172	. . . . . . 7 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = {⟨𝑥, 𝑦⟩ ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∧ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
134	130, 131, 133	3eqtr4i 2798	. . . . . 6 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
135		ltnsym2 11297	. . . . . . . . . . . 12 ⊢ (((𝑥 · 𝑄) ∈ ℝ ∧ (𝑦 · 𝑃) ∈ ℝ) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
136	112, 114, 135	syl2anc 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
137	136	ex 417	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
138		imnan 404	. . . . . . . . . 10 ⊢ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ ¬ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
139	137, 138	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → ¬ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
140	139	nexdv 1959	. . . . . . . 8 ⊢ (𝜑 → ¬ ∃𝑦((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
141	140	nexdv 1959	. . . . . . 7 ⊢ (𝜑 → ¬ ∃𝑥∃𝑦((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
142		opabn0 5529	. . . . . . . 8 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} ≠ ∅ ↔ ∃𝑥∃𝑦((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
143	142	necon1bbii 3009	. . . . . . 7 ⊢ (¬ ∃𝑥∃𝑦((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = ∅)
144	141, 143	sylib 221	. . . . . 6 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = ∅)
145	134, 144	eqtrid 2812	. . . . 5 ⊢ (𝜑 → ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = ∅)
146		hashun 14409	. . . . 5 ⊢ (({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin ∧ 𝑆 ∈ Fin ∧ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = ∅) → (♯‘({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆)) = ((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆)))
147	25, 42, 145, 146	syl3anc 1394	. . . 4 ⊢ (𝜑 → (♯‘({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆)) = ((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆)))
148		hashxp 14461	. . . . . 6 ⊢ (((1...𝑀) ∈ Fin ∧ (1...𝑁) ∈ Fin) → (♯‘((1...𝑀) × (1...𝑁))) = ((♯‘(1...𝑀)) · (♯‘(1...𝑁))))
149	19, 20, 148	syl2anc 595	. . . . 5 ⊢ (𝜑 → (♯‘((1...𝑀) × (1...𝑁))) = ((♯‘(1...𝑀)) · (♯‘(1...𝑁))))
150	2, 6	gausslemma2dlem0b 27479	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ)
151	150	nnnn0d 12556	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
152		hashfz1 14373	. . . . . . 7 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(1...𝑀)) = 𝑀)
153	151, 152	syl 18	. . . . . 6 ⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀)
154	52	nnnn0d 12556	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
155		hashfz1 14373	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(1...𝑁)) = 𝑁)
156	154, 155	syl 18	. . . . . 6 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
157	153, 156	oveq12d 7418	. . . . 5 ⊢ (𝜑 → ((♯‘(1...𝑀)) · (♯‘(1...𝑁))) = (𝑀 · 𝑁))
158	149, 157	eqtrd 2800	. . . 4 ⊢ (𝜑 → (♯‘((1...𝑀) × (1...𝑁))) = (𝑀 · 𝑁))
159	129, 147, 158	3eqtr3d 2808	. . 3 ⊢ (𝜑 → ((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆)) = (𝑀 · 𝑁))
160	159	oveq2d 7416	. 2 ⊢ (𝜑 → (-1↑((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆))) = (-1↑(𝑀 · 𝑁)))
161	36, 47, 160	3eqtr2d 2806	1 ⊢ (𝜑 → ((𝑃 /_L 𝑄) · (𝑄 /_L 𝑃)) = (-1↑(𝑀 · 𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 = wceq 1563 ∃wex 1802 ∈ wcel 2145 ≠ wne 2960 ∖ cdif 3904 ∪ cun 3905 ∩ cin 3906 ⊆ wss 3907 ∅c0 4288 {csn 4585 class class class wbr 5105 {copab 5167 × cxp 5650 ^◡ccnv 5651 Rel wrel 5657 ‘cfv 6525 (class class class)co 7400 ≈ cen 8928 Fincfn 8931 ℂcc 11086 ℝcr 11087 1c1 11089 + caddc 11091 · cmul 11093 < clt 11231 ≤ cle 11232 − cmin 11429 -cneg 11430 / cdiv 11859 ℕcn 12224 2c2 12286 ℕ₀cn0 12495 ℤcz 12582 ℤ_≥cuz 12853 ℝ⁺crp 13007 ...cfz 13526 ↑cexp 14088 ♯chash 14357 ∥ cdvds 16300 gcd cgcd 16542 ℙcprime 16719 /_L clgs 27416

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5232 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 ax-inf2 9598 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165 ax-pre-sup 11166 ax-addf 11167 ax-mulf 11168

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4869 df-int 4909 df-iun 4954 df-disj 5073 df-br 5106 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5547 df-eprel 5552 df-po 5560 df-so 5561 df-fr 5605 df-se 5606 df-we 5607 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-pred 6292 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-isom 6534 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-of 7664 df-om 7851 df-1st 7974 df-2nd 7975 df-supp 8145 df-tpos 8210 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-2o 8442 df-oadd 8445 df-er 8682 df-ec 8684 df-qs 8688 df-map 8814 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-fsupp 9310 df-sup 9390 df-inf 9391 df-oi 9460 df-dju 9875 df-card 9913 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-div 11860 df-nn 12225 df-2 12294 df-3 12295 df-4 12296 df-5 12297 df-6 12298 df-7 12299 df-8 12300 df-9 12301 df-n0 12496 df-xnn0 12569 df-z 12583 df-dec 12703 df-uz 12854 df-q 12964 df-rp 13008 df-fz 13527 df-fzo 13674 df-fl 13816 df-mod 13894 df-seq 14029 df-exp 14089 df-hash 14358 df-cj 15140 df-re 15141 df-im 15142 df-sqrt 15276 df-abs 15277 df-clim 15529 df-sum 15728 df-dvds 16301 df-gcd 16543 df-prm 16720 df-phi 16815 df-pc 16887 df-struct 17197 df-sets 17214 df-slot 17232 df-ndx 17244 df-base 17260 df-ress 17281 df-plusg 17313 df-mulr 17314 df-starv 17315 df-sca 17316 df-vsca 17317 df-ip 17318 df-tset 17319 df-ple 17320 df-ds 17322 df-unif 17323 df-0g 17484 df-gsum 17485 df-imas 17552 df-qus 17553 df-mgm 18688 df-sgrp 18767 df-mnd 18783 df-mhm 18831 df-submnd 18832 df-grp 18993 df-minusg 18994 df-sbg 18995 df-mulg 19125 df-subg 19180 df-nsg 19181 df-eqg 19182 df-ghm 19275 df-cntz 19378 df-cmn 19843 df-abl 19844 df-mgp 20208 df-rng 20222 df-ur 20255 df-ring 20308 df-cring 20309 df-oppr 20410 df-dvdsr 20430 df-unit 20431 df-invr 20461 df-dvr 20474 df-rhm 20545 df-nzr 20587 df-subrng 20622 df-subrg 20646 df-rlreg 20770 df-domn 20771 df-idom 20772 df-drng 20806 df-field 20807 df-lmod 20952 df-lss 21022 df-lsp 21062 df-sra 21263 df-rgmod 21264 df-lidl 21301 df-rsp 21302 df-2idl 21351 df-cnfld 21483 df-zring 21557 df-zrh 21613 df-zn 21616 df-lgs 27417

This theorem is referenced by: lgsquad 27505

W3C validator