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 27718

Description: Lemma for lgsquad 27719. (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 3010	. . . . 5 ⊢ (𝜑 → 𝑄 ≠ 𝑃)
5		lgsquad.5	. . . . 5 ⊢ 𝑁 = ((𝑄 − 1) / 2)
6		lgsquad.4	. . . . 5 ⊢ 𝑀 = ((𝑃 − 1) / 2)
7		eleq1w 2843	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ (1...𝑀) ↔ 𝑧 ∈ (1...𝑀)))
8		eleq1w 2843	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ (1...𝑁) ↔ 𝑤 ∈ (1...𝑁)))
9	7, 8	bi2anan9 650	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑧 ∈ (1...𝑀) ∧ 𝑤 ∈ (1...𝑁))))
10	9	biancomd 469	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀))))
11		oveq1 7431	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑥 · 𝑄) = (𝑧 · 𝑄))
12		oveq1 7431	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (𝑦 · 𝑃) = (𝑤 · 𝑃))
13	11, 12	breqan12d 5118	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 · 𝑄) < (𝑦 · 𝑃) ↔ (𝑧 · 𝑄) < (𝑤 · 𝑃)))
14	10, 13	anbi12d 644	. . . . . . 7 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ↔ ((𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀)) ∧ (𝑧 · 𝑄) < (𝑤 · 𝑃))))
15	14	ancoms 464	. . . . . 6 ⊢ ((𝑦 = 𝑤 ∧ 𝑥 = 𝑧) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ↔ ((𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀)) ∧ (𝑧 · 𝑄) < (𝑤 · 𝑃))))
16	15	cbvopabv 5177	. . . . 5 ⊢ {⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} = {⟨𝑤, 𝑧⟩ ∣ ((𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀)) ∧ (𝑧 · 𝑄) < (𝑤 · 𝑃))}
17	1, 2, 4, 5, 6, 16	lgsquadlem2 27717	. . . 4 ⊢ (𝜑 → (𝑃 /_L 𝑄) = ( -1↑(♯‘{⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})))
18		relopabv 5800	. . . . . . . 8 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}
19		fzfid 14123	. . . . . . . . . 10 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
20		fzfid 14123	. . . . . . . . . 10 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
21		xpfi 9319	. . . . . . . . . 10 ⊢ (((1...𝑀) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((1...𝑀) × (1...𝑁)) ∈ Fin)
22	19, 20, 21	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin)
23		opabssxp 5744	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ⊆ ((1...𝑀) × (1...𝑁))
24		ssfi 9196	. . . . . . . . 9 ⊢ ((((1...𝑀) × (1...𝑁)) ∈ Fin ∧ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ⊆ ((1...𝑀) × (1...𝑁))) → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin)
25	22, 23, 24	sylancl 598	. . . . . . . 8 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin)
26		cnven 9069	. . . . . . . 8 ⊢ ((Rel {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∧ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin) → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ ^◡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})
27	18, 25, 26	sylancr 599	. . . . . . 7 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ ^◡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})
28		cnvopab 6133	. . . . . . 7 ⊢ ^◡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} = {⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}
29	27, 28	breqtrdi 5145	. . . . . 6 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ {⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})
30		hasheni 14499	. . . . . 6 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ {⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} → (♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) = (♯‘{⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}))
31	29, 30	syl 18	. . . . 5 ⊢ (𝜑 → (♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) = (♯‘{⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}))
32	31	oveq2d 7440	. . . 4 ⊢ (𝜑 → ( -1↑(♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})) = ( -1↑(♯‘{⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})))
33	17, 32	eqtr4d 2798	. . 3 ⊢ (𝜑 → (𝑃 /_L 𝑄) = ( -1↑(♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})))
34		lgsquad.6	. . . 4 ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}
35	2, 1, 3, 6, 5, 34	lgsquadlem2 27717	. . 3 ⊢ (𝜑 → (𝑄 /_L 𝑃) = ( -1↑(♯‘𝑆)))
36	33, 35	oveq12d 7442	. 2 ⊢ (𝜑 → ((𝑃 /_L 𝑄) · (𝑄 /_L 𝑃)) = (( -1↑(♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})) · ( -1↑(♯‘𝑆))))
37		neg1cn 12312	. . . 4 ⊢ -1 ∈ ℂ
38	37	a1i 11	. . 3 ⊢ (𝜑 → -1 ∈ ℂ)
39		opabssxp 5744	. . . . . 6 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁))
40	34, 39	eqsstri 3955	. . . . 5 ⊢ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))
41		ssfi 9196	. . . . 5 ⊢ ((((1...𝑀) × (1...𝑁)) ∈ Fin ∧ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin)
42	22, 40, 41	sylancl 598	. . . 4 ⊢ (𝜑 → 𝑆 ∈ Fin)
43		hashcl 14507	. . . 4 ⊢ (𝑆 ∈ Fin → (♯‘𝑆) ∈ ℕ₀)
44	42, 43	syl 18	. . 3 ⊢ (𝜑 → (♯‘𝑆) ∈ ℕ₀)
45		hashcl 14507	. . . 4 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin → (♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) ∈ ℕ₀)
46	25, 45	syl 18	. . 3 ⊢ (𝜑 → (♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) ∈ ℕ₀)
47	38, 44, 46	expaddd 14298	. 2 ⊢ (𝜑 → ( -1↑((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆))) = (( -1↑(♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})) · ( -1↑(♯‘𝑆))))
48	1	eldifad 4050	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄 ∈ ℙ)
49	48	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈ ℙ)
50		prmnn 16858	. . . . . . . . . . . . . . . 16 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℕ)
51	49, 50	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈ ℕ)
52	1, 5	gausslemma2dlem0b 27693	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℕ)
53	52	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ∈ ℕ)
54	53	nnzd 12726	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ∈ ℤ)
55		prmz 16859	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
56	49, 55	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈ ℤ)
57		peano2zm 12746	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑄 ∈ ℤ → (𝑄 − 1) ∈ ℤ)
58	56, 57	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ ℤ)
59	53	nnred 12357	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ∈ ℝ)
60	58	zred 12810	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ ℝ)
61		prmuz2 16880	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ (ℤ_≥‘2))
62	49, 61	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈ (ℤ_≥‘2))
63		uz2m1nn 13057	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑄 ∈ (ℤ_≥‘2) → (𝑄 − 1) ∈ ℕ)
64	62, 63	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ ℕ)
65	64	nnrpd 13169	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ ℝ⁺)
66		rphalflt 13158	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 − 1) ∈ ℝ⁺ → ((𝑄 − 1) / 2) < (𝑄 − 1))
67	65, 66	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑄 − 1) / 2) < (𝑄 − 1))
68	5, 67	eqbrtrid 5139	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 < (𝑄 − 1))
69	59, 60, 68	ltled 11465	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ≤ (𝑄 − 1))
70		eluz2 12978	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑄 − 1) ∈ (ℤ_≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ (𝑄 − 1) ∈ ℤ ∧ 𝑁 ≤ (𝑄 − 1)))
71	54, 58, 69, 70	syl3anbrc 1362	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ (ℤ_≥‘𝑁))
72		fzss2 13705	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄 − 1) ∈ (ℤ_≥‘𝑁) → (1...𝑁) ⊆ (1...(𝑄 − 1)))
73	71, 72	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (1...𝑁) ⊆ (1...(𝑄 − 1)))
74		simprr 785	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ (1...𝑁))
75	73, 74	sseldd 3910	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ (1...(𝑄 − 1)))
76		fzm1ndvds 16501	. . . . . . . . . . . . . . 15 ⊢ ((𝑄 ∈ ℕ ∧ 𝑦 ∈ (1...(𝑄 − 1))) → ¬ 𝑄 ∥ 𝑦)
77	51, 75, 76	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ 𝑄 ∥ 𝑦)
78	4	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ≠ 𝑃)
79	2	eldifad 4050	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑃 ∈ ℙ)
80	79	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℙ)
81		prmrp 16897	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄 ∈ ℙ ∧ 𝑃 ∈ ℙ) → ((𝑄 gcd 𝑃) = 1 ↔ 𝑄 ≠ 𝑃))
82	49, 80, 81	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑄 gcd 𝑃) = 1 ↔ 𝑄 ≠ 𝑃))
83	78, 82	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 gcd 𝑃) = 1)
84		prmz 16859	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
85	80, 84	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℤ)
86		elfzelz 13663	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℤ)
87	86	ad2antll 742	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ ℤ)
88		coprmdvds 16837	. . . . . . . . . . . . . . . 16 ⊢ ((𝑄 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑄 ∥ (𝑃 · 𝑦) ∧ (𝑄 gcd 𝑃) = 1) → 𝑄 ∥ 𝑦))
89	56, 85, 87, 88	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑄 ∥ (𝑃 · 𝑦) ∧ (𝑄 gcd 𝑃) = 1) → 𝑄 ∥ 𝑦))
90	83, 89	mpan2d 707	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 ∥ (𝑃 · 𝑦) → 𝑄 ∥ 𝑦))
91	77, 90	mtod 201	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ 𝑄 ∥ (𝑃 · 𝑦))
92		prmnn 16858	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
93	80, 92	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℕ)
94	93	nncnd 12358	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℂ)
95		elfznn 13694	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
96	95	ad2antll 742	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ ℕ)
97	96	nncnd 12358	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ ℂ)
98	94, 97	mulcomd 11337	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑃 · 𝑦) = (𝑦 · 𝑃))
99	98	breq2d 5114	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 ∥ (𝑃 · 𝑦) ↔ 𝑄 ∥ (𝑦 · 𝑃)))
100	91, 99	mtbid 327	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ 𝑄 ∥ (𝑦 · 𝑃))
101		elfzelz 13663	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...𝑀) → 𝑥 ∈ ℤ)
102	101	ad2antrl 741	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑥 ∈ ℤ)
103		dvdsmul2 16457	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℤ ∧ 𝑄 ∈ ℤ) → 𝑄 ∥ (𝑥 · 𝑄))
104	102, 56, 103	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∥ (𝑥 · 𝑄))
105		breq2 5106	. . . . . . . . . . . . . 14 ⊢ ((𝑥 · 𝑄) = (𝑦 · 𝑃) → (𝑄 ∥ (𝑥 · 𝑄) ↔ 𝑄 ∥ (𝑦 · 𝑃)))
106	104, 105	syl5ibcom 248	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑥 · 𝑄) = (𝑦 · 𝑃) → 𝑄 ∥ (𝑦 · 𝑃)))
107	106	necon3bd 2969	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (¬ 𝑄 ∥ (𝑦 · 𝑃) → (𝑥 · 𝑄) ≠ (𝑦 · 𝑃)))
108	100, 107	mpd 16	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑥 · 𝑄) ≠ (𝑦 · 𝑃))
109		elfznn 13694	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (1...𝑀) → 𝑥 ∈ ℕ)
110	109	ad2antrl 741	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑥 ∈ ℕ)
111	110, 51	nnmulcld 12398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑥 · 𝑄) ∈ ℕ)
112	111	nnred 12357	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑥 · 𝑄) ∈ ℝ)
113	96, 93	nnmulcld 12398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑦 · 𝑃) ∈ ℕ)
114	113	nnred 12357	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑦 · 𝑃) ∈ ℝ)
115	112, 114	lttri2d 11456	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑥 · 𝑄) ≠ (𝑦 · 𝑃) ↔ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
116	108, 115	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
117	116	ex 418	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) → ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
118	117	pm4.71rd 572	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)))))
119		ancom 466	. . . . . . . 8 ⊢ ((((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
120	118, 119	bitr2di 291	. . . . . . 7 ⊢ (𝜑 → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))))
121	120	opabbidv 5170	. . . . . 6 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))})
122		unopab 5184	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}) = {⟨𝑥, 𝑦⟩ ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∨ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
123	34	uneq2i 4163	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
124		andi 1025	. . . . . . . 8 ⊢ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∨ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
125	124	opabbii 5171	. . . . . . 7 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = {⟨𝑥, 𝑦⟩ ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∨ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
126	122, 123, 125	3eqtr4i 2793	. . . . . 6 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
127		df-xp 5657	. . . . . 6 ⊢ ((1...𝑀) × (1...𝑁)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))}
128	121, 126, 127	3eqtr4g 2820	. . . . 5 ⊢ (𝜑 → ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆) = ((1...𝑀) × (1...𝑁)))
129	128	fveq2d 6894	. . . 4 ⊢ (𝜑 → (♯‘({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆)) = (♯‘((1...𝑀) × (1...𝑁))))
130		inopab 5808	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}) = {⟨𝑥, 𝑦⟩ ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∧ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
131	34	ineq2i 4113	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
132		anandi 689	. . . . . . . 8 ⊢ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∧ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
133	132	opabbii 5171	. . . . . . 7 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = {⟨𝑥, 𝑦⟩ ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∧ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
134	130, 131, 133	3eqtr4i 2793	. . . . . 6 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
135		ltnsym2 11416	. . . . . . . . . . . 12 ⊢ (((𝑥 · 𝑄) ∈ ℝ ∧ (𝑦 · 𝑃) ∈ ℝ) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
136	112, 114, 135	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
137	136	ex 418	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
138		imnan 405	. . . . . . . . . 10 ⊢ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ ¬ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
139	137, 138	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → ¬ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
140	139	nexdv 1968	. . . . . . . 8 ⊢ (𝜑 → ¬ ∃𝑦((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
141	140	nexdv 1968	. . . . . . 7 ⊢ (𝜑 → ¬ ∃𝑥∃𝑦((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
142		opabn0 5528	. . . . . . . 8 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} ≠ ∅ ↔ ∃𝑥∃𝑦((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
143	142	necon1bbii 3004	. . . . . . 7 ⊢ (¬ ∃𝑥∃𝑦((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = ∅)
144	141, 143	sylib 221	. . . . . 6 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = ∅)
145	134, 144	eqtrid 2807	. . . . 5 ⊢ (𝜑 → ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = ∅)
146		hashun 14533	. . . . 5 ⊢ (({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin ∧ 𝑆 ∈ Fin ∧ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = ∅) → (♯‘({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆)) = ((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆)))
147	25, 42, 145, 146	syl3anc 1398	. . . 4 ⊢ (𝜑 → (♯‘({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆)) = ((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆)))
148		hashxp 14586	. . . . . 6 ⊢ (((1...𝑀) ∈ Fin ∧ (1...𝑁) ∈ Fin) → (♯‘((1...𝑀) × (1...𝑁))) = ((♯‘(1...𝑀)) · (♯‘(1...𝑁))))
149	19, 20, 148	syl2anc 596	. . . . 5 ⊢ (𝜑 → (♯‘((1...𝑀) × (1...𝑁))) = ((♯‘(1...𝑀)) · (♯‘(1...𝑁))))
150	2, 6	gausslemma2dlem0b 27693	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ)
151	150	nnnn0d 12674	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
152		hashfz1 14497	. . . . . . 7 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(1...𝑀)) = 𝑀)
153	151, 152	syl 18	. . . . . 6 ⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀)
154	52	nnnn0d 12674	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
155		hashfz1 14497	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(1...𝑁)) = 𝑁)
156	154, 155	syl 18	. . . . . 6 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
157	153, 156	oveq12d 7442	. . . . 5 ⊢ (𝜑 → ((♯‘(1...𝑀)) · (♯‘(1...𝑁))) = (𝑀 · 𝑁))
158	149, 157	eqtrd 2795	. . . 4 ⊢ (𝜑 → (♯‘((1...𝑀) × (1...𝑁))) = (𝑀 · 𝑁))
159	129, 147, 158	3eqtr3d 2803	. . 3 ⊢ (𝜑 → ((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆)) = (𝑀 · 𝑁))
160	159	oveq2d 7440	. 2 ⊢ (𝜑 → ( -1↑((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆))) = ( -1↑(𝑀 · 𝑁)))
161	36, 47, 160	3eqtr2d 2801	1 ⊢ (𝜑 → ((𝑃 /_L 𝑄) · (𝑄 /_L 𝑃)) = ( -1↑(𝑀 · 𝑁)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1569 ∃wex 1811 ∈ wcel 2144 ≠ wne 2955 ⊆ wss 3896 ∖ cdif 4044 ∩ cin 4088 ∪ cun 4148 ∅c0 4277 {csn 4584 class class class wbr 5102 {copab 5166 × cxp 5649 ^◡ccnv 5650 Rel wrel 5656 ‘cfv 6543 (class class class)co 7424 ≈ cen 8978 Fincfn 8981 ℂcc 11205 ℝcr 11206 1c1 11208 + caddc 11210 · cmul 11212 < clt 11350 ≤ cle 11351 − cmin 11548 -cneg 11549 / cdiv 11980 ℕcn 12342 2c2 12404 ℕ₀cn0 12613 ℤcz 12700 ℤ_≥cuz 12972 ℝ⁺crp 13127 ...cfz 13646 ↑cexp 14211 ♯chash 14481 ∥ cdvds 16431 gcd cgcd 16673 ℙcprime 16855 /_L clgs 27630

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5327 ax-pr 5391 ax-un 7755 ax-inf2 9649 ax-cnex 11263 ax-resscn 11264 ax-1cn 11265 ax-icn 11266 ax-addcl 11267 ax-addrcl 11268 ax-mulcl 11269 ax-mulrcl 11270 ax-mulcom 11271 ax-addass 11272 ax-mulass 11273 ax-distr 11274 ax-i2m1 11275 ax-1ne0 11276 ax-1rid 11277 ax-rnegex 11278 ax-rrecex 11279 ax-cnre 11280 ax-pre-lttri 11281 ax-pre-lttrn 11282 ax-pre-ltadd 11283 ax-pre-mulgt0 11284 ax-pre-sup 11285 ax-addf 11286 ax-mulf 11287

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-disj 5070 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6307 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6497 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7381 df-ov 7427 df-oprab 7428 df-mpo 7429 df-of 7697 df-om 7882 df-1st 8005 df-2nd 8006 df-supp 8185 df-tpos 8251 df-frecs 8307 df-wrecs 8338 df-recs 8387 df-rdg 8426 df-1o 8484 df-2o 8485 df-oadd 8488 df-er 8725 df-ec 8727 df-qs 8731 df-map 8857 df-en 8982 df-dom 8983 df-sdom 8984 df-fin 8985 df-fsupp 9362 df-sup 9441 df-inf 9442 df-oi 9511 df-dju 9989 df-card 10027 df-pnf 11352 df-mnf 11353 df-xr 11354 df-ltxr 11355 df-le 11356 df-sub 11550 df-neg 11551 df-div 11981 df-nn 12343 df-2 12412 df-3 12413 df-4 12414 df-5 12415 df-6 12416 df-7 12417 df-8 12418 df-9 12419 df-n0 12614 df-xnn0 12687 df-z 12701 df-dec 12822 df-uz 12973 df-q 13083 df-rp 13128 df-fz 13647 df-fzo 13796 df-fl 13939 df-mod 14017 df-seq 14152 df-exp 14212 df-hash 14482 df-cj 15275 df-re 15276 df-im 15277 df-sqrt 15411 df-abs 15412 df-clim 15664 df-sum 15863 df-dvds 16432 df-gcd 16674 df-prm 16856 df-phi 16952 df-pc 17024 df-struct 17334 df-sets 17351 df-slot 17369 df-ndx 17381 df-base 17397 df-ress 17418 df-plusg 17450 df-mulr 17451 df-starv 17452 df-sca 17453 df-vsca 17454 df-ip 17455 df-tset 17456 df-ple 17457 df-ds 17459 df-unif 17460 df-0g 17621 df-gsum 17622 df-imas 17689 df-qus 17690 df-mgm 18825 df-sgrp 18917 df-mnd 18933 df-mhm 18987 df-submnd 18988 df-grp 19156 df-minusg 19157 df-sbg 19158 df-mulg 19287 df-subg 19342 df-nsg 19343 df-eqg 19344 df-ghm 19437 df-cntz 19540 df-cmn 20005 df-abl 20006 df-mgp 20370 df-rng 20384 df-ur 20417 df-ring 20470 df-cring 20471 df-oppr 20576 df-dvdsr 20596 df-unit 20597 df-invr 20627 df-dvr 20640 df-rhm 20711 df-nzr 20772 df-subrng 20807 df-subrg 20831 df-rlreg 20955 df-domn 20956 df-idom 20957 df-drng 20991 df-field 20992 df-lmod 21146 df-lss 21216 df-lsp 21256 df-sra 21457 df-rgmod 21458 df-lidl 21495 df-rsp 21496 df-2idl 21552 df-cnfld 21688 df-zring 21762 df-zrh 21818 df-zn 21821 df-lgs 27631

This theorem is used by: lgsquad 27719

W3C validator