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 ℝ\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 ℝ\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}\upharpoonright }_{ℝ}\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\leftrightarrow 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]v\le c\leftrightarrow \forall v\in \mathrm{abs}\left[F\left[ℝ\right]\right]v\le C\right)$$
28	1 3	extoimad	$$⊢\phi \to \forall v\in \mathrm{abs}\left[F\left[ℝ\right]\right]v\le C$$
29	2 27 28	rspcedvd	$$⊢\phi \to \exists c\in ℝ\forall v\in \mathrm{abs}\left[F\left[ℝ\right]\right]v\le c$$
30	1 3	extoimad	$$⊢\phi \to \forall t\in \mathrm{abs}\left[F\left[ℝ\right]\right]t\le C$$
31	16 24 29 2 30	suprleubrd	$$⊢\phi \to sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)\le C$$