Theorem ivthlem1

Description: Lemma for ivth . The set S of all x values with ( Fx ) less than U is lower bounded by A and upper bounded by B . (Contributed by Mario Carneiro, 17-Jun-2014)

	Ref	Expression
Hypotheses	ivth.1	$$⊢\phi \to A\in ℝ$$
	ivth.2	$$⊢\phi \to B\in ℝ$$
	ivth.3	$$⊢\phi \to U\in ℝ$$
	ivth.4	$$⊢\phi \to A<B$$
	ivth.5	$$⊢\phi \to \left[A,B\right]\subseteq D$$
	ivth.7	$$⊢\phi \to F:D\underset{cn}{⟶}ℂ$$
	ivth.8	$$⊢\left(\phi \wedge x\in \left[A,B\right]\right)\to F\left(x\right)\in ℝ$$
	ivth.9	$$⊢\phi \to \left(F\left(A\right)<U\wedge U<F\left(B\right)\right)$$
	ivth.10	$$⊢S=\left\{x\in \left[A,B\right]|F\left(x\right)\le U\right\}$$
Assertion	ivthlem1	$$⊢\phi \to \left(A\in S\wedge \forall z\in Sz\le B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ivth.1	$$⊢\phi \to A\in ℝ$$
2		ivth.2	$$⊢\phi \to B\in ℝ$$
3		ivth.3	$$⊢\phi \to U\in ℝ$$
4		ivth.4	$$⊢\phi \to A<B$$
5		ivth.5	$$⊢\phi \to \left[A,B\right]\subseteq D$$
6		ivth.7	$$⊢\phi \to F:D\underset{cn}{⟶}ℂ$$
7		ivth.8	$$⊢\left(\phi \wedge x\in \left[A,B\right]\right)\to F\left(x\right)\in ℝ$$
8		ivth.9	$$⊢\phi \to \left(F\left(A\right)<U\wedge U<F\left(B\right)\right)$$
9		ivth.10	$$⊢S=\left\{x\in \left[A,B\right]|F\left(x\right)\le U\right\}$$
10	1	rexrd	$$⊢\phi \to A\in {ℝ}^{*}$$
11	2	rexrd	$$⊢\phi \to B\in {ℝ}^{*}$$
12	1 2 4	ltled	$$⊢\phi \to A\le B$$
13		lbicc2	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge A\le B\right)\to A\in \left[A,B\right]$$
14	10 11 12 13	syl3anc	$$⊢\phi \to A\in \left[A,B\right]$$
15		fveq2	$$⊢x=A\to F\left(x\right)=F\left(A\right)$$
16	15	eleq1d	$$⊢x=A\to \left(F\left(x\right)\in ℝ\leftrightarrow F\left(A\right)\in ℝ\right)$$
17	7	ralrimiva	$$⊢\phi \to \forall x\in \left[A,B\right]F\left(x\right)\in ℝ$$
18	16 17 14	rspcdva	$$⊢\phi \to F\left(A\right)\in ℝ$$
19	8	simpld	$$⊢\phi \to F\left(A\right)<U$$
20	18 3 19	ltled	$$⊢\phi \to F\left(A\right)\le U$$
21	15	breq1d	$$⊢x=A\to \left(F\left(x\right)\le U\leftrightarrow F\left(A\right)\le U\right)$$
22	21 9	elrab2	$$⊢A\in S\leftrightarrow \left(A\in \left[A,B\right]\wedge F\left(A\right)\le U\right)$$
23	14 20 22	sylanbrc	$$⊢\phi \to A\in S$$
24	9	ssrab3	$$⊢S\subseteq \left[A,B\right]$$
25	24	sseli	$$⊢z\in S\to z\in \left[A,B\right]$$
26		iccleub	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge z\in \left[A,B\right]\right)\to z\le B$$
27	26	3expia	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(z\in \left[A,B\right]\to z\le B\right)$$
28	10 11 27	syl2anc	$$⊢\phi \to \left(z\in \left[A,B\right]\to z\le B\right)$$
29	25 28	syl5	$$⊢\phi \to \left(z\in S\to z\le B\right)$$
30	29	ralrimiv	$$⊢\phi \to \forall z\in Sz\le B$$
31	23 30	jca	$$⊢\phi \to \left(A\in S\wedge \forall z\in Sz\le B\right)$$