| Step |
Hyp |
Ref |
Expression |
| 1 |
|
rlimclim1.1 |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
| 2 |
|
rlimclim1.2 |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
| 3 |
|
rlimclim1.3 |
⊢ ( 𝜑 → 𝐹 ⇝𝑟 𝐴 ) |
| 4 |
|
rlimclim1.4 |
⊢ ( 𝜑 → 𝑍 ⊆ dom 𝐹 ) |
| 5 |
|
fvex |
⊢ ( 𝐹 ‘ 𝑤 ) ∈ V |
| 6 |
5
|
rgenw |
⊢ ∀ 𝑤 ∈ dom 𝐹 ( 𝐹 ‘ 𝑤 ) ∈ V |
| 7 |
6
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∀ 𝑤 ∈ dom 𝐹 ( 𝐹 ‘ 𝑤 ) ∈ V ) |
| 8 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ ) |
| 9 |
|
rlimf |
⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐹 : dom 𝐹 ⟶ ℂ ) |
| 10 |
3 9
|
syl |
⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℂ ) |
| 11 |
10
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐹 : dom 𝐹 ⟶ ℂ ) |
| 12 |
11
|
feqmptd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐹 = ( 𝑤 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑤 ) ) ) |
| 13 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐹 ⇝𝑟 𝐴 ) |
| 14 |
12 13
|
eqbrtrrd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝑤 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑤 ) ) ⇝𝑟 𝐴 ) |
| 15 |
7 8 14
|
rlimi |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) |
| 16 |
2
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → 𝑀 ∈ ℤ ) |
| 17 |
|
flcl |
⊢ ( 𝑧 ∈ ℝ → ( ⌊ ‘ 𝑧 ) ∈ ℤ ) |
| 18 |
17
|
peano2zd |
⊢ ( 𝑧 ∈ ℝ → ( ( ⌊ ‘ 𝑧 ) + 1 ) ∈ ℤ ) |
| 19 |
18
|
ad2antrl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → ( ( ⌊ ‘ 𝑧 ) + 1 ) ∈ ℤ ) |
| 20 |
19 16
|
ifcld |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ∈ ℤ ) |
| 21 |
16
|
zred |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → 𝑀 ∈ ℝ ) |
| 22 |
19
|
zred |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → ( ( ⌊ ‘ 𝑧 ) + 1 ) ∈ ℝ ) |
| 23 |
|
max1 |
⊢ ( ( 𝑀 ∈ ℝ ∧ ( ( ⌊ ‘ 𝑧 ) + 1 ) ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) |
| 24 |
21 22 23
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) |
| 25 |
|
eluz2 |
⊢ ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ∈ ℤ ∧ 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) |
| 26 |
16 20 24 25
|
syl3anbrc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) |
| 27 |
26 1
|
eleqtrrdi |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ∈ 𝑍 ) |
| 28 |
|
simplrl |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑧 ∈ ℝ ) |
| 29 |
18
|
zred |
⊢ ( 𝑧 ∈ ℝ → ( ( ⌊ ‘ 𝑧 ) + 1 ) ∈ ℝ ) |
| 30 |
28 29
|
syl |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → ( ( ⌊ ‘ 𝑧 ) + 1 ) ∈ ℝ ) |
| 31 |
21
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑀 ∈ ℝ ) |
| 32 |
30 31
|
ifcld |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ∈ ℝ ) |
| 33 |
|
eluzelre |
⊢ ( 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) → 𝑘 ∈ ℝ ) |
| 34 |
33
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑘 ∈ ℝ ) |
| 35 |
|
fllep1 |
⊢ ( 𝑧 ∈ ℝ → 𝑧 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) ) |
| 36 |
28 35
|
syl |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑧 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) ) |
| 37 |
|
max2 |
⊢ ( ( 𝑀 ∈ ℝ ∧ ( ( ⌊ ‘ 𝑧 ) + 1 ) ∈ ℝ ) → ( ( ⌊ ‘ 𝑧 ) + 1 ) ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) |
| 38 |
31 30 37
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → ( ( ⌊ ‘ 𝑧 ) + 1 ) ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) |
| 39 |
28 30 32 36 38
|
letrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑧 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) |
| 40 |
|
eluzle |
⊢ ( 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ≤ 𝑘 ) |
| 41 |
40
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ≤ 𝑘 ) |
| 42 |
28 32 34 39 41
|
letrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑧 ≤ 𝑘 ) |
| 43 |
|
breq2 |
⊢ ( 𝑤 = 𝑘 → ( 𝑧 ≤ 𝑤 ↔ 𝑧 ≤ 𝑘 ) ) |
| 44 |
43
|
imbrov2fvoveq |
⊢ ( 𝑤 = 𝑘 → ( ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ↔ ( 𝑧 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) ) ) |
| 45 |
|
simplrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) |
| 46 |
4
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑍 ⊆ dom 𝐹 ) |
| 47 |
1
|
uztrn2 |
⊢ ( ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑘 ∈ 𝑍 ) |
| 48 |
27 47
|
sylan |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑘 ∈ 𝑍 ) |
| 49 |
46 48
|
sseldd |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑘 ∈ dom 𝐹 ) |
| 50 |
44 45 49
|
rspcdva |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → ( 𝑧 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) ) |
| 51 |
42 50
|
mpd |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) |
| 52 |
51
|
ralrimiva |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) |
| 53 |
|
fveq2 |
⊢ ( 𝑗 = if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) |
| 54 |
53
|
raleqdv |
⊢ ( 𝑗 = if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) ) |
| 55 |
54
|
rspcev |
⊢ ( ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) |
| 56 |
27 52 55
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) |
| 57 |
15 56
|
rexlimddv |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) |
| 58 |
57
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) |
| 59 |
|
rlimpm |
⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐹 ∈ ( ℂ ↑pm ℝ ) ) |
| 60 |
3 59
|
syl |
⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑pm ℝ ) ) |
| 61 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) ) |
| 62 |
|
rlimcl |
⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐴 ∈ ℂ ) |
| 63 |
3 62
|
syl |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
| 64 |
4
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ dom 𝐹 ) |
| 65 |
10
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
| 66 |
64 65
|
syldan |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
| 67 |
1 2 60 61 63 66
|
clim2c |
⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) ) |
| 68 |
58 67
|
mpbird |
⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 ) |