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 | | addclpi 6311 |
. . . . . 6
⊢
((f ∈ N ∧ g ∈ N) → (f +N g) ∈
N) |
15 | 14 | adantl 262 |
. . . . 5
⊢
((((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) ∧ (f ∈ N ∧ g ∈ N)) → (f +N g) ∈
N) |
16 | | simp3l 931 |
. . . . . 6
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → v ∈
N) |
17 | | simp1r 928 |
. . . . . 6
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → y ∈
N) |
18 | | mulclpi 6312 |
. . . . . 6
⊢
((v ∈ N ∧ y ∈ N) → (v ·N y) ∈
N) |
19 | 16, 17, 18 | syl2anc 391 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (v ·N y) ∈
N) |
20 | | simp3r 932 |
. . . . . 6
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → u ∈
N) |
21 | | simp1l 927 |
. . . . . 6
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → x ∈
N) |
22 | | mulclpi 6312 |
. . . . . 6
⊢
((u ∈ N ∧ x ∈ N) → (u ·N x) ∈
N) |
23 | 20, 21, 22 | syl2anc 391 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (u ·N x) ∈
N) |
24 | 15, 19, 23 | caovcld 5596 |
. . . 4
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ((v ·N y) +N (u ·N x)) ∈
N) |
25 | | mulclpi 6312 |
. . . . 5
⊢
((u ∈ N ∧ y ∈ N) → (u ·N y) ∈
N) |
26 | 20, 17, 25 | syl2anc 391 |
. . . 4
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (u ·N y) ∈
N) |
27 | | mulclpi 6312 |
. . . . . . 7
⊢
((f ∈ N ∧ g ∈ N) → (f ·N g) ∈
N) |
28 | 27 | adantl 262 |
. . . . . 6
⊢
((((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) ∧ (f ∈ N ∧ g ∈ N)) → (f ·N g) ∈
N) |
29 | | simp2r 930 |
. . . . . 6
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → w ∈
N) |
30 | 28, 16, 29 | caovcld 5596 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (v ·N w) ∈
N) |
31 | | simp2l 929 |
. . . . . 6
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → z ∈
N) |
32 | | mulclpi 6312 |
. . . . . 6
⊢
((u ∈ N ∧ z ∈ N) → (u ·N z) ∈
N) |
33 | 20, 31, 32 | syl2anc 391 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (u ·N z) ∈
N) |
34 | 15, 30, 33 | caovcld 5596 |
. . . 4
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ((v ·N w) +N (u ·N z)) ∈
N) |
35 | | mulclpi 6312 |
. . . . 5
⊢
((u ∈ N ∧ w ∈ N) → (u ·N w) ∈
N) |
36 | 20, 29, 35 | syl2anc 391 |
. . . 4
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (u ·N w) ∈
N) |
37 | | ordpipqqs 6358 |
. . . 4
⊢
(((((v
·N y)
+N (u
·N x))
∈ N ∧ (u
·N y) ∈ N) ∧ (((v
·N w)
+N (u
·N z))
∈ N ∧ (u
·N w) ∈ N)) → ([〈((v ·N y) +N (u ·N x)), (u
·N y)〉] ~Q
<Q [〈((v
·N w)
+N (u
·N z)),
(u ·N
w)〉] ~Q
↔ (((v
·N y)
+N (u
·N x))
·N (u
·N w))
<N ((u
·N y)
·N ((v
·N w)
+N (u
·N z))))) |
38 | 24, 26, 34, 36, 37 | syl22anc 1135 |
. . 3
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ([〈((v ·N y) +N (u ·N x)), (u
·N y)〉] ~Q
<Q [〈((v
·N w)
+N (u
·N z)),
(u ·N
w)〉] ~Q
↔ (((v
·N y)
+N (u
·N x))
·N (u
·N w))
<N ((u
·N y)
·N ((v
·N w)
+N (u
·N z))))) |
39 | | simp3 905 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (v ∈
N ∧ u ∈
N)) |
40 | | simp1 903 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (x ∈
N ∧ y ∈
N)) |
41 | | addpipqqs 6354 |
. . . . 5
⊢
(((v ∈ N ∧ u ∈ N) ∧ (x ∈ N ∧ y ∈ N)) → ([〈v, u〉]
~Q +Q [〈x, y〉]
~Q ) = [〈((v
·N y)
+N (u
·N x)),
(u ·N
y)〉] ~Q
) |
42 | 39, 40, 41 | syl2anc 391 |
. . . 4
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ([〈v, u〉]
~Q +Q [〈x, y〉]
~Q ) = [〈((v
·N y)
+N (u
·N x)),
(u ·N
y)〉] ~Q
) |
43 | | simp2 904 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (z ∈
N ∧ w ∈
N)) |
44 | | addpipqqs 6354 |
. . . . 5
⊢
(((v ∈ N ∧ u ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → ([〈v, u〉]
~Q +Q [〈z, w〉]
~Q ) = [〈((v
·N w)
+N (u
·N z)),
(u ·N
w)〉] ~Q
) |
45 | 39, 43, 44 | syl2anc 391 |
. . . 4
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ([〈v, u〉]
~Q +Q [〈z, w〉]
~Q ) = [〈((v
·N w)
+N (u
·N z)),
(u ·N
w)〉] ~Q
) |
46 | 42, 45 | 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 y) +N (u ·N x)), (u
·N y)〉] ~Q
<Q [〈((v
·N w)
+N (u
·N z)),
(u ·N
w)〉] ~Q
)) |
47 | | 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))) |
48 | 47 | 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))) |
49 | | mulclpi 6312 |
. . . . . 6
⊢
((x ∈ N ∧ w ∈ N) → (x ·N w) ∈
N) |
50 | 21, 29, 49 | syl2anc 391 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (x ·N w) ∈
N) |
51 | | mulclpi 6312 |
. . . . . 6
⊢
((y ∈ N ∧ z ∈ N) → (y ·N z) ∈
N) |
52 | 17, 31, 51 | syl2anc 391 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (y ·N z) ∈
N) |
53 | | mulclpi 6312 |
. . . . . 6
⊢
((u ∈ N ∧ u ∈ N) → (u ·N u) ∈
N) |
54 | 20, 20, 53 | syl2anc 391 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (u ·N u) ∈
N) |
55 | | ltmpig 6323 |
. . . . 5
⊢
(((x
·N w) ∈ N ∧ (y
·N z) ∈ N ∧ (u
·N u) ∈ N) → ((x ·N w) <N (y ·N z) ↔ ((u
·N u)
·N (x
·N w))
<N ((u
·N u)
·N (y
·N z)))) |
56 | 50, 52, 54, 55 | syl3anc 1134 |
. . . 4
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ((x ·N w) <N (y ·N z) ↔ ((u
·N u)
·N (x
·N w))
<N ((u
·N u)
·N (y
·N z)))) |
57 | | mulclpi 6312 |
. . . . . . 7
⊢
(((u
·N x) ∈ N ∧ (u
·N w) ∈ N) → ((u ·N x) ·N (u ·N w)) ∈
N) |
58 | 23, 36, 57 | syl2anc 391 |
. . . . . 6
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ((u ·N x) ·N (u ·N w)) ∈
N) |
59 | | mulclpi 6312 |
. . . . . . 7
⊢
(((u
·N y) ∈ N ∧ (u
·N z) ∈ N) → ((u ·N y) ·N (u ·N z)) ∈
N) |
60 | 26, 33, 59 | syl2anc 391 |
. . . . . 6
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ((u ·N y) ·N (u ·N z)) ∈
N) |
61 | | mulclpi 6312 |
. . . . . . 7
⊢
(((v
·N y) ∈ N ∧ (u
·N w) ∈ N) → ((v ·N y) ·N (u ·N w)) ∈
N) |
62 | 19, 36, 61 | syl2anc 391 |
. . . . . 6
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ((v ·N y) ·N (u ·N w)) ∈
N) |
63 | | ltapig 6322 |
. . . . . 6
⊢
((((u
·N x)
·N (u
·N w))
∈ N ∧ ((u
·N y)
·N (u
·N z))
∈ N ∧ ((v
·N y)
·N (u
·N w))
∈ N) → (((u ·N x) ·N (u ·N w)) <N ((u ·N y) ·N (u ·N z)) ↔ (((v
·N y)
·N (u
·N w))
+N ((u
·N x)
·N (u
·N w)))
<N (((v
·N y)
·N (u
·N w))
+N ((u
·N y)
·N (u
·N z))))) |
64 | 58, 60, 62, 63 | syl3anc 1134 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (((u ·N x) ·N (u ·N w)) <N ((u ·N y) ·N (u ·N z)) ↔ (((v
·N y)
·N (u
·N w))
+N ((u
·N x)
·N (u
·N w)))
<N (((v
·N y)
·N (u
·N w))
+N ((u
·N y)
·N (u
·N z))))) |
65 | | mulcompig 6315 |
. . . . . . . 8
⊢
((f ∈ N ∧ g ∈ N) → (f ·N g) = (g
·N f)) |
66 | 65 | 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)) |
67 | | mulasspig 6316 |
. . . . . . . 8
⊢
((f ∈ N ∧ g ∈ N ∧ ℎ
∈ N) → ((f ·N g) ·N ℎ) = (f ·N (g ·N ℎ))) |
68 | 67 | 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 ℎ))) |
69 | 20, 20, 21, 66, 68, 29, 28 | caov4d 5627 |
. . . . . 6
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ((u ·N u) ·N (x ·N w)) = ((u
·N x)
·N (u
·N w))) |
70 | 20, 20, 17, 66, 68, 31, 28 | caov4d 5627 |
. . . . . 6
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ((u ·N u) ·N (y ·N z)) = ((u
·N y)
·N (u
·N z))) |
71 | 69, 70 | breq12d 3768 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (((u ·N u) ·N (x ·N w)) <N ((u ·N u) ·N (y ·N z)) ↔ ((u
·N x)
·N (u
·N w))
<N ((u
·N y)
·N (u
·N z)))) |
72 | | distrpig 6317 |
. . . . . . . 8
⊢
((f ∈ N ∧ g ∈ N ∧ ℎ
∈ N) → (f ·N (g +N ℎ)) = ((f
·N g)
+N (f
·N ℎ))) |
73 | 72 | 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 (f
·N ℎ))) |
74 | 73, 19, 23, 36, 15, 66 | caovdir2d 5619 |
. . . . . 6
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (((v ·N y) +N (u ·N x)) ·N (u ·N w)) = (((v
·N y)
·N (u
·N w))
+N ((u
·N x)
·N (u
·N w)))) |
75 | 73, 26, 30, 33 | caovdid 5618 |
. . . . . . 7
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ((u ·N y) ·N ((v ·N w) +N (u ·N z))) = (((u
·N y)
·N (v
·N w))
+N ((u
·N y)
·N (u
·N z)))) |
76 | 20, 17, 16, 66, 68, 29, 28 | caov411d 5628 |
. . . . . . . 8
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ((u ·N y) ·N (v ·N w)) = ((v
·N y)
·N (u
·N w))) |
77 | 76 | oveq1d 5470 |
. . . . . . 7
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (((u ·N y) ·N (v ·N w)) +N ((u ·N y) ·N (u ·N z))) = (((v
·N y)
·N (u
·N w))
+N ((u
·N y)
·N (u
·N z)))) |
78 | 75, 77 | eqtrd 2069 |
. . . . . 6
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ((u ·N y) ·N ((v ·N w) +N (u ·N z))) = (((v
·N y)
·N (u
·N w))
+N ((u
·N y)
·N (u
·N z)))) |
79 | 74, 78 | breq12d 3768 |
. . . . 5
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ((((v ·N y) +N (u ·N x)) ·N (u ·N w)) <N ((u ·N y) ·N ((v ·N w) +N (u ·N z))) ↔ (((v
·N y)
·N (u
·N w))
+N ((u
·N x)
·N (u
·N w)))
<N (((v
·N y)
·N (u
·N w))
+N ((u
·N y)
·N (u
·N z))))) |
80 | 64, 71, 79 | 3bitr4d 209 |
. . . 4
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (((u ·N u) ·N (x ·N w)) <N ((u ·N u) ·N (y ·N z)) ↔ (((v
·N y)
+N (u
·N x))
·N (u
·N w))
<N ((u
·N y)
·N ((v
·N w)
+N (u
·N z))))) |
81 | 48, 56, 80 | 3bitrd 203 |
. . 3
⊢
(((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ([〈x, y〉]
~Q <Q [〈z, w〉]
~Q ↔ (((v
·N y)
+N (u
·N x))
·N (u
·N w))
<N ((u
·N y)
·N ((v
·N w)
+N (u
·N z))))) |
82 | 38, 46, 81 | 3bitr4rd 210 |
. 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 ))) |
83 | 1, 5, 9, 13, 82 | 3ecoptocl 6131 |
1
⊢
((A ∈ Q ∧ B ∈ Q ∧ 𝐶 ∈
Q) → (A
<Q B ↔
(𝐶
+Q A)
<Q (𝐶 +Q B))) |