Metamath Proof Explorer

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

Proof

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