Step |
Hyp |
Ref |
Expression |
1 |
|
climlimsup.1 |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
2 |
|
climlimsup.2 |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
3 |
|
climlimsup.3 |
⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ ) |
4 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 : 𝑍 ⟶ ℝ ) |
5 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝑀 ∈ ℤ ) |
6 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ∈ dom ⇝ ) |
7 |
2
|
climcau |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) |
8 |
5 6 7
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 ) |
9 |
2 4 8
|
caurcvg |
⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) |
10 |
|
climrel |
⊢ Rel ⇝ |
11 |
|
releldm |
⊢ ( ( Rel ⇝ ∧ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) → 𝐹 ∈ dom ⇝ ) |
12 |
10 11
|
mpan |
⊢ ( 𝐹 ⇝ ( lim sup ‘ 𝐹 ) → 𝐹 ∈ dom ⇝ ) |
13 |
12
|
adantl |
⊢ ( ( 𝜑 ∧ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) → 𝐹 ∈ dom ⇝ ) |
14 |
9 13
|
impbida |
⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) ) |