Theorem dvferm2lem

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 }$$
	dvferm2.r	$$⊢\phi \to \forall y\in \left(A,U\right)F\left(y\right)\le F\left(U\right)$$
	dvferm2.z	$$⊢\phi \to F_{ℝ}^{\prime }\left(U\right)<0$$
	dvferm2.t	$$⊢\phi \to T\in {ℝ}^{+}$$
	dvferm2.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)$$
	dvferm2.x	$$⊢S=\frac{if\left(A\le U-T,U-T,A\right)+U}{2}$$
Assertion	dvferm2lem	$$⊢\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		dvferm2.r	$$⊢\phi \to \forall y\in \left(A,U\right)F\left(y\right)\le F\left(U\right)$$
7		dvferm2.z	$$⊢\phi \to F_{ℝ}^{\prime }\left(U\right)<0$$
8		dvferm2.t	$$⊢\phi \to T\in {ℝ}^{+}$$
9		dvferm2.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		dvferm2.x	$$⊢S=\frac{if\left(A\le U-T,U-T,A\right)+U}{2}$$
11		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
12	11	a1i	$$⊢\phi \to \mathrm{-\infty }\in {ℝ}^{*}$$
13		ioossre	$$⊢\left(A,B\right)\subseteq ℝ$$
14	13 3	sseldi	$$⊢\phi \to U\in ℝ$$
15	8	rpred	$$⊢\phi \to T\in ℝ$$
16	14 15	resubcld	$$⊢\phi \to U-T\in ℝ$$
17	16	rexrd	$$⊢\phi \to U-T\in {ℝ}^{*}$$
18		ne0i	$$⊢U\in \left(A,B\right)\to \left(A,B\right)\ne \varnothing$$
19		ndmioo	$$⊢\neg \left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A,B\right)=\varnothing$$
20	19	necon1ai	$$⊢\left(A,B\right)\ne \varnothing \to \left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)$$
21	3 18 20	3syl	$$⊢\phi \to \left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)$$
22	21	simpld	$$⊢\phi \to A\in {ℝ}^{*}$$
23	17 22	ifcld	$$⊢\phi \to if\left(A\le U-T,U-T,A\right)\in {ℝ}^{*}$$
24	14	rexrd	$$⊢\phi \to U\in {ℝ}^{*}$$
25	16	mnfltd	$$⊢\phi \to \mathrm{-\infty }<U-T$$
26		xrmax2	$$⊢\left(A\in {ℝ}^{*}\wedge U-T\in {ℝ}^{*}\right)\to U-T\le if\left(A\le U-T,U-T,A\right)$$
27	22 17 26	syl2anc	$$⊢\phi \to U-T\le if\left(A\le U-T,U-T,A\right)$$
28	12 17 23 25 27	xrltletrd	$$⊢\phi \to \mathrm{-\infty }<if\left(A\le U-T,U-T,A\right)$$
29	14 8	ltsubrpd	$$⊢\phi \to U-T<U$$
30		eliooord	$$⊢U\in \left(A,B\right)\to \left(A<U\wedge U<B\right)$$
31	3 30	syl	$$⊢\phi \to \left(A<U\wedge U<B\right)$$
32	31	simpld	$$⊢\phi \to A<U$$
33		breq1	$$⊢U-T=if\left(A\le U-T,U-T,A\right)\to \left(U-T<U\leftrightarrow if\left(A\le U-T,U-T,A\right)<U\right)$$
34		breq1	$$⊢A=if\left(A\le U-T,U-T,A\right)\to \left(A<U\leftrightarrow if\left(A\le U-T,U-T,A\right)<U\right)$$
35	33 34	ifboth	$$⊢\left(U-T<U\wedge A<U\right)\to if\left(A\le U-T,U-T,A\right)<U$$
36	29 32 35	syl2anc	$$⊢\phi \to if\left(A\le U-T,U-T,A\right)<U$$
37		xrre2	$$⊢\left(\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge if\left(A\le U-T,U-T,A\right)\in {ℝ}^{*}\wedge U\in {ℝ}^{*}\right)\wedge \left(\mathrm{-\infty }<if\left(A\le U-T,U-T,A\right)\wedge if\left(A\le U-T,U-T,A\right)<U\right)\right)\to if\left(A\le U-T,U-T,A\right)\in ℝ$$
38	12 23 24 28 36 37	syl32anc	$$⊢\phi \to if\left(A\le U-T,U-T,A\right)\in ℝ$$
39	38 14	readdcld	$$⊢\phi \to if\left(A\le U-T,U-T,A\right)+U\in ℝ$$
40	39	rehalfcld	$$⊢\phi \to \frac{if\left(A\le U-T,U-T,A\right)+U}{2}\in ℝ$$
41	10 40	eqeltrid	$$⊢\phi \to S\in ℝ$$
42		avglt2	$$⊢\left(if\left(A\le U-T,U-T,A\right)\in ℝ\wedge U\in ℝ\right)\to \left(if\left(A\le U-T,U-T,A\right)<U\leftrightarrow \frac{if\left(A\le U-T,U-T,A\right)+U}{2}<U\right)$$
43	38 14 42	syl2anc	$$⊢\phi \to \left(if\left(A\le U-T,U-T,A\right)<U\leftrightarrow \frac{if\left(A\le U-T,U-T,A\right)+U}{2}<U\right)$$
44	36 43	mpbid	$$⊢\phi \to \frac{if\left(A\le U-T,U-T,A\right)+U}{2}<U$$
45	10 44	eqbrtrid	$$⊢\phi \to S<U$$
46	41 45	ltned	$$⊢\phi \to S\ne U$$
47	41 14 45	ltled	$$⊢\phi \to S\le U$$
48	41 14 47	abssuble0d	$$⊢\phi \to \left|S-U\right|=U-S$$
49		avglt1	$$⊢\left(if\left(A\le U-T,U-T,A\right)\in ℝ\wedge U\in ℝ\right)\to \left(if\left(A\le U-T,U-T,A\right)<U\leftrightarrow if\left(A\le U-T,U-T,A\right)<\frac{if\left(A\le U-T,U-T,A\right)+U}{2}\right)$$
50	38 14 49	syl2anc	$$⊢\phi \to \left(if\left(A\le U-T,U-T,A\right)<U\leftrightarrow if\left(A\le U-T,U-T,A\right)<\frac{if\left(A\le U-T,U-T,A\right)+U}{2}\right)$$
51	36 50	mpbid	$$⊢\phi \to if\left(A\le U-T,U-T,A\right)<\frac{if\left(A\le U-T,U-T,A\right)+U}{2}$$
52	51 10	breqtrrdi	$$⊢\phi \to if\left(A\le U-T,U-T,A\right)<S$$
53	16 38 41 27 52	lelttrd	$$⊢\phi \to U-T<S$$
54	14 15 41 53	ltsub23d	$$⊢\phi \to U-S<T$$
55	48 54	eqbrtrd	$$⊢\phi \to \left|S-U\right|<T$$
56		neeq1	$$⊢z=S\to \left(z\ne U\leftrightarrow S\ne U\right)$$
57		fvoveq1	$$⊢z=S\to \left|z-U\right|=\left|S-U\right|$$
58	57	breq1d	$$⊢z=S\to \left(\left|z-U\right|<T\leftrightarrow \left|S-U\right|<T\right)$$
59	56 58	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)$$
60		fveq2	$$⊢z=S\to F\left(z\right)=F\left(S\right)$$
61	60	oveq1d	$$⊢z=S\to F\left(z\right)-F\left(U\right)=F\left(S\right)-F\left(U\right)$$
62		oveq1	$$⊢z=S\to z-U=S-U$$
63	61 62	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}$$
64	63	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|$$
65	64	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)$$
66	59 65	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)$$
67	21	simprd	$$⊢\phi \to B\in {ℝ}^{*}$$
68	31	simprd	$$⊢\phi \to U<B$$
69	24 67 68	xrltled	$$⊢\phi \to U\le B$$
70		iooss2	$$⊢\left(B\in {ℝ}^{*}\wedge U\le B\right)\to \left(A,U\right)\subseteq \left(A,B\right)$$
71	67 69 70	syl2anc	$$⊢\phi \to \left(A,U\right)\subseteq \left(A,B\right)$$
72	71 4	sstrd	$$⊢\phi \to \left(A,U\right)\subseteq X$$
73	41	rexrd	$$⊢\phi \to S\in {ℝ}^{*}$$
74		xrmax1	$$⊢\left(A\in {ℝ}^{*}\wedge U-T\in {ℝ}^{*}\right)\to A\le if\left(A\le U-T,U-T,A\right)$$
75	22 17 74	syl2anc	$$⊢\phi \to A\le if\left(A\le U-T,U-T,A\right)$$
76	22 23 73 75 52	xrlelttrd	$$⊢\phi \to A<S$$
77		elioo2	$$⊢\left(A\in {ℝ}^{*}\wedge U\in {ℝ}^{*}\right)\to \left(S\in \left(A,U\right)\leftrightarrow \left(S\in ℝ\wedge A<S\wedge S<U\right)\right)$$
78	22 24 77	syl2anc	$$⊢\phi \to \left(S\in \left(A,U\right)\leftrightarrow \left(S\in ℝ\wedge A<S\wedge S<U\right)\right)$$
79	41 76 45 78	mpbir3and	$$⊢\phi \to S\in \left(A,U\right)$$
80	72 79	sseldd	$$⊢\phi \to S\in X$$
81		eldifsn	$$⊢S\in \left(X\setminus \left\{U\right\}\right)\leftrightarrow \left(S\in X\wedge S\ne U\right)$$
82	80 46 81	sylanbrc	$$⊢\phi \to S\in \left(X\setminus \left\{U\right\}\right)$$
83	66 9 82	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)$$
84	46 55 83	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)$$
85	1 80	ffvelrnd	$$⊢\phi \to F\left(S\right)\in ℝ$$
86	4 3	sseldd	$$⊢\phi \to U\in X$$
87	1 86	ffvelrnd	$$⊢\phi \to F\left(U\right)\in ℝ$$
88	85 87	resubcld	$$⊢\phi \to F\left(S\right)-F\left(U\right)\in ℝ$$
89	41 14	resubcld	$$⊢\phi \to S-U\in ℝ$$
90	41	recnd	$$⊢\phi \to S\in ℂ$$
91	14	recnd	$$⊢\phi \to U\in ℂ$$
92	90 91 46	subne0d	$$⊢\phi \to S-U\ne 0$$
93	88 89 92	redivcld	$$⊢\phi \to \frac{F\left(S\right)-F\left(U\right)}{S-U}\in ℝ$$
94		dvfre	$$⊢\left(F:X⟶ℝ\wedge X\subseteq ℝ\right)\to F_{ℝ}^{\prime }:\mathrm{dom}{F}_{ℝ}^{\prime }⟶ℝ$$
95	1 2 94	syl2anc	$$⊢\phi \to F_{ℝ}^{\prime }:\mathrm{dom}{F}_{ℝ}^{\prime }⟶ℝ$$
96	95 5	ffvelrnd	$$⊢\phi \to F_{ℝ}^{\prime }\left(U\right)\in ℝ$$
97	96	renegcld	$$⊢\phi \to -F_{ℝ}^{\prime }\left(U\right)\in ℝ$$
98	93 96 97	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)-\left(-F_{ℝ}^{\prime }\left(U\right)\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)+\left(-F_{ℝ}^{\prime }\left(U\right)\right)\right)\right)$$
99	84 98	mpbid	$$⊢\phi \to \left(F_{ℝ}^{\prime }\left(U\right)-\left(-F_{ℝ}^{\prime }\left(U\right)\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)+\left(-F_{ℝ}^{\prime }\left(U\right)\right)\right)$$
100	99	simprd	$$⊢\phi \to \frac{F\left(S\right)-F\left(U\right)}{S-U}<F_{ℝ}^{\prime }\left(U\right)+\left(-F_{ℝ}^{\prime }\left(U\right)\right)$$
101	96	recnd	$$⊢\phi \to F_{ℝ}^{\prime }\left(U\right)\in ℂ$$
102	101	negidd	$$⊢\phi \to F_{ℝ}^{\prime }\left(U\right)+\left(-F_{ℝ}^{\prime }\left(U\right)\right)=0$$
103	100 102	breqtrd	$$⊢\phi \to \frac{F\left(S\right)-F\left(U\right)}{S-U}<0$$
104	93	lt0neg1d	$$⊢\phi \to \left(\frac{F\left(S\right)-F\left(U\right)}{S-U}<0\leftrightarrow 0<-\frac{F\left(S\right)-F\left(U\right)}{S-U}\right)$$
105	103 104	mpbid	$$⊢\phi \to 0<-\frac{F\left(S\right)-F\left(U\right)}{S-U}$$
106	88	recnd	$$⊢\phi \to F\left(S\right)-F\left(U\right)\in ℂ$$
107	89	recnd	$$⊢\phi \to S-U\in ℂ$$
108	106 107 92	divneg2d	$$⊢\phi \to -\frac{F\left(S\right)-F\left(U\right)}{S-U}=\frac{F\left(S\right)-F\left(U\right)}{-\left(S-U\right)}$$
109	105 108	breqtrd	$$⊢\phi \to 0<\frac{F\left(S\right)-F\left(U\right)}{-\left(S-U\right)}$$
110	89	renegcld	$$⊢\phi \to -\left(S-U\right)\in ℝ$$
111	41 14	posdifd	$$⊢\phi \to \left(S<U\leftrightarrow 0<U-S\right)$$
112	45 111	mpbid	$$⊢\phi \to 0<U-S$$
113	90 91	negsubdi2d	$$⊢\phi \to -\left(S-U\right)=U-S$$
114	112 113	breqtrrd	$$⊢\phi \to 0<-\left(S-U\right)$$
115		gt0div	$$⊢\left(F\left(S\right)-F\left(U\right)\in ℝ\wedge -\left(S-U\right)\in ℝ\wedge 0<-\left(S-U\right)\right)\to \left(0<F\left(S\right)-F\left(U\right)\leftrightarrow 0<\frac{F\left(S\right)-F\left(U\right)}{-\left(S-U\right)}\right)$$
116	88 110 114 115	syl3anc	$$⊢\phi \to \left(0<F\left(S\right)-F\left(U\right)\leftrightarrow 0<\frac{F\left(S\right)-F\left(U\right)}{-\left(S-U\right)}\right)$$
117	109 116	mpbird	$$⊢\phi \to 0<F\left(S\right)-F\left(U\right)$$
118	87 85	posdifd	$$⊢\phi \to \left(F\left(U\right)<F\left(S\right)\leftrightarrow 0<F\left(S\right)-F\left(U\right)\right)$$
119	117 118	mpbird	$$⊢\phi \to F\left(U\right)<F\left(S\right)$$
120		fveq2	$$⊢y=S\to F\left(y\right)=F\left(S\right)$$
121	120	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)$$
122	121 6 79	rspcdva	$$⊢\phi \to F\left(S\right)\le F\left(U\right)$$
123	85 87 122	lensymd	$$⊢\phi \to \neg F\left(U\right)<F\left(S\right)$$
124	119 123	pm2.65i	$$⊢\neg \phi$$