dvgt0

Description: A function on a closed interval with positive derivative is increasing. (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}{⟶} ℝ$
	dvgt0.d	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ ℝ^{+}$
Assertion	dvgt0	$⊢ φ \to F {Isom}_{<, <} ([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		dvgt0.d	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ ℝ^{+}$
5		ltso	$⊢ < 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 ℝ^{+}$
7	6	rpgt0d	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to 0 < \frac{F (y) - F (x)}{y - x}$
8		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℝ \to F : [A, B] ⟶ ℝ$
9	3 8	syl	$⊢ φ \to F : [A, B] ⟶ ℝ$
10	9	ad2antrr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F : [A, B] ⟶ ℝ$
11		simplrr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to y \in [A, B]$
12	10 11	ffvelcdmd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F (y) \in ℝ$
13		simplrl	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to x \in [A, B]$
14	10 13	ffvelcdmd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F (x) \in ℝ$
15	12 14	resubcld	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F (y) - F (x) \in ℝ$
16		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
17	1 2 16	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
18	17	ad2antrr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to [A, B] \subseteq ℝ$
19	18 11	sseldd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to y \in ℝ$
20	18 13	sseldd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to x \in ℝ$
21	19 20	resubcld	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to y - x \in ℝ$
22		simpr	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to x < y$
23	20 19	posdifd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to (x < y \leftrightarrow 0 < y - x)$
24	22 23	mpbid	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to 0 < y - x$
25		gt0div	$⊢ (F (y) - F (x) \in ℝ \land y - x \in ℝ \land 0 < y - x) \to (0 < F (y) - F (x) \leftrightarrow 0 < \frac{F (y) - F (x)}{y - x})$
26	15 21 24 25	syl3anc	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to (0 < F (y) - F (x) \leftrightarrow 0 < \frac{F (y) - F (x)}{y - x})$
27	7 26	mpbird	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to 0 < F (y) - F (x)$
28	14 12	posdifd	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to (F (x) < F (y) \leftrightarrow 0 < F (y) - F (x))$
29	27 28	mpbird	$⊢ ((φ \land (x \in [A, B] \land y \in [A, B])) \land x < y) \to F (x) < F (y)$
30	1 2 3 4 5 29	dvgt0lem2	$⊢ φ \to F {Isom}_{<, <} ([A, B], ran F)$

Metamath Proof Explorer

Theorem dvgt0

Proof