Step | Hyp | Ref
| Expression |
1 | | lgseisen.2 |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ (ℙ ∖
{2})) |
2 | | lgseisen.1 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
3 | | lgseisen.3 |
. . . . . 6
⊢ (𝜑 → 𝑃 ≠ 𝑄) |
4 | 3 | necomd 2837 |
. . . . 5
⊢ (𝜑 → 𝑄 ≠ 𝑃) |
5 | | lgsquad.5 |
. . . . 5
⊢ 𝑁 = ((𝑄 − 1) / 2) |
6 | | lgsquad.4 |
. . . . 5
⊢ 𝑀 = ((𝑃 − 1) / 2) |
7 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑥 ∈ (1...𝑀) ↔ 𝑧 ∈ (1...𝑀))) |
8 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑤 → (𝑦 ∈ (1...𝑁) ↔ 𝑤 ∈ (1...𝑁))) |
9 | 7, 8 | bi2anan9 913 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑧 ∈ (1...𝑀) ∧ 𝑤 ∈ (1...𝑁)))) |
10 | | ancom 465 |
. . . . . . . . 9
⊢ ((𝑧 ∈ (1...𝑀) ∧ 𝑤 ∈ (1...𝑁)) ↔ (𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀))) |
11 | 9, 10 | syl6bb 275 |
. . . . . . . 8
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀)))) |
12 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑥 · 𝑄) = (𝑧 · 𝑄)) |
13 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑦 = 𝑤 → (𝑦 · 𝑃) = (𝑤 · 𝑃)) |
14 | 12, 13 | breqan12d 4599 |
. . . . . . . 8
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 · 𝑄) < (𝑦 · 𝑃) ↔ (𝑧 · 𝑄) < (𝑤 · 𝑃))) |
15 | 11, 14 | anbi12d 743 |
. . . . . . 7
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ↔ ((𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀)) ∧ (𝑧 · 𝑄) < (𝑤 · 𝑃)))) |
16 | 15 | ancoms 468 |
. . . . . 6
⊢ ((𝑦 = 𝑤 ∧ 𝑥 = 𝑧) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ↔ ((𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀)) ∧ (𝑧 · 𝑄) < (𝑤 · 𝑃)))) |
17 | 16 | cbvopabv 4654 |
. . . . 5
⊢
{〈𝑦, 𝑥〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} = {〈𝑤, 𝑧〉 ∣ ((𝑤 ∈ (1...𝑁) ∧ 𝑧 ∈ (1...𝑀)) ∧ (𝑧 · 𝑄) < (𝑤 · 𝑃))} |
18 | 1, 2, 4, 5, 6, 17 | lgsquadlem2 24906 |
. . . 4
⊢ (𝜑 → (𝑃 /L 𝑄) = (-1↑(#‘{〈𝑦, 𝑥〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}))) |
19 | | relopab 5169 |
. . . . . . . 8
⊢ Rel
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} |
20 | | fzfid 12634 |
. . . . . . . . . 10
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
21 | | fzfid 12634 |
. . . . . . . . . 10
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
22 | | xpfi 8116 |
. . . . . . . . . 10
⊢
(((1...𝑀) ∈ Fin
∧ (1...𝑁) ∈ Fin)
→ ((1...𝑀) ×
(1...𝑁)) ∈
Fin) |
23 | 20, 21, 22 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin) |
24 | | opabssxp 5116 |
. . . . . . . . 9
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ⊆ ((1...𝑀) × (1...𝑁)) |
25 | | ssfi 8065 |
. . . . . . . . 9
⊢
((((1...𝑀) ×
(1...𝑁)) ∈ Fin ∧
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ⊆ ((1...𝑀) × (1...𝑁))) → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin) |
26 | 23, 24, 25 | sylancl 693 |
. . . . . . . 8
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin) |
27 | | cnven 7918 |
. . . . . . . 8
⊢ ((Rel
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∧ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin) → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ ◡{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) |
28 | 19, 26, 27 | sylancr 694 |
. . . . . . 7
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ ◡{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) |
29 | | cnvopab 5452 |
. . . . . . 7
⊢ ◡{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} = {〈𝑦, 𝑥〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} |
30 | 28, 29 | syl6breq 4624 |
. . . . . 6
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ {〈𝑦, 𝑥〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) |
31 | | hasheni 12998 |
. . . . . 6
⊢
({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ≈ {〈𝑦, 𝑥〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} → (#‘{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) = (#‘{〈𝑦, 𝑥〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})) |
32 | 30, 31 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) = (#‘{〈𝑦, 𝑥〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})) |
33 | 32 | oveq2d 6565 |
. . . 4
⊢ (𝜑 →
(-1↑(#‘{〈𝑥,
𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})) = (-1↑(#‘{〈𝑦, 𝑥〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}))) |
34 | 18, 33 | eqtr4d 2647 |
. . 3
⊢ (𝜑 → (𝑃 /L 𝑄) = (-1↑(#‘{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}))) |
35 | | lgsquad.6 |
. . . 4
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} |
36 | 2, 1, 3, 6, 5, 35 | lgsquadlem2 24906 |
. . 3
⊢ (𝜑 → (𝑄 /L 𝑃) = (-1↑(#‘𝑆))) |
37 | 34, 36 | oveq12d 6567 |
. 2
⊢ (𝜑 → ((𝑃 /L 𝑄) · (𝑄 /L 𝑃)) = ((-1↑(#‘{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})) · (-1↑(#‘𝑆)))) |
38 | | neg1cn 11001 |
. . . 4
⊢ -1 ∈
ℂ |
39 | 38 | a1i 11 |
. . 3
⊢ (𝜑 → -1 ∈
ℂ) |
40 | | opabssxp 5116 |
. . . . . 6
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁)) |
41 | 35, 40 | eqsstri 3598 |
. . . . 5
⊢ 𝑆 ⊆ ((1...𝑀) × (1...𝑁)) |
42 | | ssfi 8065 |
. . . . 5
⊢
((((1...𝑀) ×
(1...𝑁)) ∈ Fin ∧
𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin) |
43 | 23, 41, 42 | sylancl 693 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ Fin) |
44 | | hashcl 13009 |
. . . 4
⊢ (𝑆 ∈ Fin →
(#‘𝑆) ∈
ℕ0) |
45 | 43, 44 | syl 17 |
. . 3
⊢ (𝜑 → (#‘𝑆) ∈
ℕ0) |
46 | | hashcl 13009 |
. . . 4
⊢
({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin → (#‘{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) ∈
ℕ0) |
47 | 26, 46 | syl 17 |
. . 3
⊢ (𝜑 → (#‘{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) ∈
ℕ0) |
48 | 39, 45, 47 | expaddd 12872 |
. 2
⊢ (𝜑 →
(-1↑((#‘{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (#‘𝑆))) = ((-1↑(#‘{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))})) · (-1↑(#‘𝑆)))) |
49 | 1 | eldifad 3552 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑄 ∈ ℙ) |
50 | 49 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈ ℙ) |
51 | | prmnn 15226 |
. . . . . . . . . . . . . . . 16
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℕ) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈ ℕ) |
53 | | oddprm 15353 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑄 ∈ (ℙ ∖ {2})
→ ((𝑄 − 1) / 2)
∈ ℕ) |
54 | 1, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑄 − 1) / 2) ∈
ℕ) |
55 | 5, 54 | syl5eqel 2692 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℕ) |
56 | 55 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ∈ ℕ) |
57 | 56 | nnzd 11357 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ∈ ℤ) |
58 | | prmz 15227 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℤ) |
59 | 50, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈ ℤ) |
60 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑄 ∈ ℤ → (𝑄 − 1) ∈
ℤ) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ ℤ) |
62 | 56 | nnred 10912 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ∈ ℝ) |
63 | 61 | zred 11358 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ ℝ) |
64 | | prmuz2 15246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
(ℤ≥‘2)) |
65 | 50, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∈
(ℤ≥‘2)) |
66 | | uz2m1nn 11639 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑄 ∈
(ℤ≥‘2) → (𝑄 − 1) ∈ ℕ) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈ ℕ) |
68 | 67 | nnrpd 11746 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈
ℝ+) |
69 | | rphalflt 11736 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑄 − 1) ∈
ℝ+ → ((𝑄 − 1) / 2) < (𝑄 − 1)) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑄 − 1) / 2) < (𝑄 − 1)) |
71 | 5, 70 | syl5eqbr 4618 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 < (𝑄 − 1)) |
72 | 62, 63, 71 | ltled 10064 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑁 ≤ (𝑄 − 1)) |
73 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑄 − 1) ∈
(ℤ≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ (𝑄 − 1) ∈ ℤ ∧ 𝑁 ≤ (𝑄 − 1))) |
74 | 57, 61, 72, 73 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 − 1) ∈
(ℤ≥‘𝑁)) |
75 | | fzss2 12252 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑄 − 1) ∈
(ℤ≥‘𝑁) → (1...𝑁) ⊆ (1...(𝑄 − 1))) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (1...𝑁) ⊆ (1...(𝑄 − 1))) |
77 | | simprr 792 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ (1...𝑁)) |
78 | 76, 77 | sseldd 3569 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ (1...(𝑄 − 1))) |
79 | | fzm1ndvds 14882 |
. . . . . . . . . . . . . . 15
⊢ ((𝑄 ∈ ℕ ∧ 𝑦 ∈ (1...(𝑄 − 1))) → ¬ 𝑄 ∥ 𝑦) |
80 | 52, 78, 79 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ 𝑄 ∥ 𝑦) |
81 | 4 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ≠ 𝑃) |
82 | 2 | eldifad 3552 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑃 ∈ ℙ) |
83 | 82 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℙ) |
84 | | prmrp 15262 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑄 ∈ ℙ ∧ 𝑃 ∈ ℙ) → ((𝑄 gcd 𝑃) = 1 ↔ 𝑄 ≠ 𝑃)) |
85 | 50, 83, 84 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑄 gcd 𝑃) = 1 ↔ 𝑄 ≠ 𝑃)) |
86 | 81, 85 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 gcd 𝑃) = 1) |
87 | | prmz 15227 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
88 | 83, 87 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℤ) |
89 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℤ) |
90 | 89 | ad2antll 761 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ ℤ) |
91 | | coprmdvds 15204 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑄 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑄 ∥ (𝑃 · 𝑦) ∧ (𝑄 gcd 𝑃) = 1) → 𝑄 ∥ 𝑦)) |
92 | 59, 88, 90, 91 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑄 ∥ (𝑃 · 𝑦) ∧ (𝑄 gcd 𝑃) = 1) → 𝑄 ∥ 𝑦)) |
93 | 86, 92 | mpan2d 706 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 ∥ (𝑃 · 𝑦) → 𝑄 ∥ 𝑦)) |
94 | 80, 93 | mtod 188 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ 𝑄 ∥ (𝑃 · 𝑦)) |
95 | | prmnn 15226 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
96 | 83, 95 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℕ) |
97 | 96 | nncnd 10913 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑃 ∈ ℂ) |
98 | | elfznn 12241 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ) |
99 | 98 | ad2antll 761 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ ℕ) |
100 | 99 | nncnd 10913 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑦 ∈ ℂ) |
101 | 97, 100 | mulcomd 9940 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑃 · 𝑦) = (𝑦 · 𝑃)) |
102 | 101 | breq2d 4595 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑄 ∥ (𝑃 · 𝑦) ↔ 𝑄 ∥ (𝑦 · 𝑃))) |
103 | 94, 102 | mtbid 313 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ 𝑄 ∥ (𝑦 · 𝑃)) |
104 | | elfzelz 12213 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1...𝑀) → 𝑥 ∈ ℤ) |
105 | 104 | ad2antrl 760 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑥 ∈ ℤ) |
106 | | dvdsmul2 14842 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝑄 ∈ ℤ) → 𝑄 ∥ (𝑥 · 𝑄)) |
107 | 105, 59, 106 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑄 ∥ (𝑥 · 𝑄)) |
108 | | breq2 4587 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 · 𝑄) = (𝑦 · 𝑃) → (𝑄 ∥ (𝑥 · 𝑄) ↔ 𝑄 ∥ (𝑦 · 𝑃))) |
109 | 107, 108 | syl5ibcom 234 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑥 · 𝑄) = (𝑦 · 𝑃) → 𝑄 ∥ (𝑦 · 𝑃))) |
110 | 109 | necon3bd 2796 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (¬ 𝑄 ∥ (𝑦 · 𝑃) → (𝑥 · 𝑄) ≠ (𝑦 · 𝑃))) |
111 | 103, 110 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑥 · 𝑄) ≠ (𝑦 · 𝑃)) |
112 | | elfznn 12241 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1...𝑀) → 𝑥 ∈ ℕ) |
113 | 112 | ad2antrl 760 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → 𝑥 ∈ ℕ) |
114 | 113, 52 | nnmulcld 10945 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑥 · 𝑄) ∈ ℕ) |
115 | 114 | nnred 10912 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑥 · 𝑄) ∈ ℝ) |
116 | 99, 96 | nnmulcld 10945 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑦 · 𝑃) ∈ ℕ) |
117 | 116 | nnred 10912 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → (𝑦 · 𝑃) ∈ ℝ) |
118 | 115, 117 | lttri2d 10055 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑥 · 𝑄) ≠ (𝑦 · 𝑃) ↔ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))) |
119 | 111, 118 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))) |
120 | 119 | ex 449 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) → ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))) |
121 | 120 | pm4.71rd 665 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))))) |
122 | | ancom 465 |
. . . . . . . 8
⊢ ((((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))) |
123 | 121, 122 | syl6rbb 276 |
. . . . . . 7
⊢ (𝜑 → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)))) |
124 | 123 | opabbidv 4648 |
. . . . . 6
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))}) |
125 | | unopab 4660 |
. . . . . . 7
⊢
({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}) = {〈𝑥, 𝑦〉 ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∨ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} |
126 | 35 | uneq2i 3726 |
. . . . . . 7
⊢
({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆) = ({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}) |
127 | | andi 907 |
. . . . . . . 8
⊢ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∨ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))) |
128 | 127 | opabbii 4649 |
. . . . . . 7
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = {〈𝑥, 𝑦〉 ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∨ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} |
129 | 125, 126,
128 | 3eqtr4i 2642 |
. . . . . 6
⊢
({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆) = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∨ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} |
130 | | df-xp 5044 |
. . . . . 6
⊢
((1...𝑀) ×
(1...𝑁)) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))} |
131 | 124, 129,
130 | 3eqtr4g 2669 |
. . . . 5
⊢ (𝜑 → ({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆) = ((1...𝑀) × (1...𝑁))) |
132 | 131 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (#‘({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆)) = (#‘((1...𝑀) × (1...𝑁)))) |
133 | | inopab 5174 |
. . . . . . 7
⊢
({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}) = {〈𝑥, 𝑦〉 ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∧ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} |
134 | 35 | ineq2i 3773 |
. . . . . . 7
⊢
({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = ({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}) |
135 | | anandi 867 |
. . . . . . . 8
⊢ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∧ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))) |
136 | 135 | opabbii 4649 |
. . . . . . 7
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = {〈𝑥, 𝑦〉 ∣ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃)) ∧ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} |
137 | 133, 134,
136 | 3eqtr4i 2642 |
. . . . . 6
⊢
({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} |
138 | | ltnsym2 10015 |
. . . . . . . . . . . 12
⊢ (((𝑥 · 𝑄) ∈ ℝ ∧ (𝑦 · 𝑃) ∈ ℝ) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) |
139 | 115, 117,
138 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) |
140 | 139 | ex 449 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))) |
141 | | imnan 437 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) → ¬ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ ¬ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))) |
142 | 140, 141 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → ¬ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))) |
143 | 142 | nexdv 1851 |
. . . . . . . 8
⊢ (𝜑 → ¬ ∃𝑦((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))) |
144 | 143 | nexdv 1851 |
. . . . . . 7
⊢ (𝜑 → ¬ ∃𝑥∃𝑦((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))) |
145 | | opabn0 4931 |
. . . . . . . 8
⊢
({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} ≠ ∅ ↔ ∃𝑥∃𝑦((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))) |
146 | 145 | necon1bbii 2831 |
. . . . . . 7
⊢ (¬
∃𝑥∃𝑦((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))) ↔ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = ∅) |
147 | 144, 146 | sylib 207 |
. . . . . 6
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ ((𝑥 · 𝑄) < (𝑦 · 𝑃) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))} = ∅) |
148 | 137, 147 | syl5eq 2656 |
. . . . 5
⊢ (𝜑 → ({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = ∅) |
149 | | hashun 13032 |
. . . . 5
⊢
(({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∈ Fin ∧ 𝑆 ∈ Fin ∧ ({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∩ 𝑆) = ∅) → (#‘({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆)) = ((#‘{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (#‘𝑆))) |
150 | 26, 43, 148, 149 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → (#‘({〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))} ∪ 𝑆)) = ((#‘{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (#‘𝑆))) |
151 | | hashxp 13081 |
. . . . . 6
⊢
(((1...𝑀) ∈ Fin
∧ (1...𝑁) ∈ Fin)
→ (#‘((1...𝑀)
× (1...𝑁))) =
((#‘(1...𝑀)) ·
(#‘(1...𝑁)))) |
152 | 20, 21, 151 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (#‘((1...𝑀) × (1...𝑁))) = ((#‘(1...𝑀)) · (#‘(1...𝑁)))) |
153 | | oddprm 15353 |
. . . . . . . . . 10
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
154 | 2, 153 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ) |
155 | 6, 154 | syl5eqel 2692 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℕ) |
156 | 155 | nnnn0d 11228 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
157 | | hashfz1 12996 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ (#‘(1...𝑀)) =
𝑀) |
158 | 156, 157 | syl 17 |
. . . . . 6
⊢ (𝜑 → (#‘(1...𝑀)) = 𝑀) |
159 | 55 | nnnn0d 11228 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
160 | | hashfz1 12996 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (#‘(1...𝑁)) =
𝑁) |
161 | 159, 160 | syl 17 |
. . . . . 6
⊢ (𝜑 → (#‘(1...𝑁)) = 𝑁) |
162 | 158, 161 | oveq12d 6567 |
. . . . 5
⊢ (𝜑 → ((#‘(1...𝑀)) · (#‘(1...𝑁))) = (𝑀 · 𝑁)) |
163 | 152, 162 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (#‘((1...𝑀) × (1...𝑁))) = (𝑀 · 𝑁)) |
164 | 132, 150,
163 | 3eqtr3d 2652 |
. . 3
⊢ (𝜑 → ((#‘{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (#‘𝑆)) = (𝑀 · 𝑁)) |
165 | 164 | oveq2d 6565 |
. 2
⊢ (𝜑 →
(-1↑((#‘{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑥 · 𝑄) < (𝑦 · 𝑃))}) + (#‘𝑆))) = (-1↑(𝑀 · 𝑁))) |
166 | 37, 48, 165 | 3eqtr2d 2650 |
1
⊢ (𝜑 → ((𝑃 /L 𝑄) · (𝑄 /L 𝑃)) = (-1↑(𝑀 · 𝑁))) |