dvge0

Description: A function on a closed interval with nonnegative derivative is weakly increasing. (Contributed by Mario Carneiro, 30-Apr-2016)

	Ref	Expression
Hypotheses	dvgt0.a	$⊢ φ \to A \in ℝ$
	dvgt0.b	$⊢ φ \to B \in ℝ$
	dvgt0.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
	dvge0.d	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ [0, +∞)$
	dvge0.x	$⊢ φ \to X \in [A, B]$
	dvge0.y	$⊢ φ \to Y \in [A, B]$
	dvge0.l	$⊢ φ \to X \leq Y$
Assertion	dvge0	$⊢ φ \to F (X) \leq F (Y)$

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		dvge0.d	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ [0, +∞)$
5		dvge0.x	$⊢ φ \to X \in [A, B]$
6		dvge0.y	$⊢ φ \to Y \in [A, B]$
7		dvge0.l	$⊢ φ \to X \leq Y$
8	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, +∞)$
9	8	exp31	$⊢ φ \to ((X \in [A, B] \land Y \in [A, B]) \to (X < Y \to \frac{F (Y) - F (X)}{Y - X} \in [0, +∞)))$
10	5 6 9	mp2and	$⊢ φ \to (X < Y \to \frac{F (Y) - F (X)}{Y - X} \in [0, +∞))$
11	10	imp	$⊢ (φ \land X < Y) \to \frac{F (Y) - F (X)}{Y - X} \in [0, +∞)$
12		elrege0	$⊢ \frac{F (Y) - F (X)}{Y - X} \in [0, +∞) \leftrightarrow (\frac{F (Y) - F (X)}{Y - X} \in ℝ \land 0 \leq \frac{F (Y) - F (X)}{Y - X})$
13	12	simprbi	$⊢ \frac{F (Y) - F (X)}{Y - X} \in [0, +∞) \to 0 \leq \frac{F (Y) - F (X)}{Y - X}$
14	11 13	syl	$⊢ (φ \land X < Y) \to 0 \leq \frac{F (Y) - F (X)}{Y - X}$
15		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℝ \to F : [A, B] ⟶ ℝ$
16	3 15	syl	$⊢ φ \to F : [A, B] ⟶ ℝ$
17	16 6	ffvelcdmd	$⊢ φ \to F (Y) \in ℝ$
18	16 5	ffvelcdmd	$⊢ φ \to F (X) \in ℝ$
19	17 18	resubcld	$⊢ φ \to F (Y) - F (X) \in ℝ$
20	19	adantr	$⊢ (φ \land X < Y) \to F (Y) - F (X) \in ℝ$
21		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
22	1 2 21	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
23	22 6	sseldd	$⊢ φ \to Y \in ℝ$
24	22 5	sseldd	$⊢ φ \to X \in ℝ$
25	23 24	resubcld	$⊢ φ \to Y - X \in ℝ$
26	25	adantr	$⊢ (φ \land X < Y) \to Y - X \in ℝ$
27	24 23	posdifd	$⊢ φ \to (X < Y \leftrightarrow 0 < Y - X)$
28	27	biimpa	$⊢ (φ \land X < Y) \to 0 < Y - X$
29		ge0div	$⊢ (F (Y) - F (X) \in ℝ \land Y - X \in ℝ \land 0 < Y - X) \to (0 \leq F (Y) - F (X) \leftrightarrow 0 \leq \frac{F (Y) - F (X)}{Y - X})$
30	20 26 28 29	syl3anc	$⊢ (φ \land X < Y) \to (0 \leq F (Y) - F (X) \leftrightarrow 0 \leq \frac{F (Y) - F (X)}{Y - X})$
31	14 30	mpbird	$⊢ (φ \land X < Y) \to 0 \leq F (Y) - F (X)$
32	31	ex	$⊢ φ \to (X < Y \to 0 \leq F (Y) - F (X))$
33	17 18	subge0d	$⊢ φ \to (0 \leq F (Y) - F (X) \leftrightarrow F (X) \leq F (Y))$
34	32 33	sylibd	$⊢ φ \to (X < Y \to F (X) \leq F (Y))$
35	17	leidd	$⊢ φ \to F (Y) \leq F (Y)$
36		fveq2	$⊢ X = Y \to F (X) = F (Y)$
37	36	breq1d	$⊢ X = Y \to (F (X) \leq F (Y) \leftrightarrow F (Y) \leq F (Y))$
38	35 37	syl5ibrcom	$⊢ φ \to (X = Y \to F (X) \leq F (Y))$
39	24 23	leloed	$⊢ φ \to (X \leq Y \leftrightarrow (X < Y \lor X = Y))$
40	7 39	mpbid	$⊢ φ \to (X < Y \lor X = Y)$
41	34 38 40	mpjaod	$⊢ φ \to F (X) \leq F (Y)$

Metamath Proof Explorer

Theorem dvge0

Proof