# Metamath Proof Explorer

## Theorem ivthlem3

Description: Lemma for ivth , the intermediate value theorem. Show that ( FC ) cannot be greater than U , and so establish the existence of a root of the function. (Contributed by Mario Carneiro, 30-Apr-2014) (Revised 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\}$
ivth.11 ${⊢}{C}=sup\left({S},ℝ,<\right)$
Assertion ivthlem3 ${⊢}{\phi }\to \left({C}\in \left({A},{B}\right)\wedge {F}\left({C}\right)={U}\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 ivth.11 ${⊢}{C}=sup\left({S},ℝ,<\right)$
11 9 ssrab3 ${⊢}{S}\subseteq \left[{A},{B}\right]$
12 iccssre ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left[{A},{B}\right]\subseteq ℝ$
13 1 2 12 syl2anc ${⊢}{\phi }\to \left[{A},{B}\right]\subseteq ℝ$
14 11 13 sstrid ${⊢}{\phi }\to {S}\subseteq ℝ$
15 1 2 3 4 5 6 7 8 9 ivthlem1 ${⊢}{\phi }\to \left({A}\in {S}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{z}\le {B}\right)$
16 15 simpld ${⊢}{\phi }\to {A}\in {S}$
17 16 ne0d ${⊢}{\phi }\to {S}\ne \varnothing$
18 15 simprd ${⊢}{\phi }\to \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{z}\le {B}$
19 brralrspcev ${⊢}\left({B}\in ℝ\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{z}\le {B}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{z}\le {x}$
20 2 18 19 syl2anc ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{z}\le {x}$
21 14 17 20 suprcld ${⊢}{\phi }\to sup\left({S},ℝ,<\right)\in ℝ$
22 10 21 eqeltrid ${⊢}{\phi }\to {C}\in ℝ$
23 8 simpld ${⊢}{\phi }\to {F}\left({A}\right)<{U}$
24 1 2 3 4 5 6 7 8 9 10 ivthlem2 ${⊢}{\phi }\to ¬{F}\left({C}\right)<{U}$
25 6 adantr ${⊢}\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\to {F}:{D}\underset{cn}{⟶}ℂ$
26 14 17 20 16 suprubd ${⊢}{\phi }\to {A}\le sup\left({S},ℝ,<\right)$
27 26 10 breqtrrdi ${⊢}{\phi }\to {A}\le {C}$
28 14 17 20 3jca ${⊢}{\phi }\to \left({S}\subseteq ℝ\wedge {S}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{z}\le {x}\right)$
29 suprleub ${⊢}\left(\left({S}\subseteq ℝ\wedge {S}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{z}\le {x}\right)\wedge {B}\in ℝ\right)\to \left(sup\left({S},ℝ,<\right)\le {B}↔\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{z}\le {B}\right)$
30 28 2 29 syl2anc ${⊢}{\phi }\to \left(sup\left({S},ℝ,<\right)\le {B}↔\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{z}\le {B}\right)$
31 18 30 mpbird ${⊢}{\phi }\to sup\left({S},ℝ,<\right)\le {B}$
32 10 31 eqbrtrid ${⊢}{\phi }\to {C}\le {B}$
33 elicc2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({C}\in \left[{A},{B}\right]↔\left({C}\in ℝ\wedge {A}\le {C}\wedge {C}\le {B}\right)\right)$
34 1 2 33 syl2anc ${⊢}{\phi }\to \left({C}\in \left[{A},{B}\right]↔\left({C}\in ℝ\wedge {A}\le {C}\wedge {C}\le {B}\right)\right)$
35 22 27 32 34 mpbir3and ${⊢}{\phi }\to {C}\in \left[{A},{B}\right]$
36 5 35 sseldd ${⊢}{\phi }\to {C}\in {D}$
37 36 adantr ${⊢}\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\to {C}\in {D}$
38 fveq2 ${⊢}{x}={C}\to {F}\left({x}\right)={F}\left({C}\right)$
39 38 eleq1d ${⊢}{x}={C}\to \left({F}\left({x}\right)\in ℝ↔{F}\left({C}\right)\in ℝ\right)$
40 7 ralrimiva ${⊢}{\phi }\to \forall {x}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in ℝ$
41 39 40 35 rspcdva ${⊢}{\phi }\to {F}\left({C}\right)\in ℝ$
42 difrp ${⊢}\left({U}\in ℝ\wedge {F}\left({C}\right)\in ℝ\right)\to \left({U}<{F}\left({C}\right)↔{F}\left({C}\right)-{U}\in {ℝ}^{+}\right)$
43 3 41 42 syl2anc ${⊢}{\phi }\to \left({U}<{F}\left({C}\right)↔{F}\left({C}\right)-{U}\in {ℝ}^{+}\right)$
44 43 biimpa ${⊢}\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\to {F}\left({C}\right)-{U}\in {ℝ}^{+}$
45 cncfi ${⊢}\left({F}:{D}\underset{cn}{⟶}ℂ\wedge {C}\in {D}\wedge {F}\left({C}\right)-{U}\in {ℝ}^{+}\right)\to \exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\right)$
46 25 37 44 45 syl3anc ${⊢}\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\to \exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\right)$
47 ssralv ${⊢}\left[{A},{B}\right]\subseteq {D}\to \left(\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\right)\to \forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\right)\right)$
48 5 47 syl ${⊢}{\phi }\to \left(\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\right)\to \forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\right)\right)$
49 48 ad2antrr ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\to \left(\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\right)\to \forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\right)\right)$
50 22 ad2antrr ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\to {C}\in ℝ$
51 ltsubrp ${⊢}\left({C}\in ℝ\wedge {z}\in {ℝ}^{+}\right)\to {C}-{z}<{C}$
52 50 51 sylancom ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\to {C}-{z}<{C}$
53 52 10 breqtrdi ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\to {C}-{z}
54 28 ad2antrr ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\to \left({S}\subseteq ℝ\wedge {S}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{z}\le {x}\right)$
55 rpre ${⊢}{z}\in {ℝ}^{+}\to {z}\in ℝ$
56 55 adantl ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\to {z}\in ℝ$
57 50 56 resubcld ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\to {C}-{z}\in ℝ$
58 suprlub ${⊢}\left(\left({S}\subseteq ℝ\wedge {S}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{z}\le {x}\right)\wedge {C}-{z}\in ℝ\right)\to \left({C}-{z}
59 54 57 58 syl2anc ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\to \left({C}-{z}
60 53 59 mpbid ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\to \exists {y}\in {S}\phantom{\rule{.4em}{0ex}}{C}-{z}<{y}$
61 11 sseli ${⊢}{y}\in {S}\to {y}\in \left[{A},{B}\right]$
62 61 ad2antrl ${⊢}\left(\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in {S}\wedge {C}-{z}<{y}\right)\right)\to {y}\in \left[{A},{B}\right]$
63 simplll ${⊢}\left(\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in {S}\wedge {C}-{z}<{y}\right)\right)\to {\phi }$
64 63 13 syl ${⊢}\left(\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in {S}\wedge {C}-{z}<{y}\right)\right)\to \left[{A},{B}\right]\subseteq ℝ$
65 64 62 sseldd ${⊢}\left(\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in {S}\wedge {C}-{z}<{y}\right)\right)\to {y}\in ℝ$
66 63 22 syl ${⊢}\left(\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in {S}\wedge {C}-{z}<{y}\right)\right)\to {C}\in ℝ$
67 63 28 syl ${⊢}\left(\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in {S}\wedge {C}-{z}<{y}\right)\right)\to \left({S}\subseteq ℝ\wedge {S}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{z}\le {x}\right)$
68 simprl ${⊢}\left(\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in {S}\wedge {C}-{z}<{y}\right)\right)\to {y}\in {S}$
69 suprub ${⊢}\left(\left({S}\subseteq ℝ\wedge {S}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{z}\le {x}\right)\wedge {y}\in {S}\right)\to {y}\le sup\left({S},ℝ,<\right)$
70 67 68 69 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in {S}\wedge {C}-{z}<{y}\right)\right)\to {y}\le sup\left({S},ℝ,<\right)$
71 70 10 breqtrrdi ${⊢}\left(\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in {S}\wedge {C}-{z}<{y}\right)\right)\to {y}\le {C}$
72 65 66 71 abssuble0d ${⊢}\left(\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in {S}\wedge {C}-{z}<{y}\right)\right)\to \left|{y}-{C}\right|={C}-{y}$
73 56 adantr ${⊢}\left(\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in {S}\wedge {C}-{z}<{y}\right)\right)\to {z}\in ℝ$
74 simprr ${⊢}\left(\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in {S}\wedge {C}-{z}<{y}\right)\right)\to {C}-{z}<{y}$
75 66 73 65 74 ltsub23d ${⊢}\left(\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in {S}\wedge {C}-{z}<{y}\right)\right)\to {C}-{y}<{z}$
76 72 75 eqbrtrd ${⊢}\left(\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in {S}\wedge {C}-{z}<{y}\right)\right)\to \left|{y}-{C}\right|<{z}$
77 62 76 68 jca32 ${⊢}\left(\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in {S}\wedge {C}-{z}<{y}\right)\right)\to \left({y}\in \left[{A},{B}\right]\wedge \left(\left|{y}-{C}\right|<{z}\wedge {y}\in {S}\right)\right)$
78 77 ex ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\to \left(\left({y}\in {S}\wedge {C}-{z}<{y}\right)\to \left({y}\in \left[{A},{B}\right]\wedge \left(\left|{y}-{C}\right|<{z}\wedge {y}\in {S}\right)\right)\right)$
79 78 reximdv2 ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\to \left(\exists {y}\in {S}\phantom{\rule{.4em}{0ex}}{C}-{z}<{y}\to \exists {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\wedge {y}\in {S}\right)\right)$
80 60 79 mpd ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\to \exists {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\wedge {y}\in {S}\right)$
81 r19.29 ${⊢}\left(\forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\right)\wedge \exists {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\wedge {y}\in {S}\right)\right)\to \exists {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\right)\wedge \left(\left|{y}-{C}\right|<{z}\wedge {y}\in {S}\right)\right)$
82 pm3.45 ${⊢}\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\right)\to \left(\left(\left|{y}-{C}\right|<{z}\wedge {y}\in {S}\right)\to \left(\left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\wedge {y}\in {S}\right)\right)$
83 82 imp ${⊢}\left(\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\right)\wedge \left(\left|{y}-{C}\right|<{z}\wedge {y}\in {S}\right)\right)\to \left(\left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\wedge {y}\in {S}\right)$
84 fveq2 ${⊢}{x}={y}\to {F}\left({x}\right)={F}\left({y}\right)$
85 84 eleq1d ${⊢}{x}={y}\to \left({F}\left({x}\right)\in ℝ↔{F}\left({y}\right)\in ℝ\right)$
86 40 ad2antrr ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge \left({z}\in {ℝ}^{+}\wedge {y}\in {S}\right)\right)\to \forall {x}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in ℝ$
87 61 ad2antll ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge \left({z}\in {ℝ}^{+}\wedge {y}\in {S}\right)\right)\to {y}\in \left[{A},{B}\right]$
88 85 86 87 rspcdva ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge \left({z}\in {ℝ}^{+}\wedge {y}\in {S}\right)\right)\to {F}\left({y}\right)\in ℝ$
89 41 ad2antrr ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge \left({z}\in {ℝ}^{+}\wedge {y}\in {S}\right)\right)\to {F}\left({C}\right)\in ℝ$
90 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge \left({z}\in {ℝ}^{+}\wedge {y}\in {S}\right)\right)\to {U}\in ℝ$
91 89 90 resubcld ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge \left({z}\in {ℝ}^{+}\wedge {y}\in {S}\right)\right)\to {F}\left({C}\right)-{U}\in ℝ$
92 88 89 91 absdifltd ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge \left({z}\in {ℝ}^{+}\wedge {y}\in {S}\right)\right)\to \left(\left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}↔\left({F}\left({C}\right)-\left({F}\left({C}\right)-{U}\right)<{F}\left({y}\right)\wedge {F}\left({y}\right)<{F}\left({C}\right)+{F}\left({C}\right)-{U}\right)\right)$
93 89 recnd ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge \left({z}\in {ℝ}^{+}\wedge {y}\in {S}\right)\right)\to {F}\left({C}\right)\in ℂ$
94 90 recnd ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge \left({z}\in {ℝ}^{+}\wedge {y}\in {S}\right)\right)\to {U}\in ℂ$
95 93 94 nncand ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge \left({z}\in {ℝ}^{+}\wedge {y}\in {S}\right)\right)\to {F}\left({C}\right)-\left({F}\left({C}\right)-{U}\right)={U}$
96 95 breq1d ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge \left({z}\in {ℝ}^{+}\wedge {y}\in {S}\right)\right)\to \left({F}\left({C}\right)-\left({F}\left({C}\right)-{U}\right)<{F}\left({y}\right)↔{U}<{F}\left({y}\right)\right)$
97 84 breq1d ${⊢}{x}={y}\to \left({F}\left({x}\right)\le {U}↔{F}\left({y}\right)\le {U}\right)$
98 97 9 elrab2 ${⊢}{y}\in {S}↔\left({y}\in \left[{A},{B}\right]\wedge {F}\left({y}\right)\le {U}\right)$
99 98 simprbi ${⊢}{y}\in {S}\to {F}\left({y}\right)\le {U}$
100 99 ad2antll ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge \left({z}\in {ℝ}^{+}\wedge {y}\in {S}\right)\right)\to {F}\left({y}\right)\le {U}$
101 88 90 100 lensymd ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge \left({z}\in {ℝ}^{+}\wedge {y}\in {S}\right)\right)\to ¬{U}<{F}\left({y}\right)$
102 101 pm2.21d ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge \left({z}\in {ℝ}^{+}\wedge {y}\in {S}\right)\right)\to \left({U}<{F}\left({y}\right)\to ¬{U}<{F}\left({C}\right)\right)$
103 96 102 sylbid ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge \left({z}\in {ℝ}^{+}\wedge {y}\in {S}\right)\right)\to \left({F}\left({C}\right)-\left({F}\left({C}\right)-{U}\right)<{F}\left({y}\right)\to ¬{U}<{F}\left({C}\right)\right)$
104 103 adantrd ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge \left({z}\in {ℝ}^{+}\wedge {y}\in {S}\right)\right)\to \left(\left({F}\left({C}\right)-\left({F}\left({C}\right)-{U}\right)<{F}\left({y}\right)\wedge {F}\left({y}\right)<{F}\left({C}\right)+{F}\left({C}\right)-{U}\right)\to ¬{U}<{F}\left({C}\right)\right)$
105 92 104 sylbid ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge \left({z}\in {ℝ}^{+}\wedge {y}\in {S}\right)\right)\to \left(\left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\to ¬{U}<{F}\left({C}\right)\right)$
106 105 expr ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\to \left({y}\in {S}\to \left(\left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\to ¬{U}<{F}\left({C}\right)\right)\right)$
107 106 impcomd ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\to \left(\left(\left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\wedge {y}\in {S}\right)\to ¬{U}<{F}\left({C}\right)\right)$
108 107 adantr ${⊢}\left(\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\wedge {y}\in \left[{A},{B}\right]\right)\to \left(\left(\left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\wedge {y}\in {S}\right)\to ¬{U}<{F}\left({C}\right)\right)$
109 83 108 syl5 ${⊢}\left(\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\wedge {y}\in \left[{A},{B}\right]\right)\to \left(\left(\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\right)\wedge \left(\left|{y}-{C}\right|<{z}\wedge {y}\in {S}\right)\right)\to ¬{U}<{F}\left({C}\right)\right)$
110 109 rexlimdva ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\to \left(\exists {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\right)\wedge \left(\left|{y}-{C}\right|<{z}\wedge {y}\in {S}\right)\right)\to ¬{U}<{F}\left({C}\right)\right)$
111 81 110 syl5 ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\to \left(\left(\forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\right)\wedge \exists {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\wedge {y}\in {S}\right)\right)\to ¬{U}<{F}\left({C}\right)\right)$
112 80 111 mpan2d ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\to \left(\forall {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\right)\to ¬{U}<{F}\left({C}\right)\right)$
113 49 112 syld ${⊢}\left(\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\wedge {z}\in {ℝ}^{+}\right)\to \left(\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\right)\to ¬{U}<{F}\left({C}\right)\right)$
114 113 rexlimdva ${⊢}\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\to \left(\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{F}\left({C}\right)-{U}\right)\to ¬{U}<{F}\left({C}\right)\right)$
115 46 114 mpd ${⊢}\left({\phi }\wedge {U}<{F}\left({C}\right)\right)\to ¬{U}<{F}\left({C}\right)$
116 115 pm2.01da ${⊢}{\phi }\to ¬{U}<{F}\left({C}\right)$
117 41 3 lttri3d ${⊢}{\phi }\to \left({F}\left({C}\right)={U}↔\left(¬{F}\left({C}\right)<{U}\wedge ¬{U}<{F}\left({C}\right)\right)\right)$
118 24 116 117 mpbir2and ${⊢}{\phi }\to {F}\left({C}\right)={U}$
119 23 118 breqtrrd ${⊢}{\phi }\to {F}\left({A}\right)<{F}\left({C}\right)$
120 41 ltnrd ${⊢}{\phi }\to ¬{F}\left({C}\right)<{F}\left({C}\right)$
121 fveq2 ${⊢}{C}={A}\to {F}\left({C}\right)={F}\left({A}\right)$
122 121 breq1d ${⊢}{C}={A}\to \left({F}\left({C}\right)<{F}\left({C}\right)↔{F}\left({A}\right)<{F}\left({C}\right)\right)$
123 122 notbid ${⊢}{C}={A}\to \left(¬{F}\left({C}\right)<{F}\left({C}\right)↔¬{F}\left({A}\right)<{F}\left({C}\right)\right)$
124 120 123 syl5ibcom ${⊢}{\phi }\to \left({C}={A}\to ¬{F}\left({A}\right)<{F}\left({C}\right)\right)$
125 124 necon2ad ${⊢}{\phi }\to \left({F}\left({A}\right)<{F}\left({C}\right)\to {C}\ne {A}\right)$
126 125 27 jctild ${⊢}{\phi }\to \left({F}\left({A}\right)<{F}\left({C}\right)\to \left({A}\le {C}\wedge {C}\ne {A}\right)\right)$
127 1 22 ltlend ${⊢}{\phi }\to \left({A}<{C}↔\left({A}\le {C}\wedge {C}\ne {A}\right)\right)$
128 126 127 sylibrd ${⊢}{\phi }\to \left({F}\left({A}\right)<{F}\left({C}\right)\to {A}<{C}\right)$
129 119 128 mpd ${⊢}{\phi }\to {A}<{C}$
130 8 simprd ${⊢}{\phi }\to {U}<{F}\left({B}\right)$
131 118 130 eqbrtrd ${⊢}{\phi }\to {F}\left({C}\right)<{F}\left({B}\right)$
132 fveq2 ${⊢}{B}={C}\to {F}\left({B}\right)={F}\left({C}\right)$
133 132 breq2d ${⊢}{B}={C}\to \left({F}\left({C}\right)<{F}\left({B}\right)↔{F}\left({C}\right)<{F}\left({C}\right)\right)$
134 133 notbid ${⊢}{B}={C}\to \left(¬{F}\left({C}\right)<{F}\left({B}\right)↔¬{F}\left({C}\right)<{F}\left({C}\right)\right)$
135 120 134 syl5ibrcom ${⊢}{\phi }\to \left({B}={C}\to ¬{F}\left({C}\right)<{F}\left({B}\right)\right)$
136 135 necon2ad ${⊢}{\phi }\to \left({F}\left({C}\right)<{F}\left({B}\right)\to {B}\ne {C}\right)$
137 136 32 jctild ${⊢}{\phi }\to \left({F}\left({C}\right)<{F}\left({B}\right)\to \left({C}\le {B}\wedge {B}\ne {C}\right)\right)$
138 22 2 ltlend ${⊢}{\phi }\to \left({C}<{B}↔\left({C}\le {B}\wedge {B}\ne {C}\right)\right)$
139 137 138 sylibrd ${⊢}{\phi }\to \left({F}\left({C}\right)<{F}\left({B}\right)\to {C}<{B}\right)$
140 131 139 mpd ${⊢}{\phi }\to {C}<{B}$
141 1 rexrd ${⊢}{\phi }\to {A}\in {ℝ}^{*}$
142 2 rexrd ${⊢}{\phi }\to {B}\in {ℝ}^{*}$
143 elioo2 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({C}\in \left({A},{B}\right)↔\left({C}\in ℝ\wedge {A}<{C}\wedge {C}<{B}\right)\right)$
144 141 142 143 syl2anc ${⊢}{\phi }\to \left({C}\in \left({A},{B}\right)↔\left({C}\in ℝ\wedge {A}<{C}\wedge {C}<{B}\right)\right)$
145 22 129 140 144 mpbir3and ${⊢}{\phi }\to {C}\in \left({A},{B}\right)$
146 145 118 jca ${⊢}{\phi }\to \left({C}\in \left({A},{B}\right)\wedge {F}\left({C}\right)={U}\right)$