Proof of Theorem archnq
| Step | Hyp | Ref
| Expression |
| 1 | | elpqn 10965 |
. . . 4
⊢ (𝐴 ∈ Q →
𝐴 ∈ (N
× N)) |
| 2 | | xp1st 8046 |
. . . 4
⊢ (𝐴 ∈ (N ×
N) → (1st ‘𝐴) ∈ N) |
| 3 | 1, 2 | syl 17 |
. . 3
⊢ (𝐴 ∈ Q →
(1st ‘𝐴)
∈ N) |
| 4 | | 1pi 10923 |
. . 3
⊢
1o ∈ N |
| 5 | | addclpi 10932 |
. . 3
⊢
(((1st ‘𝐴) ∈ N ∧ 1o
∈ N) → ((1st ‘𝐴) +N 1o)
∈ N) |
| 6 | 3, 4, 5 | sylancl 586 |
. 2
⊢ (𝐴 ∈ Q →
((1st ‘𝐴)
+N 1o) ∈
N) |
| 7 | | xp2nd 8047 |
. . . . . 6
⊢ (𝐴 ∈ (N ×
N) → (2nd ‘𝐴) ∈ N) |
| 8 | 1, 7 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ Q →
(2nd ‘𝐴)
∈ N) |
| 9 | | mulclpi 10933 |
. . . . 5
⊢
((((1st ‘𝐴) +N 1o)
∈ N ∧ (2nd ‘𝐴) ∈ N) →
(((1st ‘𝐴)
+N 1o) ·N
(2nd ‘𝐴))
∈ N) |
| 10 | 6, 8, 9 | syl2anc 584 |
. . . 4
⊢ (𝐴 ∈ Q →
(((1st ‘𝐴)
+N 1o) ·N
(2nd ‘𝐴))
∈ N) |
| 11 | | eqid 2737 |
. . . . . . 7
⊢
((1st ‘𝐴) +N 1o)
= ((1st ‘𝐴) +N
1o) |
| 12 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑥 = 1o →
((1st ‘𝐴)
+N 𝑥) = ((1st ‘𝐴) +N
1o)) |
| 13 | 12 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑥 = 1o →
(((1st ‘𝐴)
+N 𝑥) = ((1st ‘𝐴) +N 1o)
↔ ((1st ‘𝐴) +N 1o)
= ((1st ‘𝐴) +N
1o))) |
| 14 | 13 | rspcev 3622 |
. . . . . . 7
⊢
((1o ∈ N ∧ ((1st
‘𝐴)
+N 1o) = ((1st ‘𝐴) +N
1o)) → ∃𝑥 ∈ N ((1st
‘𝐴)
+N 𝑥) = ((1st ‘𝐴) +N
1o)) |
| 15 | 4, 11, 14 | mp2an 692 |
. . . . . 6
⊢
∃𝑥 ∈
N ((1st ‘𝐴) +N 𝑥) = ((1st
‘𝐴)
+N 1o) |
| 16 | | ltexpi 10942 |
. . . . . 6
⊢
(((1st ‘𝐴) ∈ N ∧
((1st ‘𝐴)
+N 1o) ∈ N) →
((1st ‘𝐴)
<N ((1st ‘𝐴) +N 1o)
↔ ∃𝑥 ∈
N ((1st ‘𝐴) +N 𝑥) = ((1st
‘𝐴)
+N 1o))) |
| 17 | 15, 16 | mpbiri 258 |
. . . . 5
⊢
(((1st ‘𝐴) ∈ N ∧
((1st ‘𝐴)
+N 1o) ∈ N) →
(1st ‘𝐴)
<N ((1st ‘𝐴) +N
1o)) |
| 18 | 3, 6, 17 | syl2anc 584 |
. . . 4
⊢ (𝐴 ∈ Q →
(1st ‘𝐴)
<N ((1st ‘𝐴) +N
1o)) |
| 19 | | nlt1pi 10946 |
. . . . 5
⊢ ¬
(2nd ‘𝐴)
<N 1o |
| 20 | | ltmpi 10944 |
. . . . . . 7
⊢
(((1st ‘𝐴) +N 1o)
∈ N → ((2nd ‘𝐴) <N
1o ↔ (((1st ‘𝐴) +N 1o)
·N (2nd ‘𝐴)) <N
(((1st ‘𝐴)
+N 1o) ·N
1o))) |
| 21 | 6, 20 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ Q →
((2nd ‘𝐴)
<N 1o ↔ (((1st
‘𝐴)
+N 1o) ·N
(2nd ‘𝐴))
<N (((1st ‘𝐴) +N 1o)
·N 1o))) |
| 22 | | mulidpi 10926 |
. . . . . . . 8
⊢
(((1st ‘𝐴) +N 1o)
∈ N → (((1st ‘𝐴) +N 1o)
·N 1o) = ((1st
‘𝐴)
+N 1o)) |
| 23 | 6, 22 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ Q →
(((1st ‘𝐴)
+N 1o) ·N
1o) = ((1st ‘𝐴) +N
1o)) |
| 24 | 23 | breq2d 5155 |
. . . . . 6
⊢ (𝐴 ∈ Q →
((((1st ‘𝐴) +N 1o)
·N (2nd ‘𝐴)) <N
(((1st ‘𝐴)
+N 1o) ·N
1o) ↔ (((1st ‘𝐴) +N 1o)
·N (2nd ‘𝐴)) <N
((1st ‘𝐴)
+N 1o))) |
| 25 | 21, 24 | bitrd 279 |
. . . . 5
⊢ (𝐴 ∈ Q →
((2nd ‘𝐴)
<N 1o ↔ (((1st
‘𝐴)
+N 1o) ·N
(2nd ‘𝐴))
<N ((1st ‘𝐴) +N
1o))) |
| 26 | 19, 25 | mtbii 326 |
. . . 4
⊢ (𝐴 ∈ Q →
¬ (((1st ‘𝐴) +N 1o)
·N (2nd ‘𝐴)) <N
((1st ‘𝐴)
+N 1o)) |
| 27 | | ltsopi 10928 |
. . . . 5
⊢
<N Or N |
| 28 | | ltrelpi 10929 |
. . . . 5
⊢
<N ⊆ (N ×
N) |
| 29 | 27, 28 | sotri3 6150 |
. . . 4
⊢
(((((1st ‘𝐴) +N 1o)
·N (2nd ‘𝐴)) ∈ N ∧
(1st ‘𝐴)
<N ((1st ‘𝐴) +N 1o)
∧ ¬ (((1st ‘𝐴) +N 1o)
·N (2nd ‘𝐴)) <N
((1st ‘𝐴)
+N 1o)) → (1st ‘𝐴) <N
(((1st ‘𝐴)
+N 1o) ·N
(2nd ‘𝐴))) |
| 30 | 10, 18, 26, 29 | syl3anc 1373 |
. . 3
⊢ (𝐴 ∈ Q →
(1st ‘𝐴)
<N (((1st ‘𝐴) +N 1o)
·N (2nd ‘𝐴))) |
| 31 | | pinq 10967 |
. . . . . 6
⊢
(((1st ‘𝐴) +N 1o)
∈ N → 〈((1st ‘𝐴) +N
1o), 1o〉 ∈ Q) |
| 32 | 6, 31 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ Q →
〈((1st ‘𝐴) +N
1o), 1o〉 ∈ Q) |
| 33 | | ordpinq 10983 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
〈((1st ‘𝐴) +N
1o), 1o〉 ∈ Q) → (𝐴 <Q
〈((1st ‘𝐴) +N
1o), 1o〉 ↔ ((1st ‘𝐴)
·N (2nd
‘〈((1st ‘𝐴) +N
1o), 1o〉)) <N
((1st ‘〈((1st ‘𝐴) +N
1o), 1o〉) ·N
(2nd ‘𝐴)))) |
| 34 | 32, 33 | mpdan 687 |
. . . 4
⊢ (𝐴 ∈ Q →
(𝐴
<Q 〈((1st ‘𝐴) +N
1o), 1o〉 ↔ ((1st ‘𝐴)
·N (2nd
‘〈((1st ‘𝐴) +N
1o), 1o〉)) <N
((1st ‘〈((1st ‘𝐴) +N
1o), 1o〉) ·N
(2nd ‘𝐴)))) |
| 35 | | ovex 7464 |
. . . . . . . 8
⊢
((1st ‘𝐴) +N 1o)
∈ V |
| 36 | | 1oex 8516 |
. . . . . . . 8
⊢
1o ∈ V |
| 37 | 35, 36 | op2nd 8023 |
. . . . . . 7
⊢
(2nd ‘〈((1st ‘𝐴) +N
1o), 1o〉) = 1o |
| 38 | 37 | oveq2i 7442 |
. . . . . 6
⊢
((1st ‘𝐴) ·N
(2nd ‘〈((1st ‘𝐴) +N
1o), 1o〉)) = ((1st ‘𝐴)
·N 1o) |
| 39 | | mulidpi 10926 |
. . . . . . 7
⊢
((1st ‘𝐴) ∈ N →
((1st ‘𝐴)
·N 1o) = (1st
‘𝐴)) |
| 40 | 3, 39 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ Q →
((1st ‘𝐴)
·N 1o) = (1st
‘𝐴)) |
| 41 | 38, 40 | eqtrid 2789 |
. . . . 5
⊢ (𝐴 ∈ Q →
((1st ‘𝐴)
·N (2nd
‘〈((1st ‘𝐴) +N
1o), 1o〉)) = (1st ‘𝐴)) |
| 42 | 35, 36 | op1st 8022 |
. . . . . . 7
⊢
(1st ‘〈((1st ‘𝐴) +N
1o), 1o〉) = ((1st ‘𝐴) +N
1o) |
| 43 | 42 | oveq1i 7441 |
. . . . . 6
⊢
((1st ‘〈((1st ‘𝐴) +N
1o), 1o〉) ·N
(2nd ‘𝐴))
= (((1st ‘𝐴) +N 1o)
·N (2nd ‘𝐴)) |
| 44 | 43 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ Q →
((1st ‘〈((1st ‘𝐴) +N
1o), 1o〉) ·N
(2nd ‘𝐴))
= (((1st ‘𝐴) +N 1o)
·N (2nd ‘𝐴))) |
| 45 | 41, 44 | breq12d 5156 |
. . . 4
⊢ (𝐴 ∈ Q →
(((1st ‘𝐴)
·N (2nd
‘〈((1st ‘𝐴) +N
1o), 1o〉)) <N
((1st ‘〈((1st ‘𝐴) +N
1o), 1o〉) ·N
(2nd ‘𝐴))
↔ (1st ‘𝐴) <N
(((1st ‘𝐴)
+N 1o) ·N
(2nd ‘𝐴)))) |
| 46 | 34, 45 | bitrd 279 |
. . 3
⊢ (𝐴 ∈ Q →
(𝐴
<Q 〈((1st ‘𝐴) +N
1o), 1o〉 ↔ (1st ‘𝐴) <N
(((1st ‘𝐴)
+N 1o) ·N
(2nd ‘𝐴)))) |
| 47 | 30, 46 | mpbird 257 |
. 2
⊢ (𝐴 ∈ Q →
𝐴
<Q 〈((1st ‘𝐴) +N
1o), 1o〉) |
| 48 | | opeq1 4873 |
. . . 4
⊢ (𝑥 = ((1st ‘𝐴) +N
1o) → 〈𝑥, 1o〉 =
〈((1st ‘𝐴) +N
1o), 1o〉) |
| 49 | 48 | breq2d 5155 |
. . 3
⊢ (𝑥 = ((1st ‘𝐴) +N
1o) → (𝐴
<Q 〈𝑥, 1o〉 ↔ 𝐴 <Q
〈((1st ‘𝐴) +N
1o), 1o〉)) |
| 50 | 49 | rspcev 3622 |
. 2
⊢
((((1st ‘𝐴) +N 1o)
∈ N ∧ 𝐴 <Q
〈((1st ‘𝐴) +N
1o), 1o〉) → ∃𝑥 ∈ N 𝐴 <Q 〈𝑥,
1o〉) |
| 51 | 6, 47, 50 | syl2anc 584 |
1
⊢ (𝐴 ∈ Q →
∃𝑥 ∈
N 𝐴
<Q 〈𝑥, 1o〉) |