Step | Hyp | Ref
| Expression |
1 | | imaco 5894 |
. . . 4
⊢ ((abs
∘ 𝐹) “ ℝ)
= (abs “ (𝐹 “
ℝ)) |
2 | 1 | eqcomi 2786 |
. . 3
⊢ (abs
“ (𝐹 “
ℝ)) = ((abs ∘ 𝐹) “ ℝ) |
3 | | imassrn 5731 |
. . . . 5
⊢ ((abs
∘ 𝐹) “ ℝ)
⊆ ran (abs ∘ 𝐹) |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 → ((abs ∘ 𝐹) “ ℝ) ⊆ ran
(abs ∘ 𝐹)) |
5 | | imo72b2lem1.1 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
6 | | absf 14484 |
. . . . . . . 8
⊢
abs:ℂ⟶ℝ |
7 | 6 | a1i 11 |
. . . . . . 7
⊢ (𝜑 →
abs:ℂ⟶ℝ) |
8 | | ax-resscn 10329 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ⊆
ℂ) |
10 | 7, 9 | fssresd 6321 |
. . . . . 6
⊢ (𝜑 → (abs ↾
ℝ):ℝ⟶ℝ) |
11 | 5, 10 | fco2d 39399 |
. . . . 5
⊢ (𝜑 → (abs ∘ 𝐹):ℝ⟶ℝ) |
12 | 11 | frnd 6298 |
. . . 4
⊢ (𝜑 → ran (abs ∘ 𝐹) ⊆
ℝ) |
13 | 4, 12 | sstrd 3830 |
. . 3
⊢ (𝜑 → ((abs ∘ 𝐹) “ ℝ) ⊆
ℝ) |
14 | 2, 13 | syl5eqss 3867 |
. 2
⊢ (𝜑 → (abs “ (𝐹 “ ℝ)) ⊆
ℝ) |
15 | | 0re 10378 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
16 | 15 | ne0ii 4151 |
. . . . . . 7
⊢ ℝ
≠ ∅ |
17 | 16 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ≠
∅) |
18 | 17, 11 | wnefimgd 39398 |
. . . . 5
⊢ (𝜑 → ((abs ∘ 𝐹) “ ℝ) ≠
∅) |
19 | 18 | necomd 3023 |
. . . 4
⊢ (𝜑 → ∅ ≠ ((abs ∘
𝐹) “
ℝ)) |
20 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → (abs “ (𝐹 “ ℝ)) = ((abs
∘ 𝐹) “
ℝ)) |
21 | 19, 20 | neeqtrrd 3042 |
. . 3
⊢ (𝜑 → ∅ ≠ (abs “
(𝐹 “
ℝ))) |
22 | 21 | necomd 3023 |
. 2
⊢ (𝜑 → (abs “ (𝐹 “ ℝ)) ≠
∅) |
23 | | 1red 10377 |
. . 3
⊢ (𝜑 → 1 ∈
ℝ) |
24 | | simpr 479 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 = 1) → 𝑐 = 1) |
25 | 24 | breq2d 4898 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 = 1) → (𝑡 ≤ 𝑐 ↔ 𝑡 ≤ 1)) |
26 | 25 | ralbidv 3167 |
. . 3
⊢ ((𝜑 ∧ 𝑐 = 1) → (∀𝑡 ∈ (abs “ (𝐹 “ ℝ))𝑡 ≤ 𝑐 ↔ ∀𝑡 ∈ (abs “ (𝐹 “ ℝ))𝑡 ≤ 1)) |
27 | | imo72b2lem1.6 |
. . . 4
⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1) |
28 | 5, 27 | extoimad 39402 |
. . 3
⊢ (𝜑 → ∀𝑡 ∈ (abs “ (𝐹 “ ℝ))𝑡 ≤ 1) |
29 | 23, 26, 28 | rspcedvd 3517 |
. 2
⊢ (𝜑 → ∃𝑐 ∈ ℝ ∀𝑡 ∈ (abs “ (𝐹 “ ℝ))𝑡 ≤ 𝑐) |
30 | | 0red 10380 |
. 2
⊢ (𝜑 → 0 ∈
ℝ) |
31 | | imo72b2lem1.7 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ ℝ (𝐹‘𝑥) ≠ 0) |
32 | 5 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → 𝐹:ℝ⟶ℝ) |
33 | | simprl 761 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → 𝑥 ∈ ℝ) |
34 | 32, 33 | fvco3d 39400 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → ((abs ∘ 𝐹)‘𝑥) = (abs‘(𝐹‘𝑥))) |
35 | 11 | funfvima2d 39407 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs ∘ 𝐹)‘𝑥) ∈ ((abs ∘ 𝐹) “ ℝ)) |
36 | 35 | adantrr 707 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → ((abs ∘ 𝐹)‘𝑥) ∈ ((abs ∘ 𝐹) “ ℝ)) |
37 | 36, 1 | syl6eleq 2868 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → ((abs ∘ 𝐹)‘𝑥) ∈ (abs “ (𝐹 “ ℝ))) |
38 | 34, 37 | eqeltrrd 2859 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → (abs‘(𝐹‘𝑥)) ∈ (abs “ (𝐹 “ ℝ))) |
39 | | simpr 479 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) ∧ 𝑧 = (abs‘(𝐹‘𝑥))) → 𝑧 = (abs‘(𝐹‘𝑥))) |
40 | 39 | breq2d 4898 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) ∧ 𝑧 = (abs‘(𝐹‘𝑥))) → (0 < 𝑧 ↔ 0 < (abs‘(𝐹‘𝑥)))) |
41 | 5 | ffvelrnda 6623 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
42 | 41 | adantrr 707 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → (𝐹‘𝑥) ∈ ℝ) |
43 | 42 | recnd 10405 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → (𝐹‘𝑥) ∈ ℂ) |
44 | | simprr 763 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → (𝐹‘𝑥) ≠ 0) |
45 | 43, 44 | absrpcld 14595 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → (abs‘(𝐹‘𝑥)) ∈
ℝ+) |
46 | 45 | rpgt0d 12184 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → 0 < (abs‘(𝐹‘𝑥))) |
47 | 38, 40, 46 | rspcedvd 3517 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ≠ 0)) → ∃𝑧 ∈ (abs “ (𝐹 “ ℝ))0 < 𝑧) |
48 | 31, 47 | rexlimddv 3217 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ (abs “ (𝐹 “ ℝ))0 < 𝑧) |
49 | 14, 22, 29, 30, 48 | suprlubrd 39408 |
1
⊢ (𝜑 → 0 < sup((abs “
(𝐹 “ ℝ)),
ℝ, < )) |