Metamath Proof Explorer

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 ↑ ( 𝑀 · 𝑁 ) ) )