Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
dvgt0.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
dvgt0.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
dvge0.d ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ( 0 [,) +∞ ) )
dvge0.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )
dvge0.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 [,] 𝐵 ) )
dvge0.l ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
Assertion dvge0 ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ≤ ( 𝐹 ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 dvgt0.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 dvgt0.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 dvgt0.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
4 dvge0.d ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ( 0 [,) +∞ ) )
5 dvge0.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )
6 dvge0.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 [,] 𝐵 ) )
7 dvge0.l ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
8 1 2 3 4 dvgt0lem1 ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ∈ ( 0 [,) +∞ ) )
9 8 exp31 ⊢ ( 𝜑 → ( ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑋 < 𝑌 → ( ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ∈ ( 0 [,) +∞ ) ) ) )
10 5 6 9 mp2and ⊢ ( 𝜑 → ( 𝑋 < 𝑌 → ( ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ∈ ( 0 [,) +∞ ) ) )
11 10 imp ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ∈ ( 0 [,) +∞ ) )
12 elrege0 ⊢ ( ( ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ∈ ℝ ∧ 0 ≤ ( ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ) )
13 12 simprbi ⊢ ( ( ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ∈ ( 0 [,) +∞ ) → 0 ≤ ( ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) )
14 11 13 syl ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 ≤ ( ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) )
15 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
16 3 15 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
17 16 6 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) ∈ ℝ )
18 16 5 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ℝ )
19 17 18 resubcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ )
21 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
22 1 2 21 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
23 22 6 sseldd ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
24 22 5 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
25 23 24 resubcld ⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) ∈ ℝ )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑌 − 𝑋 ) ∈ ℝ )
27 24 23 posdifd ⊢ ( 𝜑 → ( 𝑋 < 𝑌 ↔ 0 < ( 𝑌 − 𝑋 ) ) )
28 27 biimpa ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 < ( 𝑌 − 𝑋 ) )
29 ge0div ⊢ ( ( ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ ∧ ( 𝑌 − 𝑋 ) ∈ ℝ ∧ 0 < ( 𝑌 − 𝑋 ) ) → ( 0 ≤ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) ↔ 0 ≤ ( ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ) )
30 20 26 28 29 syl3anc ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 0 ≤ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) ↔ 0 ≤ ( ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ) )
31 14 30 mpbird ⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 ≤ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) )
32 31 ex ⊢ ( 𝜑 → ( 𝑋 < 𝑌 → 0 ≤ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) ) )
33 17 18 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) ↔ ( 𝐹 ‘ 𝑋 ) ≤ ( 𝐹 ‘ 𝑌 ) ) )
34 32 33 sylibd ⊢ ( 𝜑 → ( 𝑋 < 𝑌 → ( 𝐹 ‘ 𝑋 ) ≤ ( 𝐹 ‘ 𝑌 ) ) )
35 17 leidd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) ≤ ( 𝐹 ‘ 𝑌 ) )
36 fveq2 ⊢ ( 𝑋 = 𝑌 → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) )
37 36 breq1d ⊢ ( 𝑋 = 𝑌 → ( ( 𝐹 ‘ 𝑋 ) ≤ ( 𝐹 ‘ 𝑌 ) ↔ ( 𝐹 ‘ 𝑌 ) ≤ ( 𝐹 ‘ 𝑌 ) ) )
38 35 37 syl5ibrcom ⊢ ( 𝜑 → ( 𝑋 = 𝑌 → ( 𝐹 ‘ 𝑋 ) ≤ ( 𝐹 ‘ 𝑌 ) ) )
39 24 23 leloed ⊢ ( 𝜑 → ( 𝑋 ≤ 𝑌 ↔ ( 𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ) ) )
40 7 39 mpbid ⊢ ( 𝜑 → ( 𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ) )
41 34 38 40 mpjaod ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ≤ ( 𝐹 ‘ 𝑌 ) )