Step | Hyp | Ref
| Expression |
1 | | caurcvgr.1 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
2 | | caurcvgr.2 |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) |
3 | | caurcvgr.3 |
. . . . 5
⊢ (𝜑 → sup(𝐴, ℝ*, < ) =
+∞) |
4 | | caurcvgr.4 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) |
5 | | 1rp 11874 |
. . . . . 6
⊢ 1 ∈
ℝ+ |
6 | 5 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℝ+) |
7 | 1, 2, 3, 4, 6 | caucvgrlem 14447 |
. . . 4
⊢ (𝜑 → ∃𝑗 ∈ 𝐴 ((lim sup‘𝐹) ∈ ℝ ∧ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < (3 · 1)))) |
8 | | simpl 472 |
. . . . 5
⊢ (((lim
sup‘𝐹) ∈ ℝ
∧ ∀𝑘 ∈
𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < (3 · 1))) → (lim
sup‘𝐹) ∈
ℝ) |
9 | 8 | rexlimivw 3058 |
. . . 4
⊢
(∃𝑗 ∈
𝐴 ((lim sup‘𝐹) ∈ ℝ ∧
∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < (3 · 1))) → (lim
sup‘𝐹) ∈
ℝ) |
10 | 7, 9 | syl 17 |
. . 3
⊢ (𝜑 → (lim sup‘𝐹) ∈
ℝ) |
11 | 10 | recnd 10106 |
. 2
⊢ (𝜑 → (lim sup‘𝐹) ∈
ℂ) |
12 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝐴 ⊆
ℝ) |
13 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝐹:𝐴⟶ℝ) |
14 | 3 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → sup(𝐴, ℝ*, < ) =
+∞) |
15 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) |
16 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℝ+) |
17 | | 3re 11132 |
. . . . . . . . 9
⊢ 3 ∈
ℝ |
18 | | 3pos 11152 |
. . . . . . . . 9
⊢ 0 <
3 |
19 | 17, 18 | elrpii 11873 |
. . . . . . . 8
⊢ 3 ∈
ℝ+ |
20 | | rpdivcl 11894 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ+
∧ 3 ∈ ℝ+) → (𝑦 / 3) ∈
ℝ+) |
21 | 16, 19, 20 | sylancl 695 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 / 3) ∈
ℝ+) |
22 | 12, 13, 14, 15, 21 | caucvgrlem 14447 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑗 ∈ 𝐴 ((lim sup‘𝐹) ∈ ℝ ∧
∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < (3 · (𝑦 / 3))))) |
23 | | simpr 476 |
. . . . . . 7
⊢ (((lim
sup‘𝐹) ∈ ℝ
∧ ∀𝑘 ∈
𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < (3 · (𝑦 / 3)))) → ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < (3 · (𝑦 / 3)))) |
24 | 23 | reximi 3040 |
. . . . . 6
⊢
(∃𝑗 ∈
𝐴 ((lim sup‘𝐹) ∈ ℝ ∧
∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < (3 · (𝑦 / 3)))) → ∃𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < (3 · (𝑦 / 3)))) |
25 | 22, 24 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < (3 · (𝑦 / 3)))) |
26 | | ssrexv 3700 |
. . . . 5
⊢ (𝐴 ⊆ ℝ →
(∃𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < (3 · (𝑦 / 3))) → ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < (3 · (𝑦 / 3))))) |
27 | 12, 25, 26 | sylc 65 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑗 ∈ ℝ
∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < (3 · (𝑦 / 3)))) |
28 | | rpcn 11879 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℂ) |
29 | 28 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℂ) |
30 | | 3cn 11133 |
. . . . . . . . 9
⊢ 3 ∈
ℂ |
31 | 30 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 3 ∈
ℂ) |
32 | | 3ne0 11153 |
. . . . . . . . 9
⊢ 3 ≠
0 |
33 | 32 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 3 ≠
0) |
34 | 29, 31, 33 | divcan2d 10841 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (3
· (𝑦 / 3)) = 𝑦) |
35 | 34 | breq2d 4697 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
((abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < (3 · (𝑦 / 3)) ↔ (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < 𝑦)) |
36 | 35 | imbi2d 329 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ((𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < (3 · (𝑦 / 3))) ↔ (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < 𝑦))) |
37 | 36 | rexralbidv 3087 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(∃𝑗 ∈ ℝ
∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < (3 · (𝑦 / 3))) ↔ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < 𝑦))) |
38 | 27, 37 | mpbid 222 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑗 ∈ ℝ
∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < 𝑦)) |
39 | 38 | ralrimiva 2995 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < 𝑦)) |
40 | | ax-resscn 10031 |
. . . 4
⊢ ℝ
⊆ ℂ |
41 | | fss 6094 |
. . . 4
⊢ ((𝐹:𝐴⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐹:𝐴⟶ℂ) |
42 | 2, 40, 41 | sylancl 695 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
43 | | eqidd 2652 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
44 | 42, 1, 43 | rlim 14270 |
. 2
⊢ (𝜑 → (𝐹 ⇝𝑟 (lim
sup‘𝐹) ↔ ((lim
sup‘𝐹) ∈ ℂ
∧ ∀𝑦 ∈
ℝ+ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < 𝑦)))) |
45 | 11, 39, 44 | mpbir2and 977 |
1
⊢ (𝜑 → 𝐹 ⇝𝑟 (lim
sup‘𝐹)) |