Step | Hyp | Ref
| Expression |
1 | | enqex 6344 |
. 2
⊢
~Q ∈
V |
2 | | enqer 6342 |
. 2
⊢
~Q Er (N ×
N) |
3 | | df-nqqs 6332 |
. 2
⊢
Q = ((N × N) /
~Q ) |
4 | | df-ltnqqs 6337 |
. 2
⊢
<Q = {〈x,
y〉 ∣ ((x ∈
Q ∧ y ∈
Q) ∧ ∃z∃w∃v∃u((x = [〈z,
w〉] ~Q ∧ y =
[〈v, u〉] ~Q ) ∧ (z
·N u)
<N (w
·N v)))} |
5 | | enqeceq 6343 |
. . . . 5
⊢
(((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) → ([〈z, w〉]
~Q = [〈A,
B〉] ~Q ↔
(z ·N
B) = (w
·N A))) |
6 | | enqeceq 6343 |
. . . . . 6
⊢
(((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N)) → ([〈v,
u〉] ~Q =
[〈𝐶, 𝐷〉] ~Q ↔
(v ·N 𝐷) = (u ·N 𝐶))) |
7 | | eqcom 2039 |
. . . . . 6
⊢
((v
·N 𝐷) = (u
·N 𝐶) ↔ (u ·N 𝐶) = (v ·N 𝐷)) |
8 | 6, 7 | syl6bb 185 |
. . . . 5
⊢
(((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N)) → ([〈v,
u〉] ~Q =
[〈𝐶, 𝐷〉] ~Q ↔
(u ·N 𝐶) = (v ·N 𝐷))) |
9 | 5, 8 | bi2anan9 538 |
. . . 4
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → (([〈z,
w〉] ~Q =
[〈A, B〉] ~Q ∧ [〈v,
u〉] ~Q =
[〈𝐶, 𝐷〉] ~Q ) ↔
((z ·N
B) = (w
·N A) ∧ (u
·N 𝐶) = (v
·N 𝐷)))) |
10 | | oveq12 5464 |
. . . . 5
⊢
(((z
·N B) =
(w ·N
A) ∧
(u ·N 𝐶) = (v ·N 𝐷)) → ((z ·N B) ·N (u ·N 𝐶)) = ((w ·N A) ·N (v ·N 𝐷))) |
11 | | simplll 485 |
. . . . . . 7
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → z ∈ N) |
12 | | simprlr 490 |
. . . . . . 7
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → u ∈ N) |
13 | | simplrr 488 |
. . . . . . 7
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → B ∈ N) |
14 | | mulcompig 6315 |
. . . . . . . 8
⊢
((x ∈ N ∧ y ∈ N) → (x ·N y) = (y
·N x)) |
15 | 14 | adantl 262 |
. . . . . . 7
⊢
(((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) ∧ (x ∈
N ∧ y ∈
N)) → (x
·N y) =
(y ·N
x)) |
16 | | mulasspig 6316 |
. . . . . . . 8
⊢
((x ∈ N ∧ y ∈ N ∧ f ∈ N) → ((x ·N y) ·N f) = (x
·N (y
·N f))) |
17 | 16 | adantl 262 |
. . . . . . 7
⊢
(((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) ∧ (x ∈
N ∧ y ∈
N ∧ f ∈
N)) → ((x
·N y)
·N f) =
(x ·N
(y ·N
f))) |
18 | | simprrl 491 |
. . . . . . 7
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → 𝐶
∈ N) |
19 | | mulclpi 6312 |
. . . . . . . 8
⊢
((x ∈ N ∧ y ∈ N) → (x ·N y) ∈
N) |
20 | 19 | adantl 262 |
. . . . . . 7
⊢
(((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) ∧ (x ∈
N ∧ y ∈
N)) → (x
·N y) ∈ N) |
21 | 11, 12, 13, 15, 17, 18, 20 | caov4d 5627 |
. . . . . 6
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → ((z
·N u)
·N (B
·N 𝐶)) = ((z
·N B)
·N (u
·N 𝐶))) |
22 | | simpllr 486 |
. . . . . . 7
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → w ∈ N) |
23 | | simprll 489 |
. . . . . . 7
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → v ∈ N) |
24 | | simplrl 487 |
. . . . . . 7
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → A ∈ N) |
25 | | simprrr 492 |
. . . . . . 7
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → 𝐷
∈ N) |
26 | 22, 23, 24, 15, 17, 25, 20 | caov4d 5627 |
. . . . . 6
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → ((w
·N v)
·N (A
·N 𝐷)) = ((w
·N A)
·N (v
·N 𝐷))) |
27 | 21, 26 | eqeq12d 2051 |
. . . . 5
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → (((z
·N u)
·N (B
·N 𝐶)) = ((w
·N v)
·N (A
·N 𝐷)) ↔ ((z ·N B) ·N (u ·N 𝐶)) = ((w ·N A) ·N (v ·N 𝐷)))) |
28 | 10, 27 | syl5ibr 145 |
. . . 4
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → (((z
·N B) =
(w ·N
A) ∧
(u ·N 𝐶) = (v ·N 𝐷)) → ((z ·N u) ·N (B ·N 𝐶)) = ((w ·N v) ·N (A ·N 𝐷)))) |
29 | 9, 28 | sylbid 139 |
. . 3
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → (([〈z,
w〉] ~Q =
[〈A, B〉] ~Q ∧ [〈v,
u〉] ~Q =
[〈𝐶, 𝐷〉] ~Q ) →
((z ·N
u) ·N
(B ·N 𝐶)) = ((w ·N v) ·N (A ·N 𝐷)))) |
30 | | ltmpig 6323 |
. . . . 5
⊢
((x ∈ N ∧ y ∈ N ∧ f ∈ N) → (x <N y ↔ (f
·N x)
<N (f
·N y))) |
31 | 30 | adantl 262 |
. . . 4
⊢
(((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) ∧ (x ∈
N ∧ y ∈
N ∧ f ∈
N)) → (x
<N y ↔
(f ·N
x) <N (f ·N y))) |
32 | 20, 11, 12 | caovcld 5596 |
. . . 4
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → (z
·N u) ∈ N) |
33 | 20, 13, 18 | caovcld 5596 |
. . . 4
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → (B
·N 𝐶) ∈
N) |
34 | 20, 22, 23 | caovcld 5596 |
. . . 4
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → (w
·N v) ∈ N) |
35 | 20, 24, 25 | caovcld 5596 |
. . . 4
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → (A
·N 𝐷) ∈
N) |
36 | 31, 32, 33, 34, 15, 35 | caovord3d 5613 |
. . 3
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → (((z
·N u)
·N (B
·N 𝐶)) = ((w
·N v)
·N (A
·N 𝐷)) → ((z ·N u) <N (w ·N v) ↔ (A
·N 𝐷) <N (B ·N 𝐶)))) |
37 | 29, 36 | syld 40 |
. 2
⊢
((((z ∈ N ∧ w ∈ N) ∧ (A ∈ N ∧ B ∈ N)) ∧ ((v ∈ N ∧ u ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N))) → (([〈z,
w〉] ~Q =
[〈A, B〉] ~Q ∧ [〈v,
u〉] ~Q =
[〈𝐶, 𝐷〉] ~Q ) →
((z ·N
u) <N (w ·N v) ↔ (A
·N 𝐷) <N (B ·N 𝐶)))) |
38 | 1, 2, 3, 4, 37 | brecop 6132 |
1
⊢
(((A ∈ N ∧ B ∈ N) ∧ (𝐶 ∈
N ∧ 𝐷 ∈
N)) → ([〈A,
B〉] ~Q
<Q [〈𝐶, 𝐷〉] ~Q ↔
(A ·N 𝐷) <N
(B ·N 𝐶))) |