fdvposle

Description: Functions with a nonnegative derivative, i.e. monotonously growing functions, preserve ordering. (Contributed by Thierry Arnoux, 20-Dec-2021)

	Ref	Expression
Hypotheses	fdvposlt.d	$⊢ E = (C, D)$
	fdvposlt.a	$⊢ φ \to A \in E$
	fdvposlt.b	$⊢ φ \to B \in E$
	fdvposlt.f	$⊢ φ \to F : E ⟶ ℝ$
	fdvposlt.c	$⊢ φ \to F_{ℝ}^{'} : E \underset{cn}{⟶} ℝ$
	fdvposle.le	$⊢ φ \to A \leq B$
	fdvposle.1	$⊢ (φ \land x \in (A, B)) \to 0 \leq F_{ℝ}^{'} (x)$
Assertion	fdvposle	$⊢ φ \to F (A) \leq F (B)$

Proof

Step	Hyp	Ref	Expression
1		fdvposlt.d	$⊢ E = (C, D)$
2		fdvposlt.a	$⊢ φ \to A \in E$
3		fdvposlt.b	$⊢ φ \to B \in E$
4		fdvposlt.f	$⊢ φ \to F : E ⟶ ℝ$
5		fdvposlt.c	$⊢ φ \to F_{ℝ}^{'} : E \underset{cn}{⟶} ℝ$
6		fdvposle.le	$⊢ φ \to A \leq B$
7		fdvposle.1	$⊢ (φ \land x \in (A, B)) \to 0 \leq F_{ℝ}^{'} (x)$
8		ioossicc	$⊢ (A, B) \subseteq [A, B]$
9	8	a1i	$⊢ φ \to (A, B) \subseteq [A, B]$
10		ioombl	$⊢ (A, B) \in dom vol$
11	10	a1i	$⊢ φ \to (A, B) \in dom vol$
12		cncff	$⊢ F_{ℝ}^{'} : E \underset{cn}{⟶} ℝ \to F_{ℝ}^{'} : E ⟶ ℝ$
13	5 12	syl	$⊢ φ \to F_{ℝ}^{'} : E ⟶ ℝ$
14	13	adantr	$⊢ (φ \land x \in [A, B]) \to F_{ℝ}^{'} : E ⟶ ℝ$
15	1 2 3	fct2relem	$⊢ φ \to [A, B] \subseteq E$
16	15	sselda	$⊢ (φ \land x \in [A, B]) \to x \in E$
17	14 16	ffvelrnd	$⊢ (φ \land x \in [A, B]) \to F_{ℝ}^{'} (x) \in ℝ$
18		ioossre	$⊢ (C, D) \subseteq ℝ$
19	1 18	eqsstri	$⊢ E \subseteq ℝ$
20	19 2	sselid	$⊢ φ \to A \in ℝ$
21	19 3	sselid	$⊢ φ \to B \in ℝ$
22		ax-resscn	$⊢ ℝ \subseteq ℂ$
23		ssid	$⊢ ℂ \subseteq ℂ$
24		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to [A, B] \underset{cn}{⟶} ℝ \subseteq [A, B] \underset{cn}{⟶} ℂ$
25	22 23 24	mp2an	$⊢ [A, B] \underset{cn}{⟶} ℝ \subseteq [A, B] \underset{cn}{⟶} ℂ$
26	13 15	feqresmpt	$⊢ φ \to {F_{ℝ}^{'} ↾}_{[A, B]} = (x \in [A, B] ⟼ F_{ℝ}^{'} (x))$
27		rescncf	$⊢ [A, B] \subseteq E \to (F_{ℝ}^{'} : E \underset{cn}{⟶} ℝ \to ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ)$
28	15 5 27	sylc	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ$
29	26 28	eqeltrrd	$⊢ φ \to (x \in [A, B] ⟼ F_{ℝ}^{'} (x)) : [A, B] \underset{cn}{⟶} ℝ$
30	25 29	sselid	$⊢ φ \to (x \in [A, B] ⟼ F_{ℝ}^{'} (x)) : [A, B] \underset{cn}{⟶} ℂ$
31		cniccibl	$⊢ (A \in ℝ \land B \in ℝ \land (x \in [A, B] ⟼ F_{ℝ}^{'} (x)) : [A, B] \underset{cn}{⟶} ℂ) \to (x \in [A, B] ⟼ F_{ℝ}^{'} (x)) \in 𝐿^{1}$
32	20 21 30 31	syl3anc	$⊢ φ \to (x \in [A, B] ⟼ F_{ℝ}^{'} (x)) \in 𝐿^{1}$
33	9 11 17 32	iblss	$⊢ φ \to (x \in (A, B) ⟼ F_{ℝ}^{'} (x)) \in 𝐿^{1}$
34	13	adantr	$⊢ (φ \land x \in (A, B)) \to F_{ℝ}^{'} : E ⟶ ℝ$
35	9	sselda	$⊢ (φ \land x \in (A, B)) \to x \in [A, B]$
36	35 16	syldan	$⊢ (φ \land x \in (A, B)) \to x \in E$
37	34 36	ffvelrnd	$⊢ (φ \land x \in (A, B)) \to F_{ℝ}^{'} (x) \in ℝ$
38	33 37 7	itgge0	$⊢ φ \to 0 \leq \int_{(A, B)} F_{ℝ}^{'} (x) d x$
39		fss	$⊢ (F : E ⟶ ℝ \land ℝ \subseteq ℂ) \to F : E ⟶ ℂ$
40	4 22 39	sylancl	$⊢ φ \to F : E ⟶ ℂ$
41		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to E \underset{cn}{⟶} ℝ \subseteq E \underset{cn}{⟶} ℂ$
42	22 23 41	mp2an	$⊢ E \underset{cn}{⟶} ℝ \subseteq E \underset{cn}{⟶} ℂ$
43	42 5	sselid	$⊢ φ \to F_{ℝ}^{'} : E \underset{cn}{⟶} ℂ$
44	1 2 3 6 40 43	ftc2re	$⊢ φ \to \int_{(A, B)} F_{ℝ}^{'} (x) d x = F (B) - F (A)$
45	38 44	breqtrd	$⊢ φ \to 0 \leq F (B) - F (A)$
46	4 3	ffvelrnd	$⊢ φ \to F (B) \in ℝ$
47	4 2	ffvelrnd	$⊢ φ \to F (A) \in ℝ$
48	46 47	subge0d	$⊢ φ \to (0 \leq F (B) - F (A) \leftrightarrow F (A) \leq F (B))$
49	45 48	mpbid	$⊢ φ \to F (A) \leq F (B)$

Metamath Proof Explorer

Theorem fdvposle

Proof