Metamath Proof Explorer

Theorem dvlt0

Description: A function on a closed interval with negative derivative is decreasing. (Contributed by Mario Carneiro, 19-Feb-2015)

Ref Expression
Hypotheses dvgt0.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
dvgt0.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
dvgt0.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
dvlt0.d ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ( -∞ (,) 0 ) )
Assertion dvlt0 ( 𝜑 → 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) )

Proof

Step Hyp Ref Expression
1 dvgt0.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 dvgt0.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 dvgt0.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
4 dvlt0.d ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ( -∞ (,) 0 ) )
5 gtso ⊢ ◡ < Or ℝ
6 1 2 3 4 dvgt0lem1 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ∈ ( -∞ (,) 0 ) )
7 eliooord ⊢ ( ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ∈ ( -∞ (,) 0 ) → ( -∞ < ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ∧ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) < 0 ) )
8 6 7 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( -∞ < ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) ∧ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) < 0 ) )
9 8 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) < 0 )
10 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
11 3 10 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
12 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
13 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
14 12 13 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
15 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
16 12 15 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
17 14 16 resubcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
18 0red ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 0 ∈ ℝ )
19 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
20 1 2 19 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
21 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
22 21 13 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ℝ )
23 21 15 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ℝ )
24 22 23 resubcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝑦 − 𝑥 ) ∈ ℝ )
25 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 < 𝑦 )
26 23 22 posdifd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝑥 < 𝑦 ↔ 0 < ( 𝑦 − 𝑥 ) ) )
27 25 26 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 0 < ( 𝑦 − 𝑥 ) )
28 ltdivmul ⊢ ( ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ∈ ℝ ∧ ( ( 𝑦 − 𝑥 ) ∈ ℝ ∧ 0 < ( 𝑦 − 𝑥 ) ) ) → ( ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) < 0 ↔ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) < ( ( 𝑦 − 𝑥 ) · 0 ) ) )
29 17 18 24 27 28 syl112anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑦 − 𝑥 ) ) < 0 ↔ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) < ( ( 𝑦 − 𝑥 ) · 0 ) ) )
30 9 29 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) < ( ( 𝑦 − 𝑥 ) · 0 ) )
31 24 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝑦 − 𝑥 ) ∈ ℂ )
32 31 mul01d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝑦 − 𝑥 ) · 0 ) = 0 )
33 30 32 breqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) < 0 )
34 14 16 18 ltsubaddd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) < 0 ↔ ( 𝐹 ‘ 𝑦 ) < ( 0 + ( 𝐹 ‘ 𝑥 ) ) ) )
35 33 34 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐹 ‘ 𝑦 ) < ( 0 + ( 𝐹 ‘ 𝑥 ) ) )
36 16 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
37 36 addid2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 0 + ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
38 35 37 breqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐹 ‘ 𝑦 ) < ( 𝐹 ‘ 𝑥 ) )
39 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
40 fvex ⊢ ( 𝐹 ‘ 𝑦 ) ∈ V
41 39 40 brcnv ⊢ ( ( 𝐹 ‘ 𝑥 ) ◡ < ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑦 ) < ( 𝐹 ‘ 𝑥 ) )
42 38 41 sylibr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ◡ < ( 𝐹 ‘ 𝑦 ) )
43 1 2 3 4 5 42 dvgt0lem2 ⊢ ( 𝜑 → 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) )