| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elpqn 10966 | . . . . . . 7
⊢ (𝑥 ∈ Q →
𝑥 ∈ (N
× N)) | 
| 2 | 1 | adantr 480 | . . . . . 6
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ 𝑥 ∈
(N × N)) | 
| 3 |  | xp1st 8047 | . . . . . 6
⊢ (𝑥 ∈ (N ×
N) → (1st ‘𝑥) ∈ N) | 
| 4 | 2, 3 | syl 17 | . . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (1st ‘𝑥) ∈ N) | 
| 5 |  | elpqn 10966 | . . . . . . 7
⊢ (𝑦 ∈ Q →
𝑦 ∈ (N
× N)) | 
| 6 | 5 | adantl 481 | . . . . . 6
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ 𝑦 ∈
(N × N)) | 
| 7 |  | xp2nd 8048 | . . . . . 6
⊢ (𝑦 ∈ (N ×
N) → (2nd ‘𝑦) ∈ N) | 
| 8 | 6, 7 | syl 17 | . . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (2nd ‘𝑦) ∈ N) | 
| 9 |  | mulclpi 10934 | . . . . 5
⊢
(((1st ‘𝑥) ∈ N ∧
(2nd ‘𝑦)
∈ N) → ((1st ‘𝑥) ·N
(2nd ‘𝑦))
∈ N) | 
| 10 | 4, 8, 9 | syl2anc 584 | . . . 4
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ ((1st ‘𝑥) ·N
(2nd ‘𝑦))
∈ N) | 
| 11 |  | xp1st 8047 | . . . . . 6
⊢ (𝑦 ∈ (N ×
N) → (1st ‘𝑦) ∈ N) | 
| 12 | 6, 11 | syl 17 | . . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (1st ‘𝑦) ∈ N) | 
| 13 |  | xp2nd 8048 | . . . . . 6
⊢ (𝑥 ∈ (N ×
N) → (2nd ‘𝑥) ∈ N) | 
| 14 | 2, 13 | syl 17 | . . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (2nd ‘𝑥) ∈ N) | 
| 15 |  | mulclpi 10934 | . . . . 5
⊢
(((1st ‘𝑦) ∈ N ∧
(2nd ‘𝑥)
∈ N) → ((1st ‘𝑦) ·N
(2nd ‘𝑥))
∈ N) | 
| 16 | 12, 14, 15 | syl2anc 584 | . . . 4
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ ((1st ‘𝑦) ·N
(2nd ‘𝑥))
∈ N) | 
| 17 |  | ltsopi 10929 | . . . . 5
⊢ 
<N Or N | 
| 18 |  | sotric 5621 | . . . . 5
⊢ ((
<N Or N ∧ (((1st
‘𝑥)
·N (2nd ‘𝑦)) ∈ N ∧
((1st ‘𝑦)
·N (2nd ‘𝑥)) ∈ N)) →
(((1st ‘𝑥)
·N (2nd ‘𝑦)) <N
((1st ‘𝑦)
·N (2nd ‘𝑥)) ↔ ¬ (((1st
‘𝑥)
·N (2nd ‘𝑦)) = ((1st ‘𝑦)
·N (2nd ‘𝑥)) ∨ ((1st ‘𝑦)
·N (2nd ‘𝑥)) <N
((1st ‘𝑥)
·N (2nd ‘𝑦))))) | 
| 19 | 17, 18 | mpan 690 | . . . 4
⊢
((((1st ‘𝑥) ·N
(2nd ‘𝑦))
∈ N ∧ ((1st ‘𝑦) ·N
(2nd ‘𝑥))
∈ N) → (((1st ‘𝑥) ·N
(2nd ‘𝑦))
<N ((1st ‘𝑦) ·N
(2nd ‘𝑥))
↔ ¬ (((1st ‘𝑥) ·N
(2nd ‘𝑦))
= ((1st ‘𝑦) ·N
(2nd ‘𝑥))
∨ ((1st ‘𝑦) ·N
(2nd ‘𝑥))
<N ((1st ‘𝑥) ·N
(2nd ‘𝑦))))) | 
| 20 | 10, 16, 19 | syl2anc 584 | . . 3
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (((1st ‘𝑥) ·N
(2nd ‘𝑦))
<N ((1st ‘𝑦) ·N
(2nd ‘𝑥))
↔ ¬ (((1st ‘𝑥) ·N
(2nd ‘𝑦))
= ((1st ‘𝑦) ·N
(2nd ‘𝑥))
∨ ((1st ‘𝑦) ·N
(2nd ‘𝑥))
<N ((1st ‘𝑥) ·N
(2nd ‘𝑦))))) | 
| 21 |  | ordpinq 10984 | . . 3
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥
<Q 𝑦 ↔ ((1st ‘𝑥)
·N (2nd ‘𝑦)) <N
((1st ‘𝑦)
·N (2nd ‘𝑥)))) | 
| 22 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = 𝑦 → (1st ‘𝑥) = (1st ‘𝑦)) | 
| 23 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → (2nd ‘𝑥) = (2nd ‘𝑦)) | 
| 24 | 23 | eqcomd 2742 | . . . . . . 7
⊢ (𝑥 = 𝑦 → (2nd ‘𝑦) = (2nd ‘𝑥)) | 
| 25 | 22, 24 | oveq12d 7450 | . . . . . 6
⊢ (𝑥 = 𝑦 → ((1st ‘𝑥)
·N (2nd ‘𝑦)) = ((1st ‘𝑦)
·N (2nd ‘𝑥))) | 
| 26 |  | enqbreq2 10961 | . . . . . . . 8
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) → (𝑥 ~Q 𝑦 ↔ ((1st
‘𝑥)
·N (2nd ‘𝑦)) = ((1st ‘𝑦)
·N (2nd ‘𝑥)))) | 
| 27 | 1, 5, 26 | syl2an 596 | . . . . . . 7
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥
~Q 𝑦 ↔ ((1st ‘𝑥)
·N (2nd ‘𝑦)) = ((1st ‘𝑦)
·N (2nd ‘𝑥)))) | 
| 28 |  | enqeq 10975 | . . . . . . . 8
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑥
~Q 𝑦) → 𝑥 = 𝑦) | 
| 29 | 28 | 3expia 1121 | . . . . . . 7
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥
~Q 𝑦 → 𝑥 = 𝑦)) | 
| 30 | 27, 29 | sylbird 260 | . . . . . 6
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (((1st ‘𝑥) ·N
(2nd ‘𝑦))
= ((1st ‘𝑦) ·N
(2nd ‘𝑥))
→ 𝑥 = 𝑦)) | 
| 31 | 25, 30 | impbid2 226 | . . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥 = 𝑦 ↔ ((1st
‘𝑥)
·N (2nd ‘𝑦)) = ((1st ‘𝑦)
·N (2nd ‘𝑥)))) | 
| 32 |  | ordpinq 10984 | . . . . . 6
⊢ ((𝑦 ∈ Q ∧
𝑥 ∈ Q)
→ (𝑦
<Q 𝑥 ↔ ((1st ‘𝑦)
·N (2nd ‘𝑥)) <N
((1st ‘𝑥)
·N (2nd ‘𝑦)))) | 
| 33 | 32 | ancoms 458 | . . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑦
<Q 𝑥 ↔ ((1st ‘𝑦)
·N (2nd ‘𝑥)) <N
((1st ‘𝑥)
·N (2nd ‘𝑦)))) | 
| 34 | 31, 33 | orbi12d 918 | . . . 4
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ ((𝑥 = 𝑦 ∨ 𝑦 <Q 𝑥) ↔ (((1st
‘𝑥)
·N (2nd ‘𝑦)) = ((1st ‘𝑦)
·N (2nd ‘𝑥)) ∨ ((1st ‘𝑦)
·N (2nd ‘𝑥)) <N
((1st ‘𝑥)
·N (2nd ‘𝑦))))) | 
| 35 | 34 | notbid 318 | . . 3
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (¬ (𝑥 = 𝑦 ∨ 𝑦 <Q 𝑥) ↔ ¬ (((1st
‘𝑥)
·N (2nd ‘𝑦)) = ((1st ‘𝑦)
·N (2nd ‘𝑥)) ∨ ((1st ‘𝑦)
·N (2nd ‘𝑥)) <N
((1st ‘𝑥)
·N (2nd ‘𝑦))))) | 
| 36 | 20, 21, 35 | 3bitr4d 311 | . 2
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥
<Q 𝑦 ↔ ¬ (𝑥 = 𝑦 ∨ 𝑦 <Q 𝑥))) | 
| 37 | 21 | 3adant3 1132 | . . . . . 6
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → (𝑥
<Q 𝑦 ↔ ((1st ‘𝑥)
·N (2nd ‘𝑦)) <N
((1st ‘𝑦)
·N (2nd ‘𝑥)))) | 
| 38 |  | elpqn 10966 | . . . . . . . 8
⊢ (𝑧 ∈ Q →
𝑧 ∈ (N
× N)) | 
| 39 | 38 | 3ad2ant3 1135 | . . . . . . 7
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → 𝑧
∈ (N × N)) | 
| 40 |  | xp2nd 8048 | . . . . . . 7
⊢ (𝑧 ∈ (N ×
N) → (2nd ‘𝑧) ∈ N) | 
| 41 |  | ltmpi 10945 | . . . . . . 7
⊢
((2nd ‘𝑧) ∈ N →
(((1st ‘𝑥)
·N (2nd ‘𝑦)) <N
((1st ‘𝑦)
·N (2nd ‘𝑥)) ↔ ((2nd ‘𝑧)
·N ((1st ‘𝑥) ·N
(2nd ‘𝑦)))
<N ((2nd ‘𝑧) ·N
((1st ‘𝑦)
·N (2nd ‘𝑥))))) | 
| 42 | 39, 40, 41 | 3syl 18 | . . . . . 6
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → (((1st ‘𝑥) ·N
(2nd ‘𝑦))
<N ((1st ‘𝑦) ·N
(2nd ‘𝑥))
↔ ((2nd ‘𝑧) ·N
((1st ‘𝑥)
·N (2nd ‘𝑦))) <N
((2nd ‘𝑧)
·N ((1st ‘𝑦) ·N
(2nd ‘𝑥))))) | 
| 43 | 37, 42 | bitrd 279 | . . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → (𝑥
<Q 𝑦 ↔ ((2nd ‘𝑧)
·N ((1st ‘𝑥) ·N
(2nd ‘𝑦)))
<N ((2nd ‘𝑧) ·N
((1st ‘𝑦)
·N (2nd ‘𝑥))))) | 
| 44 |  | ordpinq 10984 | . . . . . . 7
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦
<Q 𝑧 ↔ ((1st ‘𝑦)
·N (2nd ‘𝑧)) <N
((1st ‘𝑧)
·N (2nd ‘𝑦)))) | 
| 45 | 44 | 3adant1 1130 | . . . . . 6
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → (𝑦
<Q 𝑧 ↔ ((1st ‘𝑦)
·N (2nd ‘𝑧)) <N
((1st ‘𝑧)
·N (2nd ‘𝑦)))) | 
| 46 | 1 | 3ad2ant1 1133 | . . . . . . 7
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → 𝑥
∈ (N × N)) | 
| 47 |  | ltmpi 10945 | . . . . . . 7
⊢
((2nd ‘𝑥) ∈ N →
(((1st ‘𝑦)
·N (2nd ‘𝑧)) <N
((1st ‘𝑧)
·N (2nd ‘𝑦)) ↔ ((2nd ‘𝑥)
·N ((1st ‘𝑦) ·N
(2nd ‘𝑧)))
<N ((2nd ‘𝑥) ·N
((1st ‘𝑧)
·N (2nd ‘𝑦))))) | 
| 48 | 46, 13, 47 | 3syl 18 | . . . . . 6
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → (((1st ‘𝑦) ·N
(2nd ‘𝑧))
<N ((1st ‘𝑧) ·N
(2nd ‘𝑦))
↔ ((2nd ‘𝑥) ·N
((1st ‘𝑦)
·N (2nd ‘𝑧))) <N
((2nd ‘𝑥)
·N ((1st ‘𝑧) ·N
(2nd ‘𝑦))))) | 
| 49 | 45, 48 | bitrd 279 | . . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → (𝑦
<Q 𝑧 ↔ ((2nd ‘𝑥)
·N ((1st ‘𝑦) ·N
(2nd ‘𝑧)))
<N ((2nd ‘𝑥) ·N
((1st ‘𝑧)
·N (2nd ‘𝑦))))) | 
| 50 | 43, 49 | anbi12d 632 | . . . 4
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → ((𝑥
<Q 𝑦 ∧ 𝑦 <Q 𝑧) ↔ (((2nd
‘𝑧)
·N ((1st ‘𝑥) ·N
(2nd ‘𝑦)))
<N ((2nd ‘𝑧) ·N
((1st ‘𝑦)
·N (2nd ‘𝑥))) ∧ ((2nd ‘𝑥)
·N ((1st ‘𝑦) ·N
(2nd ‘𝑧)))
<N ((2nd ‘𝑥) ·N
((1st ‘𝑧)
·N (2nd ‘𝑦)))))) | 
| 51 |  | fvex 6918 | . . . . . . 7
⊢
(2nd ‘𝑥) ∈ V | 
| 52 |  | fvex 6918 | . . . . . . 7
⊢
(1st ‘𝑦) ∈ V | 
| 53 |  | fvex 6918 | . . . . . . 7
⊢
(2nd ‘𝑧) ∈ V | 
| 54 |  | mulcompi 10937 | . . . . . . 7
⊢ (𝑟
·N 𝑠) = (𝑠 ·N 𝑟) | 
| 55 |  | mulasspi 10938 | . . . . . . 7
⊢ ((𝑟
·N 𝑠) ·N 𝑡) = (𝑟 ·N (𝑠
·N 𝑡)) | 
| 56 | 51, 52, 53, 54, 55 | caov13 7664 | . . . . . 6
⊢
((2nd ‘𝑥) ·N
((1st ‘𝑦)
·N (2nd ‘𝑧))) = ((2nd ‘𝑧)
·N ((1st ‘𝑦) ·N
(2nd ‘𝑥))) | 
| 57 |  | fvex 6918 | . . . . . . 7
⊢
(1st ‘𝑧) ∈ V | 
| 58 |  | fvex 6918 | . . . . . . 7
⊢
(2nd ‘𝑦) ∈ V | 
| 59 | 51, 57, 58, 54, 55 | caov13 7664 | . . . . . 6
⊢
((2nd ‘𝑥) ·N
((1st ‘𝑧)
·N (2nd ‘𝑦))) = ((2nd ‘𝑦)
·N ((1st ‘𝑧) ·N
(2nd ‘𝑥))) | 
| 60 | 56, 59 | breq12i 5151 | . . . . 5
⊢
(((2nd ‘𝑥) ·N
((1st ‘𝑦)
·N (2nd ‘𝑧))) <N
((2nd ‘𝑥)
·N ((1st ‘𝑧) ·N
(2nd ‘𝑦)))
↔ ((2nd ‘𝑧) ·N
((1st ‘𝑦)
·N (2nd ‘𝑥))) <N
((2nd ‘𝑦)
·N ((1st ‘𝑧) ·N
(2nd ‘𝑥)))) | 
| 61 |  | fvex 6918 | . . . . . . 7
⊢
(1st ‘𝑥) ∈ V | 
| 62 | 53, 61, 58, 54, 55 | caov13 7664 | . . . . . 6
⊢
((2nd ‘𝑧) ·N
((1st ‘𝑥)
·N (2nd ‘𝑦))) = ((2nd ‘𝑦)
·N ((1st ‘𝑥) ·N
(2nd ‘𝑧))) | 
| 63 |  | ltrelpi 10930 | . . . . . . 7
⊢ 
<N ⊆ (N ×
N) | 
| 64 | 17, 63 | sotri 6146 | . . . . . 6
⊢
((((2nd ‘𝑧) ·N
((1st ‘𝑥)
·N (2nd ‘𝑦))) <N
((2nd ‘𝑧)
·N ((1st ‘𝑦) ·N
(2nd ‘𝑥)))
∧ ((2nd ‘𝑧) ·N
((1st ‘𝑦)
·N (2nd ‘𝑥))) <N
((2nd ‘𝑦)
·N ((1st ‘𝑧) ·N
(2nd ‘𝑥)))) → ((2nd ‘𝑧)
·N ((1st ‘𝑥) ·N
(2nd ‘𝑦)))
<N ((2nd ‘𝑦) ·N
((1st ‘𝑧)
·N (2nd ‘𝑥)))) | 
| 65 | 62, 64 | eqbrtrrid 5178 | . . . . 5
⊢
((((2nd ‘𝑧) ·N
((1st ‘𝑥)
·N (2nd ‘𝑦))) <N
((2nd ‘𝑧)
·N ((1st ‘𝑦) ·N
(2nd ‘𝑥)))
∧ ((2nd ‘𝑧) ·N
((1st ‘𝑦)
·N (2nd ‘𝑥))) <N
((2nd ‘𝑦)
·N ((1st ‘𝑧) ·N
(2nd ‘𝑥)))) → ((2nd ‘𝑦)
·N ((1st ‘𝑥) ·N
(2nd ‘𝑧)))
<N ((2nd ‘𝑦) ·N
((1st ‘𝑧)
·N (2nd ‘𝑥)))) | 
| 66 | 60, 65 | sylan2b 594 | . . . 4
⊢
((((2nd ‘𝑧) ·N
((1st ‘𝑥)
·N (2nd ‘𝑦))) <N
((2nd ‘𝑧)
·N ((1st ‘𝑦) ·N
(2nd ‘𝑥)))
∧ ((2nd ‘𝑥) ·N
((1st ‘𝑦)
·N (2nd ‘𝑧))) <N
((2nd ‘𝑥)
·N ((1st ‘𝑧) ·N
(2nd ‘𝑦)))) → ((2nd ‘𝑦)
·N ((1st ‘𝑥) ·N
(2nd ‘𝑧)))
<N ((2nd ‘𝑦) ·N
((1st ‘𝑧)
·N (2nd ‘𝑥)))) | 
| 67 | 50, 66 | biimtrdi 253 | . . 3
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → ((𝑥
<Q 𝑦 ∧ 𝑦 <Q 𝑧) → ((2nd
‘𝑦)
·N ((1st ‘𝑥) ·N
(2nd ‘𝑧)))
<N ((2nd ‘𝑦) ·N
((1st ‘𝑧)
·N (2nd ‘𝑥))))) | 
| 68 |  | ordpinq 10984 | . . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑥
<Q 𝑧 ↔ ((1st ‘𝑥)
·N (2nd ‘𝑧)) <N
((1st ‘𝑧)
·N (2nd ‘𝑥)))) | 
| 69 | 68 | 3adant2 1131 | . . . 4
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → (𝑥
<Q 𝑧 ↔ ((1st ‘𝑥)
·N (2nd ‘𝑧)) <N
((1st ‘𝑧)
·N (2nd ‘𝑥)))) | 
| 70 | 5 | 3ad2ant2 1134 | . . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → 𝑦
∈ (N × N)) | 
| 71 |  | ltmpi 10945 | . . . . 5
⊢
((2nd ‘𝑦) ∈ N →
(((1st ‘𝑥)
·N (2nd ‘𝑧)) <N
((1st ‘𝑧)
·N (2nd ‘𝑥)) ↔ ((2nd ‘𝑦)
·N ((1st ‘𝑥) ·N
(2nd ‘𝑧)))
<N ((2nd ‘𝑦) ·N
((1st ‘𝑧)
·N (2nd ‘𝑥))))) | 
| 72 | 70, 7, 71 | 3syl 18 | . . . 4
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → (((1st ‘𝑥) ·N
(2nd ‘𝑧))
<N ((1st ‘𝑧) ·N
(2nd ‘𝑥))
↔ ((2nd ‘𝑦) ·N
((1st ‘𝑥)
·N (2nd ‘𝑧))) <N
((2nd ‘𝑦)
·N ((1st ‘𝑧) ·N
(2nd ‘𝑥))))) | 
| 73 | 69, 72 | bitrd 279 | . . 3
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → (𝑥
<Q 𝑧 ↔ ((2nd ‘𝑦)
·N ((1st ‘𝑥) ·N
(2nd ‘𝑧)))
<N ((2nd ‘𝑦) ·N
((1st ‘𝑧)
·N (2nd ‘𝑥))))) | 
| 74 | 67, 73 | sylibrd 259 | . 2
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → ((𝑥
<Q 𝑦 ∧ 𝑦 <Q 𝑧) → 𝑥 <Q 𝑧)) | 
| 75 | 36, 74 | isso2i 5628 | 1
⊢ 
<Q Or Q |