fdvposlt

Description: Functions with a positive derivative, i.e. monotonously growing functions, preserve strict 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}{⟶} ℝ$
	fdvposlt.lt	$⊢ φ \to A < B$
	fdvposlt.1	$⊢ (φ \land x \in (A, B)) \to 0 < F_{ℝ}^{'} (x)$
Assertion	fdvposlt	$⊢ φ \to F (A) < 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		fdvposlt.lt	$⊢ φ \to A < B$
7		fdvposlt.1	$⊢ (φ \land x \in (A, B)) \to 0 < F_{ℝ}^{'} (x)$
8		ioossre	$⊢ (C, D) \subseteq ℝ$
9	1 8	eqsstri	$⊢ E \subseteq ℝ$
10	9 2	sseldi	$⊢ φ \to A \in ℝ$
11	9 3	sseldi	$⊢ φ \to B \in ℝ$
12	10 11	posdifd	$⊢ φ \to (A < B \leftrightarrow 0 < B - A)$
13	6 12	mpbid	$⊢ φ \to 0 < B - A$
14	10 11 6	ltled	$⊢ φ \to A \leq B$
15		volioo	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ((A, B)) = B - A$
16	10 11 14 15	syl3anc	$⊢ φ \to vol ((A, B)) = B - A$
17	13 16	breqtrrd	$⊢ φ \to 0 < vol ((A, B))$
18		ioossicc	$⊢ (A, B) \subseteq [A, B]$
19	18	a1i	$⊢ φ \to (A, B) \subseteq [A, B]$
20		ioombl	$⊢ (A, B) \in dom vol$
21	20	a1i	$⊢ φ \to (A, B) \in dom vol$
22		cncff	$⊢ F_{ℝ}^{'} : E \underset{cn}{⟶} ℝ \to F_{ℝ}^{'} : E ⟶ ℝ$
23	5 22	syl	$⊢ φ \to F_{ℝ}^{'} : E ⟶ ℝ$
24	23	adantr	$⊢ (φ \land x \in [A, B]) \to F_{ℝ}^{'} : E ⟶ ℝ$
25	1 2 3	fct2relem	$⊢ φ \to [A, B] \subseteq E$
26	25	sselda	$⊢ (φ \land x \in [A, B]) \to x \in E$
27	24 26	ffvelrnd	$⊢ (φ \land x \in [A, B]) \to F_{ℝ}^{'} (x) \in ℝ$
28		ax-resscn	$⊢ ℝ \subseteq ℂ$
29		ssid	$⊢ ℂ \subseteq ℂ$
30		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to [A, B] \underset{cn}{⟶} ℝ \subseteq [A, B] \underset{cn}{⟶} ℂ$
31	28 29 30	mp2an	$⊢ [A, B] \underset{cn}{⟶} ℝ \subseteq [A, B] \underset{cn}{⟶} ℂ$
32	23 25	feqresmpt	$⊢ φ \to {F_{ℝ}^{'} ↾}_{[A, B]} = (x \in [A, B] ⟼ F_{ℝ}^{'} (x))$
33		rescncf	$⊢ [A, B] \subseteq E \to (F_{ℝ}^{'} : E \underset{cn}{⟶} ℝ \to ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ)$
34	25 5 33	sylc	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ$
35	32 34	eqeltrrd	$⊢ φ \to (x \in [A, B] ⟼ F_{ℝ}^{'} (x)) : [A, B] \underset{cn}{⟶} ℝ$
36	31 35	sseldi	$⊢ φ \to (x \in [A, B] ⟼ F_{ℝ}^{'} (x)) : [A, B] \underset{cn}{⟶} ℂ$
37		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}$
38	10 11 36 37	syl3anc	$⊢ φ \to (x \in [A, B] ⟼ F_{ℝ}^{'} (x)) \in 𝐿^{1}$
39	19 21 27 38	iblss	$⊢ φ \to (x \in (A, B) ⟼ F_{ℝ}^{'} (x)) \in 𝐿^{1}$
40	23	adantr	$⊢ (φ \land x \in (A, B)) \to F_{ℝ}^{'} : E ⟶ ℝ$
41	19	sselda	$⊢ (φ \land x \in (A, B)) \to x \in [A, B]$
42	41 26	syldan	$⊢ (φ \land x \in (A, B)) \to x \in E$
43	40 42	ffvelrnd	$⊢ (φ \land x \in (A, B)) \to F_{ℝ}^{'} (x) \in ℝ$
44		elrp	$⊢ F_{ℝ}^{'} (x) \in ℝ^{+} \leftrightarrow (F_{ℝ}^{'} (x) \in ℝ \land 0 < F_{ℝ}^{'} (x))$
45	43 7 44	sylanbrc	$⊢ (φ \land x \in (A, B)) \to F_{ℝ}^{'} (x) \in ℝ^{+}$
46	17 39 45	itggt0	$⊢ φ \to 0 < \int_{(A, B)} F_{ℝ}^{'} (x) d x$
47		fss	$⊢ (F : E ⟶ ℝ \land ℝ \subseteq ℂ) \to F : E ⟶ ℂ$
48	4 28 47	sylancl	$⊢ φ \to F : E ⟶ ℂ$
49		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to E \underset{cn}{⟶} ℝ \subseteq E \underset{cn}{⟶} ℂ$
50	28 29 49	mp2an	$⊢ E \underset{cn}{⟶} ℝ \subseteq E \underset{cn}{⟶} ℂ$
51	50 5	sseldi	$⊢ φ \to F_{ℝ}^{'} : E \underset{cn}{⟶} ℂ$
52	1 2 3 14 48 51	ftc2re	$⊢ φ \to \int_{(A, B)} F_{ℝ}^{'} (x) d x = F (B) - F (A)$
53	46 52	breqtrd	$⊢ φ \to 0 < F (B) - F (A)$
54	4 2	ffvelrnd	$⊢ φ \to F (A) \in ℝ$
55	4 3	ffvelrnd	$⊢ φ \to F (B) \in ℝ$
56	54 55	posdifd	$⊢ φ \to (F (A) < F (B) \leftrightarrow 0 < F (B) - F (A))$
57	53 56	mpbird	$⊢ φ \to F (A) < F (B)$

Metamath Proof Explorer

Theorem fdvposlt

Proof