lgsquadlem3 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > lgsquadlem3		GIF version

Theorem lgsquadlem3 15606

Description: Lemma for lgsquad 15607. (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 2463	. . . . 5 ⊢ (𝜑 → 𝑄 ≠ 𝑃)
5		lgsquad.5	. . . . 5 ⊢ 𝑁 = ((𝑄 − 1) / 2)
6		lgsquad.4	. . . . 5 ⊢ 𝑀 = ((𝑃 − 1) / 2)
7		eleq1w 2267	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ (1...𝑀) ↔ 𝑧 ∈ (1...𝑀)))
8		eleq1w 2267	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ (1...𝑁) ↔ 𝑤 ∈ (1...𝑁)))
9	7, 8	bi2anan9 606	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑧 ∈ (1...𝑀) ∧ 𝑤 ∈ (1...𝑁))))
10	9	biancomd 271	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀))))
11		oveq1 5961	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑥 · 𝑄) = (𝑧 · 𝑄))
12		oveq1 5961	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (𝑦 · 𝑃) = (𝑤 · 𝑃))
13	11, 12	breqan12d 4064	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 · 𝑄) < (𝑦 · 𝑃) ↔ (𝑧 · 𝑄) < (𝑤 · 𝑃)))
14	10, 13	anbi12d 473	. . . . . . 7 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ↔ ((𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀)) ∧ (𝑧 · 𝑄) < (𝑤 · 𝑃))))
15	14	ancoms 268	. . . . . 6 ⊢ ((𝑦 = 𝑤 ∧ 𝑥 = 𝑧) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ↔ ((𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀)) ∧ (𝑧 · 𝑄) < (𝑤 · 𝑃))))
16	15	cbvopabv 4121	. . . . 5 ⊢ {⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} = {⟨𝑤, 𝑧⟩ ∣ ((𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀)) ∧ (𝑧 · 𝑄) < (𝑤 · 𝑃))}
17	1, 2, 4, 5, 6, 16	lgsquadlem2 15605	. . . 4 ⊢ (𝜑 → (𝑃 /_L 𝑄) = (-1↑(♯‘{⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})))
18		relopabv 4807	. . . . . . . 8 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}
19		eqid 2206	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}
20		1zzd 9412	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℤ)
21	2, 6	gausslemma2dlem0b 15577	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℕ)
22	21	nnzd 9507	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℤ)
23	20, 22	fzfigd 10589	. . . . . . . . 9 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
24	1, 5	gausslemma2dlem0b 15577	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ)
25	24	nnzd 9507	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
26	20, 25	fzfigd 10589	. . . . . . . . 9 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
27		elfznn 10189	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (1...𝑀) → 𝑥 ∈ ℕ)
28	27	ad2antrl 490	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑥 ∈ ℕ)
29	1	eldifad 3179	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑄 ∈ ℙ)
30	29	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈ ℙ)
31		prmnn 12482	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℕ)
32	30, 31	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈ ℕ)
33	28, 32	nnmulcld 9098	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑥 · 𝑄) ∈ ℕ)
34	33	nnzd 9507	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑥 · 𝑄) ∈ ℤ)
35		elfznn 10189	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
36	35	ad2antll 491	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ ℕ)
37	2	gausslemma2dlem0a 15576	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ ℕ)
38	37	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℕ)
39	36, 38	nnmulcld 9098	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑦 · 𝑃) ∈ ℕ)
40	39	nnzd 9507	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑦 · 𝑃) ∈ ℤ)
41		zdclt 9463	. . . . . . . . . . 11 ⊢ (((𝑥 · 𝑄) ∈ ℤ ∧ (𝑦 · 𝑃) ∈ ℤ) → DECID (𝑥 · 𝑄) < (𝑦 · 𝑃))
42	34, 40, 41	syl2anc 411	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → DECID (𝑥 · 𝑄) < (𝑦 · 𝑃))
43	42	ralrimivva 2589	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ (1...𝑀)∀𝑦 ∈ (1...𝑁)DECID (𝑥 · 𝑄) < (𝑦 · 𝑃))
44	19, 23, 26, 43	opabfi 7047	. . . . . . . 8 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin)
45		cnven 6911	. . . . . . . 8 ⊢ ((Rel {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∧ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin) → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ ^◡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})
46	18, 44, 45	sylancr 414	. . . . . . 7 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ ^◡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})
47		cnvopab 5090	. . . . . . 7 ⊢ ^◡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} = {⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}
48	46, 47	breqtrdi 4089	. . . . . 6 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ {⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})
49	1, 2, 4, 5, 6, 16	lgsquadlemsfi 15602	. . . . . . 7 ⊢ (𝜑 → {⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin)
50		hashen 10942	. . . . . . 7 ⊢ (({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin ∧ {⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin) → ((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) = (♯‘{⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) ↔ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ {⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}))
51	44, 49, 50	syl2anc 411	. . . . . 6 ⊢ (𝜑 → ((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) = (♯‘{⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) ↔ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ {⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}))
52	48, 51	mpbird 167	. . . . 5 ⊢ (𝜑 → (♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) = (♯‘{⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}))
53	52	oveq2d 5970	. . . 4 ⊢ (𝜑 → (-1↑(♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})) = (-1↑(♯‘{⟨𝑦, 𝑥⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})))
54	17, 53	eqtr4d 2242	. . 3 ⊢ (𝜑 → (𝑃 /_L 𝑄) = (-1↑(♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})))
55		lgsquad.6	. . . 4 ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}
56	2, 1, 3, 6, 5, 55	lgsquadlem2 15605	. . 3 ⊢ (𝜑 → (𝑄 /_L 𝑃) = (-1↑(♯‘𝑆)))
57	54, 56	oveq12d 5972	. 2 ⊢ (𝜑 → ((𝑃 /_L 𝑄) · (𝑄 /_L 𝑃)) = ((-1↑(♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})) · (-1↑(♯‘𝑆))))
58		neg1cn 9154	. . . 4 ⊢ -1 ∈ ℂ
59	58	a1i 9	. . 3 ⊢ (𝜑 → -1 ∈ ℂ)
60	2, 1, 3, 6, 5, 55	lgsquadlemsfi 15602	. . . 4 ⊢ (𝜑 → 𝑆 ∈ Fin)
61		hashcl 10939	. . . 4 ⊢ (𝑆 ∈ Fin → (♯‘𝑆) ∈ ℕ₀)
62	60, 61	syl 14	. . 3 ⊢ (𝜑 → (♯‘𝑆) ∈ ℕ₀)
63		hashcl 10939	. . . 4 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin → (♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) ∈ ℕ₀)
64	44, 63	syl 14	. . 3 ⊢ (𝜑 → (♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) ∈ ℕ₀)
65	59, 62, 64	expaddd 10833	. 2 ⊢ (𝜑 → (-1↑((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆))) = ((-1↑(♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})) · (-1↑(♯‘𝑆))))
66	24	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ∈ ℕ)
67	66	nnzd 9507	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ∈ ℤ)
68		prmz 12483	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
69	30, 68	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈ ℤ)
70		peano2zm 9423	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑄 ∈ ℤ → (𝑄 − 1) ∈ ℤ)
71	69, 70	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ ℤ)
72	66	nnred 9062	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ∈ ℝ)
73	71	zred 9508	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ ℝ)
74		prmuz2 12503	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ (ℤ_≥‘2))
75	30, 74	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈ (ℤ_≥‘2))
76		uz2m1nn 9739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑄 ∈ (ℤ_≥‘2) → (𝑄 − 1) ∈ ℕ)
77	75, 76	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ ℕ)
78	77	nnrpd 9829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ ℝ⁺)
79		rphalflt 9818	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 − 1) ∈ ℝ⁺ → ((𝑄 − 1) / 2) < (𝑄 − 1))
80	78, 79	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑄 − 1) / 2) < (𝑄 − 1))
81	5, 80	eqbrtrid 4083	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 < (𝑄 − 1))
82	72, 73, 81	ltled 8204	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ≤ (𝑄 − 1))
83		eluz2 9667	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑄 − 1) ∈ (ℤ_≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ (𝑄 − 1) ∈ ℤ ∧ 𝑁 ≤ (𝑄 − 1)))
84	67, 71, 82, 83	syl3anbrc 1184	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ (ℤ_≥‘𝑁))
85		fzss2 10199	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄 − 1) ∈ (ℤ_≥‘𝑁) → (1...𝑁) ⊆ (1...(𝑄 − 1)))
86	84, 85	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (1...𝑁) ⊆ (1...(𝑄 − 1)))
87		simprr 531	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ (1...𝑁))
88	86, 87	sseldd 3196	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ (1...(𝑄 − 1)))
89		fzm1ndvds 12217	. . . . . . . . . . . . . . 15 ⊢ ((𝑄 ∈ ℕ ∧ 𝑦 ∈ (1...(𝑄 − 1))) → ¬ 𝑄 ∥ 𝑦)
90	32, 88, 89	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ 𝑄 ∥ 𝑦)
91	4	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ≠ 𝑃)
92	2	eldifad 3179	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑃 ∈ ℙ)
93	92	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℙ)
94		prmrp 12517	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄 ∈ ℙ ∧ 𝑃 ∈ ℙ) → ((𝑄 gcd 𝑃) = 1 ↔ 𝑄 ≠ 𝑃))
95	30, 93, 94	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑄 gcd 𝑃) = 1 ↔ 𝑄 ≠ 𝑃))
96	91, 95	mpbird 167	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 gcd 𝑃) = 1)
97		prmz 12483	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
98	93, 97	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℤ)
99		elfzelz 10160	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℤ)
100	99	ad2antll 491	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ ℤ)
101		coprmdvds 12464	. . . . . . . . . . . . . . . 16 ⊢ ((𝑄 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑄 ∥ (𝑃 · 𝑦) ∧ (𝑄 gcd 𝑃) = 1) → 𝑄 ∥ 𝑦))
102	69, 98, 100, 101	syl3anc 1250	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑄 ∥ (𝑃 · 𝑦) ∧ (𝑄 gcd 𝑃) = 1) → 𝑄 ∥ 𝑦))
103	96, 102	mpan2d 428	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 ∥ (𝑃 · 𝑦) → 𝑄 ∥ 𝑦))
104	90, 103	mtod 665	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ 𝑄 ∥ (𝑃 · 𝑦))
105	38	nncnd 9063	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℂ)
106	36	nncnd 9063	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ ℂ)
107	105, 106	mulcomd 8107	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑃 · 𝑦) = (𝑦 · 𝑃))
108	107	breq2d 4060	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 ∥ (𝑃 · 𝑦) ↔ 𝑄 ∥ (𝑦 · 𝑃)))
109	104, 108	mtbid 674	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ 𝑄 ∥ (𝑦 · 𝑃))
110		elfzelz 10160	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...𝑀) → 𝑥 ∈ ℤ)
111	110	ad2antrl 490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑥 ∈ ℤ)
112		dvdsmul2 12175	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℤ ∧ 𝑄 ∈ ℤ) → 𝑄 ∥ (𝑥 · 𝑄))
113	111, 69, 112	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∥ (𝑥 · 𝑄))
114		breq2 4052	. . . . . . . . . . . . . 14 ⊢ ((𝑥 · 𝑄) = (𝑦 · 𝑃) → (𝑄 ∥ (𝑥 · 𝑄) ↔ 𝑄 ∥ (𝑦 · 𝑃)))
115	113, 114	syl5ibcom 155	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑥 · 𝑄) = (𝑦 · 𝑃) → 𝑄 ∥ (𝑦 · 𝑃)))
116	115	necon3bd 2420	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (¬ 𝑄 ∥ (𝑦 · 𝑃) → (𝑥 · 𝑄) ≠ (𝑦 · 𝑃)))
117	109, 116	mpd 13	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑥 · 𝑄) ≠ (𝑦 · 𝑃))
118		nnq 9767	. . . . . . . . . . . . 13 ⊢ ((𝑥 · 𝑄) ∈ ℕ → (𝑥 · 𝑄) ∈ ℚ)
119	33, 118	syl 14	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑥 · 𝑄) ∈ ℚ)
120		nnq 9767	. . . . . . . . . . . . 13 ⊢ ((𝑦 · 𝑃) ∈ ℕ → (𝑦 · 𝑃) ∈ ℚ)
121	39, 120	syl 14	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑦 · 𝑃) ∈ ℚ)
122		qlttri2 9775	. . . . . . . . . . . 12 ⊢ (((𝑥 · 𝑄) ∈ ℚ ∧ (𝑦 · 𝑃) ∈ ℚ) → ((𝑥 · 𝑄) ≠ (𝑦 · 𝑃) ↔ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
123	119, 121, 122	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑥 · 𝑄) ≠ (𝑦 · 𝑃) ↔ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
124	117, 123	mpbid 147	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
125	124	ex 115	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) → ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
126	125	pm4.71rd 394	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)))))
127		ancom 266	. . . . . . . 8 ⊢ ((((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
128	126, 127	bitr2di 197	. . . . . . 7 ⊢ (𝜑 → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))))
129	128	opabbidv 4115	. . . . . 6 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))})
130		unopab 4128	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}) = {⟨𝑥, 𝑦⟩ ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∨ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
131	55	uneq2i 3326	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
132		andi 820	. . . . . . . 8 ⊢ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∨ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
133	132	opabbii 4116	. . . . . . 7 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = {⟨𝑥, 𝑦⟩ ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∨ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
134	130, 131, 133	3eqtr4i 2237	. . . . . 6 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
135		df-xp 4686	. . . . . 6 ⊢ ((1...𝑀) × (1...𝑁)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))}
136	129, 134, 135	3eqtr4g 2264	. . . . 5 ⊢ (𝜑 → ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆) = ((1...𝑀) × (1...𝑁)))
137	136	fveq2d 5590	. . . 4 ⊢ (𝜑 → (♯‘({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆)) = (♯‘((1...𝑀) × (1...𝑁))))
138		inopab 4815	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}) = {⟨𝑥, 𝑦⟩ ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∧ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
139	55	ineq2i 3373	. . . . . . 7 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
140		anandi 590	. . . . . . . 8 ⊢ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∧ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
141	140	opabbii 4116	. . . . . . 7 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = {⟨𝑥, 𝑦⟩ ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∧ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
142	138, 139, 141	3eqtr4i 2237	. . . . . 6 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))}
143	33	nnred 9062	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑥 · 𝑄) ∈ ℝ)
144	39	nnred 9062	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑦 · 𝑃) ∈ ℝ)
145		ltnsym2 8176	. . . . . . . . . . . . 13 ⊢ (((𝑥 · 𝑄) ∈ ℝ ∧ (𝑦 · 𝑃) ∈ ℝ) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
146	143, 144, 145	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
147	146	ex 115	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
148		imnan 692	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ ¬ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
149	147, 148	sylib 122	. . . . . . . . . 10 ⊢ (𝜑 → ¬ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
150	149	nexdv 1965	. . . . . . . . 9 ⊢ (𝜑 → ¬ ∃𝑦((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
151	150	nexdv 1965	. . . . . . . 8 ⊢ (𝜑 → ¬ ∃𝑥∃𝑦((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
152		opabm 4332	. . . . . . . 8 ⊢ (∃𝑗 𝑗 ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} ↔ ∃𝑥∃𝑦((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))))
153	151, 152	sylnibr 679	. . . . . . 7 ⊢ (𝜑 → ¬ ∃𝑗 𝑗 ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))})
154		notm0 3483	. . . . . . 7 ⊢ (¬ ∃𝑗 𝑗 ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} ↔ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = ∅)
155	153, 154	sylib 122	. . . . . 6 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = ∅)
156	142, 155	eqtrid 2251	. . . . 5 ⊢ (𝜑 → ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = ∅)
157		hashun 10963	. . . . 5 ⊢ (({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin ∧ 𝑆 ∈ Fin ∧ ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = ∅) → (♯‘({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆)) = ((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆)))
158	44, 60, 156, 157	syl3anc 1250	. . . 4 ⊢ (𝜑 → (♯‘({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆)) = ((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆)))
159		hashxp 10984	. . . . . 6 ⊢ (((1...𝑀) ∈ Fin ∧ (1...𝑁) ∈ Fin) → (♯‘((1...𝑀) × (1...𝑁))) = ((♯‘(1...𝑀)) · (♯‘(1...𝑁))))
160	23, 26, 159	syl2anc 411	. . . . 5 ⊢ (𝜑 → (♯‘((1...𝑀) × (1...𝑁))) = ((♯‘(1...𝑀)) · (♯‘(1...𝑁))))
161	21	nnnn0d 9361	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
162		hashfz1 10941	. . . . . . 7 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(1...𝑀)) = 𝑀)
163	161, 162	syl 14	. . . . . 6 ⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀)
164	24	nnnn0d 9361	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
165		hashfz1 10941	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(1...𝑁)) = 𝑁)
166	164, 165	syl 14	. . . . . 6 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
167	163, 166	oveq12d 5972	. . . . 5 ⊢ (𝜑 → ((♯‘(1...𝑀)) · (♯‘(1...𝑁))) = (𝑀 · 𝑁))
168	160, 167	eqtrd 2239	. . . 4 ⊢ (𝜑 → (♯‘((1...𝑀) × (1...𝑁))) = (𝑀 · 𝑁))
169	137, 158, 168	3eqtr3d 2247	. . 3 ⊢ (𝜑 → ((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆)) = (𝑀 · 𝑁))
170	169	oveq2d 5970	. 2 ⊢ (𝜑 → (-1↑((♯‘{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (♯‘𝑆))) = (-1↑(𝑀 · 𝑁)))
171	57, 65, 170	3eqtr2d 2245	1 ⊢ (𝜑 → ((𝑃 /_L 𝑄) · (𝑄 /_L 𝑃)) = (-1↑(𝑀 · 𝑁)))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 710 DECID wdc 836 = wceq 1373 ∃wex 1516 ∈ wcel 2177 ≠ wne 2377 ∖ cdif 3165 ∪ cun 3166 ∩ cin 3167 ⊆ wss 3168 ∅c0 3462 {csn 3635 class class class wbr 4048 {copab 4109 × cxp 4678 ^◡ccnv 4679 Rel wrel 4685 ‘cfv 5277 (class class class)co 5954 ≈ cen 6835 Fincfn 6837 ℂcc 7936 ℝcr 7937 1c1 7939 + caddc 7941 · cmul 7943 < clt 8120 ≤ cle 8121 − cmin 8256 -cneg 8257 / cdiv 8758 ℕcn 9049 2c2 9100 ℕ₀cn0 9308 ℤcz 9385 ℤ_≥cuz 9661 ℚcq 9753 ℝ⁺crp 9788 ...cfz 10143 ↑cexp 10696 ♯chash 10933 ∥ cdvds 12148 gcd cgcd 12324 ℙcprime 12479 /_L clgs 15524

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-coll 4164 ax-sep 4167 ax-nul 4175 ax-pow 4223 ax-pr 4258 ax-un 4485 ax-setind 4590 ax-iinf 4641 ax-cnex 8029 ax-resscn 8030 ax-1cn 8031 ax-1re 8032 ax-icn 8033 ax-addcl 8034 ax-addrcl 8035 ax-mulcl 8036 ax-mulrcl 8037 ax-addcom 8038 ax-mulcom 8039 ax-addass 8040 ax-mulass 8041 ax-distr 8042 ax-i2m1 8043 ax-0lt1 8044 ax-1rid 8045 ax-0id 8046 ax-rnegex 8047 ax-precex 8048 ax-cnre 8049 ax-pre-ltirr 8050 ax-pre-ltwlin 8051 ax-pre-lttrn 8052 ax-pre-apti 8053 ax-pre-ltadd 8054 ax-pre-mulgt0 8055 ax-pre-mulext 8056 ax-arch 8057 ax-caucvg 8058 ax-addf 8060 ax-mulf 8061

This theorem depends on definitions: df-bi 117 df-stab 833 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-xor 1396 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rmo 2493 df-rab 2494 df-v 2775 df-sbc 3001 df-csb 3096 df-dif 3170 df-un 3172 df-in 3174 df-ss 3181 df-nul 3463 df-if 3574 df-pw 3620 df-sn 3641 df-pr 3642 df-tp 3643 df-op 3644 df-uni 3854 df-int 3889 df-iun 3932 df-disj 4025 df-br 4049 df-opab 4111 df-mpt 4112 df-tr 4148 df-id 4345 df-po 4348 df-iso 4349 df-iord 4418 df-on 4420 df-ilim 4421 df-suc 4423 df-iom 4644 df-xp 4686 df-rel 4687 df-cnv 4688 df-co 4689 df-dm 4690 df-rn 4691 df-res 4692 df-ima 4693 df-iota 5238 df-fun 5279 df-fn 5280 df-f 5281 df-f1 5282 df-fo 5283 df-f1o 5284 df-fv 5285 df-isom 5286 df-riota 5909 df-ov 5957 df-oprab 5958 df-mpo 5959 df-of 6168 df-1st 6236 df-2nd 6237 df-tpos 6341 df-recs 6401 df-irdg 6466 df-frec 6487 df-1o 6512 df-2o 6513 df-oadd 6516 df-er 6630 df-ec 6632 df-qs 6636 df-map 6747 df-en 6838 df-dom 6839 df-fin 6840 df-sup 7098 df-inf 7099 df-pnf 8122 df-mnf 8123 df-xr 8124 df-ltxr 8125 df-le 8126 df-sub 8258 df-neg 8259 df-reap 8661 df-ap 8668 df-div 8759 df-inn 9050 df-2 9108 df-3 9109 df-4 9110 df-5 9111 df-6 9112 df-7 9113 df-8 9114 df-9 9115 df-n0 9309 df-z 9386 df-dec 9518 df-uz 9662 df-q 9754 df-rp 9789 df-fz 10144 df-fzo 10278 df-fl 10426 df-mod 10481 df-seqfrec 10606 df-exp 10697 df-ihash 10934 df-cj 11203 df-re 11204 df-im 11205 df-rsqrt 11359 df-abs 11360 df-clim 11640 df-sumdc 11715 df-proddc 11912 df-dvds 12149 df-gcd 12325 df-prm 12480 df-phi 12583 df-pc 12658 df-struct 12884 df-ndx 12885 df-slot 12886 df-base 12888 df-sets 12889 df-iress 12890 df-plusg 12972 df-mulr 12973 df-starv 12974 df-sca 12975 df-vsca 12976 df-ip 12977 df-tset 12978 df-ple 12979 df-ds 12981 df-unif 12982 df-0g 13140 df-igsum 13141 df-topgen 13142 df-iimas 13184 df-qus 13185 df-mgm 13238 df-sgrp 13284 df-mnd 13299 df-mhm 13341 df-submnd 13342 df-grp 13385 df-minusg 13386 df-sbg 13387 df-mulg 13506 df-subg 13556 df-nsg 13557 df-eqg 13558 df-ghm 13627 df-cmn 13672 df-abl 13673 df-mgp 13733 df-rng 13745 df-ur 13772 df-srg 13776 df-ring 13810 df-cring 13811 df-oppr 13880 df-dvdsr 13901 df-unit 13902 df-invr 13933 df-dvr 13944 df-rhm 13964 df-nzr 13992 df-subrg 14031 df-domn 14071 df-idom 14072 df-lmod 14101 df-lssm 14165 df-lsp 14199 df-sra 14247 df-rgmod 14248 df-lidl 14281 df-rsp 14282 df-2idl 14312 df-bl 14358 df-mopn 14359 df-fg 14361 df-metu 14362 df-cnfld 14369 df-zring 14403 df-zrh 14426 df-zn 14428 df-lgs 15525

This theorem is referenced by: lgsquad 15607

W3C validator