Theorem 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	$$⊢\phi \to A\in ℝ$$
	dvgt0.b	$$⊢\phi \to B\in ℝ$$
	dvgt0.f	$$⊢\phi \to F:\left[A,B\right]\underset{cn}{⟶}ℝ$$
	dvge0.d	$$⊢\phi \to F_{ℝ}^{\prime }:\left(A,B\right)⟶\left[0,\mathrm{+\infty }\right)$$
	dvge0.x	$$⊢\phi \to X\in \left[A,B\right]$$
	dvge0.y	$$⊢\phi \to Y\in \left[A,B\right]$$
	dvge0.l	$$⊢\phi \to X\le Y$$
Assertion	dvge0	$$⊢\phi \to F\left(X\right)\le F\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvgt0.a	$$⊢\phi \to A\in ℝ$$
2		dvgt0.b	$$⊢\phi \to B\in ℝ$$
3		dvgt0.f	$$⊢\phi \to F:\left[A,B\right]\underset{cn}{⟶}ℝ$$
4		dvge0.d	$$⊢\phi \to F_{ℝ}^{\prime }:\left(A,B\right)⟶\left[0,\mathrm{+\infty }\right)$$
5		dvge0.x	$$⊢\phi \to X\in \left[A,B\right]$$
6		dvge0.y	$$⊢\phi \to Y\in \left[A,B\right]$$
7		dvge0.l	$$⊢\phi \to X\le Y$$
8	1 2 3 4	dvgt0lem1	$$⊢\left(\left(\phi \wedge \left(X\in \left[A,B\right]\wedge Y\in \left[A,B\right]\right)\right)\wedge X<Y\right)\to \frac{F\left(Y\right)-F\left(X\right)}{Y-X}\in \left[0,\mathrm{+\infty }\right)$$
9	8	exp31	$$⊢\phi \to \left(\left(X\in \left[A,B\right]\wedge Y\in \left[A,B\right]\right)\to \left(X<Y\to \frac{F\left(Y\right)-F\left(X\right)}{Y-X}\in \left[0,\mathrm{+\infty }\right)\right)\right)$$
10	5 6 9	mp2and	$$⊢\phi \to \left(X<Y\to \frac{F\left(Y\right)-F\left(X\right)}{Y-X}\in \left[0,\mathrm{+\infty }\right)\right)$$
11	10	imp	$$⊢\left(\phi \wedge X<Y\right)\to \frac{F\left(Y\right)-F\left(X\right)}{Y-X}\in \left[0,\mathrm{+\infty }\right)$$
12		elrege0	$$⊢\frac{F\left(Y\right)-F\left(X\right)}{Y-X}\in \left[0,\mathrm{+\infty }\right)\leftrightarrow \left(\frac{F\left(Y\right)-F\left(X\right)}{Y-X}\in ℝ\wedge 0\le \frac{F\left(Y\right)-F\left(X\right)}{Y-X}\right)$$
13	12	simprbi	$$⊢\frac{F\left(Y\right)-F\left(X\right)}{Y-X}\in \left[0,\mathrm{+\infty }\right)\to 0\le \frac{F\left(Y\right)-F\left(X\right)}{Y-X}$$
14	11 13	syl	$$⊢\left(\phi \wedge X<Y\right)\to 0\le \frac{F\left(Y\right)-F\left(X\right)}{Y-X}$$
15		cncff	$$⊢F:\left[A,B\right]\underset{cn}{⟶}ℝ\to F:\left[A,B\right]⟶ℝ$$
16	3 15	syl	$$⊢\phi \to F:\left[A,B\right]⟶ℝ$$
17	16 6	ffvelcdmd	$$⊢\phi \to F\left(Y\right)\in ℝ$$
18	16 5	ffvelcdmd	$$⊢\phi \to F\left(X\right)\in ℝ$$
19	17 18	resubcld	$$⊢\phi \to F\left(Y\right)-F\left(X\right)\in ℝ$$
20	19	adantr	$$⊢\left(\phi \wedge X<Y\right)\to F\left(Y\right)-F\left(X\right)\in ℝ$$
21		iccssre	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left[A,B\right]\subseteq ℝ$$
22	1 2 21	syl2anc	$$⊢\phi \to \left[A,B\right]\subseteq ℝ$$
23	22 6	sseldd	$$⊢\phi \to Y\in ℝ$$
24	22 5	sseldd	$$⊢\phi \to X\in ℝ$$
25	23 24	resubcld	$$⊢\phi \to Y-X\in ℝ$$
26	25	adantr	$$⊢\left(\phi \wedge X<Y\right)\to Y-X\in ℝ$$
27	24 23	posdifd	$$⊢\phi \to \left(X<Y\leftrightarrow 0<Y-X\right)$$
28	27	biimpa	$$⊢\left(\phi \wedge X<Y\right)\to 0<Y-X$$
29		ge0div	$$⊢\left(F\left(Y\right)-F\left(X\right)\in ℝ\wedge Y-X\in ℝ\wedge 0<Y-X\right)\to \left(0\le F\left(Y\right)-F\left(X\right)\leftrightarrow 0\le \frac{F\left(Y\right)-F\left(X\right)}{Y-X}\right)$$
30	20 26 28 29	syl3anc	$$⊢\left(\phi \wedge X<Y\right)\to \left(0\le F\left(Y\right)-F\left(X\right)\leftrightarrow 0\le \frac{F\left(Y\right)-F\left(X\right)}{Y-X}\right)$$
31	14 30	mpbird	$$⊢\left(\phi \wedge X<Y\right)\to 0\le F\left(Y\right)-F\left(X\right)$$
32	31	ex	$$⊢\phi \to \left(X<Y\to 0\le F\left(Y\right)-F\left(X\right)\right)$$
33	17 18	subge0d	$$⊢\phi \to \left(0\le F\left(Y\right)-F\left(X\right)\leftrightarrow F\left(X\right)\le F\left(Y\right)\right)$$
34	32 33	sylibd	$$⊢\phi \to \left(X<Y\to F\left(X\right)\le F\left(Y\right)\right)$$
35	17	leidd	$$⊢\phi \to F\left(Y\right)\le F\left(Y\right)$$
36		fveq2	$$⊢X=Y\to F\left(X\right)=F\left(Y\right)$$
37	36	breq1d	$$⊢X=Y\to \left(F\left(X\right)\le F\left(Y\right)\leftrightarrow F\left(Y\right)\le F\left(Y\right)\right)$$
38	35 37	syl5ibrcom	$$⊢\phi \to \left(X=Y\to F\left(X\right)\le F\left(Y\right)\right)$$
39	24 23	leloed	$$⊢\phi \to \left(X\le Y\leftrightarrow \left(X<Y\vee X=Y\right)\right)$$
40	7 39	mpbid	$$⊢\phi \to \left(X<Y\vee X=Y\right)$$
41	34 38 40	mpjaod	$$⊢\phi \to F\left(X\right)\le F\left(Y\right)$$