Proof of Theorem archnq
Step | Hyp | Ref
| Expression |
1 | | elpqn 9747 |
. . . 4
⊢ (𝐴 ∈ Q →
𝐴 ∈ (N
× N)) |
2 | | xp1st 7198 |
. . . 4
⊢ (𝐴 ∈ (N ×
N) → (1st ‘𝐴) ∈ N) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝐴 ∈ Q →
(1st ‘𝐴)
∈ N) |
4 | | 1pi 9705 |
. . 3
⊢
1𝑜 ∈ N |
5 | | addclpi 9714 |
. . 3
⊢
(((1st ‘𝐴) ∈ N ∧
1𝑜 ∈ N) → ((1st
‘𝐴)
+N 1𝑜) ∈
N) |
6 | 3, 4, 5 | sylancl 694 |
. 2
⊢ (𝐴 ∈ Q →
((1st ‘𝐴)
+N 1𝑜) ∈
N) |
7 | | xp2nd 7199 |
. . . . . 6
⊢ (𝐴 ∈ (N ×
N) → (2nd ‘𝐴) ∈ N) |
8 | 1, 7 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ Q →
(2nd ‘𝐴)
∈ N) |
9 | | mulclpi 9715 |
. . . . 5
⊢
((((1st ‘𝐴) +N
1𝑜) ∈ N ∧ (2nd
‘𝐴) ∈
N) → (((1st ‘𝐴) +N
1𝑜) ·N (2nd
‘𝐴)) ∈
N) |
10 | 6, 8, 9 | syl2anc 693 |
. . . 4
⊢ (𝐴 ∈ Q →
(((1st ‘𝐴)
+N 1𝑜)
·N (2nd ‘𝐴)) ∈ N) |
11 | | eqid 2622 |
. . . . . . 7
⊢
((1st ‘𝐴) +N
1𝑜) = ((1st ‘𝐴) +N
1𝑜) |
12 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑥 = 1𝑜 →
((1st ‘𝐴)
+N 𝑥) = ((1st ‘𝐴) +N
1𝑜)) |
13 | 12 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑥 = 1𝑜 →
(((1st ‘𝐴)
+N 𝑥) = ((1st ‘𝐴) +N
1𝑜) ↔ ((1st ‘𝐴) +N
1𝑜) = ((1st ‘𝐴) +N
1𝑜))) |
14 | 13 | rspcev 3309 |
. . . . . . 7
⊢
((1𝑜 ∈ N ∧ ((1st
‘𝐴)
+N 1𝑜) = ((1st
‘𝐴)
+N 1𝑜)) → ∃𝑥 ∈ N
((1st ‘𝐴)
+N 𝑥) = ((1st ‘𝐴) +N
1𝑜)) |
15 | 4, 11, 14 | mp2an 708 |
. . . . . 6
⊢
∃𝑥 ∈
N ((1st ‘𝐴) +N 𝑥) = ((1st
‘𝐴)
+N 1𝑜) |
16 | | ltexpi 9724 |
. . . . . 6
⊢
(((1st ‘𝐴) ∈ N ∧
((1st ‘𝐴)
+N 1𝑜) ∈ N)
→ ((1st ‘𝐴) <N
((1st ‘𝐴)
+N 1𝑜) ↔ ∃𝑥 ∈ N
((1st ‘𝐴)
+N 𝑥) = ((1st ‘𝐴) +N
1𝑜))) |
17 | 15, 16 | mpbiri 248 |
. . . . 5
⊢
(((1st ‘𝐴) ∈ N ∧
((1st ‘𝐴)
+N 1𝑜) ∈ N)
→ (1st ‘𝐴) <N
((1st ‘𝐴)
+N 1𝑜)) |
18 | 3, 6, 17 | syl2anc 693 |
. . . 4
⊢ (𝐴 ∈ Q →
(1st ‘𝐴)
<N ((1st ‘𝐴) +N
1𝑜)) |
19 | | nlt1pi 9728 |
. . . . 5
⊢ ¬
(2nd ‘𝐴)
<N 1𝑜 |
20 | | ltmpi 9726 |
. . . . . . 7
⊢
(((1st ‘𝐴) +N
1𝑜) ∈ N → ((2nd
‘𝐴)
<N 1𝑜 ↔ (((1st
‘𝐴)
+N 1𝑜)
·N (2nd ‘𝐴)) <N
(((1st ‘𝐴)
+N 1𝑜)
·N 1𝑜))) |
21 | 6, 20 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ Q →
((2nd ‘𝐴)
<N 1𝑜 ↔ (((1st
‘𝐴)
+N 1𝑜)
·N (2nd ‘𝐴)) <N
(((1st ‘𝐴)
+N 1𝑜)
·N 1𝑜))) |
22 | | mulidpi 9708 |
. . . . . . . 8
⊢
(((1st ‘𝐴) +N
1𝑜) ∈ N → (((1st
‘𝐴)
+N 1𝑜)
·N 1𝑜) = ((1st
‘𝐴)
+N 1𝑜)) |
23 | 6, 22 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ Q →
(((1st ‘𝐴)
+N 1𝑜)
·N 1𝑜) = ((1st
‘𝐴)
+N 1𝑜)) |
24 | 23 | breq2d 4665 |
. . . . . 6
⊢ (𝐴 ∈ Q →
((((1st ‘𝐴) +N
1𝑜) ·N (2nd
‘𝐴))
<N (((1st ‘𝐴) +N
1𝑜) ·N
1𝑜) ↔ (((1st ‘𝐴) +N
1𝑜) ·N (2nd
‘𝐴))
<N ((1st ‘𝐴) +N
1𝑜))) |
25 | 21, 24 | bitrd 268 |
. . . . 5
⊢ (𝐴 ∈ Q →
((2nd ‘𝐴)
<N 1𝑜 ↔ (((1st
‘𝐴)
+N 1𝑜)
·N (2nd ‘𝐴)) <N
((1st ‘𝐴)
+N 1𝑜))) |
26 | 19, 25 | mtbii 316 |
. . . 4
⊢ (𝐴 ∈ Q →
¬ (((1st ‘𝐴) +N
1𝑜) ·N (2nd
‘𝐴))
<N ((1st ‘𝐴) +N
1𝑜)) |
27 | | ltsopi 9710 |
. . . . 5
⊢
<N Or N |
28 | | ltrelpi 9711 |
. . . . 5
⊢
<N ⊆ (N ×
N) |
29 | 27, 28 | sotri3 5526 |
. . . 4
⊢
(((((1st ‘𝐴) +N
1𝑜) ·N (2nd
‘𝐴)) ∈
N ∧ (1st ‘𝐴) <N
((1st ‘𝐴)
+N 1𝑜) ∧ ¬
(((1st ‘𝐴)
+N 1𝑜)
·N (2nd ‘𝐴)) <N
((1st ‘𝐴)
+N 1𝑜)) → (1st
‘𝐴)
<N (((1st ‘𝐴) +N
1𝑜) ·N (2nd
‘𝐴))) |
30 | 10, 18, 26, 29 | syl3anc 1326 |
. . 3
⊢ (𝐴 ∈ Q →
(1st ‘𝐴)
<N (((1st ‘𝐴) +N
1𝑜) ·N (2nd
‘𝐴))) |
31 | | pinq 9749 |
. . . . . 6
⊢
(((1st ‘𝐴) +N
1𝑜) ∈ N → 〈((1st
‘𝐴)
+N 1𝑜), 1𝑜〉
∈ Q) |
32 | 6, 31 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ Q →
〈((1st ‘𝐴) +N
1𝑜), 1𝑜〉 ∈
Q) |
33 | | ordpinq 9765 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
〈((1st ‘𝐴) +N
1𝑜), 1𝑜〉 ∈ Q)
→ (𝐴
<Q 〈((1st ‘𝐴) +N
1𝑜), 1𝑜〉 ↔ ((1st
‘𝐴)
·N (2nd
‘〈((1st ‘𝐴) +N
1𝑜), 1𝑜〉))
<N ((1st ‘〈((1st
‘𝐴)
+N 1𝑜),
1𝑜〉) ·N (2nd
‘𝐴)))) |
34 | 32, 33 | mpdan 702 |
. . . 4
⊢ (𝐴 ∈ Q →
(𝐴
<Q 〈((1st ‘𝐴) +N
1𝑜), 1𝑜〉 ↔ ((1st
‘𝐴)
·N (2nd
‘〈((1st ‘𝐴) +N
1𝑜), 1𝑜〉))
<N ((1st ‘〈((1st
‘𝐴)
+N 1𝑜),
1𝑜〉) ·N (2nd
‘𝐴)))) |
35 | | ovex 6678 |
. . . . . . . 8
⊢
((1st ‘𝐴) +N
1𝑜) ∈ V |
36 | 4 | elexi 3213 |
. . . . . . . 8
⊢
1𝑜 ∈ V |
37 | 35, 36 | op2nd 7177 |
. . . . . . 7
⊢
(2nd ‘〈((1st ‘𝐴) +N
1𝑜), 1𝑜〉) =
1𝑜 |
38 | 37 | oveq2i 6661 |
. . . . . 6
⊢
((1st ‘𝐴) ·N
(2nd ‘〈((1st ‘𝐴) +N
1𝑜), 1𝑜〉)) = ((1st
‘𝐴)
·N 1𝑜) |
39 | | mulidpi 9708 |
. . . . . . 7
⊢
((1st ‘𝐴) ∈ N →
((1st ‘𝐴)
·N 1𝑜) = (1st
‘𝐴)) |
40 | 3, 39 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ Q →
((1st ‘𝐴)
·N 1𝑜) = (1st
‘𝐴)) |
41 | 38, 40 | syl5eq 2668 |
. . . . 5
⊢ (𝐴 ∈ Q →
((1st ‘𝐴)
·N (2nd
‘〈((1st ‘𝐴) +N
1𝑜), 1𝑜〉)) = (1st
‘𝐴)) |
42 | 35, 36 | op1st 7176 |
. . . . . . 7
⊢
(1st ‘〈((1st ‘𝐴) +N
1𝑜), 1𝑜〉) = ((1st
‘𝐴)
+N 1𝑜) |
43 | 42 | oveq1i 6660 |
. . . . . 6
⊢
((1st ‘〈((1st ‘𝐴) +N
1𝑜), 1𝑜〉)
·N (2nd ‘𝐴)) = (((1st ‘𝐴) +N
1𝑜) ·N (2nd
‘𝐴)) |
44 | 43 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ Q →
((1st ‘〈((1st ‘𝐴) +N
1𝑜), 1𝑜〉)
·N (2nd ‘𝐴)) = (((1st ‘𝐴) +N
1𝑜) ·N (2nd
‘𝐴))) |
45 | 41, 44 | breq12d 4666 |
. . . 4
⊢ (𝐴 ∈ Q →
(((1st ‘𝐴)
·N (2nd
‘〈((1st ‘𝐴) +N
1𝑜), 1𝑜〉))
<N ((1st ‘〈((1st
‘𝐴)
+N 1𝑜),
1𝑜〉) ·N (2nd
‘𝐴)) ↔
(1st ‘𝐴)
<N (((1st ‘𝐴) +N
1𝑜) ·N (2nd
‘𝐴)))) |
46 | 34, 45 | bitrd 268 |
. . 3
⊢ (𝐴 ∈ Q →
(𝐴
<Q 〈((1st ‘𝐴) +N
1𝑜), 1𝑜〉 ↔ (1st
‘𝐴)
<N (((1st ‘𝐴) +N
1𝑜) ·N (2nd
‘𝐴)))) |
47 | 30, 46 | mpbird 247 |
. 2
⊢ (𝐴 ∈ Q →
𝐴
<Q 〈((1st ‘𝐴) +N
1𝑜), 1𝑜〉) |
48 | | opeq1 4402 |
. . . 4
⊢ (𝑥 = ((1st ‘𝐴) +N
1𝑜) → 〈𝑥, 1𝑜〉 =
〈((1st ‘𝐴) +N
1𝑜), 1𝑜〉) |
49 | 48 | breq2d 4665 |
. . 3
⊢ (𝑥 = ((1st ‘𝐴) +N
1𝑜) → (𝐴 <Q 〈𝑥, 1𝑜〉
↔ 𝐴
<Q 〈((1st ‘𝐴) +N
1𝑜), 1𝑜〉)) |
50 | 49 | rspcev 3309 |
. 2
⊢
((((1st ‘𝐴) +N
1𝑜) ∈ N ∧ 𝐴 <Q
〈((1st ‘𝐴) +N
1𝑜), 1𝑜〉) → ∃𝑥 ∈ N 𝐴 <Q
〈𝑥,
1𝑜〉) |
51 | 6, 47, 50 | syl2anc 693 |
1
⊢ (𝐴 ∈ Q →
∃𝑥 ∈
N 𝐴
<Q 〈𝑥,
1𝑜〉) |