# Metamath Proof Explorer

## Theorem ivthlem2

Description: Lemma for ivth . Show that the supremum of S cannot be less than U . If it was, continuity of F implies that there are points just above the supremum that are also less than U , a contradiction. (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\}$
ivth.11 ${⊢}{C}=sup\left({S},ℝ,<\right)$
Assertion ivthlem2 ${⊢}{\phi }\to ¬{F}\left({C}\right)<{U}$

### 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 6 adantr ${⊢}\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\to {F}:{D}\underset{cn}{⟶}ℂ$
12 9 ssrab3 ${⊢}{S}\subseteq \left[{A},{B}\right]$
13 iccssre ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left[{A},{B}\right]\subseteq ℝ$
14 1 2 13 syl2anc ${⊢}{\phi }\to \left[{A},{B}\right]\subseteq ℝ$
15 12 14 sstrid ${⊢}{\phi }\to {S}\subseteq ℝ$
16 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)$
17 16 simpld ${⊢}{\phi }\to {A}\in {S}$
18 17 ne0d ${⊢}{\phi }\to {S}\ne \varnothing$
19 16 simprd ${⊢}{\phi }\to \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{z}\le {B}$
20 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}$
21 2 19 20 syl2anc ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{z}\le {x}$
22 15 18 21 suprcld ${⊢}{\phi }\to sup\left({S},ℝ,<\right)\in ℝ$
23 10 22 eqeltrid ${⊢}{\phi }\to {C}\in ℝ$
24 15 18 21 17 suprubd ${⊢}{\phi }\to {A}\le sup\left({S},ℝ,<\right)$
25 24 10 breqtrrdi ${⊢}{\phi }\to {A}\le {C}$
26 15 18 21 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)$
27 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)$
28 26 2 27 syl2anc ${⊢}{\phi }\to \left(sup\left({S},ℝ,<\right)\le {B}↔\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{z}\le {B}\right)$
29 19 28 mpbird ${⊢}{\phi }\to sup\left({S},ℝ,<\right)\le {B}$
30 10 29 eqbrtrid ${⊢}{\phi }\to {C}\le {B}$
31 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)$
32 1 2 31 syl2anc ${⊢}{\phi }\to \left({C}\in \left[{A},{B}\right]↔\left({C}\in ℝ\wedge {A}\le {C}\wedge {C}\le {B}\right)\right)$
33 23 25 30 32 mpbir3and ${⊢}{\phi }\to {C}\in \left[{A},{B}\right]$
34 5 33 sseldd ${⊢}{\phi }\to {C}\in {D}$
35 34 adantr ${⊢}\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\to {C}\in {D}$
36 fveq2 ${⊢}{x}={C}\to {F}\left({x}\right)={F}\left({C}\right)$
37 36 eleq1d ${⊢}{x}={C}\to \left({F}\left({x}\right)\in ℝ↔{F}\left({C}\right)\in ℝ\right)$
38 7 ralrimiva ${⊢}{\phi }\to \forall {x}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in ℝ$
39 37 38 33 rspcdva ${⊢}{\phi }\to {F}\left({C}\right)\in ℝ$
40 difrp ${⊢}\left({F}\left({C}\right)\in ℝ\wedge {U}\in ℝ\right)\to \left({F}\left({C}\right)<{U}↔{U}-{F}\left({C}\right)\in {ℝ}^{+}\right)$
41 39 3 40 syl2anc ${⊢}{\phi }\to \left({F}\left({C}\right)<{U}↔{U}-{F}\left({C}\right)\in {ℝ}^{+}\right)$
42 41 biimpa ${⊢}\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\to {U}-{F}\left({C}\right)\in {ℝ}^{+}$
43 cncfi ${⊢}\left({F}:{D}\underset{cn}{⟶}ℂ\wedge {C}\in {D}\wedge {U}-{F}\left({C}\right)\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|<{U}-{F}\left({C}\right)\right)$
44 11 35 42 43 syl3anc ${⊢}\left({\phi }\wedge {F}\left({C}\right)<{U}\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|<{U}-{F}\left({C}\right)\right)$
45 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|<{U}-{F}\left({C}\right)\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|<{U}-{F}\left({C}\right)\right)\right)$
46 5 45 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|<{U}-{F}\left({C}\right)\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|<{U}-{F}\left({C}\right)\right)\right)$
47 46 ad2antrr ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\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|<{U}-{F}\left({C}\right)\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|<{U}-{F}\left({C}\right)\right)\right)$
48 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to {B}\in ℝ$
49 23 ad2antrr ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to {C}\in ℝ$
50 rphalfcl ${⊢}{z}\in {ℝ}^{+}\to \frac{{z}}{2}\in {ℝ}^{+}$
51 50 adantl ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to \frac{{z}}{2}\in {ℝ}^{+}$
52 51 rpred ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to \frac{{z}}{2}\in ℝ$
53 49 52 readdcld ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to {C}+\left(\frac{{z}}{2}\right)\in ℝ$
54 48 53 ifcld ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\in ℝ$
55 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to {A}\in ℝ$
56 25 ad2antrr ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to {A}\le {C}$
57 8 simprd ${⊢}{\phi }\to {U}<{F}\left({B}\right)$
58 fveq2 ${⊢}{x}={B}\to {F}\left({x}\right)={F}\left({B}\right)$
59 58 eleq1d ${⊢}{x}={B}\to \left({F}\left({x}\right)\in ℝ↔{F}\left({B}\right)\in ℝ\right)$
60 1 rexrd ${⊢}{\phi }\to {A}\in {ℝ}^{*}$
61 2 rexrd ${⊢}{\phi }\to {B}\in {ℝ}^{*}$
62 1 2 4 ltled ${⊢}{\phi }\to {A}\le {B}$
63 ubicc2 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}\le {B}\right)\to {B}\in \left[{A},{B}\right]$
64 60 61 62 63 syl3anc ${⊢}{\phi }\to {B}\in \left[{A},{B}\right]$
65 59 38 64 rspcdva ${⊢}{\phi }\to {F}\left({B}\right)\in ℝ$
66 lttr ${⊢}\left({F}\left({C}\right)\in ℝ\wedge {U}\in ℝ\wedge {F}\left({B}\right)\in ℝ\right)\to \left(\left({F}\left({C}\right)<{U}\wedge {U}<{F}\left({B}\right)\right)\to {F}\left({C}\right)<{F}\left({B}\right)\right)$
67 39 3 65 66 syl3anc ${⊢}{\phi }\to \left(\left({F}\left({C}\right)<{U}\wedge {U}<{F}\left({B}\right)\right)\to {F}\left({C}\right)<{F}\left({B}\right)\right)$
68 57 67 mpan2d ${⊢}{\phi }\to \left({F}\left({C}\right)<{U}\to {F}\left({C}\right)<{F}\left({B}\right)\right)$
69 68 imp ${⊢}\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\to {F}\left({C}\right)<{F}\left({B}\right)$
70 69 adantr ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to {F}\left({C}\right)<{F}\left({B}\right)$
71 39 ltnrd ${⊢}{\phi }\to ¬{F}\left({C}\right)<{F}\left({C}\right)$
72 fveq2 ${⊢}{B}={C}\to {F}\left({B}\right)={F}\left({C}\right)$
73 72 breq2d ${⊢}{B}={C}\to \left({F}\left({C}\right)<{F}\left({B}\right)↔{F}\left({C}\right)<{F}\left({C}\right)\right)$
74 73 notbid ${⊢}{B}={C}\to \left(¬{F}\left({C}\right)<{F}\left({B}\right)↔¬{F}\left({C}\right)<{F}\left({C}\right)\right)$
75 71 74 syl5ibrcom ${⊢}{\phi }\to \left({B}={C}\to ¬{F}\left({C}\right)<{F}\left({B}\right)\right)$
76 75 necon2ad ${⊢}{\phi }\to \left({F}\left({C}\right)<{F}\left({B}\right)\to {B}\ne {C}\right)$
77 76 30 jctild ${⊢}{\phi }\to \left({F}\left({C}\right)<{F}\left({B}\right)\to \left({C}\le {B}\wedge {B}\ne {C}\right)\right)$
78 23 2 ltlend ${⊢}{\phi }\to \left({C}<{B}↔\left({C}\le {B}\wedge {B}\ne {C}\right)\right)$
79 77 78 sylibrd ${⊢}{\phi }\to \left({F}\left({C}\right)<{F}\left({B}\right)\to {C}<{B}\right)$
80 79 ad2antrr ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to \left({F}\left({C}\right)<{F}\left({B}\right)\to {C}<{B}\right)$
81 70 80 mpd ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to {C}<{B}$
82 49 51 ltaddrpd ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to {C}<{C}+\left(\frac{{z}}{2}\right)$
83 breq2 ${⊢}{B}=if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\to \left({C}<{B}↔{C}
84 breq2 ${⊢}{C}+\left(\frac{{z}}{2}\right)=if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\to \left({C}<{C}+\left(\frac{{z}}{2}\right)↔{C}
85 83 84 ifboth ${⊢}\left({C}<{B}\wedge {C}<{C}+\left(\frac{{z}}{2}\right)\right)\to {C}
86 81 82 85 syl2anc ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to {C}
87 49 54 86 ltled ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to {C}\le if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)$
88 55 49 54 56 87 letrd ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to {A}\le if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)$
89 min1 ${⊢}\left({B}\in ℝ\wedge {C}+\left(\frac{{z}}{2}\right)\in ℝ\right)\to if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\le {B}$
90 48 53 89 syl2anc ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\le {B}$
91 elicc2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\in \left[{A},{B}\right]↔\left(if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\in ℝ\wedge {A}\le if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\wedge if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\le {B}\right)\right)$
92 1 2 91 syl2anc ${⊢}{\phi }\to \left(if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\in \left[{A},{B}\right]↔\left(if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\in ℝ\wedge {A}\le if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\wedge if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\le {B}\right)\right)$
93 92 ad2antrr ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to \left(if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\in \left[{A},{B}\right]↔\left(if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\in ℝ\wedge {A}\le if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\wedge if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\le {B}\right)\right)$
94 54 88 90 93 mpbir3and ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\in \left[{A},{B}\right]$
95 49 54 87 abssubge0d ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to \left|if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)-{C}\right|=if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)-{C}$
96 rpre ${⊢}{z}\in {ℝ}^{+}\to {z}\in ℝ$
97 96 adantl ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to {z}\in ℝ$
98 49 97 readdcld ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to {C}+{z}\in ℝ$
99 min2 ${⊢}\left({B}\in ℝ\wedge {C}+\left(\frac{{z}}{2}\right)\in ℝ\right)\to if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\le {C}+\left(\frac{{z}}{2}\right)$
100 48 53 99 syl2anc ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\le {C}+\left(\frac{{z}}{2}\right)$
101 rphalflt ${⊢}{z}\in {ℝ}^{+}\to \frac{{z}}{2}<{z}$
102 101 adantl ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to \frac{{z}}{2}<{z}$
103 52 97 49 102 ltadd2dd ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to {C}+\left(\frac{{z}}{2}\right)<{C}+{z}$
104 54 53 98 100 103 lelttrd ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)<{C}+{z}$
105 54 49 97 ltsubadd2d ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to \left(if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)-{C}<{z}↔if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)<{C}+{z}\right)$
106 104 105 mpbird ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)-{C}<{z}$
107 95 106 eqbrtrd ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to \left|if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)-{C}\right|<{z}$
108 fvoveq1 ${⊢}{y}=if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\to \left|{y}-{C}\right|=\left|if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)-{C}\right|$
109 108 breq1d ${⊢}{y}=if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\to \left(\left|{y}-{C}\right|<{z}↔\left|if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)-{C}\right|<{z}\right)$
110 breq2 ${⊢}{y}=if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\to \left({C}<{y}↔{C}
111 109 110 anbi12d ${⊢}{y}=if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\to \left(\left(\left|{y}-{C}\right|<{z}\wedge {C}<{y}\right)↔\left(\left|if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)-{C}\right|<{z}\wedge {C}
112 111 rspcev ${⊢}\left(if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)\in \left[{A},{B}\right]\wedge \left(\left|if\left({B}\le {C}+\left(\frac{{z}}{2}\right),{B},{C}+\left(\frac{{z}}{2}\right)\right)-{C}\right|<{z}\wedge {C}
113 94 107 86 112 syl12anc ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\to \exists {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\wedge {C}<{y}\right)$
114 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|<{U}-{F}\left({C}\right)\right)\wedge \exists {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\wedge {C}<{y}\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|<{U}-{F}\left({C}\right)\right)\wedge \left(\left|{y}-{C}\right|<{z}\wedge {C}<{y}\right)\right)$
115 pm3.45 ${⊢}\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{U}-{F}\left({C}\right)\right)\to \left(\left(\left|{y}-{C}\right|<{z}\wedge {C}<{y}\right)\to \left(\left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{U}-{F}\left({C}\right)\wedge {C}<{y}\right)\right)$
116 115 imp ${⊢}\left(\left(\left|{y}-{C}\right|<{z}\to \left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{U}-{F}\left({C}\right)\right)\wedge \left(\left|{y}-{C}\right|<{z}\wedge {C}<{y}\right)\right)\to \left(\left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{U}-{F}\left({C}\right)\wedge {C}<{y}\right)$
117 simprr ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to {C}<{y}$
118 fveq2 ${⊢}{x}={y}\to {F}\left({x}\right)={F}\left({y}\right)$
119 118 eleq1d ${⊢}{x}={y}\to \left({F}\left({x}\right)\in ℝ↔{F}\left({y}\right)\in ℝ\right)$
120 simplll ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to {\phi }$
121 120 38 syl ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to \forall {x}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in ℝ$
122 simprl ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to {y}\in \left[{A},{B}\right]$
123 119 121 122 rspcdva ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to {F}\left({y}\right)\in ℝ$
124 120 39 syl ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to {F}\left({C}\right)\in ℝ$
125 120 3 syl ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to {U}\in ℝ$
126 125 124 resubcld ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to {U}-{F}\left({C}\right)\in ℝ$
127 123 124 126 absdifltd ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to \left(\left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{U}-{F}\left({C}\right)↔\left({F}\left({C}\right)-\left({U}-{F}\left({C}\right)\right)<{F}\left({y}\right)\wedge {F}\left({y}\right)<{F}\left({C}\right)+{U}-{F}\left({C}\right)\right)\right)$
128 ltle ${⊢}\left({F}\left({y}\right)\in ℝ\wedge {U}\in ℝ\right)\to \left({F}\left({y}\right)<{U}\to {F}\left({y}\right)\le {U}\right)$
129 123 125 128 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to \left({F}\left({y}\right)<{U}\to {F}\left({y}\right)\le {U}\right)$
130 124 recnd ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to {F}\left({C}\right)\in ℂ$
131 125 recnd ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to {U}\in ℂ$
132 130 131 pncan3d ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to {F}\left({C}\right)+{U}-{F}\left({C}\right)={U}$
133 132 breq2d ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to \left({F}\left({y}\right)<{F}\left({C}\right)+{U}-{F}\left({C}\right)↔{F}\left({y}\right)<{U}\right)$
134 118 breq1d ${⊢}{x}={y}\to \left({F}\left({x}\right)\le {U}↔{F}\left({y}\right)\le {U}\right)$
135 134 9 elrab2 ${⊢}{y}\in {S}↔\left({y}\in \left[{A},{B}\right]\wedge {F}\left({y}\right)\le {U}\right)$
136 135 baib ${⊢}{y}\in \left[{A},{B}\right]\to \left({y}\in {S}↔{F}\left({y}\right)\le {U}\right)$
137 136 ad2antrl ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to \left({y}\in {S}↔{F}\left({y}\right)\le {U}\right)$
138 129 133 137 3imtr4d ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to \left({F}\left({y}\right)<{F}\left({C}\right)+{U}-{F}\left({C}\right)\to {y}\in {S}\right)$
139 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)$
140 139 10 breqtrrdi ${⊢}\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 {C}$
141 140 ex ${⊢}\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)\to \left({y}\in {S}\to {y}\le {C}\right)$
142 120 26 141 3syl ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to \left({y}\in {S}\to {y}\le {C}\right)$
143 120 14 syl ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to \left[{A},{B}\right]\subseteq ℝ$
144 143 122 sseldd ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to {y}\in ℝ$
145 120 23 syl ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to {C}\in ℝ$
146 144 145 lenltd ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to \left({y}\le {C}↔¬{C}<{y}\right)$
147 142 146 sylibd ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to \left({y}\in {S}\to ¬{C}<{y}\right)$
148 138 147 syld ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to \left({F}\left({y}\right)<{F}\left({C}\right)+{U}-{F}\left({C}\right)\to ¬{C}<{y}\right)$
149 148 adantld ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to \left(\left({F}\left({C}\right)-\left({U}-{F}\left({C}\right)\right)<{F}\left({y}\right)\wedge {F}\left({y}\right)<{F}\left({C}\right)+{U}-{F}\left({C}\right)\right)\to ¬{C}<{y}\right)$
150 127 149 sylbid ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to \left(\left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{U}-{F}\left({C}\right)\to ¬{C}<{y}\right)$
151 117 150 mt2d ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to ¬\left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{U}-{F}\left({C}\right)$
152 151 pm2.21d ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge \left({y}\in \left[{A},{B}\right]\wedge {C}<{y}\right)\right)\to \left(\left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{U}-{F}\left({C}\right)\to ¬{F}\left({C}\right)<{U}\right)$
153 152 expr ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\wedge {z}\in {ℝ}^{+}\right)\wedge {y}\in \left[{A},{B}\right]\right)\to \left({C}<{y}\to \left(\left|{F}\left({y}\right)-{F}\left({C}\right)\right|<{U}-{F}\left({C}\right)\to ¬{F}\left({C}\right)<{U}\right)\right)$
154 153 impcomd ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\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|<{U}-{F}\left({C}\right)\wedge {C}<{y}\right)\to ¬{F}\left({C}\right)<{U}\right)$
155 116 154 syl5 ${⊢}\left(\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\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|<{U}-{F}\left({C}\right)\right)\wedge \left(\left|{y}-{C}\right|<{z}\wedge {C}<{y}\right)\right)\to ¬{F}\left({C}\right)<{U}\right)$
156 155 rexlimdva ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\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|<{U}-{F}\left({C}\right)\right)\wedge \left(\left|{y}-{C}\right|<{z}\wedge {C}<{y}\right)\right)\to ¬{F}\left({C}\right)<{U}\right)$
157 114 156 syl5 ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\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|<{U}-{F}\left({C}\right)\right)\wedge \exists {y}\in \left[{A},{B}\right]\phantom{\rule{.4em}{0ex}}\left(\left|{y}-{C}\right|<{z}\wedge {C}<{y}\right)\right)\to ¬{F}\left({C}\right)<{U}\right)$
158 113 157 mpan2d ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\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|<{U}-{F}\left({C}\right)\right)\to ¬{F}\left({C}\right)<{U}\right)$
159 47 158 syld ${⊢}\left(\left({\phi }\wedge {F}\left({C}\right)<{U}\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|<{U}-{F}\left({C}\right)\right)\to ¬{F}\left({C}\right)<{U}\right)$
160 159 rexlimdva ${⊢}\left({\phi }\wedge {F}\left({C}\right)<{U}\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|<{U}-{F}\left({C}\right)\right)\to ¬{F}\left({C}\right)<{U}\right)$
161 44 160 mpd ${⊢}\left({\phi }\wedge {F}\left({C}\right)<{U}\right)\to ¬{F}\left({C}\right)<{U}$
162 161 pm2.01da ${⊢}{\phi }\to ¬{F}\left({C}\right)<{U}$