Theorem lgsquadlem3

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

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

Proof

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