Step | Hyp | Ref
| Expression |
1 | | ltrelnq 7298 |
. . . . 5
⊢
<Q ⊆ (Q ×
Q) |
2 | 1 | brel 4651 |
. . . 4
⊢ (𝑠 <Q
𝑡 → (𝑠 ∈ Q ∧
𝑡 ∈
Q)) |
3 | 2 | simpld 111 |
. . 3
⊢ (𝑠 <Q
𝑡 → 𝑠 ∈ Q) |
4 | 3 | 3ad2ant2 1008 |
. 2
⊢ ((𝜑 ∧ 𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) → 𝑠 ∈ Q) |
5 | | caucvgprpr.lim |
. . . . . . 7
⊢ 𝐿 = 〈{𝑙 ∈ Q ∣ ∃𝑟 ∈ N
〈{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉}〉 |
6 | 5 | caucvgprprlemell 7618 |
. . . . . 6
⊢ (𝑡 ∈ (1st
‘𝐿) ↔ (𝑡 ∈ Q ∧
∃𝑏 ∈
N 〈{𝑝
∣ 𝑝
<Q (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏))) |
7 | 6 | simprbi 273 |
. . . . 5
⊢ (𝑡 ∈ (1st
‘𝐿) →
∃𝑏 ∈
N 〈{𝑝
∣ 𝑝
<Q (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏)) |
8 | 7 | 3ad2ant3 1009 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) → ∃𝑏 ∈ N
〈{𝑝 ∣ 𝑝 <Q
(𝑡
+Q (*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏)) |
9 | | simpll2 1026 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) ∧ 𝑏 ∈ N) ∧ 〈{𝑝 ∣ 𝑝 <Q (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏)) → 𝑠 <Q 𝑡) |
10 | | ltanqg 7333 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q
∧ 𝑧 ∈
Q) → (𝑥
<Q 𝑦 ↔ (𝑧 +Q 𝑥) <Q
(𝑧
+Q 𝑦))) |
11 | 10 | adantl 275 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑠 <Q
𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) ∧ 𝑏 ∈ N) ∧ 〈{𝑝 ∣ 𝑝 <Q (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏)) ∧ (𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧
𝑧 ∈ Q))
→ (𝑥
<Q 𝑦 ↔ (𝑧 +Q 𝑥) <Q
(𝑧
+Q 𝑦))) |
12 | 4 | ad2antrr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) ∧ 𝑏 ∈ N) ∧ 〈{𝑝 ∣ 𝑝 <Q (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏)) → 𝑠 ∈ Q) |
13 | 2 | simprd 113 |
. . . . . . . . . . . 12
⊢ (𝑠 <Q
𝑡 → 𝑡 ∈ Q) |
14 | 13 | 3ad2ant2 1008 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) → 𝑡 ∈ Q) |
15 | 14 | ad2antrr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) ∧ 𝑏 ∈ N) ∧ 〈{𝑝 ∣ 𝑝 <Q (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏)) → 𝑡 ∈ Q) |
16 | | simplr 520 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) ∧ 𝑏 ∈ N) ∧ 〈{𝑝 ∣ 𝑝 <Q (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏)) → 𝑏 ∈ N) |
17 | | nnnq 7355 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ N →
[〈𝑏,
1o〉] ~Q ∈
Q) |
18 | | recclnq 7325 |
. . . . . . . . . . 11
⊢
([〈𝑏,
1o〉] ~Q ∈ Q →
(*Q‘[〈𝑏, 1o〉]
~Q ) ∈ Q) |
19 | 16, 17, 18 | 3syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) ∧ 𝑏 ∈ N) ∧ 〈{𝑝 ∣ 𝑝 <Q (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏)) →
(*Q‘[〈𝑏, 1o〉]
~Q ) ∈ Q) |
20 | | addcomnqg 7314 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥
+Q 𝑦) = (𝑦 +Q 𝑥)) |
21 | 20 | adantl 275 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑠 <Q
𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) ∧ 𝑏 ∈ N) ∧ 〈{𝑝 ∣ 𝑝 <Q (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏)) ∧ (𝑥 ∈ Q ∧ 𝑦 ∈ Q)) →
(𝑥
+Q 𝑦) = (𝑦 +Q 𝑥)) |
22 | 11, 12, 15, 19, 21 | caovord2d 6003 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) ∧ 𝑏 ∈ N) ∧ 〈{𝑝 ∣ 𝑝 <Q (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏)) → (𝑠 <Q 𝑡 ↔ (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )))) |
23 | 9, 22 | mpbid 146 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) ∧ 𝑏 ∈ N) ∧ 〈{𝑝 ∣ 𝑝 <Q (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏)) → (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))) |
24 | | ltnqpri 7527 |
. . . . . . . 8
⊢ ((𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) → 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P
〈{𝑝 ∣ 𝑝 <Q
(𝑡
+Q (*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉) |
25 | 23, 24 | syl 14 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) ∧ 𝑏 ∈ N) ∧ 〈{𝑝 ∣ 𝑝 <Q (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏)) → 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P
〈{𝑝 ∣ 𝑝 <Q
(𝑡
+Q (*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉) |
26 | | ltsopr 7529 |
. . . . . . . 8
⊢
<P Or P |
27 | | ltrelpr 7438 |
. . . . . . . 8
⊢
<P ⊆ (P ×
P) |
28 | 26, 27 | sotri 4994 |
. . . . . . 7
⊢
((〈{𝑝 ∣
𝑝
<Q (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P
〈{𝑝 ∣ 𝑝 <Q
(𝑡
+Q (*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉 ∧ 〈{𝑝 ∣ 𝑝 <Q (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏)) → 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏)) |
29 | 25, 28 | sylancom 417 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) ∧ 𝑏 ∈ N) ∧ 〈{𝑝 ∣ 𝑝 <Q (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏)) → 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏)) |
30 | 29 | ex 114 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) ∧ 𝑏 ∈ N) → (〈{𝑝 ∣ 𝑝 <Q (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏) → 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏))) |
31 | 30 | reximdva 2566 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) → (∃𝑏 ∈ N
〈{𝑝 ∣ 𝑝 <Q
(𝑡
+Q (*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑡 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏) → ∃𝑏 ∈ N 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏))) |
32 | 8, 31 | mpd 13 |
. . 3
⊢ ((𝜑 ∧ 𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) → ∃𝑏 ∈ N
〈{𝑝 ∣ 𝑝 <Q
(𝑠
+Q (*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏)) |
33 | | opeq1 3753 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑟 → 〈𝑏, 1o〉 = 〈𝑟,
1o〉) |
34 | 33 | eceq1d 6529 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑟 → [〈𝑏, 1o〉]
~Q = [〈𝑟, 1o〉]
~Q ) |
35 | 34 | fveq2d 5485 |
. . . . . . . . 9
⊢ (𝑏 = 𝑟 →
(*Q‘[〈𝑏, 1o〉]
~Q ) = (*Q‘[〈𝑟, 1o〉]
~Q )) |
36 | 35 | oveq2d 5853 |
. . . . . . . 8
⊢ (𝑏 = 𝑟 → (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) = (𝑠 +Q
(*Q‘[〈𝑟, 1o〉]
~Q ))) |
37 | 36 | breq2d 3989 |
. . . . . . 7
⊢ (𝑏 = 𝑟 → (𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) ↔ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )))) |
38 | 37 | abbidv 2282 |
. . . . . 6
⊢ (𝑏 = 𝑟 → {𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))} = {𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑟, 1o〉]
~Q ))}) |
39 | 36 | breq1d 3987 |
. . . . . . 7
⊢ (𝑏 = 𝑟 → ((𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞 ↔ (𝑠 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞)) |
40 | 39 | abbidv 2282 |
. . . . . 6
⊢ (𝑏 = 𝑟 → {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞} = {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}) |
41 | 38, 40 | opeq12d 3761 |
. . . . 5
⊢ (𝑏 = 𝑟 → 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉 = 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉) |
42 | | fveq2 5481 |
. . . . 5
⊢ (𝑏 = 𝑟 → (𝐹‘𝑏) = (𝐹‘𝑟)) |
43 | 41, 42 | breq12d 3990 |
. . . 4
⊢ (𝑏 = 𝑟 → (〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏) ↔ 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟))) |
44 | 43 | cbvrexv 2691 |
. . 3
⊢
(∃𝑏 ∈
N 〈{𝑝
∣ 𝑝
<Q (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑏, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑏) ↔ ∃𝑟 ∈ N 〈{𝑝 ∣ 𝑝 <Q (𝑠 +Q
(*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)) |
45 | 32, 44 | sylib 121 |
. 2
⊢ ((𝜑 ∧ 𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) → ∃𝑟 ∈ N
〈{𝑝 ∣ 𝑝 <Q
(𝑠
+Q (*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟)) |
46 | 5 | caucvgprprlemell 7618 |
. 2
⊢ (𝑠 ∈ (1st
‘𝐿) ↔ (𝑠 ∈ Q ∧
∃𝑟 ∈
N 〈{𝑝
∣ 𝑝
<Q (𝑠 +Q
(*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑠 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟))) |
47 | 4, 45, 46 | sylanbrc 414 |
1
⊢ ((𝜑 ∧ 𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) → 𝑠 ∈ (1st ‘𝐿)) |