Theorem imo72b2lem1

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

	Ref	Expression
Hypotheses	imo72b2lem1.1	$$⊢\phi \to F:ℝ⟶ℝ$$
	imo72b2lem1.7	$$⊢\phi \to \exists x\in ℝF\left(x\right)\ne 0$$
	imo72b2lem1.6	$$⊢\phi \to \forall y\in ℝ\left|F\left(y\right)\right|\le 1$$
Assertion	imo72b2lem1	$$⊢\phi \to 0<sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)$$

Proof

Step	Hyp	Ref	Expression
1		imo72b2lem1.1	$$⊢\phi \to F:ℝ⟶ℝ$$
2		imo72b2lem1.7	$$⊢\phi \to \exists x\in ℝF\left(x\right)\ne 0$$
3		imo72b2lem1.6	$$⊢\phi \to \forall y\in ℝ\left|F\left(y\right)\right|\le 1$$
4		imaco	$$⊢\left(\mathrm{abs}\circ F\right)\left[ℝ\right]=\mathrm{abs}\left[F\left[ℝ\right]\right]$$
5		imassrn	$$⊢\left(\mathrm{abs}\circ F\right)\left[ℝ\right]\subseteq \mathrm{ran}\left(\mathrm{abs}\circ F\right)$$
6		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
7	6	a1i	$$⊢\phi \to \mathrm{abs}:ℂ⟶ℝ$$
8		ax-resscn	$$⊢ℝ\subseteq ℂ$$
9	8	a1i	$$⊢\phi \to ℝ\subseteq ℂ$$
10	7 9	fssresd	$$⊢\phi \to \left({\mathrm{abs}\upharpoonright }_{ℝ}\right):ℝ⟶ℝ$$
11	1 10	fco2d	$$⊢\phi \to \left(\mathrm{abs}\circ F\right):ℝ⟶ℝ$$
12	11	frnd	$$⊢\phi \to \mathrm{ran}\left(\mathrm{abs}\circ F\right)\subseteq ℝ$$
13	5 12	sstrid	$$⊢\phi \to \left(\mathrm{abs}\circ F\right)\left[ℝ\right]\subseteq ℝ$$
14	4 13	eqsstrrid	$$⊢\phi \to \mathrm{abs}\left[F\left[ℝ\right]\right]\subseteq ℝ$$
15		0re	$$⊢0\in ℝ$$
16	15	ne0ii	$$⊢ℝ\ne \varnothing$$
17	16	a1i	$$⊢\phi \to ℝ\ne \varnothing$$
18	17 11	wnefimgd	$$⊢\phi \to \left(\mathrm{abs}\circ F\right)\left[ℝ\right]\ne \varnothing$$
19	4 18	eqnetrrid	$$⊢\phi \to \mathrm{abs}\left[F\left[ℝ\right]\right]\ne \varnothing$$
20		1red	$$⊢\phi \to 1\in ℝ$$
21		simpr	$$⊢\left(\phi \wedge c=1\right)\to c=1$$
22	21	breq2d	$$⊢\left(\phi \wedge c=1\right)\to \left(t\le c\leftrightarrow t\le 1\right)$$
23	22	ralbidv	$$⊢\left(\phi \wedge c=1\right)\to \left(\forall t\in \mathrm{abs}\left[F\left[ℝ\right]\right]t\le c\leftrightarrow \forall t\in \mathrm{abs}\left[F\left[ℝ\right]\right]t\le 1\right)$$
24	1 3	extoimad	$$⊢\phi \to \forall t\in \mathrm{abs}\left[F\left[ℝ\right]\right]t\le 1$$
25	20 23 24	rspcedvd	$$⊢\phi \to \exists c\in ℝ\forall t\in \mathrm{abs}\left[F\left[ℝ\right]\right]t\le c$$
26		0red	$$⊢\phi \to 0\in ℝ$$
27	1	adantr	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge F\left(x\right)\ne 0\right)\right)\to F:ℝ⟶ℝ$$
28		simprl	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge F\left(x\right)\ne 0\right)\right)\to x\in ℝ$$
29	27 28	fvco3d	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge F\left(x\right)\ne 0\right)\right)\to \left(\mathrm{abs}\circ F\right)\left(x\right)=\left|F\left(x\right)\right|$$
30	11	funfvima2d	$$⊢\left(\phi \wedge x\in ℝ\right)\to \left(\mathrm{abs}\circ F\right)\left(x\right)\in \left(\mathrm{abs}\circ F\right)\left[ℝ\right]$$
31	30	adantrr	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge F\left(x\right)\ne 0\right)\right)\to \left(\mathrm{abs}\circ F\right)\left(x\right)\in \left(\mathrm{abs}\circ F\right)\left[ℝ\right]$$
32	31 4	eleqtrdi	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge F\left(x\right)\ne 0\right)\right)\to \left(\mathrm{abs}\circ F\right)\left(x\right)\in \mathrm{abs}\left[F\left[ℝ\right]\right]$$
33	29 32	eqeltrrd	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge F\left(x\right)\ne 0\right)\right)\to \left|F\left(x\right)\right|\in \mathrm{abs}\left[F\left[ℝ\right]\right]$$
34		simpr	$$⊢\left(\left(\phi \wedge \left(x\in ℝ\wedge F\left(x\right)\ne 0\right)\right)\wedge z=\left|F\left(x\right)\right|\right)\to z=\left|F\left(x\right)\right|$$
35	34	breq2d	$$⊢\left(\left(\phi \wedge \left(x\in ℝ\wedge F\left(x\right)\ne 0\right)\right)\wedge z=\left|F\left(x\right)\right|\right)\to \left(0<z\leftrightarrow 0<\left|F\left(x\right)\right|\right)$$
36	1	ffvelrnda	$$⊢\left(\phi \wedge x\in ℝ\right)\to F\left(x\right)\in ℝ$$
37	36	adantrr	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge F\left(x\right)\ne 0\right)\right)\to F\left(x\right)\in ℝ$$
38	37	recnd	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge F\left(x\right)\ne 0\right)\right)\to F\left(x\right)\in ℂ$$
39		simprr	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge F\left(x\right)\ne 0\right)\right)\to F\left(x\right)\ne 0$$
40	38 39	absrpcld	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge F\left(x\right)\ne 0\right)\right)\to \left|F\left(x\right)\right|\in {ℝ}^{+}$$
41	40	rpgt0d	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge F\left(x\right)\ne 0\right)\right)\to 0<\left|F\left(x\right)\right|$$
42	33 35 41	rspcedvd	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge F\left(x\right)\ne 0\right)\right)\to \exists z\in \mathrm{abs}\left[F\left[ℝ\right]\right]0<z$$
43	2 42	rexlimddv	$$⊢\phi \to \exists z\in \mathrm{abs}\left[F\left[ℝ\right]\right]0<z$$
44	14 19 25 26 43	suprlubrd	$$⊢\phi \to 0<sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)$$