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 syl5eq ( 𝜑 → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 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 ↑ ( 𝑀 · 𝑁 ) ) )