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	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
15		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
16	12 15	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
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	addlidd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 < 𝑦 ) → ( 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 𝐹 ) )