Step | Hyp | Ref
| Expression |
1 | | df-nqqs 6332 |
. 2
⊢
Q = ((N × N) /
~Q ) |
2 | | breq1 3758 |
. . 3
⊢
([〈x, y〉] ~Q = A → ([〈x, y〉]
~Q <Q [〈z, w〉]
~Q ↔ A
<Q [〈z,
w〉] ~Q
)) |
3 | | oveq2 5463 |
. . . 4
⊢
([〈x, y〉] ~Q = A → ([〈v, u〉]
~Q ·Q [〈x, y〉]
~Q ) = ([〈v,
u〉] ~Q
·Q A)) |
4 | 3 | breq1d 3765 |
. . 3
⊢
([〈x, y〉] ~Q = A → (([〈v, u〉]
~Q ·Q [〈x, y〉]
~Q ) <Q ([〈v, u〉]
~Q ·Q [〈z, w〉]
~Q ) ↔ ([〈v, u〉]
~Q ·Q A) <Q ([〈v, u〉]
~Q ·Q [〈z, w〉]
~Q ))) |
5 | 2, 4 | bibi12d 224 |
. 2
⊢
([〈x, y〉] ~Q = A → (([〈x, y〉]
~Q <Q [〈z, w〉]
~Q ↔ ([〈v, u〉]
~Q ·Q [〈x, y〉]
~Q ) <Q ([〈v, u〉]
~Q ·Q [〈z, w〉]
~Q )) ↔ (A
<Q [〈z,
w〉] ~Q ↔
([〈v, u〉] ~Q
·Q A)
<Q ([〈v,
u〉] ~Q
·Q [〈z, w〉]
~Q )))) |
6 | | breq2 3759 |
. . 3
⊢
([〈z, w〉] ~Q = B → (A
<Q [〈z,
w〉] ~Q ↔
A <Q B)) |
7 | | oveq2 5463 |
. . . 4
⊢
([〈z, w〉] ~Q = B → ([〈v, u〉]
~Q ·Q [〈z, w〉]
~Q ) = ([〈v,
u〉] ~Q
·Q B)) |
8 | 7 | breq2d 3767 |
. . 3
⊢
([〈z, w〉] ~Q = B → (([〈v, u〉]
~Q ·Q A) <Q ([〈v, u〉]
~Q ·Q [〈z, w〉]
~Q ) ↔ ([〈v, u〉]
~Q ·Q A) <Q ([〈v, u〉]
~Q ·Q B))) |
9 | 6, 8 | bibi12d 224 |
. 2
⊢
([〈z, w〉] ~Q = B → ((A
<Q [〈z,
w〉] ~Q ↔
([〈v, u〉] ~Q
·Q A)
<Q ([〈v,
u〉] ~Q
·Q [〈z, w〉]
~Q )) ↔ (A
<Q B ↔
([〈v, u〉] ~Q
·Q A)
<Q ([〈v,
u〉] ~Q
·Q B)))) |
10 | | oveq1 5462 |
. . . 4
⊢
([〈v, u〉] ~Q = 𝐶 → ([〈v, u〉]
~Q ·Q A) = (𝐶 ·Q A)) |
11 | | oveq1 5462 |
. . . 4
⊢
([〈v, u〉] ~Q = 𝐶 → ([〈v, u〉]
~Q ·Q B) = (𝐶 ·Q B)) |
12 | 10, 11 | breq12d 3768 |
. . 3
⊢
([〈v, u〉] ~Q = 𝐶 → (([〈v, u〉]
~Q ·Q A) <Q ([〈v, u〉]
~Q ·Q B) ↔ (𝐶 ·Q A) <Q (𝐶 ·Q B))) |
13 | 12 | bibi2d 221 |
. 2
⊢
([〈v, u〉] ~Q = 𝐶 → ((A <Q B ↔ ([〈v, u〉]
~Q ·Q A) <Q ([〈v, u〉]
~Q ·Q B)) ↔ (A
<Q B ↔
(𝐶
·Q A)
<Q (𝐶 ·Q B)))) |
14 | | mulclpi 6312 |
. . . . . . . 8
⊢
((f ∈ N ∧ g ∈ N) → (f ·N g) ∈
N) |
15 | 14 | adantl 262 |
. . . . . . 7
⊢
((((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) ∧ (f ∈ N ∧ g ∈ N)) → (f ·N g) ∈
N) |
16 | | simp1l 927 |
. . . . . . 7
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → x ∈
N) |
17 | | simp2r 930 |
. . . . . . 7
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → w ∈
N) |
18 | 15, 16, 17 | caovcld 5596 |
. . . . . 6
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (x ·N w) ∈
N) |
19 | | simp1r 928 |
. . . . . . 7
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → y ∈
N) |
20 | | simp2l 929 |
. . . . . . 7
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → z ∈
N) |
21 | 15, 19, 20 | caovcld 5596 |
. . . . . 6
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (y ·N z) ∈
N) |
22 | | mulclpi 6312 |
. . . . . . 7
⊢
((v ∈ N ∧ u ∈ N) → (v ·N u) ∈
N) |
23 | 22 | 3ad2ant3 926 |
. . . . . 6
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (v ·N u) ∈
N) |
24 | | ltmpig 6323 |
. . . . . 6
⊢
(((x
·N w) ∈ N ∧ (y
·N z) ∈ N ∧ (v
·N u) ∈ N) → ((x ·N w) <N (y ·N z) ↔ ((v
·N u)
·N (x
·N w))
<N ((v
·N u)
·N (y
·N z)))) |
25 | 18, 21, 23, 24 | syl3anc 1134 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ((x ·N w) <N (y ·N z) ↔ ((v
·N u)
·N (x
·N w))
<N ((v
·N u)
·N (y
·N z)))) |
26 | | simp3l 931 |
. . . . . . 7
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → v ∈
N) |
27 | | simp3r 932 |
. . . . . . 7
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → u ∈
N) |
28 | | mulcompig 6315 |
. . . . . . . 8
⊢
((f ∈ N ∧ g ∈ N) → (f ·N g) = (g
·N f)) |
29 | 28 | adantl 262 |
. . . . . . 7
⊢
((((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) ∧ (f ∈ N ∧ g ∈ N)) → (f ·N g) = (g
·N f)) |
30 | | mulasspig 6316 |
. . . . . . . 8
⊢
((f ∈ N ∧ g ∈ N ∧ ℎ
∈ N) → ((f ·N g) ·N ℎ) = (f ·N (g ·N ℎ))) |
31 | 30 | adantl 262 |
. . . . . . 7
⊢
((((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) ∧ (f ∈ N ∧ g ∈ N ∧ ℎ
∈ N)) → ((f ·N g) ·N ℎ) = (f ·N (g ·N ℎ))) |
32 | 26, 16, 27, 29, 31, 17, 15 | caov4d 5627 |
. . . . . 6
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ((v ·N x) ·N (u ·N w)) = ((v
·N u)
·N (x
·N w))) |
33 | 27, 19, 26, 29, 31, 20, 15 | caov4d 5627 |
. . . . . . 7
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ((u ·N y) ·N (v ·N z)) = ((u
·N v)
·N (y
·N z))) |
34 | | mulcompig 6315 |
. . . . . . . . . 10
⊢
((u ∈ N ∧ v ∈ N) → (u ·N v) = (v
·N u)) |
35 | 34 | oveq1d 5470 |
. . . . . . . . 9
⊢
((u ∈ N ∧ v ∈ N) → ((u ·N v) ·N (y ·N z)) = ((v
·N u)
·N (y
·N z))) |
36 | 35 | ancoms 255 |
. . . . . . . 8
⊢
((v ∈ N ∧ u ∈ N) → ((u ·N v) ·N (y ·N z)) = ((v
·N u)
·N (y
·N z))) |
37 | 36 | 3ad2ant3 926 |
. . . . . . 7
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ((u ·N v) ·N (y ·N z)) = ((v
·N u)
·N (y
·N z))) |
38 | 33, 37 | eqtrd 2069 |
. . . . . 6
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ((u ·N y) ·N (v ·N z)) = ((v
·N u)
·N (y
·N z))) |
39 | 32, 38 | breq12d 3768 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (((v ·N x) ·N (u ·N w)) <N ((u ·N y) ·N (v ·N z)) ↔ ((v
·N u)
·N (x
·N w))
<N ((v
·N u)
·N (y
·N z)))) |
40 | 25, 39 | bitr4d 180 |
. . . 4
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ((x ·N w) <N (y ·N z) ↔ ((v
·N x)
·N (u
·N w))
<N ((u
·N y)
·N (v
·N z)))) |
41 | | ordpipqqs 6358 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → ([〈x, y〉]
~Q <Q [〈z, w〉]
~Q ↔ (x
·N w)
<N (y
·N z))) |
42 | 41 | 3adant3 923 |
. . . 4
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ([〈x, y〉]
~Q <Q [〈z, w〉]
~Q ↔ (x
·N w)
<N (y
·N z))) |
43 | 15, 26, 16 | caovcld 5596 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (v ·N x) ∈
N) |
44 | 15, 27, 19 | caovcld 5596 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (u ·N y) ∈
N) |
45 | 15, 26, 20 | caovcld 5596 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (v ·N z) ∈
N) |
46 | 15, 27, 17 | caovcld 5596 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (u ·N w) ∈
N) |
47 | | ordpipqqs 6358 |
. . . . 5
⊢
((((v
·N x) ∈ N ∧ (u
·N y) ∈ N) ∧ ((v
·N z) ∈ N ∧ (u
·N w) ∈ N)) → ([〈(v ·N x), (u
·N y)〉] ~Q
<Q [〈(v
·N z),
(u ·N
w)〉] ~Q
↔ ((v
·N x)
·N (u
·N w))
<N ((u
·N y)
·N (v
·N z)))) |
48 | 43, 44, 45, 46, 47 | syl22anc 1135 |
. . . 4
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ([〈(v ·N x), (u
·N y)〉] ~Q
<Q [〈(v
·N z),
(u ·N
w)〉] ~Q
↔ ((v
·N x)
·N (u
·N w))
<N ((u
·N y)
·N (v
·N z)))) |
49 | 40, 42, 48 | 3bitr4d 209 |
. . 3
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ([〈x, y〉]
~Q <Q [〈z, w〉]
~Q ↔ [〈(v ·N x), (u
·N y)〉] ~Q
<Q [〈(v
·N z),
(u ·N
w)〉] ~Q
)) |
50 | | mulpipqqs 6357 |
. . . . . 6
⊢
(((v ∈ N ∧ u ∈ N) ∧ (x ∈ N ∧ y ∈ N)) → ([〈v, u〉]
~Q ·Q [〈x, y〉]
~Q ) = [〈(v
·N x),
(u ·N
y)〉] ~Q
) |
51 | 50 | ancoms 255 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ([〈v, u〉]
~Q ·Q [〈x, y〉]
~Q ) = [〈(v
·N x),
(u ·N
y)〉] ~Q
) |
52 | 51 | 3adant2 922 |
. . . 4
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ([〈v, u〉]
~Q ·Q [〈x, y〉]
~Q ) = [〈(v
·N x),
(u ·N
y)〉] ~Q
) |
53 | | mulpipqqs 6357 |
. . . . . 6
⊢
(((v ∈ N ∧ u ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → ([〈v, u〉]
~Q ·Q [〈z, w〉]
~Q ) = [〈(v
·N z),
(u ·N
w)〉] ~Q
) |
54 | 53 | ancoms 255 |
. . . . 5
⊢
(((z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ([〈v, u〉]
~Q ·Q [〈z, w〉]
~Q ) = [〈(v
·N z),
(u ·N
w)〉] ~Q
) |
55 | 54 | 3adant1 921 |
. . . 4
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ([〈v, u〉]
~Q ·Q [〈z, w〉]
~Q ) = [〈(v
·N z),
(u ·N
w)〉] ~Q
) |
56 | 52, 55 | breq12d 3768 |
. . 3
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (([〈v, u〉]
~Q ·Q [〈x, y〉]
~Q ) <Q ([〈v, u〉]
~Q ·Q [〈z, w〉]
~Q ) ↔ [〈(v ·N x), (u
·N y)〉] ~Q
<Q [〈(v
·N z),
(u ·N
w)〉] ~Q
)) |
57 | 49, 56 | bitr4d 180 |
. 2
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ([〈x, y〉]
~Q <Q [〈z, w〉]
~Q ↔ ([〈v, u〉]
~Q ·Q [〈x, y〉]
~Q ) <Q ([〈v, u〉]
~Q ·Q [〈z, w〉]
~Q ))) |
58 | 1, 5, 9, 13, 57 | 3ecoptocl 6131 |
1
⊢
((A ∈ Q ∧ B ∈ Q ∧ 𝐶 ∈
Q) → (A
<Q B ↔
(𝐶
·Q A)
<Q (𝐶 ·Q B))) |