Step | Hyp | Ref
| Expression |
1 | | imo72b2lem0.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
2 | | imo72b2lem0.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 1, 2 | ffvelrnd 6268 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℝ) |
4 | 3 | recnd 9947 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℂ) |
5 | 4 | idi 2 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℂ) |
6 | | imo72b2lem0.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:ℝ⟶ℝ) |
7 | | imo72b2lem0.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℝ) |
8 | 6, 7 | ffvelrnd 6268 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘𝐵) ∈ ℝ) |
9 | 8 | recnd 9947 |
. . . . . 6
⊢ (𝜑 → (𝐺‘𝐵) ∈ ℂ) |
10 | 9 | idi 2 |
. . . . 5
⊢ (𝜑 → (𝐺‘𝐵) ∈ ℂ) |
11 | 5, 10 | mulcld 9939 |
. . . 4
⊢ (𝜑 → ((𝐹‘𝐴) · (𝐺‘𝐵)) ∈ ℂ) |
12 | 11 | abscld 14023 |
. . 3
⊢ (𝜑 → (abs‘((𝐹‘𝐴) · (𝐺‘𝐵))) ∈ ℝ) |
13 | | imaco 5557 |
. . . . . 6
⊢ ((abs
∘ 𝐹) “ ℝ)
= (abs “ (𝐹 “
ℝ)) |
14 | 13 | eqcomi 2619 |
. . . . 5
⊢ (abs
“ (𝐹 “
ℝ)) = ((abs ∘ 𝐹) “ ℝ) |
15 | | imassrn 5396 |
. . . . . . 7
⊢ ((abs
∘ 𝐹) “ ℝ)
⊆ ran (abs ∘ 𝐹) |
16 | 15 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ((abs ∘ 𝐹) “ ℝ) ⊆ ran
(abs ∘ 𝐹)) |
17 | | absf 13925 |
. . . . . . . . . 10
⊢
abs:ℂ⟶ℝ |
18 | 17 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 →
abs:ℂ⟶ℝ) |
19 | | ax-resscn 9872 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℝ ⊆
ℂ) |
21 | 18, 20 | fssresd 5984 |
. . . . . . . 8
⊢ (𝜑 → (abs ↾
ℝ):ℝ⟶ℝ) |
22 | 1, 21 | fco2d 37481 |
. . . . . . 7
⊢ (𝜑 → (abs ∘ 𝐹):ℝ⟶ℝ) |
23 | | frn 5966 |
. . . . . . 7
⊢ ((abs
∘ 𝐹):ℝ⟶ℝ → ran (abs
∘ 𝐹) ⊆
ℝ) |
24 | 22, 23 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran (abs ∘ 𝐹) ⊆
ℝ) |
25 | 16, 24 | sstrd 3578 |
. . . . 5
⊢ (𝜑 → ((abs ∘ 𝐹) “ ℝ) ⊆
ℝ) |
26 | 14, 25 | syl5eqss 3612 |
. . . 4
⊢ (𝜑 → (abs “ (𝐹 “ ℝ)) ⊆
ℝ) |
27 | | 0re 9919 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
28 | 27 | ne0ii 3882 |
. . . . . . . . 9
⊢ ℝ
≠ ∅ |
29 | 28 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ≠
∅) |
30 | 29, 22 | wnefimgd 37480 |
. . . . . . 7
⊢ (𝜑 → ((abs ∘ 𝐹) “ ℝ) ≠
∅) |
31 | 30 | necomd 2837 |
. . . . . 6
⊢ (𝜑 → ∅ ≠ ((abs ∘
𝐹) “
ℝ)) |
32 | 14 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (abs “ (𝐹 “ ℝ)) = ((abs
∘ 𝐹) “
ℝ)) |
33 | 31, 32 | neeqtrrd 2856 |
. . . . 5
⊢ (𝜑 → ∅ ≠ (abs “
(𝐹 “
ℝ))) |
34 | 33 | necomd 2837 |
. . . 4
⊢ (𝜑 → (abs “ (𝐹 “ ℝ)) ≠
∅) |
35 | | 1red 9934 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℝ) |
36 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 = 1) → 𝑐 = 1) |
37 | 36 | breq2d 4595 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 = 1) → (𝑥 ≤ 𝑐 ↔ 𝑥 ≤ 1)) |
38 | 37 | ralbidv 2969 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 = 1) → (∀𝑥 ∈ (abs “ (𝐹 “ ℝ))𝑥 ≤ 𝑐 ↔ ∀𝑥 ∈ (abs “ (𝐹 “ ℝ))𝑥 ≤ 1)) |
39 | | imo72b2lem0.6 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1) |
40 | 1, 39 | extoimad 37486 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ (abs “ (𝐹 “ ℝ))𝑥 ≤ 1) |
41 | 35, 38, 40 | rspcedvd 3289 |
. . . 4
⊢ (𝜑 → ∃𝑐 ∈ ℝ ∀𝑥 ∈ (abs “ (𝐹 “ ℝ))𝑥 ≤ 𝑐) |
42 | 26, 34, 41 | suprcld 37483 |
. . 3
⊢ (𝜑 → sup((abs “ (𝐹 “ ℝ)), ℝ,
< ) ∈ ℝ) |
43 | | 2re 10967 |
. . . 4
⊢ 2 ∈
ℝ |
44 | 43 | a1i 11 |
. . 3
⊢ (𝜑 → 2 ∈
ℝ) |
45 | | imo72b2lem0.5 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘(𝐴 + 𝐵)) + (𝐹‘(𝐴 − 𝐵))) = (2 · ((𝐹‘𝐴) · (𝐺‘𝐵)))) |
46 | 45 | idi 2 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹‘(𝐴 + 𝐵)) + (𝐹‘(𝐴 − 𝐵))) = (2 · ((𝐹‘𝐴) · (𝐺‘𝐵)))) |
47 | 46 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 → (abs‘((𝐹‘(𝐴 + 𝐵)) + (𝐹‘(𝐴 − 𝐵)))) = (abs‘(2 · ((𝐹‘𝐴) · (𝐺‘𝐵))))) |
48 | | 2cnd 10970 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℂ) |
49 | 48, 11 | mulcld 9939 |
. . . . . . . 8
⊢ (𝜑 → (2 · ((𝐹‘𝐴) · (𝐺‘𝐵))) ∈ ℂ) |
50 | 49 | abscld 14023 |
. . . . . . 7
⊢ (𝜑 → (abs‘(2 ·
((𝐹‘𝐴) · (𝐺‘𝐵)))) ∈ ℝ) |
51 | 47, 50 | eqeltrd 2688 |
. . . . . 6
⊢ (𝜑 → (abs‘((𝐹‘(𝐴 + 𝐵)) + (𝐹‘(𝐴 − 𝐵)))) ∈ ℝ) |
52 | 1 | idi 2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
53 | 2 | idi 2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
54 | 7 | idi 2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) |
55 | 53, 54 | readdcld 9948 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ) |
56 | 52, 55 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘(𝐴 + 𝐵)) ∈ ℝ) |
57 | 56 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘(𝐴 + 𝐵)) ∈ ℂ) |
58 | 57 | abscld 14023 |
. . . . . . 7
⊢ (𝜑 → (abs‘(𝐹‘(𝐴 + 𝐵))) ∈ ℝ) |
59 | 53, 54 | resubcld 10337 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ) |
60 | 52, 59 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘(𝐴 − 𝐵)) ∈ ℝ) |
61 | 60 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘(𝐴 − 𝐵)) ∈ ℂ) |
62 | 61 | abscld 14023 |
. . . . . . 7
⊢ (𝜑 → (abs‘(𝐹‘(𝐴 − 𝐵))) ∈ ℝ) |
63 | 58, 62 | readdcld 9948 |
. . . . . 6
⊢ (𝜑 → ((abs‘(𝐹‘(𝐴 + 𝐵))) + (abs‘(𝐹‘(𝐴 − 𝐵)))) ∈ ℝ) |
64 | 44, 42 | remulcld 9949 |
. . . . . 6
⊢ (𝜑 → (2 · sup((abs
“ (𝐹 “
ℝ)), ℝ, < )) ∈ ℝ) |
65 | 57, 61 | abstrid 14043 |
. . . . . 6
⊢ (𝜑 → (abs‘((𝐹‘(𝐴 + 𝐵)) + (𝐹‘(𝐴 − 𝐵)))) ≤ ((abs‘(𝐹‘(𝐴 + 𝐵))) + (abs‘(𝐹‘(𝐴 − 𝐵))))) |
66 | 1, 55 | fvco3d 37484 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs ∘ 𝐹)‘(𝐴 + 𝐵)) = (abs‘(𝐹‘(𝐴 + 𝐵)))) |
67 | 55, 22 | wfximgfd 37485 |
. . . . . . . . . . 11
⊢ (𝜑 → ((abs ∘ 𝐹)‘(𝐴 + 𝐵)) ∈ ((abs ∘ 𝐹) “ ℝ)) |
68 | 32 | idi 2 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs “ (𝐹 “ ℝ)) = ((abs
∘ 𝐹) “
ℝ)) |
69 | 67, 68 | eleqtrrd 2691 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs ∘ 𝐹)‘(𝐴 + 𝐵)) ∈ (abs “ (𝐹 “ ℝ))) |
70 | 66, 69 | eqeltrrd 2689 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘(𝐹‘(𝐴 + 𝐵))) ∈ (abs “ (𝐹 “ ℝ))) |
71 | 26, 34, 41, 70 | suprubd 37482 |
. . . . . . . 8
⊢ (𝜑 → (abs‘(𝐹‘(𝐴 + 𝐵))) ≤ sup((abs “ (𝐹 “ ℝ)), ℝ, <
)) |
72 | 1, 59 | fvco3d 37484 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs ∘ 𝐹)‘(𝐴 − 𝐵)) = (abs‘(𝐹‘(𝐴 − 𝐵)))) |
73 | 59, 22 | wfximgfd 37485 |
. . . . . . . . . . 11
⊢ (𝜑 → ((abs ∘ 𝐹)‘(𝐴 − 𝐵)) ∈ ((abs ∘ 𝐹) “ ℝ)) |
74 | 73, 32 | eleqtrrd 2691 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs ∘ 𝐹)‘(𝐴 − 𝐵)) ∈ (abs “ (𝐹 “ ℝ))) |
75 | 72, 74 | eqeltrrd 2689 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘(𝐹‘(𝐴 − 𝐵))) ∈ (abs “ (𝐹 “ ℝ))) |
76 | 26, 34, 41, 75 | suprubd 37482 |
. . . . . . . 8
⊢ (𝜑 → (abs‘(𝐹‘(𝐴 − 𝐵))) ≤ sup((abs “ (𝐹 “ ℝ)), ℝ, <
)) |
77 | 58, 62, 42, 42, 71, 76 | le2addd 10525 |
. . . . . . 7
⊢ (𝜑 → ((abs‘(𝐹‘(𝐴 + 𝐵))) + (abs‘(𝐹‘(𝐴 − 𝐵)))) ≤ (sup((abs “ (𝐹 “ ℝ)), ℝ,
< ) + sup((abs “ (𝐹 “ ℝ)), ℝ, <
))) |
78 | 42 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → sup((abs “ (𝐹 “ ℝ)), ℝ,
< ) ∈ ℂ) |
79 | 78 | 2timesd 11152 |
. . . . . . . 8
⊢ (𝜑 → (2 · sup((abs
“ (𝐹 “
ℝ)), ℝ, < )) = (sup((abs “ (𝐹 “ ℝ)), ℝ, < ) +
sup((abs “ (𝐹 “
ℝ)), ℝ, < ))) |
80 | 79 | eqcomd 2616 |
. . . . . . 7
⊢ (𝜑 → (sup((abs “ (𝐹 “ ℝ)), ℝ,
< ) + sup((abs “ (𝐹 “ ℝ)), ℝ, < )) = (2
· sup((abs “ (𝐹 “ ℝ)), ℝ, <
))) |
81 | 80, 64 | eqeltrd 2688 |
. . . . . . 7
⊢ (𝜑 → (sup((abs “ (𝐹 “ ℝ)), ℝ,
< ) + sup((abs “ (𝐹 “ ℝ)), ℝ, < )) ∈
ℝ) |
82 | 77, 80, 63, 81 | leeq2d 37476 |
. . . . . 6
⊢ (𝜑 → ((abs‘(𝐹‘(𝐴 + 𝐵))) + (abs‘(𝐹‘(𝐴 − 𝐵)))) ≤ (2 · sup((abs “
(𝐹 “ ℝ)),
ℝ, < ))) |
83 | 51, 63, 64, 65, 82 | letrd 10073 |
. . . . 5
⊢ (𝜑 → (abs‘((𝐹‘(𝐴 + 𝐵)) + (𝐹‘(𝐴 − 𝐵)))) ≤ (2 · sup((abs “
(𝐹 “ ℝ)),
ℝ, < ))) |
84 | 83, 47, 51, 64 | leeq1d 37475 |
. . . 4
⊢ (𝜑 → (abs‘(2 ·
((𝐹‘𝐴) · (𝐺‘𝐵)))) ≤ (2 · sup((abs “
(𝐹 “ ℝ)),
ℝ, < ))) |
85 | | 0le2 10988 |
. . . . . 6
⊢ 0 ≤
2 |
86 | 85 | a1i 11 |
. . . . 5
⊢ (𝜑 → 0 ≤ 2) |
87 | 3 | idi 2 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℝ) |
88 | 8 | idi 2 |
. . . . . 6
⊢ (𝜑 → (𝐺‘𝐵) ∈ ℝ) |
89 | 87, 88 | remulcld 9949 |
. . . . 5
⊢ (𝜑 → ((𝐹‘𝐴) · (𝐺‘𝐵)) ∈ ℝ) |
90 | 86, 44, 89 | absmulrposd 37477 |
. . . 4
⊢ (𝜑 → (abs‘(2 ·
((𝐹‘𝐴) · (𝐺‘𝐵)))) = (2 · (abs‘((𝐹‘𝐴) · (𝐺‘𝐵))))) |
91 | 84, 90, 50, 64 | leeq1d 37475 |
. . 3
⊢ (𝜑 → (2 ·
(abs‘((𝐹‘𝐴) · (𝐺‘𝐵)))) ≤ (2 · sup((abs “
(𝐹 “ ℝ)),
ℝ, < ))) |
92 | | 2pos 10989 |
. . . 4
⊢ 0 <
2 |
93 | 92 | a1i 11 |
. . 3
⊢ (𝜑 → 0 < 2) |
94 | 12, 42, 44, 91, 93 | wwlemuld 37474 |
. 2
⊢ (𝜑 → (abs‘((𝐹‘𝐴) · (𝐺‘𝐵))) ≤ sup((abs “ (𝐹 “ ℝ)), ℝ, <
)) |
95 | 4, 9 | absmuld 14041 |
. . 3
⊢ (𝜑 → (abs‘((𝐹‘𝐴) · (𝐺‘𝐵))) = ((abs‘(𝐹‘𝐴)) · (abs‘(𝐺‘𝐵)))) |
96 | 95 | idi 2 |
. 2
⊢ (𝜑 → (abs‘((𝐹‘𝐴) · (𝐺‘𝐵))) = ((abs‘(𝐹‘𝐴)) · (abs‘(𝐺‘𝐵)))) |
97 | 94, 96, 12, 42 | leeq1d 37475 |
1
⊢ (𝜑 → ((abs‘(𝐹‘𝐴)) · (abs‘(𝐺‘𝐵))) ≤ sup((abs “ (𝐹 “ ℝ)), ℝ, <
)) |