Step | Hyp | Ref
| Expression |
1 | | df-nqqs 6332 |
. 2
⊢
Q = ((N × N) /
~Q ) |
2 | | breq1 3758 |
. . 3
⊢
([〈z, w〉] ~Q = A → ([〈z, w〉]
~Q <Q [〈u, v〉]
~Q ↔ A
<Q [〈u,
v〉] ~Q
)) |
3 | | eqeq1 2043 |
. . 3
⊢
([〈z, w〉] ~Q = A → ([〈z, w〉]
~Q = [〈u,
v〉] ~Q ↔
A = [〈u, v〉]
~Q )) |
4 | | breq2 3759 |
. . 3
⊢
([〈z, w〉] ~Q = A → ([〈u, v〉]
~Q <Q [〈z, w〉]
~Q ↔ [〈u, v〉]
~Q <Q A)) |
5 | 2, 3, 4 | 3orbi123d 1205 |
. 2
⊢
([〈z, w〉] ~Q = A → (([〈z, w〉]
~Q <Q [〈u, v〉]
~Q ∨ [〈z, w〉]
~Q = [〈u,
v〉] ~Q ∨ [〈u,
v〉] ~Q
<Q [〈z,
w〉] ~Q )
↔ (A <Q
[〈u, v〉] ~Q ∨ A =
[〈u, v〉] ~Q ∨ [〈u,
v〉] ~Q
<Q A))) |
6 | | breq2 3759 |
. . 3
⊢
([〈u, v〉] ~Q = B → (A
<Q [〈u,
v〉] ~Q ↔
A <Q B)) |
7 | | eqeq2 2046 |
. . 3
⊢
([〈u, v〉] ~Q = B → (A =
[〈u, v〉] ~Q ↔ A = B)) |
8 | | breq1 3758 |
. . 3
⊢
([〈u, v〉] ~Q = B → ([〈u, v〉]
~Q <Q A ↔ B
<Q A)) |
9 | 6, 7, 8 | 3orbi123d 1205 |
. 2
⊢
([〈u, v〉] ~Q = B → ((A
<Q [〈u,
v〉] ~Q ∨ A =
[〈u, v〉] ~Q ∨ [〈u,
v〉] ~Q
<Q A) ↔
(A <Q B ∨ A = B ∨ B
<Q A))) |
10 | | mulclpi 6312 |
. . . . 5
⊢
((z ∈ N ∧ v ∈ N) → (z ·N v) ∈
N) |
11 | 10 | ad2ant2rl 480 |
. . . 4
⊢
(((z ∈ N ∧ w ∈ N) ∧ (u ∈ N ∧ v ∈ N)) → (z ·N v) ∈
N) |
12 | | mulclpi 6312 |
. . . . 5
⊢
((w ∈ N ∧ u ∈ N) → (w ·N u) ∈
N) |
13 | 12 | ad2ant2lr 479 |
. . . 4
⊢
(((z ∈ N ∧ w ∈ N) ∧ (u ∈ N ∧ v ∈ N)) → (w ·N u) ∈
N) |
14 | | pitri3or 6306 |
. . . 4
⊢
(((z
·N v) ∈ N ∧ (w
·N u) ∈ N) → ((z ·N v) <N (w ·N u) ∨ (z ·N v) = (w
·N u) ∨ (w
·N u)
<N (z
·N v))) |
15 | 11, 13, 14 | syl2anc 391 |
. . 3
⊢
(((z ∈ N ∧ w ∈ N) ∧ (u ∈ N ∧ v ∈ N)) → ((z ·N v) <N (w ·N u) ∨ (z ·N v) = (w
·N u) ∨ (w
·N u)
<N (z
·N v))) |
16 | | ordpipqqs 6358 |
. . . 4
⊢
(((z ∈ N ∧ w ∈ N) ∧ (u ∈ N ∧ v ∈ N)) → ([〈z, w〉]
~Q <Q [〈u, v〉]
~Q ↔ (z
·N v)
<N (w
·N u))) |
17 | | enqeceq 6343 |
. . . 4
⊢
(((z ∈ N ∧ w ∈ N) ∧ (u ∈ N ∧ v ∈ N)) → ([〈z, w〉]
~Q = [〈u,
v〉] ~Q ↔
(z ·N
v) = (w
·N u))) |
18 | | ordpipqqs 6358 |
. . . . . 6
⊢
(((u ∈ N ∧ v ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → ([〈u, v〉]
~Q <Q [〈z, w〉]
~Q ↔ (u
·N w)
<N (v
·N z))) |
19 | 18 | ancoms 255 |
. . . . 5
⊢
(((z ∈ N ∧ w ∈ N) ∧ (u ∈ N ∧ v ∈ N)) → ([〈u, v〉]
~Q <Q [〈z, w〉]
~Q ↔ (u
·N w)
<N (v
·N z))) |
20 | | mulcompig 6315 |
. . . . . . 7
⊢
((w ∈ N ∧ u ∈ N) → (w ·N u) = (u
·N w)) |
21 | 20 | ad2ant2lr 479 |
. . . . . 6
⊢
(((z ∈ N ∧ w ∈ N) ∧ (u ∈ N ∧ v ∈ N)) → (w ·N u) = (u
·N w)) |
22 | | mulcompig 6315 |
. . . . . . 7
⊢
((z ∈ N ∧ v ∈ N) → (z ·N v) = (v
·N z)) |
23 | 22 | ad2ant2rl 480 |
. . . . . 6
⊢
(((z ∈ N ∧ w ∈ N) ∧ (u ∈ N ∧ v ∈ N)) → (z ·N v) = (v
·N z)) |
24 | 21, 23 | breq12d 3768 |
. . . . 5
⊢
(((z ∈ N ∧ w ∈ N) ∧ (u ∈ N ∧ v ∈ N)) → ((w ·N u) <N (z ·N v) ↔ (u
·N w)
<N (v
·N z))) |
25 | 19, 24 | bitr4d 180 |
. . . 4
⊢
(((z ∈ N ∧ w ∈ N) ∧ (u ∈ N ∧ v ∈ N)) → ([〈u, v〉]
~Q <Q [〈z, w〉]
~Q ↔ (w
·N u)
<N (z
·N v))) |
26 | 16, 17, 25 | 3orbi123d 1205 |
. . 3
⊢
(((z ∈ N ∧ w ∈ N) ∧ (u ∈ N ∧ v ∈ N)) → (([〈z, w〉]
~Q <Q [〈u, v〉]
~Q ∨ [〈z, w〉]
~Q = [〈u,
v〉] ~Q ∨ [〈u,
v〉] ~Q
<Q [〈z,
w〉] ~Q )
↔ ((z
·N v)
<N (w
·N u) ∨ (z
·N v) =
(w ·N
u) ∨
(w ·N
u) <N (z ·N v)))) |
27 | 15, 26 | mpbird 156 |
. 2
⊢
(((z ∈ N ∧ w ∈ N) ∧ (u ∈ N ∧ v ∈ N)) → ([〈z, w〉]
~Q <Q [〈u, v〉]
~Q ∨ [〈z, w〉]
~Q = [〈u,
v〉] ~Q ∨ [〈u,
v〉] ~Q
<Q [〈z,
w〉] ~Q
)) |
28 | 1, 5, 9, 27 | 2ecoptocl 6130 |
1
⊢
((A ∈ Q ∧ B ∈ Q) → (A <Q B ∨ A = B ∨ B
<Q A)) |