Step | Hyp | Ref
| Expression |
1 | | imaco 5640 |
. . . 4
⊢ ((abs
∘ 𝐹) “ ℝ)
= (abs “ (𝐹 “
ℝ)) |
2 | 1 | eqcomi 2631 |
. . 3
⊢ (abs
“ (𝐹 “
ℝ)) = ((abs ∘ 𝐹) “ ℝ) |
3 | | imassrn 5477 |
. . . . 5
⊢ ((abs
∘ 𝐹) “ ℝ)
⊆ ran (abs ∘ 𝐹) |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 → ((abs ∘ 𝐹) “ ℝ) ⊆ ran
(abs ∘ 𝐹)) |
5 | | imo72b2lem1.1 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
6 | | absf 14077 |
. . . . . . . 8
⊢
abs:ℂ⟶ℝ |
7 | 6 | a1i 11 |
. . . . . . 7
⊢ (𝜑 →
abs:ℂ⟶ℝ) |
8 | | ax-resscn 9993 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ⊆
ℂ) |
10 | 7, 9 | fssresd 6071 |
. . . . . 6
⊢ (𝜑 → (abs ↾
ℝ):ℝ⟶ℝ) |
11 | 5, 10 | fco2d 38461 |
. . . . 5
⊢ (𝜑 → (abs ∘ 𝐹):ℝ⟶ℝ) |
12 | | frn 6053 |
. . . . 5
⊢ ((abs
∘ 𝐹):ℝ⟶ℝ → ran (abs
∘ 𝐹) ⊆
ℝ) |
13 | 11, 12 | syl 17 |
. . . 4
⊢ (𝜑 → ran (abs ∘ 𝐹) ⊆
ℝ) |
14 | 4, 13 | sstrd 3613 |
. . 3
⊢ (𝜑 → ((abs ∘ 𝐹) “ ℝ) ⊆
ℝ) |
15 | 2, 14 | syl5eqss 3649 |
. 2
⊢ (𝜑 → (abs “ (𝐹 “ ℝ)) ⊆
ℝ) |
16 | | 0re 10040 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
17 | 16 | ne0ii 3923 |
. . . . . . 7
⊢ ℝ
≠ ∅ |
18 | 17 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ≠
∅) |
19 | 18, 11 | wnefimgd 38460 |
. . . . 5
⊢ (𝜑 → ((abs ∘ 𝐹) “ ℝ) ≠
∅) |
20 | 19 | necomd 2849 |
. . . 4
⊢ (𝜑 → ∅ ≠ ((abs ∘
𝐹) “
ℝ)) |
21 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → (abs “ (𝐹 “ ℝ)) = ((abs
∘ 𝐹) “
ℝ)) |
22 | 20, 21 | neeqtrrd 2868 |
. . 3
⊢ (𝜑 → ∅ ≠ (abs “
(𝐹 “
ℝ))) |
23 | 22 | necomd 2849 |
. 2
⊢ (𝜑 → (abs “ (𝐹 “ ℝ)) ≠
∅) |
24 | | 1red 10055 |
. . 3
⊢ (𝜑 → 1 ∈
ℝ) |
25 | | simpr 477 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 = 1) → 𝑐 = 1) |
26 | 25 | breq2d 4665 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 = 1) → (𝑡 ≤ 𝑐 ↔ 𝑡 ≤ 1)) |
27 | 26 | ralbidv 2986 |
. . 3
⊢ ((𝜑 ∧ 𝑐 = 1) → (∀𝑡 ∈ (abs “ (𝐹 “ ℝ))𝑡 ≤ 𝑐 ↔ ∀𝑡 ∈ (abs “ (𝐹 “ ℝ))𝑡 ≤ 1)) |
28 | | imo72b2lem1.6 |
. . . 4
⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1) |
29 | 5, 28 | extoimad 38464 |
. . 3
⊢ (𝜑 → ∀𝑡 ∈ (abs “ (𝐹 “ ℝ))𝑡 ≤ 1) |
30 | 24, 27, 29 | rspcedvd 3317 |
. 2
⊢ (𝜑 → ∃𝑐 ∈ ℝ ∀𝑡 ∈ (abs “ (𝐹 “ ℝ))𝑡 ≤ 𝑐) |
31 | | 0red 10041 |
. 2
⊢ (𝜑 → 0 ∈
ℝ) |
32 | | imo72b2lem1.7 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ ℝ (𝐹‘𝑥) ≠ 0) |
33 | 5 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → 𝐹:ℝ⟶ℝ) |
34 | | simprl 794 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → 𝑥 ∈ ℝ) |
35 | 33, 34 | fvco3d 38462 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → ((abs ∘ 𝐹)‘𝑥) = (abs‘(𝐹‘𝑥))) |
36 | 11 | funfvima2d 38469 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs ∘ 𝐹)‘𝑥) ∈ ((abs ∘ 𝐹) “ ℝ)) |
37 | 36 | adantrr 753 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → ((abs ∘ 𝐹)‘𝑥) ∈ ((abs ∘ 𝐹) “ ℝ)) |
38 | 37, 1 | syl6eleq 2711 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → ((abs ∘ 𝐹)‘𝑥) ∈ (abs “ (𝐹 “ ℝ))) |
39 | 35, 38 | eqeltrrd 2702 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → (abs‘(𝐹‘𝑥)) ∈ (abs “ (𝐹 “ ℝ))) |
40 | | simpr 477 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) ∧ 𝑧 = (abs‘(𝐹‘𝑥))) → 𝑧 = (abs‘(𝐹‘𝑥))) |
41 | 40 | breq2d 4665 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) ∧ 𝑧 = (abs‘(𝐹‘𝑥))) → (0 < 𝑧 ↔ 0 < (abs‘(𝐹‘𝑥)))) |
42 | 5 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
43 | 42 | adantrr 753 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → (𝐹‘𝑥) ∈ ℝ) |
44 | 43 | recnd 10068 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → (𝐹‘𝑥) ∈ ℂ) |
45 | | simprr 796 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → (𝐹‘𝑥) ≠ 0) |
46 | 44, 45 | absrpcld 14187 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → (abs‘(𝐹‘𝑥)) ∈
ℝ+) |
47 | 46 | rpgt0d 11875 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → 0 < (abs‘(𝐹‘𝑥))) |
48 | 39, 41, 47 | rspcedvd 3317 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → ∃𝑧 ∈ (abs “ (𝐹 “ ℝ))0 < 𝑧) |
49 | 32, 48 | rexlimddv 3035 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ (abs “ (𝐹 “ ℝ))0 < 𝑧) |
50 | 15, 23, 30, 31, 49 | suprlubrd 38470 |
1
⊢ (𝜑 → 0 < sup((abs “
(𝐹 “ ℝ)),
ℝ, < )) |