Step | Hyp | Ref
| Expression |
1 | | imaco 5557 |
. . . 4
⊢ ((abs
∘ 𝐹) “ ℝ)
= (abs “ (𝐹 “
ℝ)) |
2 | 1 | eqcomi 2619 |
. . 3
⊢ (abs
“ (𝐹 “
ℝ)) = ((abs ∘ 𝐹) “ ℝ) |
3 | | imassrn 5396 |
. . . . 5
⊢ ((abs
∘ 𝐹) “ ℝ)
⊆ ran (abs ∘ 𝐹) |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 → ((abs ∘ 𝐹) “ ℝ) ⊆ ran
(abs ∘ 𝐹)) |
5 | | imo72b2lem1.1 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
6 | | absf 13925 |
. . . . . . . 8
⊢
abs:ℂ⟶ℝ |
7 | 6 | a1i 11 |
. . . . . . 7
⊢ (𝜑 →
abs:ℂ⟶ℝ) |
8 | | ax-resscn 9872 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ⊆
ℂ) |
10 | 7, 9 | fssresd 5984 |
. . . . . 6
⊢ (𝜑 → (abs ↾
ℝ):ℝ⟶ℝ) |
11 | 5, 10 | fco2d 37481 |
. . . . 5
⊢ (𝜑 → (abs ∘ 𝐹):ℝ⟶ℝ) |
12 | | frn 5966 |
. . . . 5
⊢ ((abs
∘ 𝐹):ℝ⟶ℝ → ran (abs
∘ 𝐹) ⊆
ℝ) |
13 | 11, 12 | syl 17 |
. . . 4
⊢ (𝜑 → ran (abs ∘ 𝐹) ⊆
ℝ) |
14 | 4, 13 | sstrd 3578 |
. . 3
⊢ (𝜑 → ((abs ∘ 𝐹) “ ℝ) ⊆
ℝ) |
15 | 2, 14 | syl5eqss 3612 |
. 2
⊢ (𝜑 → (abs “ (𝐹 “ ℝ)) ⊆
ℝ) |
16 | | 0re 9919 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
17 | 16 | ne0ii 3882 |
. . . . . . 7
⊢ ℝ
≠ ∅ |
18 | 17 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ≠
∅) |
19 | 18, 11 | wnefimgd 37480 |
. . . . 5
⊢ (𝜑 → ((abs ∘ 𝐹) “ ℝ) ≠
∅) |
20 | 19 | necomd 2837 |
. . . 4
⊢ (𝜑 → ∅ ≠ ((abs ∘
𝐹) “
ℝ)) |
21 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → (abs “ (𝐹 “ ℝ)) = ((abs
∘ 𝐹) “
ℝ)) |
22 | 20, 21 | neeqtrrd 2856 |
. . 3
⊢ (𝜑 → ∅ ≠ (abs “
(𝐹 “
ℝ))) |
23 | 22 | necomd 2837 |
. 2
⊢ (𝜑 → (abs “ (𝐹 “ ℝ)) ≠
∅) |
24 | | 1red 9934 |
. . 3
⊢ (𝜑 → 1 ∈
ℝ) |
25 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 = 1) → 𝑐 = 1) |
26 | 25 | breq2d 4595 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 = 1) → (𝑡 ≤ 𝑐 ↔ 𝑡 ≤ 1)) |
27 | 26 | ralbidv 2969 |
. . 3
⊢ ((𝜑 ∧ 𝑐 = 1) → (∀𝑡 ∈ (abs “ (𝐹 “ ℝ))𝑡 ≤ 𝑐 ↔ ∀𝑡 ∈ (abs “ (𝐹 “ ℝ))𝑡 ≤ 1)) |
28 | | imo72b2lem1.6 |
. . . 4
⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1) |
29 | 5, 28 | extoimad 37486 |
. . 3
⊢ (𝜑 → ∀𝑡 ∈ (abs “ (𝐹 “ ℝ))𝑡 ≤ 1) |
30 | 24, 27, 29 | rspcedvd 3289 |
. 2
⊢ (𝜑 → ∃𝑐 ∈ ℝ ∀𝑡 ∈ (abs “ (𝐹 “ ℝ))𝑡 ≤ 𝑐) |
31 | | 0red 9920 |
. 2
⊢ (𝜑 → 0 ∈
ℝ) |
32 | | imo72b2lem1.7 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ ℝ (𝐹‘𝑥) ≠ 0) |
33 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → 𝐹:ℝ⟶ℝ) |
34 | | simprl 790 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → 𝑥 ∈ ℝ) |
35 | 33, 34 | fvco3d 37484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → ((abs ∘ 𝐹)‘𝑥) = (abs‘(𝐹‘𝑥))) |
36 | 11 | funfvima2d 37491 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs ∘ 𝐹)‘𝑥) ∈ ((abs ∘ 𝐹) “ ℝ)) |
37 | 36 | adantrr 749 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → ((abs ∘ 𝐹)‘𝑥) ∈ ((abs ∘ 𝐹) “ ℝ)) |
38 | 37, 1 | syl6eleq 2698 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → ((abs ∘ 𝐹)‘𝑥) ∈ (abs “ (𝐹 “ ℝ))) |
39 | 35, 38 | eqeltrrd 2689 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → (abs‘(𝐹‘𝑥)) ∈ (abs “ (𝐹 “ ℝ))) |
40 | | simpr 476 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) ∧ 𝑧 = (abs‘(𝐹‘𝑥))) → 𝑧 = (abs‘(𝐹‘𝑥))) |
41 | 40 | breq2d 4595 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) ∧ 𝑧 = (abs‘(𝐹‘𝑥))) → (0 < 𝑧 ↔ 0 < (abs‘(𝐹‘𝑥)))) |
42 | 5 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
43 | 42 | adantrr 749 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → (𝐹‘𝑥) ∈ ℝ) |
44 | 43 | recnd 9947 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → (𝐹‘𝑥) ∈ ℂ) |
45 | | simprr 792 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → (𝐹‘𝑥) ≠ 0) |
46 | 44, 45 | absrpcld 14035 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → (abs‘(𝐹‘𝑥)) ∈
ℝ+) |
47 | 46 | rpgt0d 11751 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → 0 < (abs‘(𝐹‘𝑥))) |
48 | 39, 41, 47 | rspcedvd 3289 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → ∃𝑧 ∈ (abs “ (𝐹 “ ℝ))0 < 𝑧) |
49 | 32, 48 | rexlimddv 3017 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ (abs “ (𝐹 “ ℝ))0 < 𝑧) |
50 | 15, 23, 30, 31, 49 | suprlubrd 37492 |
1
⊢ (𝜑 → 0 < sup((abs “
(𝐹 “ ℝ)),
ℝ, < )) |