Theorem dvferm1lem

Description: Lemma for dvferm . (Contributed by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Hypotheses	dvferm.a	$$⊢\phi \to F:X⟶ℝ$$
	dvferm.b	$$⊢\phi \to X\subseteq ℝ$$
	dvferm.u	$$⊢\phi \to U\in \left(A,B\right)$$
	dvferm.s	$$⊢\phi \to \left(A,B\right)\subseteq X$$
	dvferm.d	$$⊢\phi \to U\in \mathrm{dom}{F}_{ℝ}^{\prime }$$
	dvferm1.r	$$⊢\phi \to \forall y\in \left(U,B\right)F\left(y\right)\le F\left(U\right)$$
	dvferm1.z	$$⊢\phi \to 0<F_{ℝ}^{\prime }\left(U\right)$$
	dvferm1.t	$$⊢\phi \to T\in {ℝ}^{+}$$
	dvferm1.l	$$⊢\phi \to \forall z\in \left(X\setminus \left\{U\right\}\right)\left(\left(z\ne U\wedge \left|z-U\right|<T\right)\to \left|\left(\frac{F\left(z\right)-F\left(U\right)}{z-U}\right)-F_{ℝ}^{\prime }\left(U\right)\right|<F_{ℝ}^{\prime }\left(U\right)\right)$$
	dvferm1.x	$$⊢S=\frac{U+if\left(B\le U+T,B,U+T\right)}{2}$$
Assertion	dvferm1lem	$$⊢\neg \phi$$

Proof

Step	Hyp	Ref	Expression
1		dvferm.a	$$⊢\phi \to F:X⟶ℝ$$
2		dvferm.b	$$⊢\phi \to X\subseteq ℝ$$
3		dvferm.u	$$⊢\phi \to U\in \left(A,B\right)$$
4		dvferm.s	$$⊢\phi \to \left(A,B\right)\subseteq X$$
5		dvferm.d	$$⊢\phi \to U\in \mathrm{dom}{F}_{ℝ}^{\prime }$$
6		dvferm1.r	$$⊢\phi \to \forall y\in \left(U,B\right)F\left(y\right)\le F\left(U\right)$$
7		dvferm1.z	$$⊢\phi \to 0<F_{ℝ}^{\prime }\left(U\right)$$
8		dvferm1.t	$$⊢\phi \to T\in {ℝ}^{+}$$
9		dvferm1.l	$$⊢\phi \to \forall z\in \left(X\setminus \left\{U\right\}\right)\left(\left(z\ne U\wedge \left|z-U\right|<T\right)\to \left|\left(\frac{F\left(z\right)-F\left(U\right)}{z-U}\right)-F_{ℝ}^{\prime }\left(U\right)\right|<F_{ℝ}^{\prime }\left(U\right)\right)$$
10		dvferm1.x	$$⊢S=\frac{U+if\left(B\le U+T,B,U+T\right)}{2}$$
11		dvfre	$$⊢\left(F:X⟶ℝ\wedge X\subseteq ℝ\right)\to F_{ℝ}^{\prime }:\mathrm{dom}{F}_{ℝ}^{\prime }⟶ℝ$$
12	1 2 11	syl2anc	$$⊢\phi \to F_{ℝ}^{\prime }:\mathrm{dom}{F}_{ℝ}^{\prime }⟶ℝ$$
13	12 5	ffvelrnd	$$⊢\phi \to F_{ℝ}^{\prime }\left(U\right)\in ℝ$$
14	13	recnd	$$⊢\phi \to F_{ℝ}^{\prime }\left(U\right)\in ℂ$$
15	14	subidd	$$⊢\phi \to F_{ℝ}^{\prime }\left(U\right)-F_{ℝ}^{\prime }\left(U\right)=0$$
16		ioossre	$$⊢\left(A,B\right)\subseteq ℝ$$
17	16 3	sseldi	$$⊢\phi \to U\in ℝ$$
18		eliooord	$$⊢U\in \left(A,B\right)\to \left(A<U\wedge U<B\right)$$
19	3 18	syl	$$⊢\phi \to \left(A<U\wedge U<B\right)$$
20	19	simprd	$$⊢\phi \to U<B$$
21	17 8	ltaddrpd	$$⊢\phi \to U<U+T$$
22		breq2	$$⊢B=if\left(B\le U+T,B,U+T\right)\to \left(U<B\leftrightarrow U<if\left(B\le U+T,B,U+T\right)\right)$$
23		breq2	$$⊢U+T=if\left(B\le U+T,B,U+T\right)\to \left(U<U+T\leftrightarrow U<if\left(B\le U+T,B,U+T\right)\right)$$
24	22 23	ifboth	$$⊢\left(U<B\wedge U<U+T\right)\to U<if\left(B\le U+T,B,U+T\right)$$
25	20 21 24	syl2anc	$$⊢\phi \to U<if\left(B\le U+T,B,U+T\right)$$
26		ne0i	$$⊢U\in \left(A,B\right)\to \left(A,B\right)\ne \varnothing$$
27		ndmioo	$$⊢\neg \left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A,B\right)=\varnothing$$
28	27	necon1ai	$$⊢\left(A,B\right)\ne \varnothing \to \left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)$$
29	3 26 28	3syl	$$⊢\phi \to \left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)$$
30	29	simprd	$$⊢\phi \to B\in {ℝ}^{*}$$
31	8	rpred	$$⊢\phi \to T\in ℝ$$
32	17 31	readdcld	$$⊢\phi \to U+T\in ℝ$$
33	32	rexrd	$$⊢\phi \to U+T\in {ℝ}^{*}$$
34	30 33	ifcld	$$⊢\phi \to if\left(B\le U+T,B,U+T\right)\in {ℝ}^{*}$$
35		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
36	35	a1i	$$⊢\phi \to \mathrm{-\infty }\in {ℝ}^{*}$$
37	17	rexrd	$$⊢\phi \to U\in {ℝ}^{*}$$
38	17	mnfltd	$$⊢\phi \to \mathrm{-\infty }<U$$
39	36 37 30 38 20	xrlttrd	$$⊢\phi \to \mathrm{-\infty }<B$$
40	32	mnfltd	$$⊢\phi \to \mathrm{-\infty }<U+T$$
41		breq2	$$⊢B=if\left(B\le U+T,B,U+T\right)\to \left(\mathrm{-\infty }<B\leftrightarrow \mathrm{-\infty }<if\left(B\le U+T,B,U+T\right)\right)$$
42		breq2	$$⊢U+T=if\left(B\le U+T,B,U+T\right)\to \left(\mathrm{-\infty }<U+T\leftrightarrow \mathrm{-\infty }<if\left(B\le U+T,B,U+T\right)\right)$$
43	41 42	ifboth	$$⊢\left(\mathrm{-\infty }<B\wedge \mathrm{-\infty }<U+T\right)\to \mathrm{-\infty }<if\left(B\le U+T,B,U+T\right)$$
44	39 40 43	syl2anc	$$⊢\phi \to \mathrm{-\infty }<if\left(B\le U+T,B,U+T\right)$$
45		xrmin2	$$⊢\left(B\in {ℝ}^{*}\wedge U+T\in {ℝ}^{*}\right)\to if\left(B\le U+T,B,U+T\right)\le U+T$$
46	30 33 45	syl2anc	$$⊢\phi \to if\left(B\le U+T,B,U+T\right)\le U+T$$
47		xrre	$$⊢\left(\left(if\left(B\le U+T,B,U+T\right)\in {ℝ}^{*}\wedge U+T\in ℝ\right)\wedge \left(\mathrm{-\infty }<if\left(B\le U+T,B,U+T\right)\wedge if\left(B\le U+T,B,U+T\right)\le U+T\right)\right)\to if\left(B\le U+T,B,U+T\right)\in ℝ$$
48	34 32 44 46 47	syl22anc	$$⊢\phi \to if\left(B\le U+T,B,U+T\right)\in ℝ$$
49		avglt1	$$⊢\left(U\in ℝ\wedge if\left(B\le U+T,B,U+T\right)\in ℝ\right)\to \left(U<if\left(B\le U+T,B,U+T\right)\leftrightarrow U<\frac{U+if\left(B\le U+T,B,U+T\right)}{2}\right)$$
50	17 48 49	syl2anc	$$⊢\phi \to \left(U<if\left(B\le U+T,B,U+T\right)\leftrightarrow U<\frac{U+if\left(B\le U+T,B,U+T\right)}{2}\right)$$
51	25 50	mpbid	$$⊢\phi \to U<\frac{U+if\left(B\le U+T,B,U+T\right)}{2}$$
52	51 10	breqtrrdi	$$⊢\phi \to U<S$$
53	17 52	gtned	$$⊢\phi \to S\ne U$$
54	17 48	readdcld	$$⊢\phi \to U+if\left(B\le U+T,B,U+T\right)\in ℝ$$
55	54	rehalfcld	$$⊢\phi \to \frac{U+if\left(B\le U+T,B,U+T\right)}{2}\in ℝ$$
56	10 55	eqeltrid	$$⊢\phi \to S\in ℝ$$
57	17 56 52	ltled	$$⊢\phi \to U\le S$$
58	17 56 57	abssubge0d	$$⊢\phi \to \left|S-U\right|=S-U$$
59		avglt2	$$⊢\left(U\in ℝ\wedge if\left(B\le U+T,B,U+T\right)\in ℝ\right)\to \left(U<if\left(B\le U+T,B,U+T\right)\leftrightarrow \frac{U+if\left(B\le U+T,B,U+T\right)}{2}<if\left(B\le U+T,B,U+T\right)\right)$$
60	17 48 59	syl2anc	$$⊢\phi \to \left(U<if\left(B\le U+T,B,U+T\right)\leftrightarrow \frac{U+if\left(B\le U+T,B,U+T\right)}{2}<if\left(B\le U+T,B,U+T\right)\right)$$
61	25 60	mpbid	$$⊢\phi \to \frac{U+if\left(B\le U+T,B,U+T\right)}{2}<if\left(B\le U+T,B,U+T\right)$$
62	10 61	eqbrtrid	$$⊢\phi \to S<if\left(B\le U+T,B,U+T\right)$$
63	56 48 32 62 46	ltletrd	$$⊢\phi \to S<U+T$$
64	56 17 31	ltsubadd2d	$$⊢\phi \to \left(S-U<T\leftrightarrow S<U+T\right)$$
65	63 64	mpbird	$$⊢\phi \to S-U<T$$
66	58 65	eqbrtrd	$$⊢\phi \to \left|S-U\right|<T$$
67		neeq1	$$⊢z=S\to \left(z\ne U\leftrightarrow S\ne U\right)$$
68		fvoveq1	$$⊢z=S\to \left|z-U\right|=\left|S-U\right|$$
69	68	breq1d	$$⊢z=S\to \left(\left|z-U\right|<T\leftrightarrow \left|S-U\right|<T\right)$$
70	67 69	anbi12d	$$⊢z=S\to \left(\left(z\ne U\wedge \left|z-U\right|<T\right)\leftrightarrow \left(S\ne U\wedge \left|S-U\right|<T\right)\right)$$
71		fveq2	$$⊢z=S\to F\left(z\right)=F\left(S\right)$$
72	71	oveq1d	$$⊢z=S\to F\left(z\right)-F\left(U\right)=F\left(S\right)-F\left(U\right)$$
73		oveq1	$$⊢z=S\to z-U=S-U$$
74	72 73	oveq12d	$$⊢z=S\to \frac{F\left(z\right)-F\left(U\right)}{z-U}=\frac{F\left(S\right)-F\left(U\right)}{S-U}$$
75	74	fvoveq1d	$$⊢z=S\to \left|\left(\frac{F\left(z\right)-F\left(U\right)}{z-U}\right)-F_{ℝ}^{\prime }\left(U\right)\right|=\left|\left(\frac{F\left(S\right)-F\left(U\right)}{S-U}\right)-F_{ℝ}^{\prime }\left(U\right)\right|$$
76	75	breq1d	$$⊢z=S\to \left(\left|\left(\frac{F\left(z\right)-F\left(U\right)}{z-U}\right)-F_{ℝ}^{\prime }\left(U\right)\right|<F_{ℝ}^{\prime }\left(U\right)\leftrightarrow \left|\left(\frac{F\left(S\right)-F\left(U\right)}{S-U}\right)-F_{ℝ}^{\prime }\left(U\right)\right|<F_{ℝ}^{\prime }\left(U\right)\right)$$
77	70 76	imbi12d	$$⊢z=S\to \left(\left(\left(z\ne U\wedge \left|z-U\right|<T\right)\to \left|\left(\frac{F\left(z\right)-F\left(U\right)}{z-U}\right)-F_{ℝ}^{\prime }\left(U\right)\right|<F_{ℝ}^{\prime }\left(U\right)\right)\leftrightarrow \left(\left(S\ne U\wedge \left|S-U\right|<T\right)\to \left|\left(\frac{F\left(S\right)-F\left(U\right)}{S-U}\right)-F_{ℝ}^{\prime }\left(U\right)\right|<F_{ℝ}^{\prime }\left(U\right)\right)\right)$$
78	29	simpld	$$⊢\phi \to A\in {ℝ}^{*}$$
79	19	simpld	$$⊢\phi \to A<U$$
80	78 37 79	xrltled	$$⊢\phi \to A\le U$$
81		iooss1	$$⊢\left(A\in {ℝ}^{*}\wedge A\le U\right)\to \left(U,B\right)\subseteq \left(A,B\right)$$
82	78 80 81	syl2anc	$$⊢\phi \to \left(U,B\right)\subseteq \left(A,B\right)$$
83	82 4	sstrd	$$⊢\phi \to \left(U,B\right)\subseteq X$$
84	56	rexrd	$$⊢\phi \to S\in {ℝ}^{*}$$
85		xrmin1	$$⊢\left(B\in {ℝ}^{*}\wedge U+T\in {ℝ}^{*}\right)\to if\left(B\le U+T,B,U+T\right)\le B$$
86	30 33 85	syl2anc	$$⊢\phi \to if\left(B\le U+T,B,U+T\right)\le B$$
87	84 34 30 62 86	xrltletrd	$$⊢\phi \to S<B$$
88		elioo2	$$⊢\left(U\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(S\in \left(U,B\right)\leftrightarrow \left(S\in ℝ\wedge U<S\wedge S<B\right)\right)$$
89	37 30 88	syl2anc	$$⊢\phi \to \left(S\in \left(U,B\right)\leftrightarrow \left(S\in ℝ\wedge U<S\wedge S<B\right)\right)$$
90	56 52 87 89	mpbir3and	$$⊢\phi \to S\in \left(U,B\right)$$
91	83 90	sseldd	$$⊢\phi \to S\in X$$
92		eldifsn	$$⊢S\in \left(X\setminus \left\{U\right\}\right)\leftrightarrow \left(S\in X\wedge S\ne U\right)$$
93	91 53 92	sylanbrc	$$⊢\phi \to S\in \left(X\setminus \left\{U\right\}\right)$$
94	77 9 93	rspcdva	$$⊢\phi \to \left(\left(S\ne U\wedge \left|S-U\right|<T\right)\to \left|\left(\frac{F\left(S\right)-F\left(U\right)}{S-U}\right)-F_{ℝ}^{\prime }\left(U\right)\right|<F_{ℝ}^{\prime }\left(U\right)\right)$$
95	53 66 94	mp2and	$$⊢\phi \to \left|\left(\frac{F\left(S\right)-F\left(U\right)}{S-U}\right)-F_{ℝ}^{\prime }\left(U\right)\right|<F_{ℝ}^{\prime }\left(U\right)$$
96	1 91	ffvelrnd	$$⊢\phi \to F\left(S\right)\in ℝ$$
97	4 3	sseldd	$$⊢\phi \to U\in X$$
98	1 97	ffvelrnd	$$⊢\phi \to F\left(U\right)\in ℝ$$
99	96 98	resubcld	$$⊢\phi \to F\left(S\right)-F\left(U\right)\in ℝ$$
100	56 17	resubcld	$$⊢\phi \to S-U\in ℝ$$
101	17 56	posdifd	$$⊢\phi \to \left(U<S\leftrightarrow 0<S-U\right)$$
102	52 101	mpbid	$$⊢\phi \to 0<S-U$$
103	100 102	elrpd	$$⊢\phi \to S-U\in {ℝ}^{+}$$
104	99 103	rerpdivcld	$$⊢\phi \to \frac{F\left(S\right)-F\left(U\right)}{S-U}\in ℝ$$
105	104 13 13	absdifltd	$$⊢\phi \to \left(\left|\left(\frac{F\left(S\right)-F\left(U\right)}{S-U}\right)-F_{ℝ}^{\prime }\left(U\right)\right|<F_{ℝ}^{\prime }\left(U\right)\leftrightarrow \left(F_{ℝ}^{\prime }\left(U\right)-F_{ℝ}^{\prime }\left(U\right)<\frac{F\left(S\right)-F\left(U\right)}{S-U}\wedge \frac{F\left(S\right)-F\left(U\right)}{S-U}<F_{ℝ}^{\prime }\left(U\right)+F_{ℝ}^{\prime }\left(U\right)\right)\right)$$
106	95 105	mpbid	$$⊢\phi \to \left(F_{ℝ}^{\prime }\left(U\right)-F_{ℝ}^{\prime }\left(U\right)<\frac{F\left(S\right)-F\left(U\right)}{S-U}\wedge \frac{F\left(S\right)-F\left(U\right)}{S-U}<F_{ℝ}^{\prime }\left(U\right)+F_{ℝ}^{\prime }\left(U\right)\right)$$
107	106	simpld	$$⊢\phi \to F_{ℝ}^{\prime }\left(U\right)-F_{ℝ}^{\prime }\left(U\right)<\frac{F\left(S\right)-F\left(U\right)}{S-U}$$
108	15 107	eqbrtrrd	$$⊢\phi \to 0<\frac{F\left(S\right)-F\left(U\right)}{S-U}$$
109		gt0div	$$⊢\left(F\left(S\right)-F\left(U\right)\in ℝ\wedge S-U\in ℝ\wedge 0<S-U\right)\to \left(0<F\left(S\right)-F\left(U\right)\leftrightarrow 0<\frac{F\left(S\right)-F\left(U\right)}{S-U}\right)$$
110	99 100 102 109	syl3anc	$$⊢\phi \to \left(0<F\left(S\right)-F\left(U\right)\leftrightarrow 0<\frac{F\left(S\right)-F\left(U\right)}{S-U}\right)$$
111	108 110	mpbird	$$⊢\phi \to 0<F\left(S\right)-F\left(U\right)$$
112	98 96	posdifd	$$⊢\phi \to \left(F\left(U\right)<F\left(S\right)\leftrightarrow 0<F\left(S\right)-F\left(U\right)\right)$$
113	111 112	mpbird	$$⊢\phi \to F\left(U\right)<F\left(S\right)$$
114		fveq2	$$⊢y=S\to F\left(y\right)=F\left(S\right)$$
115	114	breq1d	$$⊢y=S\to \left(F\left(y\right)\le F\left(U\right)\leftrightarrow F\left(S\right)\le F\left(U\right)\right)$$
116	115 6 90	rspcdva	$$⊢\phi \to F\left(S\right)\le F\left(U\right)$$
117	96 98 116	lensymd	$$⊢\phi \to \neg F\left(U\right)<F\left(S\right)$$
118	113 117	pm2.65i	$$⊢\neg \phi$$