Theorem 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	⊢ 𝐸 = ( 𝐶 (,) 𝐷 )
	fdvposlt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐸 )
	fdvposlt.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐸 )
	fdvposlt.f	⊢ ( 𝜑 → 𝐹 : 𝐸 ⟶ ℝ )
	fdvposlt.c	⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( 𝐸 –cn→ ℝ ) )
	fdvposlt.lt	⊢ ( 𝜑 → 𝐴 < 𝐵 )
	fdvposlt.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 < ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
Assertion	fdvposlt	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fdvposlt.d	⊢ 𝐸 = ( 𝐶 (,) 𝐷 )
2		fdvposlt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐸 )
3		fdvposlt.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐸 )
4		fdvposlt.f	⊢ ( 𝜑 → 𝐹 : 𝐸 ⟶ ℝ )
5		fdvposlt.c	⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( 𝐸 –cn→ ℝ ) )
6		fdvposlt.lt	⊢ ( 𝜑 → 𝐴 < 𝐵 )
7		fdvposlt.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 < ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
8		ioossre	⊢ ( 𝐶 (,) 𝐷 ) ⊆ ℝ
9	1 8	eqsstri	⊢ 𝐸 ⊆ ℝ
10	9 2	sselid	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
11	9 3	sselid	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
12	10 11	posdifd	⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
13	6 12	mpbid	⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
14	10 11 6	ltled	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
15		volioo	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
16	10 11 14 15	syl3anc	⊢ ( 𝜑 → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
17	13 16	breqtrrd	⊢ ( 𝜑 → 0 < ( vol ‘ ( 𝐴 (,) 𝐵 ) ) )
18		ioossicc	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
19	18	a1i	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
20		ioombl	⊢ ( 𝐴 (,) 𝐵 ) ∈ dom vol
21	20	a1i	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ dom vol )
22		cncff	⊢ ( ( ℝ D 𝐹 ) ∈ ( 𝐸 –cn→ ℝ ) → ( ℝ D 𝐹 ) : 𝐸 ⟶ ℝ )
23	5 22	syl	⊢ ( 𝜑 → ( ℝ D 𝐹 ) : 𝐸 ⟶ ℝ )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ℝ D 𝐹 ) : 𝐸 ⟶ ℝ )
25	1 2 3	fct2relem	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ 𝐸 )
26	25	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ 𝐸 )
27	24 26	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℝ )
28		ax-resscn	⊢ ℝ ⊆ ℂ
29		ssid	⊢ ℂ ⊆ ℂ
30		cncfss	⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ⊆ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
31	28 29 30	mp2an	⊢ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ⊆ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ )
32	23 25	feqresmpt	⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
33		rescncf	⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐸 → ( ( ℝ D 𝐹 ) ∈ ( 𝐸 –cn→ ℝ ) → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ) )
34	25 5 33	sylc	⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
35	32 34	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
36	31 35	sselid	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
37		cniccibl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ∈ 𝐿1 )
38	10 11 36 37	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ∈ 𝐿1 )
39	19 21 27 38	iblss	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ∈ 𝐿1 )
40	23	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ℝ D 𝐹 ) : 𝐸 ⟶ ℝ )
41	19	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
42	41 26	syldan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ 𝐸 )
43	40 42	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℝ )
44		elrp	⊢ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℝ+ ↔ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℝ ∧ 0 < ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
45	43 7 44	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℝ+ )
46	17 39 45	itggt0	⊢ ( 𝜑 → 0 < ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) d 𝑥 )
47		fss	⊢ ( ( 𝐹 : 𝐸 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : 𝐸 ⟶ ℂ )
48	4 28 47	sylancl	⊢ ( 𝜑 → 𝐹 : 𝐸 ⟶ ℂ )
49		cncfss	⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐸 –cn→ ℝ ) ⊆ ( 𝐸 –cn→ ℂ ) )
50	28 29 49	mp2an	⊢ ( 𝐸 –cn→ ℝ ) ⊆ ( 𝐸 –cn→ ℂ )
51	50 5	sselid	⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( 𝐸 –cn→ ℂ ) )
52	1 2 3 14 48 51	ftc2re	⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) d 𝑥 = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )
53	46 52	breqtrd	⊢ ( 𝜑 → 0 < ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )
54	4 2	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
55	4 3	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ℝ )
56	54 55	posdifd	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐵 ) ↔ 0 < ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ) )
57	53 56	mpbird	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐵 ) )