Step | Hyp | Ref
| Expression |
1 | | addnqf 10562 |
. . 3
⊢
+Q :(Q ×
Q)⟶Q |
2 | 1 | fdmi 6557 |
. 2
⊢ dom
+Q = (Q ×
Q) |
3 | | ltrelnq 10540 |
. 2
⊢
<Q ⊆ (Q ×
Q) |
4 | | 0nnq 10538 |
. 2
⊢ ¬
∅ ∈ Q |
5 | | ordpinq 10557 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
<Q 𝐵 ↔ ((1st ‘𝐴)
·N (2nd ‘𝐵)) <N
((1st ‘𝐵)
·N (2nd ‘𝐴)))) |
6 | 5 | 3adant3 1134 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
<Q 𝐵 ↔ ((1st ‘𝐴)
·N (2nd ‘𝐵)) <N
((1st ‘𝐵)
·N (2nd ‘𝐴)))) |
7 | | elpqn 10539 |
. . . . . . 7
⊢ (𝐶 ∈ Q →
𝐶 ∈ (N
× N)) |
8 | 7 | 3ad2ant3 1137 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐶
∈ (N × N)) |
9 | | elpqn 10539 |
. . . . . . 7
⊢ (𝐴 ∈ Q →
𝐴 ∈ (N
× N)) |
10 | 9 | 3ad2ant1 1135 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐴
∈ (N × N)) |
11 | | addpipq2 10550 |
. . . . . 6
⊢ ((𝐶 ∈ (N ×
N) ∧ 𝐴
∈ (N × N)) → (𝐶 +pQ 𝐴) = 〈(((1st
‘𝐶)
·N (2nd ‘𝐴)) +N
((1st ‘𝐴)
·N (2nd ‘𝐶))), ((2nd ‘𝐶)
·N (2nd ‘𝐴))〉) |
12 | 8, 10, 11 | syl2anc 587 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐶
+pQ 𝐴) = 〈(((1st ‘𝐶)
·N (2nd ‘𝐴)) +N
((1st ‘𝐴)
·N (2nd ‘𝐶))), ((2nd ‘𝐶)
·N (2nd ‘𝐴))〉) |
13 | | elpqn 10539 |
. . . . . . 7
⊢ (𝐵 ∈ Q →
𝐵 ∈ (N
× N)) |
14 | 13 | 3ad2ant2 1136 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐵
∈ (N × N)) |
15 | | addpipq2 10550 |
. . . . . 6
⊢ ((𝐶 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐶 +pQ 𝐵) = 〈(((1st
‘𝐶)
·N (2nd ‘𝐵)) +N
((1st ‘𝐵)
·N (2nd ‘𝐶))), ((2nd ‘𝐶)
·N (2nd ‘𝐵))〉) |
16 | 8, 14, 15 | syl2anc 587 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐶
+pQ 𝐵) = 〈(((1st ‘𝐶)
·N (2nd ‘𝐵)) +N
((1st ‘𝐵)
·N (2nd ‘𝐶))), ((2nd ‘𝐶)
·N (2nd ‘𝐵))〉) |
17 | 12, 16 | breq12d 5066 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐶
+pQ 𝐴) <pQ (𝐶 +pQ
𝐵) ↔
〈(((1st ‘𝐶) ·N
(2nd ‘𝐴))
+N ((1st ‘𝐴) ·N
(2nd ‘𝐶))), ((2nd ‘𝐶)
·N (2nd ‘𝐴))〉 <pQ
〈(((1st ‘𝐶) ·N
(2nd ‘𝐵))
+N ((1st ‘𝐵) ·N
(2nd ‘𝐶))), ((2nd ‘𝐶)
·N (2nd ‘𝐵))〉)) |
18 | | addpqnq 10552 |
. . . . . . . 8
⊢ ((𝐶 ∈ Q ∧
𝐴 ∈ Q)
→ (𝐶
+Q 𝐴) = ([Q]‘(𝐶 +pQ
𝐴))) |
19 | 18 | ancoms 462 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐶 ∈ Q)
→ (𝐶
+Q 𝐴) = ([Q]‘(𝐶 +pQ
𝐴))) |
20 | 19 | 3adant2 1133 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐶
+Q 𝐴) = ([Q]‘(𝐶 +pQ
𝐴))) |
21 | | addpqnq 10552 |
. . . . . . . 8
⊢ ((𝐶 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐶
+Q 𝐵) = ([Q]‘(𝐶 +pQ
𝐵))) |
22 | 21 | ancoms 462 |
. . . . . . 7
⊢ ((𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ (𝐶
+Q 𝐵) = ([Q]‘(𝐶 +pQ
𝐵))) |
23 | 22 | 3adant1 1132 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐶
+Q 𝐵) = ([Q]‘(𝐶 +pQ
𝐵))) |
24 | 20, 23 | breq12d 5066 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐶
+Q 𝐴) <Q (𝐶 +Q
𝐵) ↔
([Q]‘(𝐶
+pQ 𝐴)) <Q
([Q]‘(𝐶
+pQ 𝐵)))) |
25 | | lterpq 10584 |
. . . . 5
⊢ ((𝐶 +pQ
𝐴)
<pQ (𝐶 +pQ 𝐵) ↔
([Q]‘(𝐶
+pQ 𝐴)) <Q
([Q]‘(𝐶
+pQ 𝐵))) |
26 | 24, 25 | bitr4di 292 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐶
+Q 𝐴) <Q (𝐶 +Q
𝐵) ↔ (𝐶 +pQ
𝐴)
<pQ (𝐶 +pQ 𝐵))) |
27 | | xp2nd 7794 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (N ×
N) → (2nd ‘𝐶) ∈ N) |
28 | 8, 27 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (2nd ‘𝐶) ∈ N) |
29 | | mulclpi 10507 |
. . . . . . . . 9
⊢
(((2nd ‘𝐶) ∈ N ∧
(2nd ‘𝐶)
∈ N) → ((2nd ‘𝐶) ·N
(2nd ‘𝐶))
∈ N) |
30 | 28, 28, 29 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((2nd ‘𝐶) ·N
(2nd ‘𝐶))
∈ N) |
31 | | ltmpi 10518 |
. . . . . . . 8
⊢
(((2nd ‘𝐶) ·N
(2nd ‘𝐶))
∈ N → (((1st ‘𝐴) ·N
(2nd ‘𝐵))
<N ((1st ‘𝐵) ·N
(2nd ‘𝐴))
↔ (((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐴) ·N
(2nd ‘𝐵)))
<N (((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴))))) |
32 | 30, 31 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((1st ‘𝐴) ·N
(2nd ‘𝐵))
<N ((1st ‘𝐵) ·N
(2nd ‘𝐴))
↔ (((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐴) ·N
(2nd ‘𝐵)))
<N (((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴))))) |
33 | | xp2nd 7794 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (N ×
N) → (2nd ‘𝐵) ∈ N) |
34 | 14, 33 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (2nd ‘𝐵) ∈ N) |
35 | | mulclpi 10507 |
. . . . . . . . . 10
⊢
(((2nd ‘𝐶) ∈ N ∧
(2nd ‘𝐵)
∈ N) → ((2nd ‘𝐶) ·N
(2nd ‘𝐵))
∈ N) |
36 | 28, 34, 35 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((2nd ‘𝐶) ·N
(2nd ‘𝐵))
∈ N) |
37 | | xp1st 7793 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (N ×
N) → (1st ‘𝐶) ∈ N) |
38 | 8, 37 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (1st ‘𝐶) ∈ N) |
39 | | xp2nd 7794 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (N ×
N) → (2nd ‘𝐴) ∈ N) |
40 | 10, 39 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (2nd ‘𝐴) ∈ N) |
41 | | mulclpi 10507 |
. . . . . . . . . 10
⊢
(((1st ‘𝐶) ∈ N ∧
(2nd ‘𝐴)
∈ N) → ((1st ‘𝐶) ·N
(2nd ‘𝐴))
∈ N) |
42 | 38, 40, 41 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((1st ‘𝐶) ·N
(2nd ‘𝐴))
∈ N) |
43 | | mulclpi 10507 |
. . . . . . . . 9
⊢
((((2nd ‘𝐶) ·N
(2nd ‘𝐵))
∈ N ∧ ((1st ‘𝐶) ·N
(2nd ‘𝐴))
∈ N) → (((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
∈ N) |
44 | 36, 42, 43 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
∈ N) |
45 | | ltapi 10517 |
. . . . . . . 8
⊢
((((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
∈ N → ((((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐴) ·N
(2nd ‘𝐵)))
<N (((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴)))
↔ ((((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
+N (((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐴) ·N
(2nd ‘𝐵)))) <N
((((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
+N (((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴)))))) |
46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐴) ·N
(2nd ‘𝐵)))
<N (((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴)))
↔ ((((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
+N (((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐴) ·N
(2nd ‘𝐵)))) <N
((((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
+N (((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴)))))) |
47 | 32, 46 | bitrd 282 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((1st ‘𝐴) ·N
(2nd ‘𝐵))
<N ((1st ‘𝐵) ·N
(2nd ‘𝐴))
↔ ((((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
+N (((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐴) ·N
(2nd ‘𝐵)))) <N
((((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
+N (((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴)))))) |
48 | | mulcompi 10510 |
. . . . . . . . . 10
⊢
(((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐴) ·N
(2nd ‘𝐵)))
= (((1st ‘𝐴) ·N
(2nd ‘𝐵))
·N ((2nd ‘𝐶) ·N
(2nd ‘𝐶))) |
49 | | fvex 6730 |
. . . . . . . . . . 11
⊢
(1st ‘𝐴) ∈ V |
50 | | fvex 6730 |
. . . . . . . . . . 11
⊢
(2nd ‘𝐵) ∈ V |
51 | | fvex 6730 |
. . . . . . . . . . 11
⊢
(2nd ‘𝐶) ∈ V |
52 | | mulcompi 10510 |
. . . . . . . . . . 11
⊢ (𝑥
·N 𝑦) = (𝑦 ·N 𝑥) |
53 | | mulasspi 10511 |
. . . . . . . . . . 11
⊢ ((𝑥
·N 𝑦) ·N 𝑧) = (𝑥 ·N (𝑦
·N 𝑧)) |
54 | 49, 50, 51, 52, 53, 51 | caov411 7440 |
. . . . . . . . . 10
⊢
(((1st ‘𝐴) ·N
(2nd ‘𝐵))
·N ((2nd ‘𝐶) ·N
(2nd ‘𝐶)))
= (((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐴) ·N
(2nd ‘𝐶))) |
55 | 48, 54 | eqtri 2765 |
. . . . . . . . 9
⊢
(((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐴) ·N
(2nd ‘𝐵)))
= (((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐴) ·N
(2nd ‘𝐶))) |
56 | 55 | oveq2i 7224 |
. . . . . . . 8
⊢
((((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
+N (((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐴) ·N
(2nd ‘𝐵)))) = ((((2nd ‘𝐶)
·N (2nd ‘𝐵)) ·N
((1st ‘𝐶)
·N (2nd ‘𝐴))) +N
(((2nd ‘𝐶)
·N (2nd ‘𝐵)) ·N
((1st ‘𝐴)
·N (2nd ‘𝐶)))) |
57 | | distrpi 10512 |
. . . . . . . 8
⊢
(((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N (((1st ‘𝐶) ·N
(2nd ‘𝐴))
+N ((1st ‘𝐴) ·N
(2nd ‘𝐶)))) = ((((2nd ‘𝐶)
·N (2nd ‘𝐵)) ·N
((1st ‘𝐶)
·N (2nd ‘𝐴))) +N
(((2nd ‘𝐶)
·N (2nd ‘𝐵)) ·N
((1st ‘𝐴)
·N (2nd ‘𝐶)))) |
58 | | mulcompi 10510 |
. . . . . . . 8
⊢
(((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N (((1st ‘𝐶) ·N
(2nd ‘𝐴))
+N ((1st ‘𝐴) ·N
(2nd ‘𝐶)))) = ((((1st ‘𝐶)
·N (2nd ‘𝐴)) +N
((1st ‘𝐴)
·N (2nd ‘𝐶))) ·N
((2nd ‘𝐶)
·N (2nd ‘𝐵))) |
59 | 56, 57, 58 | 3eqtr2i 2771 |
. . . . . . 7
⊢
((((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
+N (((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐴) ·N
(2nd ‘𝐵)))) = ((((1st ‘𝐶)
·N (2nd ‘𝐴)) +N
((1st ‘𝐴)
·N (2nd ‘𝐶))) ·N
((2nd ‘𝐶)
·N (2nd ‘𝐵))) |
60 | | mulcompi 10510 |
. . . . . . . . . 10
⊢
(((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
= (((1st ‘𝐶) ·N
(2nd ‘𝐴))
·N ((2nd ‘𝐶) ·N
(2nd ‘𝐵))) |
61 | | fvex 6730 |
. . . . . . . . . . 11
⊢
(1st ‘𝐶) ∈ V |
62 | | fvex 6730 |
. . . . . . . . . . 11
⊢
(2nd ‘𝐴) ∈ V |
63 | 61, 62, 51, 52, 53, 50 | caov411 7440 |
. . . . . . . . . 10
⊢
(((1st ‘𝐶) ·N
(2nd ‘𝐴))
·N ((2nd ‘𝐶) ·N
(2nd ‘𝐵)))
= (((2nd ‘𝐶) ·N
(2nd ‘𝐴))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐵))) |
64 | 60, 63 | eqtri 2765 |
. . . . . . . . 9
⊢
(((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
= (((2nd ‘𝐶) ·N
(2nd ‘𝐴))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐵))) |
65 | | mulcompi 10510 |
. . . . . . . . . 10
⊢
(((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴)))
= (((1st ‘𝐵) ·N
(2nd ‘𝐴))
·N ((2nd ‘𝐶) ·N
(2nd ‘𝐶))) |
66 | | fvex 6730 |
. . . . . . . . . . 11
⊢
(1st ‘𝐵) ∈ V |
67 | 66, 62, 51, 52, 53, 51 | caov411 7440 |
. . . . . . . . . 10
⊢
(((1st ‘𝐵) ·N
(2nd ‘𝐴))
·N ((2nd ‘𝐶) ·N
(2nd ‘𝐶)))
= (((2nd ‘𝐶) ·N
(2nd ‘𝐴))
·N ((1st ‘𝐵) ·N
(2nd ‘𝐶))) |
68 | 65, 67 | eqtri 2765 |
. . . . . . . . 9
⊢
(((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴)))
= (((2nd ‘𝐶) ·N
(2nd ‘𝐴))
·N ((1st ‘𝐵) ·N
(2nd ‘𝐶))) |
69 | 64, 68 | oveq12i 7225 |
. . . . . . . 8
⊢
((((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
+N (((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴)))) = ((((2nd ‘𝐶)
·N (2nd ‘𝐴)) ·N
((1st ‘𝐶)
·N (2nd ‘𝐵))) +N
(((2nd ‘𝐶)
·N (2nd ‘𝐴)) ·N
((1st ‘𝐵)
·N (2nd ‘𝐶)))) |
70 | | distrpi 10512 |
. . . . . . . 8
⊢
(((2nd ‘𝐶) ·N
(2nd ‘𝐴))
·N (((1st ‘𝐶) ·N
(2nd ‘𝐵))
+N ((1st ‘𝐵) ·N
(2nd ‘𝐶)))) = ((((2nd ‘𝐶)
·N (2nd ‘𝐴)) ·N
((1st ‘𝐶)
·N (2nd ‘𝐵))) +N
(((2nd ‘𝐶)
·N (2nd ‘𝐴)) ·N
((1st ‘𝐵)
·N (2nd ‘𝐶)))) |
71 | | mulcompi 10510 |
. . . . . . . 8
⊢
(((2nd ‘𝐶) ·N
(2nd ‘𝐴))
·N (((1st ‘𝐶) ·N
(2nd ‘𝐵))
+N ((1st ‘𝐵) ·N
(2nd ‘𝐶)))) = ((((1st ‘𝐶)
·N (2nd ‘𝐵)) +N
((1st ‘𝐵)
·N (2nd ‘𝐶))) ·N
((2nd ‘𝐶)
·N (2nd ‘𝐴))) |
72 | 69, 70, 71 | 3eqtr2i 2771 |
. . . . . . 7
⊢
((((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
+N (((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴)))) = ((((1st ‘𝐶)
·N (2nd ‘𝐵)) +N
((1st ‘𝐵)
·N (2nd ‘𝐶))) ·N
((2nd ‘𝐶)
·N (2nd ‘𝐴))) |
73 | 59, 72 | breq12i 5062 |
. . . . . 6
⊢
(((((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
+N (((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐴) ·N
(2nd ‘𝐵)))) <N
((((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
+N (((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴)))) ↔ ((((1st ‘𝐶)
·N (2nd ‘𝐴)) +N
((1st ‘𝐴)
·N (2nd ‘𝐶))) ·N
((2nd ‘𝐶)
·N (2nd ‘𝐵))) <N
((((1st ‘𝐶) ·N
(2nd ‘𝐵))
+N ((1st ‘𝐵) ·N
(2nd ‘𝐶)))
·N ((2nd ‘𝐶) ·N
(2nd ‘𝐴)))) |
74 | 47, 73 | bitrdi 290 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((1st ‘𝐴) ·N
(2nd ‘𝐵))
<N ((1st ‘𝐵) ·N
(2nd ‘𝐴))
↔ ((((1st ‘𝐶) ·N
(2nd ‘𝐴))
+N ((1st ‘𝐴) ·N
(2nd ‘𝐶)))
·N ((2nd ‘𝐶) ·N
(2nd ‘𝐵)))
<N ((((1st ‘𝐶) ·N
(2nd ‘𝐵))
+N ((1st ‘𝐵) ·N
(2nd ‘𝐶)))
·N ((2nd ‘𝐶) ·N
(2nd ‘𝐴))))) |
75 | | ordpipq 10556 |
. . . . 5
⊢
(〈(((1st ‘𝐶) ·N
(2nd ‘𝐴))
+N ((1st ‘𝐴) ·N
(2nd ‘𝐶))), ((2nd ‘𝐶)
·N (2nd ‘𝐴))〉 <pQ
〈(((1st ‘𝐶) ·N
(2nd ‘𝐵))
+N ((1st ‘𝐵) ·N
(2nd ‘𝐶))), ((2nd ‘𝐶)
·N (2nd ‘𝐵))〉 ↔ ((((1st
‘𝐶)
·N (2nd ‘𝐴)) +N
((1st ‘𝐴)
·N (2nd ‘𝐶))) ·N
((2nd ‘𝐶)
·N (2nd ‘𝐵))) <N
((((1st ‘𝐶) ·N
(2nd ‘𝐵))
+N ((1st ‘𝐵) ·N
(2nd ‘𝐶)))
·N ((2nd ‘𝐶) ·N
(2nd ‘𝐴)))) |
76 | 74, 75 | bitr4di 292 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((1st ‘𝐴) ·N
(2nd ‘𝐵))
<N ((1st ‘𝐵) ·N
(2nd ‘𝐴))
↔ 〈(((1st ‘𝐶) ·N
(2nd ‘𝐴))
+N ((1st ‘𝐴) ·N
(2nd ‘𝐶))), ((2nd ‘𝐶)
·N (2nd ‘𝐴))〉 <pQ
〈(((1st ‘𝐶) ·N
(2nd ‘𝐵))
+N ((1st ‘𝐵) ·N
(2nd ‘𝐶))), ((2nd ‘𝐶)
·N (2nd ‘𝐵))〉)) |
77 | 17, 26, 76 | 3bitr4rd 315 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((1st ‘𝐴) ·N
(2nd ‘𝐵))
<N ((1st ‘𝐵) ·N
(2nd ‘𝐴))
↔ (𝐶
+Q 𝐴) <Q (𝐶 +Q
𝐵))) |
78 | 6, 77 | bitrd 282 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
<Q 𝐵 ↔ (𝐶 +Q 𝐴) <Q
(𝐶
+Q 𝐵))) |
79 | 2, 3, 4, 78 | ndmovord 7398 |
1
⊢ (𝐶 ∈ Q →
(𝐴
<Q 𝐵 ↔ (𝐶 +Q 𝐴) <Q
(𝐶
+Q 𝐵))) |