dvferm2

Description: One-sided version of dvferm . A point U which is the local maximum of its left neighborhood has derivative at least zero. (Contributed by Mario Carneiro, 24-Feb-2015) (Proof shortened by Mario Carneiro, 28-Dec-2016)

	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_{ℝ}^{'}$
	dvferm2.r	$⊢ φ \to \forall y \in (A, U) F (y) \leq F (U)$
Assertion	dvferm2	$⊢ φ \to 0 \leq F_{ℝ}^{'} (U)$

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		dvferm2.r	$⊢ φ \to \forall y \in (A, U) F (y) \leq F (U)$
7		fveq2	$⊢ x = z \to F (x) = F (z)$
8	7	oveq1d	$⊢ x = z \to F (x) - F (U) = F (z) - F (U)$
9		oveq1	$⊢ x = z \to x - U = z - U$
10	8 9	oveq12d	$⊢ x = z \to \frac{F (x) - F (U)}{x - U} = \frac{F (z) - F (U)}{z - U}$
11		eqid	$⊢ (x \in (X ∖ \{U\}) ⟼ \frac{F (x) - F (U)}{x - U}) = (x \in (X ∖ \{U\}) ⟼ \frac{F (x) - F (U)}{x - U})$
12		ovex	$⊢ \frac{F (z) - F (U)}{z - U} \in V$
13	10 11 12	fvmpt	$⊢ z \in (X ∖ \{U\}) \to (x \in (X ∖ \{U\}) ⟼ \frac{F (x) - F (U)}{x - U}) (z) = \frac{F (z) - F (U)}{z - U}$
14	13	fvoveq1d	$⊢ z \in (X ∖ \{U\}) \to \|(x \in (X ∖ \{U\}) ⟼ \frac{F (x) - F (U)}{x - U}) (z) - F_{ℝ}^{'} (U)\| = \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\|$
15		id	$⊢ y = - F_{ℝ}^{'} (U) \to y = - F_{ℝ}^{'} (U)$
16	14 15	breqan12rd	$⊢ (y = - F_{ℝ}^{'} (U) \land z \in (X ∖ \{U\})) \to (\|(x \in (X ∖ \{U\}) ⟼ \frac{F (x) - F (U)}{x - U}) (z) - F_{ℝ}^{'} (U)\| < y \leftrightarrow \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\| < - F_{ℝ}^{'} (U))$
17	16	imbi2d	$⊢ (y = - F_{ℝ}^{'} (U) \land z \in (X ∖ \{U\})) \to (((z \neq U \land \|z - U\| < u) \to \|(x \in (X ∖ \{U\}) ⟼ \frac{F (x) - F (U)}{x - U}) (z) - F_{ℝ}^{'} (U)\| < y) \leftrightarrow ((z \neq U \land \|z - U\| < u) \to \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\| < - F_{ℝ}^{'} (U)))$
18	17	ralbidva	$⊢ y = - F_{ℝ}^{'} (U) \to (\forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(x \in (X ∖ \{U\}) ⟼ \frac{F (x) - F (U)}{x - U}) (z) - F_{ℝ}^{'} (U)\| < y) \leftrightarrow \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\| < - F_{ℝ}^{'} (U)))$
19	18	rexbidv	$⊢ y = - F_{ℝ}^{'} (U) \to (\exists u \in ℝ^{+} \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(x \in (X ∖ \{U\}) ⟼ \frac{F (x) - F (U)}{x - U}) (z) - F_{ℝ}^{'} (U)\| < y) \leftrightarrow \exists u \in ℝ^{+} \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\| < - F_{ℝ}^{'} (U)))$
20		dvf	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ$
21		ffun	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ \to Fun F_{ℝ}^{'}$
22		funfvbrb	$⊢ Fun F_{ℝ}^{'} \to (U \in dom F_{ℝ}^{'} \leftrightarrow U F_{ℝ}^{'} F_{ℝ}^{'} (U))$
23	20 21 22	mp2b	$⊢ U \in dom F_{ℝ}^{'} \leftrightarrow U F_{ℝ}^{'} F_{ℝ}^{'} (U)$
24	5 23	sylib	$⊢ φ \to U F_{ℝ}^{'} F_{ℝ}^{'} (U)$
25		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
26		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
27		ax-resscn	$⊢ ℝ \subseteq ℂ$
28	27	a1i	$⊢ φ \to ℝ \subseteq ℂ$
29		fss	$⊢ (F : X ⟶ ℝ \land ℝ \subseteq ℂ) \to F : X ⟶ ℂ$
30	1 27 29	sylancl	$⊢ φ \to F : X ⟶ ℂ$
31	25 26 11 28 30 2	eldv	$⊢ φ \to (U F_{ℝ}^{'} F_{ℝ}^{'} (U) \leftrightarrow (U \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) (X) \land F_{ℝ}^{'} (U) \in ((x \in (X ∖ \{U\}) ⟼ \frac{F (x) - F (U)}{x - U}) {lim}_{ℂ} U)))$
32	24 31	mpbid	$⊢ φ \to (U \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) (X) \land F_{ℝ}^{'} (U) \in ((x \in (X ∖ \{U\}) ⟼ \frac{F (x) - F (U)}{x - U}) {lim}_{ℂ} U))$
33	32	simprd	$⊢ φ \to F_{ℝ}^{'} (U) \in ((x \in (X ∖ \{U\}) ⟼ \frac{F (x) - F (U)}{x - U}) {lim}_{ℂ} U)$
34	33	adantr	$⊢ (φ \land F_{ℝ}^{'} (U) < 0) \to F_{ℝ}^{'} (U) \in ((x \in (X ∖ \{U\}) ⟼ \frac{F (x) - F (U)}{x - U}) {lim}_{ℂ} U)$
35	2 27	sstrdi	$⊢ φ \to X \subseteq ℂ$
36	4 3	sseldd	$⊢ φ \to U \in X$
37	30 35 36	dvlem	$⊢ (φ \land x \in (X ∖ \{U\})) \to \frac{F (x) - F (U)}{x - U} \in ℂ$
38	37	fmpttd	$⊢ φ \to (x \in (X ∖ \{U\}) ⟼ \frac{F (x) - F (U)}{x - U}) : X ∖ \{U\} ⟶ ℂ$
39	38	adantr	$⊢ (φ \land F_{ℝ}^{'} (U) < 0) \to (x \in (X ∖ \{U\}) ⟼ \frac{F (x) - F (U)}{x - U}) : X ∖ \{U\} ⟶ ℂ$
40	35	adantr	$⊢ (φ \land F_{ℝ}^{'} (U) < 0) \to X \subseteq ℂ$
41	40	ssdifssd	$⊢ (φ \land F_{ℝ}^{'} (U) < 0) \to X ∖ \{U\} \subseteq ℂ$
42	35 36	sseldd	$⊢ φ \to U \in ℂ$
43	42	adantr	$⊢ (φ \land F_{ℝ}^{'} (U) < 0) \to U \in ℂ$
44	39 41 43	ellimc3	$⊢ (φ \land F_{ℝ}^{'} (U) < 0) \to (F_{ℝ}^{'} (U) \in ((x \in (X ∖ \{U\}) ⟼ \frac{F (x) - F (U)}{x - U}) {lim}_{ℂ} U) \leftrightarrow (F_{ℝ}^{'} (U) \in ℂ \land \forall y \in ℝ^{+} \exists u \in ℝ^{+} \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(x \in (X ∖ \{U\}) ⟼ \frac{F (x) - F (U)}{x - U}) (z) - F_{ℝ}^{'} (U)\| < y)))$
45	34 44	mpbid	$⊢ (φ \land F_{ℝ}^{'} (U) < 0) \to (F_{ℝ}^{'} (U) \in ℂ \land \forall y \in ℝ^{+} \exists u \in ℝ^{+} \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(x \in (X ∖ \{U\}) ⟼ \frac{F (x) - F (U)}{x - U}) (z) - F_{ℝ}^{'} (U)\| < y))$
46	45	simprd	$⊢ (φ \land F_{ℝ}^{'} (U) < 0) \to \forall y \in ℝ^{+} \exists u \in ℝ^{+} \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(x \in (X ∖ \{U\}) ⟼ \frac{F (x) - F (U)}{x - U}) (z) - F_{ℝ}^{'} (U)\| < y)$
47		dvfre	$⊢ (F : X ⟶ ℝ \land X \subseteq ℝ) \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
48	1 2 47	syl2anc	$⊢ φ \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
49	48 5	ffvelrnd	$⊢ φ \to F_{ℝ}^{'} (U) \in ℝ$
50	49	adantr	$⊢ (φ \land F_{ℝ}^{'} (U) < 0) \to F_{ℝ}^{'} (U) \in ℝ$
51	50	renegcld	$⊢ (φ \land F_{ℝ}^{'} (U) < 0) \to - F_{ℝ}^{'} (U) \in ℝ$
52	49	lt0neg1d	$⊢ φ \to (F_{ℝ}^{'} (U) < 0 \leftrightarrow 0 < - F_{ℝ}^{'} (U))$
53	52	biimpa	$⊢ (φ \land F_{ℝ}^{'} (U) < 0) \to 0 < - F_{ℝ}^{'} (U)$
54	51 53	elrpd	$⊢ (φ \land F_{ℝ}^{'} (U) < 0) \to - F_{ℝ}^{'} (U) \in ℝ^{+}$
55	19 46 54	rspcdva	$⊢ (φ \land F_{ℝ}^{'} (U) < 0) \to \exists u \in ℝ^{+} \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\| < - F_{ℝ}^{'} (U))$
56	1	ad3antrrr	$⊢ (((φ \land F_{ℝ}^{'} (U) < 0) \land u \in ℝ^{+}) \land \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\| < - F_{ℝ}^{'} (U))) \to F : X ⟶ ℝ$
57	2	ad3antrrr	$⊢ (((φ \land F_{ℝ}^{'} (U) < 0) \land u \in ℝ^{+}) \land \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\| < - F_{ℝ}^{'} (U))) \to X \subseteq ℝ$
58	3	ad3antrrr	$⊢ (((φ \land F_{ℝ}^{'} (U) < 0) \land u \in ℝ^{+}) \land \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\| < - F_{ℝ}^{'} (U))) \to U \in (A, B)$
59	4	ad3antrrr	$⊢ (((φ \land F_{ℝ}^{'} (U) < 0) \land u \in ℝ^{+}) \land \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\| < - F_{ℝ}^{'} (U))) \to (A, B) \subseteq X$
60	5	ad3antrrr	$⊢ (((φ \land F_{ℝ}^{'} (U) < 0) \land u \in ℝ^{+}) \land \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\| < - F_{ℝ}^{'} (U))) \to U \in dom F_{ℝ}^{'}$
61	6	ad3antrrr	$⊢ (((φ \land F_{ℝ}^{'} (U) < 0) \land u \in ℝ^{+}) \land \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\| < - F_{ℝ}^{'} (U))) \to \forall y \in (A, U) F (y) \leq F (U)$
62		simpllr	$⊢ (((φ \land F_{ℝ}^{'} (U) < 0) \land u \in ℝ^{+}) \land \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\| < - F_{ℝ}^{'} (U))) \to F_{ℝ}^{'} (U) < 0$
63		simplr	$⊢ (((φ \land F_{ℝ}^{'} (U) < 0) \land u \in ℝ^{+}) \land \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\| < - F_{ℝ}^{'} (U))) \to u \in ℝ^{+}$
64		simpr	$⊢ (((φ \land F_{ℝ}^{'} (U) < 0) \land u \in ℝ^{+}) \land \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\| < - F_{ℝ}^{'} (U))) \to \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\| < - F_{ℝ}^{'} (U))$
65		eqid	$⊢ \frac{if (A \leq U - u, U - u, A) + U}{2} = \frac{if (A \leq U - u, U - u, A) + U}{2}$
66	56 57 58 59 60 61 62 63 64 65	dvferm2lem	$⊢ \neg (((φ \land F_{ℝ}^{'} (U) < 0) \land u \in ℝ^{+}) \land \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\| < - F_{ℝ}^{'} (U)))$
67	66	imnani	$⊢ ((φ \land F_{ℝ}^{'} (U) < 0) \land u \in ℝ^{+}) \to \neg \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\| < - F_{ℝ}^{'} (U))$
68	67	nrexdv	$⊢ (φ \land F_{ℝ}^{'} (U) < 0) \to \neg \exists u \in ℝ^{+} \forall z \in (X ∖ \{U\}) ((z \neq U \land \|z - U\| < u) \to \|(\frac{F (z) - F (U)}{z - U}) - F_{ℝ}^{'} (U)\| < - F_{ℝ}^{'} (U))$
69	55 68	pm2.65da	$⊢ φ \to \neg F_{ℝ}^{'} (U) < 0$
70		0re	$⊢ 0 \in ℝ$
71		lenlt	$⊢ (0 \in ℝ \land F_{ℝ}^{'} (U) \in ℝ) \to (0 \leq F_{ℝ}^{'} (U) \leftrightarrow \neg F_{ℝ}^{'} (U) < 0)$
72	70 49 71	sylancr	$⊢ φ \to (0 \leq F_{ℝ}^{'} (U) \leftrightarrow \neg F_{ℝ}^{'} (U) < 0)$
73	69 72	mpbird	$⊢ φ \to 0 \leq F_{ℝ}^{'} (U)$

Metamath Proof Explorer

Theorem dvferm2

Proof