Step | Hyp | Ref
| Expression |
1 | | elq 9531 |
. . . 4
⊢ (𝑁 ∈ ℚ ↔
∃𝑧 ∈ ℤ
∃𝑤 ∈ ℕ
𝑁 = (𝑧 / 𝑤)) |
2 | 1 | biimpi 119 |
. . 3
⊢ (𝑁 ∈ ℚ →
∃𝑧 ∈ ℤ
∃𝑤 ∈ ℕ
𝑁 = (𝑧 / 𝑤)) |
3 | 2 | adantl 275 |
. 2
⊢ ((𝑀 ∈ ℚ ∧ 𝑁 ∈ ℚ) →
∃𝑧 ∈ ℤ
∃𝑤 ∈ ℕ
𝑁 = (𝑧 / 𝑤)) |
4 | | elq 9531 |
. . . . . . 7
⊢ (𝑀 ∈ ℚ ↔
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℕ
𝑀 = (𝑥 / 𝑦)) |
5 | 4 | biimpi 119 |
. . . . . 6
⊢ (𝑀 ∈ ℚ →
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℕ
𝑀 = (𝑥 / 𝑦)) |
6 | 5 | ad3antrrr 484 |
. . . . 5
⊢ ((((𝑀 ∈ ℚ ∧ 𝑁 ∈ ℚ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝑀 = (𝑥 / 𝑦)) |
7 | | simplrl 525 |
. . . . . . . . . 10
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → 𝑥 ∈ ℤ) |
8 | | simplrr 526 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ ℚ ∧ 𝑁 ∈ ℚ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) → 𝑤 ∈ ℕ) |
9 | 8 | ad2antrr 480 |
. . . . . . . . . . 11
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → 𝑤 ∈ ℕ) |
10 | 9 | nnzd 9285 |
. . . . . . . . . 10
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → 𝑤 ∈ ℤ) |
11 | 7, 10 | zmulcld 9292 |
. . . . . . . . 9
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → (𝑥 · 𝑤) ∈ ℤ) |
12 | | simplrl 525 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℚ ∧ 𝑁 ∈ ℚ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) → 𝑧 ∈ ℤ) |
13 | 12 | ad2antrr 480 |
. . . . . . . . . 10
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → 𝑧 ∈ ℤ) |
14 | | simplrr 526 |
. . . . . . . . . . 11
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → 𝑦 ∈ ℕ) |
15 | 14 | nnzd 9285 |
. . . . . . . . . 10
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → 𝑦 ∈ ℤ) |
16 | 13, 15 | zmulcld 9292 |
. . . . . . . . 9
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → (𝑧 · 𝑦) ∈ ℤ) |
17 | | ztri3or 9210 |
. . . . . . . . 9
⊢ (((𝑥 · 𝑤) ∈ ℤ ∧ (𝑧 · 𝑦) ∈ ℤ) → ((𝑥 · 𝑤) < (𝑧 · 𝑦) ∨ (𝑥 · 𝑤) = (𝑧 · 𝑦) ∨ (𝑧 · 𝑦) < (𝑥 · 𝑤))) |
18 | 11, 16, 17 | syl2anc 409 |
. . . . . . . 8
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → ((𝑥 · 𝑤) < (𝑧 · 𝑦) ∨ (𝑥 · 𝑤) = (𝑧 · 𝑦) ∨ (𝑧 · 𝑦) < (𝑥 · 𝑤))) |
19 | | simpllr 524 |
. . . . . . . . . . 11
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → 𝑁 = (𝑧 / 𝑤)) |
20 | 19 | breq2d 3977 |
. . . . . . . . . 10
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → ((𝑥 / 𝑦) < 𝑁 ↔ (𝑥 / 𝑦) < (𝑧 / 𝑤))) |
21 | | breq1 3968 |
. . . . . . . . . . 11
⊢ (𝑀 = (𝑥 / 𝑦) → (𝑀 < 𝑁 ↔ (𝑥 / 𝑦) < 𝑁)) |
22 | 21 | adantl 275 |
. . . . . . . . . 10
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → (𝑀 < 𝑁 ↔ (𝑥 / 𝑦) < 𝑁)) |
23 | 7 | zred 9286 |
. . . . . . . . . . 11
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → 𝑥 ∈ ℝ) |
24 | 9 | nnrpd 9601 |
. . . . . . . . . . 11
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → 𝑤 ∈ ℝ+) |
25 | 13 | zred 9286 |
. . . . . . . . . . 11
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → 𝑧 ∈ ℝ) |
26 | 14 | nnrpd 9601 |
. . . . . . . . . . 11
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → 𝑦 ∈ ℝ+) |
27 | 23, 24, 25, 26 | lt2mul2divd 9672 |
. . . . . . . . . 10
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → ((𝑥 · 𝑤) < (𝑧 · 𝑦) ↔ (𝑥 / 𝑦) < (𝑧 / 𝑤))) |
28 | 20, 22, 27 | 3bitr4rd 220 |
. . . . . . . . 9
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → ((𝑥 · 𝑤) < (𝑧 · 𝑦) ↔ 𝑀 < 𝑁)) |
29 | | simpr 109 |
. . . . . . . . . . 11
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → 𝑀 = (𝑥 / 𝑦)) |
30 | 29, 19 | eqeq12d 2172 |
. . . . . . . . . 10
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → (𝑀 = 𝑁 ↔ (𝑥 / 𝑦) = (𝑧 / 𝑤))) |
31 | 7 | zcnd 9287 |
. . . . . . . . . . 11
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → 𝑥 ∈ ℂ) |
32 | 13 | zcnd 9287 |
. . . . . . . . . . 11
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → 𝑧 ∈ ℂ) |
33 | 14 | nncnd 8847 |
. . . . . . . . . . . 12
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → 𝑦 ∈ ℂ) |
34 | 14 | nnap0d 8879 |
. . . . . . . . . . . 12
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → 𝑦 # 0) |
35 | 33, 34 | jca 304 |
. . . . . . . . . . 11
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → (𝑦 ∈ ℂ ∧ 𝑦 # 0)) |
36 | 9 | nncnd 8847 |
. . . . . . . . . . . 12
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → 𝑤 ∈ ℂ) |
37 | 9 | nnap0d 8879 |
. . . . . . . . . . . 12
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → 𝑤 # 0) |
38 | 36, 37 | jca 304 |
. . . . . . . . . . 11
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → (𝑤 ∈ ℂ ∧ 𝑤 # 0)) |
39 | | divmuleqap 8590 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) ∧ ((𝑦 ∈ ℂ ∧ 𝑦 # 0) ∧ (𝑤 ∈ ℂ ∧ 𝑤 # 0))) → ((𝑥 / 𝑦) = (𝑧 / 𝑤) ↔ (𝑥 · 𝑤) = (𝑧 · 𝑦))) |
40 | 31, 32, 35, 38, 39 | syl22anc 1221 |
. . . . . . . . . 10
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → ((𝑥 / 𝑦) = (𝑧 / 𝑤) ↔ (𝑥 · 𝑤) = (𝑧 · 𝑦))) |
41 | 30, 40 | bitr2d 188 |
. . . . . . . . 9
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → ((𝑥 · 𝑤) = (𝑧 · 𝑦) ↔ 𝑀 = 𝑁)) |
42 | 25, 26, 23, 24 | lt2mul2divd 9672 |
. . . . . . . . . 10
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → ((𝑧 · 𝑦) < (𝑥 · 𝑤) ↔ (𝑧 / 𝑤) < (𝑥 / 𝑦))) |
43 | 19, 29 | breq12d 3978 |
. . . . . . . . . 10
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → (𝑁 < 𝑀 ↔ (𝑧 / 𝑤) < (𝑥 / 𝑦))) |
44 | 42, 43 | bitr4d 190 |
. . . . . . . . 9
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → ((𝑧 · 𝑦) < (𝑥 · 𝑤) ↔ 𝑁 < 𝑀)) |
45 | 28, 41, 44 | 3orbi123d 1293 |
. . . . . . . 8
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → (((𝑥 · 𝑤) < (𝑧 · 𝑦) ∨ (𝑥 · 𝑤) = (𝑧 · 𝑦) ∨ (𝑧 · 𝑦) < (𝑥 · 𝑤)) ↔ (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀))) |
46 | 18, 45 | mpbid 146 |
. . . . . . 7
⊢
((((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑀 = (𝑥 / 𝑦)) → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀)) |
47 | 46 | ex 114 |
. . . . . 6
⊢
(((((𝑀 ∈
ℚ ∧ 𝑁 ∈
ℚ) ∧ (𝑧 ∈
ℤ ∧ 𝑤 ∈
ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝑀 = (𝑥 / 𝑦) → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀))) |
48 | 47 | rexlimdvva 2582 |
. . . . 5
⊢ ((((𝑀 ∈ ℚ ∧ 𝑁 ∈ ℚ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝑀 = (𝑥 / 𝑦) → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀))) |
49 | 6, 48 | mpd 13 |
. . . 4
⊢ ((((𝑀 ∈ ℚ ∧ 𝑁 ∈ ℚ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) ∧ 𝑁 = (𝑧 / 𝑤)) → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀)) |
50 | 49 | ex 114 |
. . 3
⊢ (((𝑀 ∈ ℚ ∧ 𝑁 ∈ ℚ) ∧ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ)) → (𝑁 = (𝑧 / 𝑤) → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀))) |
51 | 50 | rexlimdvva 2582 |
. 2
⊢ ((𝑀 ∈ ℚ ∧ 𝑁 ∈ ℚ) →
(∃𝑧 ∈ ℤ
∃𝑤 ∈ ℕ
𝑁 = (𝑧 / 𝑤) → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀))) |
52 | 3, 51 | mpd 13 |
1
⊢ ((𝑀 ∈ ℚ ∧ 𝑁 ∈ ℚ) → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀)) |