Step | Hyp | Ref
| Expression |
1 | | rlimf 15062 |
. . . . . 6
⊢ (𝐹 ⇝𝑟
𝐴 → 𝐹:dom 𝐹⟶ℂ) |
2 | 1 | ffvelrnda 6904 |
. . . . 5
⊢ ((𝐹 ⇝𝑟
𝐴 ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ) |
3 | 2 | ralrimiva 3105 |
. . . 4
⊢ (𝐹 ⇝𝑟
𝐴 → ∀𝑧 ∈ dom 𝐹(𝐹‘𝑧) ∈ ℂ) |
4 | | 1rp 12590 |
. . . . 5
⊢ 1 ∈
ℝ+ |
5 | 4 | a1i 11 |
. . . 4
⊢ (𝐹 ⇝𝑟
𝐴 → 1 ∈
ℝ+) |
6 | 1 | feqmptd 6780 |
. . . . 5
⊢ (𝐹 ⇝𝑟
𝐴 → 𝐹 = (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧))) |
7 | | id 22 |
. . . . 5
⊢ (𝐹 ⇝𝑟
𝐴 → 𝐹 ⇝𝑟 𝐴) |
8 | 6, 7 | eqbrtrrd 5077 |
. . . 4
⊢ (𝐹 ⇝𝑟
𝐴 → (𝑧 ∈ dom 𝐹 ↦ (𝐹‘𝑧)) ⇝𝑟 𝐴) |
9 | 3, 5, 8 | rlimi 15074 |
. . 3
⊢ (𝐹 ⇝𝑟
𝐴 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑦 ≤ 𝑧 → (abs‘((𝐹‘𝑧) − 𝐴)) < 1)) |
10 | | rlimcl 15064 |
. . . . . . . 8
⊢ (𝐹 ⇝𝑟
𝐴 → 𝐴 ∈ ℂ) |
11 | 10 | adantr 484 |
. . . . . . 7
⊢ ((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) → 𝐴 ∈ ℂ) |
12 | 11 | abscld 15000 |
. . . . . 6
⊢ ((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) → (abs‘𝐴) ∈
ℝ) |
13 | | peano2re 11005 |
. . . . . 6
⊢
((abs‘𝐴)
∈ ℝ → ((abs‘𝐴) + 1) ∈ ℝ) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ ((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) → ((abs‘𝐴) + 1) ∈
ℝ) |
15 | 2 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ℂ) |
16 | 11 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → 𝐴 ∈ ℂ) |
17 | 15, 16 | abs2difd 15021 |
. . . . . . . . . 10
⊢ (((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → ((abs‘(𝐹‘𝑧)) − (abs‘𝐴)) ≤ (abs‘((𝐹‘𝑧) − 𝐴))) |
18 | 15 | abscld 15000 |
. . . . . . . . . . . 12
⊢ (((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (abs‘(𝐹‘𝑧)) ∈ ℝ) |
19 | 12 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (abs‘𝐴) ∈ ℝ) |
20 | 18, 19 | resubcld 11260 |
. . . . . . . . . . 11
⊢ (((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → ((abs‘(𝐹‘𝑧)) − (abs‘𝐴)) ∈ ℝ) |
21 | 15, 16 | subcld 11189 |
. . . . . . . . . . . 12
⊢ (((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → ((𝐹‘𝑧) − 𝐴) ∈ ℂ) |
22 | 21 | abscld 15000 |
. . . . . . . . . . 11
⊢ (((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (abs‘((𝐹‘𝑧) − 𝐴)) ∈ ℝ) |
23 | | 1red 10834 |
. . . . . . . . . . 11
⊢ (((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → 1 ∈ ℝ) |
24 | | lelttr 10923 |
. . . . . . . . . . 11
⊢
((((abs‘(𝐹‘𝑧)) − (abs‘𝐴)) ∈ ℝ ∧ (abs‘((𝐹‘𝑧) − 𝐴)) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((((abs‘(𝐹‘𝑧)) − (abs‘𝐴)) ≤ (abs‘((𝐹‘𝑧) − 𝐴)) ∧ (abs‘((𝐹‘𝑧) − 𝐴)) < 1) → ((abs‘(𝐹‘𝑧)) − (abs‘𝐴)) < 1)) |
25 | 20, 22, 23, 24 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → ((((abs‘(𝐹‘𝑧)) − (abs‘𝐴)) ≤ (abs‘((𝐹‘𝑧) − 𝐴)) ∧ (abs‘((𝐹‘𝑧) − 𝐴)) < 1) → ((abs‘(𝐹‘𝑧)) − (abs‘𝐴)) < 1)) |
26 | 17, 25 | mpand 695 |
. . . . . . . . 9
⊢ (((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → ((abs‘((𝐹‘𝑧) − 𝐴)) < 1 → ((abs‘(𝐹‘𝑧)) − (abs‘𝐴)) < 1)) |
27 | 18, 19, 23 | ltsubadd2d 11430 |
. . . . . . . . 9
⊢ (((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → (((abs‘(𝐹‘𝑧)) − (abs‘𝐴)) < 1 ↔ (abs‘(𝐹‘𝑧)) < ((abs‘𝐴) + 1))) |
28 | 26, 27 | sylibd 242 |
. . . . . . . 8
⊢ (((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → ((abs‘((𝐹‘𝑧) − 𝐴)) < 1 → (abs‘(𝐹‘𝑧)) < ((abs‘𝐴) + 1))) |
29 | 14 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → ((abs‘𝐴) + 1) ∈ ℝ) |
30 | | ltle 10921 |
. . . . . . . . 9
⊢
(((abs‘(𝐹‘𝑧)) ∈ ℝ ∧ ((abs‘𝐴) + 1) ∈ ℝ) →
((abs‘(𝐹‘𝑧)) < ((abs‘𝐴) + 1) → (abs‘(𝐹‘𝑧)) ≤ ((abs‘𝐴) + 1))) |
31 | 18, 29, 30 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → ((abs‘(𝐹‘𝑧)) < ((abs‘𝐴) + 1) → (abs‘(𝐹‘𝑧)) ≤ ((abs‘𝐴) + 1))) |
32 | 28, 31 | syld 47 |
. . . . . . 7
⊢ (((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → ((abs‘((𝐹‘𝑧) − 𝐴)) < 1 → (abs‘(𝐹‘𝑧)) ≤ ((abs‘𝐴) + 1))) |
33 | 32 | imim2d 57 |
. . . . . 6
⊢ (((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ dom 𝐹) → ((𝑦 ≤ 𝑧 → (abs‘((𝐹‘𝑧) − 𝐴)) < 1) → (𝑦 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ ((abs‘𝐴) + 1)))) |
34 | 33 | ralimdva 3100 |
. . . . 5
⊢ ((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) → (∀𝑧 ∈ dom 𝐹(𝑦 ≤ 𝑧 → (abs‘((𝐹‘𝑧) − 𝐴)) < 1) → ∀𝑧 ∈ dom 𝐹(𝑦 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ ((abs‘𝐴) + 1)))) |
35 | | breq2 5057 |
. . . . . . . 8
⊢ (𝑤 = ((abs‘𝐴) + 1) → ((abs‘(𝐹‘𝑧)) ≤ 𝑤 ↔ (abs‘(𝐹‘𝑧)) ≤ ((abs‘𝐴) + 1))) |
36 | 35 | imbi2d 344 |
. . . . . . 7
⊢ (𝑤 = ((abs‘𝐴) + 1) → ((𝑦 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑤) ↔ (𝑦 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ ((abs‘𝐴) + 1)))) |
37 | 36 | ralbidv 3118 |
. . . . . 6
⊢ (𝑤 = ((abs‘𝐴) + 1) → (∀𝑧 ∈ dom 𝐹(𝑦 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑤) ↔ ∀𝑧 ∈ dom 𝐹(𝑦 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ ((abs‘𝐴) + 1)))) |
38 | 37 | rspcev 3537 |
. . . . 5
⊢
((((abs‘𝐴) +
1) ∈ ℝ ∧ ∀𝑧 ∈ dom 𝐹(𝑦 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ ((abs‘𝐴) + 1))) → ∃𝑤 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑦 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑤)) |
39 | 14, 34, 38 | syl6an 684 |
. . . 4
⊢ ((𝐹 ⇝𝑟
𝐴 ∧ 𝑦 ∈ ℝ) → (∀𝑧 ∈ dom 𝐹(𝑦 ≤ 𝑧 → (abs‘((𝐹‘𝑧) − 𝐴)) < 1) → ∃𝑤 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑦 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑤))) |
40 | 39 | reximdva 3193 |
. . 3
⊢ (𝐹 ⇝𝑟
𝐴 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑦 ≤ 𝑧 → (abs‘((𝐹‘𝑧) − 𝐴)) < 1) → ∃𝑦 ∈ ℝ ∃𝑤 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑦 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑤))) |
41 | 9, 40 | mpd 15 |
. 2
⊢ (𝐹 ⇝𝑟
𝐴 → ∃𝑦 ∈ ℝ ∃𝑤 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑦 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑤)) |
42 | | rlimss 15063 |
. . 3
⊢ (𝐹 ⇝𝑟
𝐴 → dom 𝐹 ⊆
ℝ) |
43 | | elo12 15088 |
. . 3
⊢ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ) → (𝐹 ∈ 𝑂(1) ↔ ∃𝑦 ∈ ℝ ∃𝑤 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑦 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑤))) |
44 | 1, 42, 43 | syl2anc 587 |
. 2
⊢ (𝐹 ⇝𝑟
𝐴 → (𝐹 ∈ 𝑂(1) ↔ ∃𝑦 ∈ ℝ ∃𝑤 ∈ ℝ ∀𝑧 ∈ dom 𝐹(𝑦 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑤))) |
45 | 41, 44 | mpbird 260 |
1
⊢ (𝐹 ⇝𝑟
𝐴 → 𝐹 ∈ 𝑂(1)) |