Step | Hyp | Ref
| Expression |
1 | | df-nqqs 7297 |
. 2
⊢
Q = ((N × N) /
~Q ) |
2 | | breq1 3990 |
. . 3
⊢
([〈𝑧, 𝑤〉]
~Q = 𝐴 → ([〈𝑧, 𝑤〉] ~Q
<Q [〈𝑢, 𝑣〉] ~Q ↔
𝐴
<Q [〈𝑢, 𝑣〉] ~Q
)) |
3 | | eqeq1 2177 |
. . 3
⊢
([〈𝑧, 𝑤〉]
~Q = 𝐴 → ([〈𝑧, 𝑤〉] ~Q =
[〈𝑢, 𝑣〉]
~Q ↔ 𝐴 = [〈𝑢, 𝑣〉] ~Q
)) |
4 | | breq2 3991 |
. . 3
⊢
([〈𝑧, 𝑤〉]
~Q = 𝐴 → ([〈𝑢, 𝑣〉] ~Q
<Q [〈𝑧, 𝑤〉] ~Q ↔
[〈𝑢, 𝑣〉]
~Q <Q 𝐴)) |
5 | 2, 3, 4 | 3orbi123d 1306 |
. 2
⊢
([〈𝑧, 𝑤〉]
~Q = 𝐴 → (([〈𝑧, 𝑤〉] ~Q
<Q [〈𝑢, 𝑣〉] ~Q ∨
[〈𝑧, 𝑤〉]
~Q = [〈𝑢, 𝑣〉] ~Q ∨
[〈𝑢, 𝑣〉]
~Q <Q [〈𝑧, 𝑤〉] ~Q ) ↔
(𝐴
<Q [〈𝑢, 𝑣〉] ~Q ∨
𝐴 = [〈𝑢, 𝑣〉] ~Q ∨
[〈𝑢, 𝑣〉]
~Q <Q 𝐴))) |
6 | | breq2 3991 |
. . 3
⊢
([〈𝑢, 𝑣〉]
~Q = 𝐵 → (𝐴 <Q [〈𝑢, 𝑣〉] ~Q ↔
𝐴
<Q 𝐵)) |
7 | | eqeq2 2180 |
. . 3
⊢
([〈𝑢, 𝑣〉]
~Q = 𝐵 → (𝐴 = [〈𝑢, 𝑣〉] ~Q ↔
𝐴 = 𝐵)) |
8 | | breq1 3990 |
. . 3
⊢
([〈𝑢, 𝑣〉]
~Q = 𝐵 → ([〈𝑢, 𝑣〉] ~Q
<Q 𝐴 ↔ 𝐵 <Q 𝐴)) |
9 | 6, 7, 8 | 3orbi123d 1306 |
. 2
⊢
([〈𝑢, 𝑣〉]
~Q = 𝐵 → ((𝐴 <Q [〈𝑢, 𝑣〉] ~Q ∨
𝐴 = [〈𝑢, 𝑣〉] ~Q ∨
[〈𝑢, 𝑣〉]
~Q <Q 𝐴) ↔ (𝐴 <Q 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 <Q 𝐴))) |
10 | | mulclpi 7277 |
. . . . 5
⊢ ((𝑧 ∈ N ∧
𝑣 ∈ N)
→ (𝑧
·N 𝑣) ∈ N) |
11 | 10 | ad2ant2rl 508 |
. . . 4
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑢 ∈
N ∧ 𝑣
∈ N)) → (𝑧 ·N 𝑣) ∈
N) |
12 | | mulclpi 7277 |
. . . . 5
⊢ ((𝑤 ∈ N ∧
𝑢 ∈ N)
→ (𝑤
·N 𝑢) ∈ N) |
13 | 12 | ad2ant2lr 507 |
. . . 4
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑢 ∈
N ∧ 𝑣
∈ N)) → (𝑤 ·N 𝑢) ∈
N) |
14 | | pitri3or 7271 |
. . . 4
⊢ (((𝑧
·N 𝑣) ∈ N ∧ (𝑤
·N 𝑢) ∈ N) → ((𝑧
·N 𝑣) <N (𝑤
·N 𝑢) ∨ (𝑧 ·N 𝑣) = (𝑤 ·N 𝑢) ∨ (𝑤 ·N 𝑢) <N
(𝑧
·N 𝑣))) |
15 | 11, 13, 14 | syl2anc 409 |
. . 3
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑢 ∈
N ∧ 𝑣
∈ N)) → ((𝑧 ·N 𝑣) <N
(𝑤
·N 𝑢) ∨ (𝑧 ·N 𝑣) = (𝑤 ·N 𝑢) ∨ (𝑤 ·N 𝑢) <N
(𝑧
·N 𝑣))) |
16 | | ordpipqqs 7323 |
. . . 4
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑢 ∈
N ∧ 𝑣
∈ N)) → ([〈𝑧, 𝑤〉] ~Q
<Q [〈𝑢, 𝑣〉] ~Q ↔
(𝑧
·N 𝑣) <N (𝑤
·N 𝑢))) |
17 | | enqeceq 7308 |
. . . 4
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑢 ∈
N ∧ 𝑣
∈ N)) → ([〈𝑧, 𝑤〉] ~Q =
[〈𝑢, 𝑣〉]
~Q ↔ (𝑧 ·N 𝑣) = (𝑤 ·N 𝑢))) |
18 | | ordpipqqs 7323 |
. . . . . 6
⊢ (((𝑢 ∈ N ∧
𝑣 ∈ N)
∧ (𝑧 ∈
N ∧ 𝑤
∈ N)) → ([〈𝑢, 𝑣〉] ~Q
<Q [〈𝑧, 𝑤〉] ~Q ↔
(𝑢
·N 𝑤) <N (𝑣
·N 𝑧))) |
19 | 18 | ancoms 266 |
. . . . 5
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑢 ∈
N ∧ 𝑣
∈ N)) → ([〈𝑢, 𝑣〉] ~Q
<Q [〈𝑧, 𝑤〉] ~Q ↔
(𝑢
·N 𝑤) <N (𝑣
·N 𝑧))) |
20 | | mulcompig 7280 |
. . . . . . 7
⊢ ((𝑤 ∈ N ∧
𝑢 ∈ N)
→ (𝑤
·N 𝑢) = (𝑢 ·N 𝑤)) |
21 | 20 | ad2ant2lr 507 |
. . . . . 6
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑢 ∈
N ∧ 𝑣
∈ N)) → (𝑤 ·N 𝑢) = (𝑢 ·N 𝑤)) |
22 | | mulcompig 7280 |
. . . . . . 7
⊢ ((𝑧 ∈ N ∧
𝑣 ∈ N)
→ (𝑧
·N 𝑣) = (𝑣 ·N 𝑧)) |
23 | 22 | ad2ant2rl 508 |
. . . . . 6
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑢 ∈
N ∧ 𝑣
∈ N)) → (𝑧 ·N 𝑣) = (𝑣 ·N 𝑧)) |
24 | 21, 23 | breq12d 4000 |
. . . . 5
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑢 ∈
N ∧ 𝑣
∈ N)) → ((𝑤 ·N 𝑢) <N
(𝑧
·N 𝑣) ↔ (𝑢 ·N 𝑤) <N
(𝑣
·N 𝑧))) |
25 | 19, 24 | bitr4d 190 |
. . . 4
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑢 ∈
N ∧ 𝑣
∈ N)) → ([〈𝑢, 𝑣〉] ~Q
<Q [〈𝑧, 𝑤〉] ~Q ↔
(𝑤
·N 𝑢) <N (𝑧
·N 𝑣))) |
26 | 16, 17, 25 | 3orbi123d 1306 |
. . 3
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑢 ∈
N ∧ 𝑣
∈ N)) → (([〈𝑧, 𝑤〉] ~Q
<Q [〈𝑢, 𝑣〉] ~Q ∨
[〈𝑧, 𝑤〉]
~Q = [〈𝑢, 𝑣〉] ~Q ∨
[〈𝑢, 𝑣〉]
~Q <Q [〈𝑧, 𝑤〉] ~Q ) ↔
((𝑧
·N 𝑣) <N (𝑤
·N 𝑢) ∨ (𝑧 ·N 𝑣) = (𝑤 ·N 𝑢) ∨ (𝑤 ·N 𝑢) <N
(𝑧
·N 𝑣)))) |
27 | 15, 26 | mpbird 166 |
. 2
⊢ (((𝑧 ∈ N ∧
𝑤 ∈ N)
∧ (𝑢 ∈
N ∧ 𝑣
∈ N)) → ([〈𝑧, 𝑤〉] ~Q
<Q [〈𝑢, 𝑣〉] ~Q ∨
[〈𝑧, 𝑤〉]
~Q = [〈𝑢, 𝑣〉] ~Q ∨
[〈𝑢, 𝑣〉]
~Q <Q [〈𝑧, 𝑤〉] ~Q
)) |
28 | 1, 5, 9, 27 | 2ecoptocl 6597 |
1
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
<Q 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 <Q 𝐴)) |