dvferm1

Description: One-sided version of dvferm . A point U which is the local maximum of its right neighborhood has derivative at most 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_{ℝ}^{'}$
	dvferm1.r	$⊢ φ \to \forall y \in (U, B) F (y) \leq F (U)$
Assertion	dvferm1	$⊢ φ \to F_{ℝ}^{'} (U) \leq 0$

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		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 0 < F_{ℝ}^{'} (U)) \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 0 < F_{ℝ}^{'} (U)) \to (x \in (X ∖ \{U\}) ⟼ \frac{F (x) - F (U)}{x - U}) : X ∖ \{U\} ⟶ ℂ$
40	35	adantr	$⊢ (φ \land 0 < F_{ℝ}^{'} (U)) \to X \subseteq ℂ$
41	40	ssdifssd	$⊢ (φ \land 0 < F_{ℝ}^{'} (U)) \to X ∖ \{U\} \subseteq ℂ$
42	35 36	sseldd	$⊢ φ \to U \in ℂ$
43	42	adantr	$⊢ (φ \land 0 < F_{ℝ}^{'} (U)) \to U \in ℂ$
44	39 41 43	ellimc3	$⊢ (φ \land 0 < F_{ℝ}^{'} (U)) \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 0 < F_{ℝ}^{'} (U)) \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 0 < F_{ℝ}^{'} (U)) \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	anim1i	$⊢ (φ \land 0 < F_{ℝ}^{'} (U)) \to (F_{ℝ}^{'} (U) \in ℝ \land 0 < F_{ℝ}^{'} (U))$
51		elrp	$⊢ F_{ℝ}^{'} (U) \in ℝ^{+} \leftrightarrow (F_{ℝ}^{'} (U) \in ℝ \land 0 < F_{ℝ}^{'} (U))$
52	50 51	sylibr	$⊢ (φ \land 0 < F_{ℝ}^{'} (U)) \to F_{ℝ}^{'} (U) \in ℝ^{+}$
53	19 46 52	rspcdva	$⊢ (φ \land 0 < F_{ℝ}^{'} (U)) \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))$
54	1	ad3antrrr	$⊢ (((φ \land 0 < F_{ℝ}^{'} (U)) \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 ⟶ ℝ$
55	2	ad3antrrr	$⊢ (((φ \land 0 < F_{ℝ}^{'} (U)) \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 ℝ$
56	3	ad3antrrr	$⊢ (((φ \land 0 < F_{ℝ}^{'} (U)) \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)$
57	4	ad3antrrr	$⊢ (((φ \land 0 < F_{ℝ}^{'} (U)) \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$
58	5	ad3antrrr	$⊢ (((φ \land 0 < F_{ℝ}^{'} (U)) \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_{ℝ}^{'}$
59	6	ad3antrrr	$⊢ (((φ \land 0 < F_{ℝ}^{'} (U)) \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 (U, B) F (y) \leq F (U)$
60		simpllr	$⊢ (((φ \land 0 < F_{ℝ}^{'} (U)) \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 0 < F_{ℝ}^{'} (U)$
61		simplr	$⊢ (((φ \land 0 < F_{ℝ}^{'} (U)) \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 ℝ^{+}$
62		simpr	$⊢ (((φ \land 0 < F_{ℝ}^{'} (U)) \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))$
63		eqid	$⊢ \frac{U + if (B \leq U + u, B, U + u)}{2} = \frac{U + if (B \leq U + u, B, U + u)}{2}$
64	54 55 56 57 58 59 60 61 62 63	dvferm1lem	$⊢ \neg (((φ \land 0 < F_{ℝ}^{'} (U)) \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)))$
65	64	imnani	$⊢ ((φ \land 0 < F_{ℝ}^{'} (U)) \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))$
66	65	nrexdv	$⊢ (φ \land 0 < F_{ℝ}^{'} (U)) \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))$
67	53 66	pm2.65da	$⊢ φ \to \neg 0 < F_{ℝ}^{'} (U)$
68		0re	$⊢ 0 \in ℝ$
69		lenlt	$⊢ (F_{ℝ}^{'} (U) \in ℝ \land 0 \in ℝ) \to (F_{ℝ}^{'} (U) \leq 0 \leftrightarrow \neg 0 < F_{ℝ}^{'} (U))$
70	49 68 69	sylancl	$⊢ φ \to (F_{ℝ}^{'} (U) \leq 0 \leftrightarrow \neg 0 < F_{ℝ}^{'} (U))$
71	67 70	mpbird	$⊢ φ \to F_{ℝ}^{'} (U) \leq 0$

Metamath Proof Explorer

Theorem dvferm1

Proof