Step | Hyp | Ref
| Expression |
1 | | oveq1 5881 |
. . . . . . . 8
⊢ (𝑙 = 𝑋 → (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) = (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))) |
2 | 1 | breq2d 4015 |
. . . . . . 7
⊢ (𝑙 = 𝑋 → (𝑝 <Q (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) ↔ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )))) |
3 | 2 | abbidv 2295 |
. . . . . 6
⊢ (𝑙 = 𝑋 → {𝑝 ∣ 𝑝 <Q (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))} = {𝑝 ∣ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}) |
4 | 1 | breq1d 4013 |
. . . . . . 7
⊢ (𝑙 = 𝑋 → ((𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞 ↔ (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞)) |
5 | 4 | abbidv 2295 |
. . . . . 6
⊢ (𝑙 = 𝑋 → {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞} = {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}) |
6 | 3, 5 | opeq12d 3786 |
. . . . 5
⊢ (𝑙 = 𝑋 → ⟨{𝑝 ∣ 𝑝 <Q (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩ = ⟨{𝑝 ∣ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩) |
7 | 6 | breq1d 4013 |
. . . 4
⊢ (𝑙 = 𝑋 → (⟨{𝑝 ∣ 𝑝 <Q (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟) ↔ ⟨{𝑝 ∣ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟))) |
8 | 7 | rexbidv 2478 |
. . 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 (𝐹‘𝑟))) |
9 | | caucvgprprlemell.lim |
. . . . 5
⊢ 𝐿 = ⟨{𝑙 ∈ 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 𝑞}⟩}⟩ |
10 | 9 | fveq2i 5518 |
. . . 4
⊢
(1st ‘𝐿) = (1st ‘⟨{𝑙 ∈ 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 𝑞}⟩}⟩) |
11 | | nqex 7361 |
. . . . . 6
⊢
Q ∈ V |
12 | 11 | rabex 4147 |
. . . . 5
⊢ {𝑙 ∈ Q ∣
∃𝑟 ∈
N ⟨{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)} ∈ V |
13 | 11 | rabex 4147 |
. . . . 5
⊢ {𝑢 ∈ Q ∣
∃𝑟 ∈
N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )}, {𝑞 ∣
(*Q‘[⟨𝑟, 1o⟩]
~Q ) <Q 𝑞}⟩)<P
⟨{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩} ∈
V |
14 | 12, 13 | op1st 6146 |
. . . 4
⊢
(1st ‘⟨{𝑙 ∈ 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 𝑞}⟩}⟩) = {𝑙 ∈ Q ∣
∃𝑟 ∈
N ⟨{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)} |
15 | 10, 14 | eqtri 2198 |
. . 3
⊢
(1st ‘𝐿) = {𝑙 ∈ Q ∣ ∃𝑟 ∈ N
⟨{𝑝 ∣ 𝑝 <Q
(𝑙
+Q (*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)} |
16 | 8, 15 | elrab2 2896 |
. 2
⊢ (𝑋 ∈ (1st
‘𝐿) ↔ (𝑋 ∈ Q ∧
∃𝑟 ∈
N ⟨{𝑝
∣ 𝑝
<Q (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟))) |
17 | | opeq1 3778 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑎 → ⟨𝑟, 1o⟩ = ⟨𝑎,
1o⟩) |
18 | 17 | eceq1d 6570 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑎 → [⟨𝑟, 1o⟩]
~Q = [⟨𝑎, 1o⟩]
~Q ) |
19 | 18 | fveq2d 5519 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑎 →
(*Q‘[⟨𝑟, 1o⟩]
~Q ) = (*Q‘[⟨𝑎, 1o⟩]
~Q )) |
20 | 19 | oveq2d 5890 |
. . . . . . . . 9
⊢ (𝑟 = 𝑎 → (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) = (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q ))) |
21 | 20 | breq2d 4015 |
. . . . . . . 8
⊢ (𝑟 = 𝑎 → (𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) ↔ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q )))) |
22 | 21 | abbidv 2295 |
. . . . . . 7
⊢ (𝑟 = 𝑎 → {𝑝 ∣ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))} = {𝑝 ∣ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q ))}) |
23 | 20 | breq1d 4013 |
. . . . . . . 8
⊢ (𝑟 = 𝑎 → ((𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞 ↔ (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q )) <Q 𝑞)) |
24 | 23 | abbidv 2295 |
. . . . . . 7
⊢ (𝑟 = 𝑎 → {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞} = {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q )) <Q 𝑞}) |
25 | 22, 24 | opeq12d 3786 |
. . . . . 6
⊢ (𝑟 = 𝑎 → ⟨{𝑝 ∣ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩ = ⟨{𝑝 ∣ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q )) <Q 𝑞}⟩) |
26 | | fveq2 5515 |
. . . . . 6
⊢ (𝑟 = 𝑎 → (𝐹‘𝑟) = (𝐹‘𝑎)) |
27 | 25, 26 | breq12d 4016 |
. . . . 5
⊢ (𝑟 = 𝑎 → (⟨{𝑝 ∣ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟) ↔ ⟨{𝑝 ∣ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑎))) |
28 | 27 | cbvrexv 2704 |
. . . 4
⊢
(∃𝑟 ∈
N ⟨{𝑝
∣ 𝑝
<Q (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟) ↔ ∃𝑎 ∈ N ⟨{𝑝 ∣ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑎)) |
29 | | opeq1 3778 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → ⟨𝑎, 1o⟩ = ⟨𝑏,
1o⟩) |
30 | 29 | eceq1d 6570 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑏 → [⟨𝑎, 1o⟩]
~Q = [⟨𝑏, 1o⟩]
~Q ) |
31 | 30 | fveq2d 5519 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 →
(*Q‘[⟨𝑎, 1o⟩]
~Q ) = (*Q‘[⟨𝑏, 1o⟩]
~Q )) |
32 | 31 | oveq2d 5890 |
. . . . . . . . 9
⊢ (𝑎 = 𝑏 → (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q )) = (𝑋 +Q
(*Q‘[⟨𝑏, 1o⟩]
~Q ))) |
33 | 32 | breq2d 4015 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → (𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q )) ↔ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑏, 1o⟩]
~Q )))) |
34 | 33 | abbidv 2295 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → {𝑝 ∣ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q ))} = {𝑝 ∣ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑏, 1o⟩]
~Q ))}) |
35 | 32 | breq1d 4013 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → ((𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q )) <Q 𝑞 ↔ (𝑋 +Q
(*Q‘[⟨𝑏, 1o⟩]
~Q )) <Q 𝑞)) |
36 | 35 | abbidv 2295 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q )) <Q 𝑞} = {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑏, 1o⟩]
~Q )) <Q 𝑞}) |
37 | 34, 36 | opeq12d 3786 |
. . . . . 6
⊢ (𝑎 = 𝑏 → ⟨{𝑝 ∣ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q )) <Q 𝑞}⟩ = ⟨{𝑝 ∣ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑏, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑏, 1o⟩]
~Q )) <Q 𝑞}⟩) |
38 | | fveq2 5515 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (𝐹‘𝑎) = (𝐹‘𝑏)) |
39 | 37, 38 | breq12d 4016 |
. . . . 5
⊢ (𝑎 = 𝑏 → (⟨{𝑝 ∣ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑎) ↔ ⟨{𝑝 ∣ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑏, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑏, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑏))) |
40 | 39 | cbvrexv 2704 |
. . . 4
⊢
(∃𝑎 ∈
N ⟨{𝑝
∣ 𝑝
<Q (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑎, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑎) ↔ ∃𝑏 ∈ N ⟨{𝑝 ∣ 𝑝 <Q (𝑋 +Q
(*Q‘[⟨𝑏, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑏, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑏)) |
41 | 28, 40 | bitri 184 |
. . 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 (𝐹‘𝑏)) |
42 | 41 | anbi2i 457 |
. 2
⊢ ((𝑋 ∈ Q ∧
∃𝑟 ∈
N ⟨{𝑝
∣ 𝑝
<Q (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑟, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)) ↔ (𝑋 ∈ Q ∧ ∃𝑏 ∈ N
⟨{𝑝 ∣ 𝑝 <Q
(𝑋
+Q (*Q‘[⟨𝑏, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑏, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑏))) |
43 | 16, 42 | bitri 184 |
1
⊢ (𝑋 ∈ (1st
‘𝐿) ↔ (𝑋 ∈ Q ∧
∃𝑏 ∈
N ⟨{𝑝
∣ 𝑝
<Q (𝑋 +Q
(*Q‘[⟨𝑏, 1o⟩]
~Q ))}, {𝑞 ∣ (𝑋 +Q
(*Q‘[⟨𝑏, 1o⟩]
~Q )) <Q 𝑞}⟩<P (𝐹‘𝑏))) |