Step | Hyp | Ref
| Expression |
1 | | caucvgprpr.f |
. 2
⊢ (𝜑 → 𝐹:N⟶P) |
2 | | caucvgprpr.cau |
. 2
⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N
𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P 〈{𝑙 ∣ 𝑙 <Q
(*Q‘[〈𝑛, 1o〉]
~Q )}, {𝑢 ∣
(*Q‘[〈𝑛, 1o〉]
~Q ) <Q 𝑢}〉)))) |
3 | | caucvgprpr.bnd |
. 2
⊢ (𝜑 → ∀𝑚 ∈ N 𝐴<P (𝐹‘𝑚)) |
4 | | caucvgprpr.lim |
. . 3
⊢ 𝐿 = 〈{𝑙 ∈ 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 𝑞}〉}〉 |
5 | | opeq1 3743 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝑠 → 〈𝑟, 1o〉 = 〈𝑠,
1o〉) |
6 | 5 | eceq1d 6518 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑠 → [〈𝑟, 1o〉]
~Q = [〈𝑠, 1o〉]
~Q ) |
7 | 6 | fveq2d 5474 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑠 →
(*Q‘[〈𝑟, 1o〉]
~Q ) = (*Q‘[〈𝑠, 1o〉]
~Q )) |
8 | 7 | oveq2d 5842 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑠 → (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) = (𝑙 +Q
(*Q‘[〈𝑠, 1o〉]
~Q ))) |
9 | 8 | breq2d 3979 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑠 → (𝑝 <Q (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) ↔ 𝑝 <Q (𝑙 +Q
(*Q‘[〈𝑠, 1o〉]
~Q )))) |
10 | 9 | abbidv 2275 |
. . . . . . . . 9
⊢ (𝑟 = 𝑠 → {𝑝 ∣ 𝑝 <Q (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q ))} = {𝑝 ∣ 𝑝 <Q (𝑙 +Q
(*Q‘[〈𝑠, 1o〉]
~Q ))}) |
11 | 8 | breq1d 3977 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑠 → ((𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞 ↔ (𝑙 +Q
(*Q‘[〈𝑠, 1o〉]
~Q )) <Q 𝑞)) |
12 | 11 | abbidv 2275 |
. . . . . . . . 9
⊢ (𝑟 = 𝑠 → {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞} = {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑠, 1o〉]
~Q )) <Q 𝑞}) |
13 | 10, 12 | opeq12d 3751 |
. . . . . . . 8
⊢ (𝑟 = 𝑠 → 〈{𝑝 ∣ 𝑝 <Q (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉 = 〈{𝑝 ∣ 𝑝 <Q (𝑙 +Q
(*Q‘[〈𝑠, 1o〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑠, 1o〉]
~Q )) <Q 𝑞}〉) |
14 | | fveq2 5470 |
. . . . . . . 8
⊢ (𝑟 = 𝑠 → (𝐹‘𝑟) = (𝐹‘𝑠)) |
15 | 13, 14 | breq12d 3980 |
. . . . . . 7
⊢ (𝑟 = 𝑠 → (〈{𝑝 ∣ 𝑝 <Q (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟) ↔ 〈{𝑝 ∣ 𝑝 <Q (𝑙 +Q
(*Q‘[〈𝑠, 1o〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑠, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑠))) |
16 | 15 | cbvrexv 2681 |
. . . . . 6
⊢
(∃𝑟 ∈
N 〈{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟) ↔ ∃𝑠 ∈ N 〈{𝑝 ∣ 𝑝 <Q (𝑙 +Q
(*Q‘[〈𝑠, 1o〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑠, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑠)) |
17 | 16 | a1i 9 |
. . . . 5
⊢ (𝑙 ∈ Q →
(∃𝑟 ∈
N 〈{𝑝
∣ 𝑝
<Q (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑟, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑟) ↔ ∃𝑠 ∈ N 〈{𝑝 ∣ 𝑝 <Q (𝑙 +Q
(*Q‘[〈𝑠, 1o〉]
~Q ))}, {𝑞 ∣ (𝑙 +Q
(*Q‘[〈𝑠, 1o〉]
~Q )) <Q 𝑞}〉<P (𝐹‘𝑠))) |
18 | 17 | rabbiia 2697 |
. . . 4
⊢ {𝑙 ∈ 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 (𝐹‘𝑠)} |
19 | 7 | breq2d 3979 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑠 → (𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q ) ↔ 𝑝 <Q
(*Q‘[〈𝑠, 1o〉]
~Q ))) |
20 | 19 | abbidv 2275 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑠 → {𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )} = {𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑠, 1o〉]
~Q )}) |
21 | 7 | breq1d 3977 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑠 →
((*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞 ↔
(*Q‘[〈𝑠, 1o〉]
~Q ) <Q 𝑞)) |
22 | 21 | abbidv 2275 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑠 → {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞} = {𝑞 ∣
(*Q‘[〈𝑠, 1o〉]
~Q ) <Q 𝑞}) |
23 | 20, 22 | opeq12d 3751 |
. . . . . . . . 9
⊢ (𝑟 = 𝑠 → 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉 = 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑠, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑠, 1o〉]
~Q ) <Q 𝑞}〉) |
24 | 14, 23 | oveq12d 5844 |
. . . . . . . 8
⊢ (𝑟 = 𝑠 → ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉) = ((𝐹‘𝑠) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑠, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑠, 1o〉]
~Q ) <Q 𝑞}〉)) |
25 | 24 | breq1d 3977 |
. . . . . . 7
⊢ (𝑟 = 𝑠 → (((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉 ↔ ((𝐹‘𝑠) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑠, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑠, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉)) |
26 | 25 | cbvrexv 2681 |
. . . . . 6
⊢
(∃𝑟 ∈
N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉 ↔ ∃𝑠 ∈ N ((𝐹‘𝑠) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑠, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑠, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉) |
27 | 26 | a1i 9 |
. . . . 5
⊢ (𝑢 ∈ Q →
(∃𝑟 ∈
N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉 ↔ ∃𝑠 ∈ N ((𝐹‘𝑠) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑠, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑠, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉)) |
28 | 27 | rabbiia 2697 |
. . . 4
⊢ {𝑢 ∈ Q ∣
∃𝑟 ∈
N ((𝐹‘𝑟) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑟, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑟, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉} = {𝑢 ∈ Q ∣ ∃𝑠 ∈ N ((𝐹‘𝑠) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑠, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑠, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉} |
29 | 18, 28 | opeq12i 3748 |
. . 3
⊢
〈{𝑙 ∈
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 (𝐹‘𝑠)}, {𝑢 ∈ Q ∣ ∃𝑠 ∈ N ((𝐹‘𝑠) +P 〈{𝑝 ∣ 𝑝 <Q
(*Q‘[〈𝑠, 1o〉]
~Q )}, {𝑞 ∣
(*Q‘[〈𝑠, 1o〉]
~Q ) <Q 𝑞}〉)<P
〈{𝑝 ∣ 𝑝 <Q
𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}〉}〉 |
30 | 4, 29 | eqtri 2178 |
. 2
⊢ 𝐿 = 〈{𝑙 ∈ 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 𝑞}〉}〉 |
31 | 1, 2, 3, 30 | caucvgprprlemcl 7626 |
1
⊢ (𝜑 → 𝐿 ∈ P) |