dvlt0

Description: A function on a closed interval with negative derivative is decreasing. (Contributed by Mario Carneiro, 19-Feb-2015)

	Ref	Expression
Hypotheses	dvgt0.a	$⊢ φ \to A \in ℝ$
	dvgt0.b	$⊢ φ \to B \in ℝ$
	dvgt0.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
	dvlt0.d	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ (−∞, 0)$
Assertion	dvlt0	$⊢ φ \to F {Isom}_{<, <^{-1}} ([A, B], ran F)$

Proof

Step	Hyp	Ref	Expression
1		dvgt0.a	$⊢ φ \to A \in ℝ$
2		dvgt0.b	$⊢ φ \to B \in ℝ$
3		dvgt0.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
4		dvlt0.d	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ (−∞, 0)$
5		gtso	$⊢ <^{-1} Or ℝ$
6	1 2 3 4	dvgt0lem1	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \frac{F (y) - F (x)}{y - x} \in (−∞, 0)$
7		eliooord	$⊢ \frac{F (y) - F (x)}{y - x} \in (−∞, 0) \to (−∞ < \frac{F (y) - F (x)}{y - x} \land \frac{F (y) - F (x)}{y - x} < 0)$
8	6 7	syl	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to (−∞ < \frac{F (y) - F (x)}{y - x} \land \frac{F (y) - F (x)}{y - x} < 0)$
9	8	simprd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to \frac{F (y) - F (x)}{y - x} < 0$
10		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℝ \to F : [A, B] ⟶ ℝ$
11	3 10	syl	$⊢ φ \to F : [A, B] ⟶ ℝ$
12	11	ad2antrr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F : [A, B] ⟶ ℝ$
13		simplrr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to y \in [A, B]$
14	12 13	ffvelrnd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F (y) \in ℝ$
15		simplrl	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to x \in [A, B]$
16	12 15	ffvelrnd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F (x) \in ℝ$
17	14 16	resubcld	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F (y) - F (x) \in ℝ$
18		0red	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to 0 \in ℝ$
19		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
20	1 2 19	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
21	20	ad2antrr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to [A, B] \subseteq ℝ$
22	21 13	sseldd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to y \in ℝ$
23	21 15	sseldd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to x \in ℝ$
24	22 23	resubcld	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to y - x \in ℝ$
25		simpr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to x < y$
26	23 22	posdifd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to (x < y \leftrightarrow 0 < y - x)$
27	25 26	mpbid	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to 0 < y - x$
28		ltdivmul	$⊢ (F (y) - F (x) \in ℝ \land 0 \in ℝ \land (y - x \in ℝ \land 0 < y - x)) \to (\frac{F (y) - F (x)}{y - x} < 0 \leftrightarrow F (y) - F (x) < (y - x) \cdot 0)$
29	17 18 24 27 28	syl112anc	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to (\frac{F (y) - F (x)}{y - x} < 0 \leftrightarrow F (y) - F (x) < (y - x) \cdot 0)$
30	9 29	mpbid	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F (y) - F (x) < (y - x) \cdot 0$
31	24	recnd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to y - x \in ℂ$
32	31	mul01d	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to (y - x) \cdot 0 = 0$
33	30 32	breqtrd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F (y) - F (x) < 0$
34	14 16 18	ltsubaddd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to (F (y) - F (x) < 0 \leftrightarrow F (y) < 0 + F (x))$
35	33 34	mpbid	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F (y) < 0 + F (x)$
36	16	recnd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F (x) \in ℂ$
37	36	addid2d	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to 0 + F (x) = F (x)$
38	35 37	breqtrd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F (y) < F (x)$
39		fvex	$⊢ F (x) \in V$
40		fvex	$⊢ F (y) \in V$
41	39 40	brcnv	$⊢ F (x) <^{-1} F (y) \leftrightarrow F (y) < F (x)$
42	38 41	sylibr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F (x) <^{-1} F (y)$
43	1 2 3 4 5 42	dvgt0lem2	$⊢ φ \to F {Isom}_{<, <^{-1}} ([A, B], ran F)$

Metamath Proof Explorer

Theorem dvlt0

Proof