| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | addnqf 10988 | . . 3
⊢ 
+Q :(Q ×
Q)⟶Q | 
| 2 | 1 | fdmi 6747 | . 2
⊢ dom
+Q = (Q ×
Q) | 
| 3 |  | ltrelnq 10966 | . 2
⊢ 
<Q ⊆ (Q ×
Q) | 
| 4 |  | 0nnq 10964 | . 2
⊢  ¬
∅ ∈ Q | 
| 5 |  | ordpinq 10983 | . . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
<Q 𝐵 ↔ ((1st ‘𝐴)
·N (2nd ‘𝐵)) <N
((1st ‘𝐵)
·N (2nd ‘𝐴)))) | 
| 6 | 5 | 3adant3 1133 | . . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
<Q 𝐵 ↔ ((1st ‘𝐴)
·N (2nd ‘𝐵)) <N
((1st ‘𝐵)
·N (2nd ‘𝐴)))) | 
| 7 |  | elpqn 10965 | . . . . . . 7
⊢ (𝐶 ∈ Q →
𝐶 ∈ (N
× N)) | 
| 8 | 7 | 3ad2ant3 1136 | . . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐶
∈ (N × N)) | 
| 9 |  | elpqn 10965 | . . . . . . 7
⊢ (𝐴 ∈ Q →
𝐴 ∈ (N
× N)) | 
| 10 | 9 | 3ad2ant1 1134 | . . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐴
∈ (N × N)) | 
| 11 |  | addpipq2 10976 | . . . . . 6
⊢ ((𝐶 ∈ (N ×
N) ∧ 𝐴
∈ (N × N)) → (𝐶 +pQ 𝐴) = 〈(((1st
‘𝐶)
·N (2nd ‘𝐴)) +N
((1st ‘𝐴)
·N (2nd ‘𝐶))), ((2nd ‘𝐶)
·N (2nd ‘𝐴))〉) | 
| 12 | 8, 10, 11 | syl2anc 584 | . . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐶
+pQ 𝐴) = 〈(((1st ‘𝐶)
·N (2nd ‘𝐴)) +N
((1st ‘𝐴)
·N (2nd ‘𝐶))), ((2nd ‘𝐶)
·N (2nd ‘𝐴))〉) | 
| 13 |  | elpqn 10965 | . . . . . . 7
⊢ (𝐵 ∈ Q →
𝐵 ∈ (N
× N)) | 
| 14 | 13 | 3ad2ant2 1135 | . . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐵
∈ (N × N)) | 
| 15 |  | addpipq2 10976 | . . . . . 6
⊢ ((𝐶 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐶 +pQ 𝐵) = 〈(((1st
‘𝐶)
·N (2nd ‘𝐵)) +N
((1st ‘𝐵)
·N (2nd ‘𝐶))), ((2nd ‘𝐶)
·N (2nd ‘𝐵))〉) | 
| 16 | 8, 14, 15 | syl2anc 584 | . . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐶
+pQ 𝐵) = 〈(((1st ‘𝐶)
·N (2nd ‘𝐵)) +N
((1st ‘𝐵)
·N (2nd ‘𝐶))), ((2nd ‘𝐶)
·N (2nd ‘𝐵))〉) | 
| 17 | 12, 16 | breq12d 5156 | . . . 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 10978 | . . . . . . . 8
⊢ ((𝐶 ∈ Q ∧
𝐴 ∈ Q)
→ (𝐶
+Q 𝐴) = ([Q]‘(𝐶 +pQ
𝐴))) | 
| 19 | 18 | ancoms 458 | . . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐶 ∈ Q)
→ (𝐶
+Q 𝐴) = ([Q]‘(𝐶 +pQ
𝐴))) | 
| 20 | 19 | 3adant2 1132 | . . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐶
+Q 𝐴) = ([Q]‘(𝐶 +pQ
𝐴))) | 
| 21 |  | addpqnq 10978 | . . . . . . . 8
⊢ ((𝐶 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐶
+Q 𝐵) = ([Q]‘(𝐶 +pQ
𝐵))) | 
| 22 | 21 | ancoms 458 | . . . . . . 7
⊢ ((𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ (𝐶
+Q 𝐵) = ([Q]‘(𝐶 +pQ
𝐵))) | 
| 23 | 22 | 3adant1 1131 | . . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐶
+Q 𝐵) = ([Q]‘(𝐶 +pQ
𝐵))) | 
| 24 | 20, 23 | breq12d 5156 | . . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐶
+Q 𝐴) <Q (𝐶 +Q
𝐵) ↔
([Q]‘(𝐶
+pQ 𝐴)) <Q
([Q]‘(𝐶
+pQ 𝐵)))) | 
| 25 |  | lterpq 11010 | . . . . 5
⊢ ((𝐶 +pQ
𝐴)
<pQ (𝐶 +pQ 𝐵) ↔
([Q]‘(𝐶
+pQ 𝐴)) <Q
([Q]‘(𝐶
+pQ 𝐵))) | 
| 26 | 24, 25 | bitr4di 289 | . . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐶
+Q 𝐴) <Q (𝐶 +Q
𝐵) ↔ (𝐶 +pQ
𝐴)
<pQ (𝐶 +pQ 𝐵))) | 
| 27 |  | xp2nd 8047 | . . . . . . . . . 10
⊢ (𝐶 ∈ (N ×
N) → (2nd ‘𝐶) ∈ N) | 
| 28 | 8, 27 | syl 17 | . . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (2nd ‘𝐶) ∈ N) | 
| 29 |  | mulclpi 10933 | . . . . . . . . 9
⊢
(((2nd ‘𝐶) ∈ N ∧
(2nd ‘𝐶)
∈ N) → ((2nd ‘𝐶) ·N
(2nd ‘𝐶))
∈ N) | 
| 30 | 28, 28, 29 | syl2anc 584 | . . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((2nd ‘𝐶) ·N
(2nd ‘𝐶))
∈ N) | 
| 31 |  | ltmpi 10944 | . . . . . . . 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 8047 | . . . . . . . . . . 11
⊢ (𝐵 ∈ (N ×
N) → (2nd ‘𝐵) ∈ N) | 
| 34 | 14, 33 | syl 17 | . . . . . . . . . 10
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (2nd ‘𝐵) ∈ N) | 
| 35 |  | mulclpi 10933 | . . . . . . . . . 10
⊢
(((2nd ‘𝐶) ∈ N ∧
(2nd ‘𝐵)
∈ N) → ((2nd ‘𝐶) ·N
(2nd ‘𝐵))
∈ N) | 
| 36 | 28, 34, 35 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((2nd ‘𝐶) ·N
(2nd ‘𝐵))
∈ N) | 
| 37 |  | xp1st 8046 | . . . . . . . . . . 11
⊢ (𝐶 ∈ (N ×
N) → (1st ‘𝐶) ∈ N) | 
| 38 | 8, 37 | syl 17 | . . . . . . . . . 10
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (1st ‘𝐶) ∈ N) | 
| 39 |  | xp2nd 8047 | . . . . . . . . . . 11
⊢ (𝐴 ∈ (N ×
N) → (2nd ‘𝐴) ∈ N) | 
| 40 | 10, 39 | syl 17 | . . . . . . . . . 10
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (2nd ‘𝐴) ∈ N) | 
| 41 |  | mulclpi 10933 | . . . . . . . . . 10
⊢
(((1st ‘𝐶) ∈ N ∧
(2nd ‘𝐴)
∈ N) → ((1st ‘𝐶) ·N
(2nd ‘𝐴))
∈ N) | 
| 42 | 38, 40, 41 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((1st ‘𝐶) ·N
(2nd ‘𝐴))
∈ N) | 
| 43 |  | mulclpi 10933 | . . . . . . . . 9
⊢
((((2nd ‘𝐶) ·N
(2nd ‘𝐵))
∈ N ∧ ((1st ‘𝐶) ·N
(2nd ‘𝐴))
∈ N) → (((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
∈ N) | 
| 44 | 36, 42, 43 | syl2anc 584 | . . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
∈ N) | 
| 45 |  | ltapi 10943 | . . . . . . . 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 279 | . . . . . 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 10936 | . . . . . . . . . 10
⊢
(((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐴) ·N
(2nd ‘𝐵)))
= (((1st ‘𝐴) ·N
(2nd ‘𝐵))
·N ((2nd ‘𝐶) ·N
(2nd ‘𝐶))) | 
| 49 |  | fvex 6919 | . . . . . . . . . . 11
⊢
(1st ‘𝐴) ∈ V | 
| 50 |  | fvex 6919 | . . . . . . . . . . 11
⊢
(2nd ‘𝐵) ∈ V | 
| 51 |  | fvex 6919 | . . . . . . . . . . 11
⊢
(2nd ‘𝐶) ∈ V | 
| 52 |  | mulcompi 10936 | . . . . . . . . . . 11
⊢ (𝑥
·N 𝑦) = (𝑦 ·N 𝑥) | 
| 53 |  | mulasspi 10937 | . . . . . . . . . . 11
⊢ ((𝑥
·N 𝑦) ·N 𝑧) = (𝑥 ·N (𝑦
·N 𝑧)) | 
| 54 | 49, 50, 51, 52, 53, 51 | caov411 7665 | . . . . . . . . . 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 7442 | . . . . . . . 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 10938 | . . . . . . . 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 10936 | . . . . . . . 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 10936 | . . . . . . . . . 10
⊢
(((2nd ‘𝐶) ·N
(2nd ‘𝐵))
·N ((1st ‘𝐶) ·N
(2nd ‘𝐴)))
= (((1st ‘𝐶) ·N
(2nd ‘𝐴))
·N ((2nd ‘𝐶) ·N
(2nd ‘𝐵))) | 
| 61 |  | fvex 6919 | . . . . . . . . . . 11
⊢
(1st ‘𝐶) ∈ V | 
| 62 |  | fvex 6919 | . . . . . . . . . . 11
⊢
(2nd ‘𝐴) ∈ V | 
| 63 | 61, 62, 51, 52, 53, 50 | caov411 7665 | . . . . . . . . . 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 10936 | . . . . . . . . . 10
⊢
(((2nd ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴)))
= (((1st ‘𝐵) ·N
(2nd ‘𝐴))
·N ((2nd ‘𝐶) ·N
(2nd ‘𝐶))) | 
| 66 |  | fvex 6919 | . . . . . . . . . . 11
⊢
(1st ‘𝐵) ∈ V | 
| 67 | 66, 62, 51, 52, 53, 51 | caov411 7665 | . . . . . . . . . 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 7443 | . . . . . . . 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 10938 | . . . . . . . 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 10936 | . . . . . . . 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 5152 | . . . . . 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 287 | . . . . 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 10982 | . . . . 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 289 | . . . 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 312 | . . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((1st ‘𝐴) ·N
(2nd ‘𝐵))
<N ((1st ‘𝐵) ·N
(2nd ‘𝐴))
↔ (𝐶
+Q 𝐴) <Q (𝐶 +Q
𝐵))) | 
| 78 | 6, 77 | bitrd 279 | . 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
<Q 𝐵 ↔ (𝐶 +Q 𝐴) <Q
(𝐶
+Q 𝐵))) | 
| 79 | 2, 3, 4, 78 | ndmovord 7623 | 1
⊢ (𝐶 ∈ Q →
(𝐴
<Q 𝐵 ↔ (𝐶 +Q 𝐴) <Q
(𝐶
+Q 𝐵))) |