# Metamath Proof Explorer

## Theorem imo72b2lem2

Description: Lemma for imo72b2 . (Contributed by Stanislas Polu, 9-Mar-2020)

Ref Expression
Hypotheses imo72b2lem2.1 ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
imo72b2lem2.2 ${⊢}{\phi }\to {C}\in ℝ$
imo72b2lem2.3 ${⊢}{\phi }\to \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left|{F}\left({z}\right)\right|\le {C}$
Assertion imo72b2lem2 ${⊢}{\phi }\to sup\left(\mathrm{abs}\left[{F}\left[ℝ\right]\right],ℝ,<\right)\le {C}$

### Proof

Step Hyp Ref Expression
1 imo72b2lem2.1 ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
2 imo72b2lem2.2 ${⊢}{\phi }\to {C}\in ℝ$
3 imo72b2lem2.3 ${⊢}{\phi }\to \forall {z}\in ℝ\phantom{\rule{.4em}{0ex}}\left|{F}\left({z}\right)\right|\le {C}$
4 imaco ${⊢}\left(\mathrm{abs}\circ {F}\right)\left[ℝ\right]=\mathrm{abs}\left[{F}\left[ℝ\right]\right]$
5 4 eqcomi ${⊢}\mathrm{abs}\left[{F}\left[ℝ\right]\right]=\left(\mathrm{abs}\circ {F}\right)\left[ℝ\right]$
6 imassrn ${⊢}\left(\mathrm{abs}\circ {F}\right)\left[ℝ\right]\subseteq \mathrm{ran}\left(\mathrm{abs}\circ {F}\right)$
7 6 a1i ${⊢}{\phi }\to \left(\mathrm{abs}\circ {F}\right)\left[ℝ\right]\subseteq \mathrm{ran}\left(\mathrm{abs}\circ {F}\right)$
8 absf ${⊢}\mathrm{abs}:ℂ⟶ℝ$
9 8 a1i ${⊢}{\phi }\to \mathrm{abs}:ℂ⟶ℝ$
10 ax-resscn ${⊢}ℝ\subseteq ℂ$
11 10 a1i ${⊢}{\phi }\to ℝ\subseteq ℂ$
12 9 11 fssresd ${⊢}{\phi }\to \left({\mathrm{abs}↾}_{ℝ}\right):ℝ⟶ℝ$
13 1 12 fco2d ${⊢}{\phi }\to \left(\mathrm{abs}\circ {F}\right):ℝ⟶ℝ$
14 13 frnd ${⊢}{\phi }\to \mathrm{ran}\left(\mathrm{abs}\circ {F}\right)\subseteq ℝ$
15 7 14 sstrd ${⊢}{\phi }\to \left(\mathrm{abs}\circ {F}\right)\left[ℝ\right]\subseteq ℝ$
16 5 15 eqsstrid ${⊢}{\phi }\to \mathrm{abs}\left[{F}\left[ℝ\right]\right]\subseteq ℝ$
17 0re ${⊢}0\in ℝ$
18 17 ne0ii ${⊢}ℝ\ne \varnothing$
19 18 a1i ${⊢}{\phi }\to ℝ\ne \varnothing$
20 19 13 wnefimgd ${⊢}{\phi }\to \left(\mathrm{abs}\circ {F}\right)\left[ℝ\right]\ne \varnothing$
21 20 necomd ${⊢}{\phi }\to \varnothing \ne \left(\mathrm{abs}\circ {F}\right)\left[ℝ\right]$
22 5 a1i ${⊢}{\phi }\to \mathrm{abs}\left[{F}\left[ℝ\right]\right]=\left(\mathrm{abs}\circ {F}\right)\left[ℝ\right]$
23 21 22 neeqtrrd ${⊢}{\phi }\to \varnothing \ne \mathrm{abs}\left[{F}\left[ℝ\right]\right]$
24 23 necomd ${⊢}{\phi }\to \mathrm{abs}\left[{F}\left[ℝ\right]\right]\ne \varnothing$
25 simpr ${⊢}\left({\phi }\wedge {c}={C}\right)\to {c}={C}$
26 25 breq2d ${⊢}\left({\phi }\wedge {c}={C}\right)\to \left({v}\le {c}↔{v}\le {C}\right)$
27 26 ralbidv ${⊢}\left({\phi }\wedge {c}={C}\right)\to \left(\forall {v}\in \mathrm{abs}\left[{F}\left[ℝ\right]\right]\phantom{\rule{.4em}{0ex}}{v}\le {c}↔\forall {v}\in \mathrm{abs}\left[{F}\left[ℝ\right]\right]\phantom{\rule{.4em}{0ex}}{v}\le {C}\right)$
28 1 3 extoimad ${⊢}{\phi }\to \forall {v}\in \mathrm{abs}\left[{F}\left[ℝ\right]\right]\phantom{\rule{.4em}{0ex}}{v}\le {C}$
29 2 27 28 rspcedvd ${⊢}{\phi }\to \exists {c}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{abs}\left[{F}\left[ℝ\right]\right]\phantom{\rule{.4em}{0ex}}{v}\le {c}$
30 1 3 extoimad ${⊢}{\phi }\to \forall {t}\in \mathrm{abs}\left[{F}\left[ℝ\right]\right]\phantom{\rule{.4em}{0ex}}{t}\le {C}$
31 16 24 29 2 30 suprleubrd ${⊢}{\phi }\to sup\left(\mathrm{abs}\left[{F}\left[ℝ\right]\right],ℝ,<\right)\le {C}$