Step |
Hyp |
Ref |
Expression |
1 |
|
rlimf |
⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐹 : dom 𝐹 ⟶ ℂ ) |
2 |
1
|
ffvelrnda |
⊢ ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑧 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ ) |
3 |
2
|
ralrimiva |
⊢ ( 𝐹 ⇝𝑟 𝐴 → ∀ 𝑧 ∈ dom 𝐹 ( 𝐹 ‘ 𝑧 ) ∈ ℂ ) |
4 |
|
1rp |
⊢ 1 ∈ ℝ+ |
5 |
4
|
a1i |
⊢ ( 𝐹 ⇝𝑟 𝐴 → 1 ∈ ℝ+ ) |
6 |
1
|
feqmptd |
⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐹 = ( 𝑧 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑧 ) ) ) |
7 |
|
id |
⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐹 ⇝𝑟 𝐴 ) |
8 |
6 7
|
eqbrtrrd |
⊢ ( 𝐹 ⇝𝑟 𝐴 → ( 𝑧 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑧 ) ) ⇝𝑟 𝐴 ) |
9 |
3 5 8
|
rlimi |
⊢ ( 𝐹 ⇝𝑟 𝐴 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐴 ) ) < 1 ) ) |
10 |
|
rlimcl |
⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐴 ∈ ℂ ) |
11 |
10
|
adantr |
⊢ ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) → 𝐴 ∈ ℂ ) |
12 |
11
|
abscld |
⊢ ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) → ( abs ‘ 𝐴 ) ∈ ℝ ) |
13 |
|
peano2re |
⊢ ( ( abs ‘ 𝐴 ) ∈ ℝ → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℝ ) |
14 |
12 13
|
syl |
⊢ ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℝ ) |
15 |
2
|
adantlr |
⊢ ( ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ ) |
16 |
11
|
adantr |
⊢ ( ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → 𝐴 ∈ ℂ ) |
17 |
15 16
|
abs2difd |
⊢ ( ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) − ( abs ‘ 𝐴 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐴 ) ) ) |
18 |
15
|
abscld |
⊢ ( ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ ) |
19 |
12
|
adantr |
⊢ ( ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( abs ‘ 𝐴 ) ∈ ℝ ) |
20 |
18 19
|
resubcld |
⊢ ( ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) − ( abs ‘ 𝐴 ) ) ∈ ℝ ) |
21 |
15 16
|
subcld |
⊢ ( ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑧 ) − 𝐴 ) ∈ ℂ ) |
22 |
21
|
abscld |
⊢ ( ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐴 ) ) ∈ ℝ ) |
23 |
|
1red |
⊢ ( ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → 1 ∈ ℝ ) |
24 |
|
lelttr |
⊢ ( ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) − ( abs ‘ 𝐴 ) ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐴 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) − ( abs ‘ 𝐴 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐴 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐴 ) ) < 1 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) − ( abs ‘ 𝐴 ) ) < 1 ) ) |
25 |
20 22 23 24
|
syl3anc |
⊢ ( ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) − ( abs ‘ 𝐴 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐴 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐴 ) ) < 1 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) − ( abs ‘ 𝐴 ) ) < 1 ) ) |
26 |
17 25
|
mpand |
⊢ ( ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐴 ) ) < 1 → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) − ( abs ‘ 𝐴 ) ) < 1 ) ) |
27 |
18 19 23
|
ltsubadd2d |
⊢ ( ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) − ( abs ‘ 𝐴 ) ) < 1 ↔ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) < ( ( abs ‘ 𝐴 ) + 1 ) ) ) |
28 |
26 27
|
sylibd |
⊢ ( ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐴 ) ) < 1 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) < ( ( abs ‘ 𝐴 ) + 1 ) ) ) |
29 |
14
|
adantr |
⊢ ( ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℝ ) |
30 |
|
ltle |
⊢ ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ ∧ ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℝ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) < ( ( abs ‘ 𝐴 ) + 1 ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) ) |
31 |
18 29 30
|
syl2anc |
⊢ ( ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) < ( ( abs ‘ 𝐴 ) + 1 ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) ) |
32 |
28 31
|
syld |
⊢ ( ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐴 ) ) < 1 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) ) |
33 |
32
|
imim2d |
⊢ ( ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐴 ) ) < 1 ) → ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) ) ) |
34 |
33
|
ralimdva |
⊢ ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐴 ) ) < 1 ) → ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) ) ) |
35 |
|
breq2 |
⊢ ( 𝑤 = ( ( abs ‘ 𝐴 ) + 1 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑤 ↔ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) ) |
36 |
35
|
imbi2d |
⊢ ( 𝑤 = ( ( abs ‘ 𝐴 ) + 1 ) → ( ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑤 ) ↔ ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) ) ) |
37 |
36
|
ralbidv |
⊢ ( 𝑤 = ( ( abs ‘ 𝐴 ) + 1 ) → ( ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑤 ) ↔ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) ) ) |
38 |
37
|
rspcev |
⊢ ( ( ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℝ ∧ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) ) → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑤 ) ) |
39 |
14 34 38
|
syl6an |
⊢ ( ( 𝐹 ⇝𝑟 𝐴 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐴 ) ) < 1 ) → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑤 ) ) ) |
40 |
39
|
reximdva |
⊢ ( 𝐹 ⇝𝑟 𝐴 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐴 ) ) < 1 ) → ∃ 𝑦 ∈ ℝ ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑤 ) ) ) |
41 |
9 40
|
mpd |
⊢ ( 𝐹 ⇝𝑟 𝐴 → ∃ 𝑦 ∈ ℝ ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑤 ) ) |
42 |
|
rlimss |
⊢ ( 𝐹 ⇝𝑟 𝐴 → dom 𝐹 ⊆ ℝ ) |
43 |
|
elo12 |
⊢ ( ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℝ ) → ( 𝐹 ∈ 𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑤 ) ) ) |
44 |
1 42 43
|
syl2anc |
⊢ ( 𝐹 ⇝𝑟 𝐴 → ( 𝐹 ∈ 𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑤 ) ) ) |
45 |
41 44
|
mpbird |
⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐹 ∈ 𝑂(1) ) |