Step | Hyp | Ref
| Expression |
1 | | 1rp 11836 |
. . . 4
⊢ 1 ∈
ℝ+ |
2 | 1 | ne0ii 3923 |
. . 3
⊢
ℝ+ ≠ ∅ |
3 | | caurcvg2.3 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) |
4 | | r19.2z 4060 |
. . 3
⊢
((ℝ+ ≠ ∅ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) → ∃𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) |
5 | 2, 3, 4 | sylancr 695 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) |
6 | | simpl 473 |
. . . . . 6
⊢ (((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → (𝐹‘𝑘) ∈ ℝ) |
7 | 6 | ralimi 2952 |
. . . . 5
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℝ) |
8 | | eqid 2622 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑗) = (ℤ≥‘𝑗) |
9 | | simprr 796 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℝ)) → ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℝ) |
10 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
11 | 10 | eleq1d 2686 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝑛) ∈ ℝ)) |
12 | 11 | rspccva 3308 |
. . . . . . . . . . 11
⊢
((∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℝ ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑛) ∈ ℝ) |
13 | 9, 12 | sylan 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℝ)) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑛) ∈ ℝ) |
14 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(ℤ≥‘𝑗) ↦ (𝐹‘𝑛)) = (𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛)) |
15 | 13, 14 | fmptd 6385 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℝ)) → (𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛)):(ℤ≥‘𝑗)⟶ℝ) |
16 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑚 → (ℤ≥‘𝑗) =
(ℤ≥‘𝑚)) |
17 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑚 → (𝐹‘𝑗) = (𝐹‘𝑚)) |
18 | 17 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑚 → ((𝐹‘𝑘) − (𝐹‘𝑗)) = ((𝐹‘𝑘) − (𝐹‘𝑚))) |
19 | 18 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 𝑚 → (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) = (abs‘((𝐹‘𝑘) − (𝐹‘𝑚)))) |
20 | 19 | breq1d 4663 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑚 → ((abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥 ↔ (abs‘((𝐹‘𝑘) − (𝐹‘𝑚))) < 𝑥)) |
21 | 20 | anbi2d 740 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑚 → (((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) ↔ ((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑚))) < 𝑥))) |
22 | 16, 21 | raleqbidv 3152 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑚 → (∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) ↔ ∀𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑚))) < 𝑥))) |
23 | 22 | cbvrexv 3172 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) ↔ ∃𝑚 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑚))) < 𝑥)) |
24 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖)) |
25 | 24 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝑖) ∈ ℝ)) |
26 | 24 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) − (𝐹‘𝑚)) = ((𝐹‘𝑖) − (𝐹‘𝑚))) |
27 | 26 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑖 → (abs‘((𝐹‘𝑘) − (𝐹‘𝑚))) = (abs‘((𝐹‘𝑖) − (𝐹‘𝑚)))) |
28 | 27 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑖 → ((abs‘((𝐹‘𝑘) − (𝐹‘𝑚))) < 𝑥 ↔ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥)) |
29 | 25, 28 | anbi12d 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑖 → (((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑚))) < 𝑥) ↔ ((𝐹‘𝑖) ∈ ℝ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥))) |
30 | 29 | cbvralv 3171 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑘 ∈
(ℤ≥‘𝑚)((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑚))) < 𝑥) ↔ ∀𝑖 ∈ (ℤ≥‘𝑚)((𝐹‘𝑖) ∈ ℝ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥)) |
31 | | recn 10026 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑖) ∈ ℝ → (𝐹‘𝑖) ∈ ℂ) |
32 | 31 | anim1i 592 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘𝑖) ∈ ℝ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥) → ((𝐹‘𝑖) ∈ ℂ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥)) |
33 | 32 | ralimi 2952 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑖 ∈
(ℤ≥‘𝑚)((𝐹‘𝑖) ∈ ℝ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥) → ∀𝑖 ∈ (ℤ≥‘𝑚)((𝐹‘𝑖) ∈ ℂ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥)) |
34 | 30, 33 | sylbi 207 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑘 ∈
(ℤ≥‘𝑚)((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑚))) < 𝑥) → ∀𝑖 ∈ (ℤ≥‘𝑚)((𝐹‘𝑖) ∈ ℂ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥)) |
35 | 34 | reximi 3011 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑚 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑚)((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑚))) < 𝑥) → ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ≥‘𝑚)((𝐹‘𝑖) ∈ ℂ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥)) |
36 | 23, 35 | sylbi 207 |
. . . . . . . . . . . . . 14
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ≥‘𝑚)((𝐹‘𝑖) ∈ ℂ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥)) |
37 | 36 | ralimi 2952 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∀𝑥 ∈ ℝ+ ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ≥‘𝑚)((𝐹‘𝑖) ∈ ℂ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥)) |
38 | 3, 37 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ≥‘𝑚)((𝐹‘𝑖) ∈ ℂ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥)) |
39 | 38 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℝ)) → ∀𝑥 ∈ ℝ+
∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ≥‘𝑚)((𝐹‘𝑖) ∈ ℂ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥)) |
40 | | caucvg.1 |
. . . . . . . . . . . . 13
⊢ 𝑍 =
(ℤ≥‘𝑀) |
41 | 40, 8 | cau4 14096 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ 𝑍 → (∀𝑥 ∈ ℝ+ ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ≥‘𝑚)((𝐹‘𝑖) ∈ ℂ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑚 ∈
(ℤ≥‘𝑗)∀𝑖 ∈ (ℤ≥‘𝑚)((𝐹‘𝑖) ∈ ℂ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥))) |
42 | 41 | ad2antrl 764 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℝ)) → (∀𝑥 ∈ ℝ+
∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ≥‘𝑚)((𝐹‘𝑖) ∈ ℂ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑚 ∈
(ℤ≥‘𝑗)∀𝑖 ∈ (ℤ≥‘𝑚)((𝐹‘𝑖) ∈ ℂ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥))) |
43 | 39, 42 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℝ)) → ∀𝑥 ∈ ℝ+
∃𝑚 ∈
(ℤ≥‘𝑗)∀𝑖 ∈ (ℤ≥‘𝑚)((𝐹‘𝑖) ∈ ℂ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥)) |
44 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑖) ∈ ℂ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥) → (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥) |
45 | 8 | uztrn2 11705 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚 ∈
(ℤ≥‘𝑗) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) → 𝑖 ∈ (ℤ≥‘𝑗)) |
46 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑖 → (𝐹‘𝑛) = (𝐹‘𝑖)) |
47 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹‘𝑖) ∈ V |
48 | 46, 14, 47 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈
(ℤ≥‘𝑗) → ((𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑖) = (𝐹‘𝑖)) |
49 | 45, 48 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈
(ℤ≥‘𝑗) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) → ((𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑖) = (𝐹‘𝑖)) |
50 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚)) |
51 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹‘𝑚) ∈ V |
52 | 50, 14, 51 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈
(ℤ≥‘𝑗) → ((𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑚) = (𝐹‘𝑚)) |
53 | 52 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈
(ℤ≥‘𝑗) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) → ((𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑚) = (𝐹‘𝑚)) |
54 | 49, 53 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈
(ℤ≥‘𝑗) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) → (((𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑖) − ((𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑚)) = ((𝐹‘𝑖) − (𝐹‘𝑚))) |
55 | 54 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈
(ℤ≥‘𝑗) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) → (abs‘(((𝑛 ∈
(ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑖) − ((𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑚))) = (abs‘((𝐹‘𝑖) − (𝐹‘𝑚)))) |
56 | 55 | breq1d 4663 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈
(ℤ≥‘𝑗) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) → ((abs‘(((𝑛 ∈
(ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑖) − ((𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑚))) < 𝑥 ↔ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥)) |
57 | 44, 56 | syl5ibr 236 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈
(ℤ≥‘𝑗) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) → (((𝐹‘𝑖) ∈ ℂ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥) → (abs‘(((𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑖) − ((𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑚))) < 𝑥)) |
58 | 57 | ralimdva 2962 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈
(ℤ≥‘𝑗) → (∀𝑖 ∈ (ℤ≥‘𝑚)((𝐹‘𝑖) ∈ ℂ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥) → ∀𝑖 ∈ (ℤ≥‘𝑚)(abs‘(((𝑛 ∈
(ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑖) − ((𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑚))) < 𝑥)) |
59 | 58 | reximia 3009 |
. . . . . . . . . . 11
⊢
(∃𝑚 ∈
(ℤ≥‘𝑗)∀𝑖 ∈ (ℤ≥‘𝑚)((𝐹‘𝑖) ∈ ℂ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥) → ∃𝑚 ∈ (ℤ≥‘𝑗)∀𝑖 ∈ (ℤ≥‘𝑚)(abs‘(((𝑛 ∈
(ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑖) − ((𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑚))) < 𝑥) |
60 | 59 | ralimi 2952 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
ℝ+ ∃𝑚 ∈ (ℤ≥‘𝑗)∀𝑖 ∈ (ℤ≥‘𝑚)((𝐹‘𝑖) ∈ ℂ ∧ (abs‘((𝐹‘𝑖) − (𝐹‘𝑚))) < 𝑥) → ∀𝑥 ∈ ℝ+ ∃𝑚 ∈
(ℤ≥‘𝑗)∀𝑖 ∈ (ℤ≥‘𝑚)(abs‘(((𝑛 ∈
(ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑖) − ((𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑚))) < 𝑥) |
61 | 43, 60 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℝ)) → ∀𝑥 ∈ ℝ+
∃𝑚 ∈
(ℤ≥‘𝑗)∀𝑖 ∈ (ℤ≥‘𝑚)(abs‘(((𝑛 ∈
(ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑖) − ((𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛))‘𝑚))) < 𝑥) |
62 | 8, 15, 61 | caurcvg 14407 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℝ)) → (𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛)) ⇝ (lim sup‘(𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛)))) |
63 | | eluzelz 11697 |
. . . . . . . . . . 11
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑗 ∈ ℤ) |
64 | 63, 40 | eleq2s 2719 |
. . . . . . . . . 10
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ) |
65 | 64 | ad2antrl 764 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℝ)) → 𝑗 ∈ ℤ) |
66 | | caurcvg2.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
67 | 66 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℝ)) → 𝐹 ∈ 𝑉) |
68 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) |
69 | 68 | cbvmptv 4750 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(ℤ≥‘𝑗) ↦ (𝐹‘𝑛)) = (𝑘 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑘)) |
70 | 8, 69 | climmpt 14302 |
. . . . . . . . 9
⊢ ((𝑗 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (𝐹 ⇝ (lim sup‘(𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛))) ↔ (𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛)) ⇝ (lim sup‘(𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛))))) |
71 | 65, 67, 70 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℝ)) → (𝐹 ⇝ (lim sup‘(𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛))) ↔ (𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛)) ⇝ (lim sup‘(𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛))))) |
72 | 62, 71 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℝ)) → 𝐹 ⇝ (lim sup‘(𝑛 ∈ (ℤ≥‘𝑗) ↦ (𝐹‘𝑛)))) |
73 | | climrel 14223 |
. . . . . . . 8
⊢ Rel
⇝ |
74 | 73 | releldmi 5362 |
. . . . . . 7
⊢ (𝐹 ⇝ (lim sup‘(𝑛 ∈
(ℤ≥‘𝑗) ↦ (𝐹‘𝑛))) → 𝐹 ∈ dom ⇝ ) |
75 | 72, 74 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℝ)) → 𝐹 ∈ dom ⇝ ) |
76 | 75 | expr 643 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ ℝ → 𝐹 ∈ dom ⇝ )) |
77 | 7, 76 | syl5 34 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → 𝐹 ∈ dom ⇝ )) |
78 | 77 | rexlimdva 3031 |
. . 3
⊢ (𝜑 → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → 𝐹 ∈ dom ⇝ )) |
79 | 78 | rexlimdvw 3034 |
. 2
⊢ (𝜑 → (∃𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → 𝐹 ∈ dom ⇝ )) |
80 | 5, 79 | mpd 15 |
1
⊢ (𝜑 → 𝐹 ∈ dom ⇝ ) |