| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mulnqf 10989 | . . 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 |  | elpqn 10965 | . . . . . . . . . 10
⊢ (𝐶 ∈ Q →
𝐶 ∈ (N
× N)) | 
| 6 | 5 | 3ad2ant3 1136 | . . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐶
∈ (N × N)) | 
| 7 |  | xp1st 8046 | . . . . . . . . 9
⊢ (𝐶 ∈ (N ×
N) → (1st ‘𝐶) ∈ N) | 
| 8 | 6, 7 | syl 17 | . . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (1st ‘𝐶) ∈ N) | 
| 9 |  | xp2nd 8047 | . . . . . . . . 9
⊢ (𝐶 ∈ (N ×
N) → (2nd ‘𝐶) ∈ N) | 
| 10 | 6, 9 | syl 17 | . . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (2nd ‘𝐶) ∈ N) | 
| 11 |  | mulclpi 10933 | . . . . . . . 8
⊢
(((1st ‘𝐶) ∈ N ∧
(2nd ‘𝐶)
∈ N) → ((1st ‘𝐶) ·N
(2nd ‘𝐶))
∈ N) | 
| 12 | 8, 10, 11 | syl2anc 584 | . . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((1st ‘𝐶) ·N
(2nd ‘𝐶))
∈ N) | 
| 13 |  | ltmpi 10944 | . . . . . . 7
⊢
(((1st ‘𝐶) ·N
(2nd ‘𝐶))
∈ N → (((1st ‘𝐴) ·N
(2nd ‘𝐵))
<N ((1st ‘𝐵) ·N
(2nd ‘𝐴))
↔ (((1st ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐴) ·N
(2nd ‘𝐵)))
<N (((1st ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴))))) | 
| 14 | 12, 13 | syl 17 | . . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((1st ‘𝐴) ·N
(2nd ‘𝐵))
<N ((1st ‘𝐵) ·N
(2nd ‘𝐴))
↔ (((1st ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐴) ·N
(2nd ‘𝐵)))
<N (((1st ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴))))) | 
| 15 |  | fvex 6919 | . . . . . . . 8
⊢
(1st ‘𝐶) ∈ V | 
| 16 |  | fvex 6919 | . . . . . . . 8
⊢
(2nd ‘𝐶) ∈ V | 
| 17 |  | fvex 6919 | . . . . . . . 8
⊢
(1st ‘𝐴) ∈ V | 
| 18 |  | mulcompi 10936 | . . . . . . . 8
⊢ (𝑥
·N 𝑦) = (𝑦 ·N 𝑥) | 
| 19 |  | mulasspi 10937 | . . . . . . . 8
⊢ ((𝑥
·N 𝑦) ·N 𝑧) = (𝑥 ·N (𝑦
·N 𝑧)) | 
| 20 |  | fvex 6919 | . . . . . . . 8
⊢
(2nd ‘𝐵) ∈ V | 
| 21 | 15, 16, 17, 18, 19, 20 | caov4 7664 | . . . . . . 7
⊢
(((1st ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐴) ·N
(2nd ‘𝐵)))
= (((1st ‘𝐶) ·N
(1st ‘𝐴))
·N ((2nd ‘𝐶) ·N
(2nd ‘𝐵))) | 
| 22 |  | fvex 6919 | . . . . . . . 8
⊢
(1st ‘𝐵) ∈ V | 
| 23 |  | fvex 6919 | . . . . . . . 8
⊢
(2nd ‘𝐴) ∈ V | 
| 24 | 15, 16, 22, 18, 19, 23 | caov4 7664 | . . . . . . 7
⊢
(((1st ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴)))
= (((1st ‘𝐶) ·N
(1st ‘𝐵))
·N ((2nd ‘𝐶) ·N
(2nd ‘𝐴))) | 
| 25 | 21, 24 | breq12i 5152 | . . . . . 6
⊢
((((1st ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐴) ·N
(2nd ‘𝐵)))
<N (((1st ‘𝐶) ·N
(2nd ‘𝐶))
·N ((1st ‘𝐵) ·N
(2nd ‘𝐴)))
↔ (((1st ‘𝐶) ·N
(1st ‘𝐴))
·N ((2nd ‘𝐶) ·N
(2nd ‘𝐵)))
<N (((1st ‘𝐶) ·N
(1st ‘𝐵))
·N ((2nd ‘𝐶) ·N
(2nd ‘𝐴)))) | 
| 26 | 14, 25 | bitrdi 287 | . . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((1st ‘𝐴) ·N
(2nd ‘𝐵))
<N ((1st ‘𝐵) ·N
(2nd ‘𝐴))
↔ (((1st ‘𝐶) ·N
(1st ‘𝐴))
·N ((2nd ‘𝐶) ·N
(2nd ‘𝐵)))
<N (((1st ‘𝐶) ·N
(1st ‘𝐵))
·N ((2nd ‘𝐶) ·N
(2nd ‘𝐴))))) | 
| 27 |  | ordpipq 10982 | . . . . 5
⊢
(〈((1st ‘𝐶) ·N
(1st ‘𝐴)),
((2nd ‘𝐶)
·N (2nd ‘𝐴))〉 <pQ
〈((1st ‘𝐶) ·N
(1st ‘𝐵)),
((2nd ‘𝐶)
·N (2nd ‘𝐵))〉 ↔ (((1st
‘𝐶)
·N (1st ‘𝐴)) ·N
((2nd ‘𝐶)
·N (2nd ‘𝐵))) <N
(((1st ‘𝐶)
·N (1st ‘𝐵)) ·N
((2nd ‘𝐶)
·N (2nd ‘𝐴)))) | 
| 28 | 26, 27 | bitr4di 289 | . . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((1st ‘𝐴) ·N
(2nd ‘𝐵))
<N ((1st ‘𝐵) ·N
(2nd ‘𝐴))
↔ 〈((1st ‘𝐶) ·N
(1st ‘𝐴)),
((2nd ‘𝐶)
·N (2nd ‘𝐴))〉 <pQ
〈((1st ‘𝐶) ·N
(1st ‘𝐵)),
((2nd ‘𝐶)
·N (2nd ‘𝐵))〉)) | 
| 29 |  | elpqn 10965 | . . . . . . 7
⊢ (𝐴 ∈ Q →
𝐴 ∈ (N
× N)) | 
| 30 | 29 | 3ad2ant1 1134 | . . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐴
∈ (N × N)) | 
| 31 |  | mulpipq2 10979 | . . . . . 6
⊢ ((𝐶 ∈ (N ×
N) ∧ 𝐴
∈ (N × N)) → (𝐶 ·pQ 𝐴) = 〈((1st
‘𝐶)
·N (1st ‘𝐴)), ((2nd ‘𝐶)
·N (2nd ‘𝐴))〉) | 
| 32 | 6, 30, 31 | syl2anc 584 | . . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐶
·pQ 𝐴) = 〈((1st ‘𝐶)
·N (1st ‘𝐴)), ((2nd ‘𝐶)
·N (2nd ‘𝐴))〉) | 
| 33 |  | elpqn 10965 | . . . . . . 7
⊢ (𝐵 ∈ Q →
𝐵 ∈ (N
× N)) | 
| 34 | 33 | 3ad2ant2 1135 | . . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐵
∈ (N × N)) | 
| 35 |  | mulpipq2 10979 | . . . . . 6
⊢ ((𝐶 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐶 ·pQ 𝐵) = 〈((1st
‘𝐶)
·N (1st ‘𝐵)), ((2nd ‘𝐶)
·N (2nd ‘𝐵))〉) | 
| 36 | 6, 34, 35 | syl2anc 584 | . . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐶
·pQ 𝐵) = 〈((1st ‘𝐶)
·N (1st ‘𝐵)), ((2nd ‘𝐶)
·N (2nd ‘𝐵))〉) | 
| 37 | 32, 36 | breq12d 5156 | . . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐶
·pQ 𝐴) <pQ (𝐶
·pQ 𝐵) ↔ 〈((1st ‘𝐶)
·N (1st ‘𝐴)), ((2nd ‘𝐶)
·N (2nd ‘𝐴))〉 <pQ
〈((1st ‘𝐶) ·N
(1st ‘𝐵)),
((2nd ‘𝐶)
·N (2nd ‘𝐵))〉)) | 
| 38 | 28, 37 | bitr4d 282 | . . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((1st ‘𝐴) ·N
(2nd ‘𝐵))
<N ((1st ‘𝐵) ·N
(2nd ‘𝐴))
↔ (𝐶
·pQ 𝐴) <pQ (𝐶
·pQ 𝐵))) | 
| 39 |  | ordpinq 10983 | . . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
<Q 𝐵 ↔ ((1st ‘𝐴)
·N (2nd ‘𝐵)) <N
((1st ‘𝐵)
·N (2nd ‘𝐴)))) | 
| 40 | 39 | 3adant3 1133 | . . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
<Q 𝐵 ↔ ((1st ‘𝐴)
·N (2nd ‘𝐵)) <N
((1st ‘𝐵)
·N (2nd ‘𝐴)))) | 
| 41 |  | mulpqnq 10981 | . . . . . . 7
⊢ ((𝐶 ∈ Q ∧
𝐴 ∈ Q)
→ (𝐶
·Q 𝐴) = ([Q]‘(𝐶
·pQ 𝐴))) | 
| 42 | 41 | ancoms 458 | . . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐶 ∈ Q)
→ (𝐶
·Q 𝐴) = ([Q]‘(𝐶
·pQ 𝐴))) | 
| 43 | 42 | 3adant2 1132 | . . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐶
·Q 𝐴) = ([Q]‘(𝐶
·pQ 𝐴))) | 
| 44 |  | mulpqnq 10981 | . . . . . . 7
⊢ ((𝐶 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐶
·Q 𝐵) = ([Q]‘(𝐶
·pQ 𝐵))) | 
| 45 | 44 | ancoms 458 | . . . . . 6
⊢ ((𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ (𝐶
·Q 𝐵) = ([Q]‘(𝐶
·pQ 𝐵))) | 
| 46 | 45 | 3adant1 1131 | . . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐶
·Q 𝐵) = ([Q]‘(𝐶
·pQ 𝐵))) | 
| 47 | 43, 46 | breq12d 5156 | . . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐶
·Q 𝐴) <Q (𝐶
·Q 𝐵) ↔ ([Q]‘(𝐶
·pQ 𝐴)) <Q
([Q]‘(𝐶
·pQ 𝐵)))) | 
| 48 |  | lterpq 11010 | . . . 4
⊢ ((𝐶
·pQ 𝐴) <pQ (𝐶
·pQ 𝐵) ↔ ([Q]‘(𝐶
·pQ 𝐴)) <Q
([Q]‘(𝐶
·pQ 𝐵))) | 
| 49 | 47, 48 | bitr4di 289 | . . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐶
·Q 𝐴) <Q (𝐶
·Q 𝐵) ↔ (𝐶 ·pQ 𝐴)
<pQ (𝐶 ·pQ 𝐵))) | 
| 50 | 38, 40, 49 | 3bitr4d 311 | . 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
<Q 𝐵 ↔ (𝐶 ·Q 𝐴) <Q
(𝐶
·Q 𝐵))) | 
| 51 | 2, 3, 4, 50 | ndmovord 7623 | 1
⊢ (𝐶 ∈ Q →
(𝐴
<Q 𝐵 ↔ (𝐶 ·Q 𝐴) <Q
(𝐶
·Q 𝐵))) |