dvferm1lem

	Ref	Expression
Hypotheses	dvferm.a	$⊢ φ \to F : X ⟶ ℝ$
	dvferm.b	$⊢ φ \to X \subseteq ℝ$
	dvferm.u	$⊢ φ \to U \in (A, B)$
	dvferm.s	$⊢ φ \to (A, B) \subseteq X$
	dvferm.d	$⊢ φ \to U \in dom F_{ℝ}^{'}$
	dvferm1.r	$⊢ φ \to \forall y \in (U, B) F (y) \leq F (U)$
	dvferm1.z	$⊢ φ \to 0 < F_{ℝ}^{'} (U)$
	dvferm1.t	$⊢ φ \to T \in ℝ^{+}$
	dvferm1.l	$⊢ φ \to \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < T) \to \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\| < F_{ℝ}^{'} (U))$
	dvferm1.x	$⊢ S = \frac{U + if (B \leq U + T, B, U + T)}{2}$
Assertion	dvferm1lem	$⊢ \neg φ$

Proof

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

Metamath Proof Explorer

Theorem dvferm1lem

Proof