Metamath Proof Explorer

Theorem fdvnegge

Description: Functions with a nonpositive derivative, i.e., decreasing 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→ ℝ ) )
fdvnegge.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
fdvnegge.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ≤ 0 )
Assertion fdvnegge ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ≤ ( 𝐹 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 fdvposlt.d ⊢ 𝐸 = ( 𝐶 (,) 𝐷 )
2 fdvposlt.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐸 )
3 fdvposlt.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐸 )
4 fdvposlt.f ⊢ ( 𝜑 → 𝐹 : 𝐸 ⟶ ℝ )
5 fdvposlt.c ⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( 𝐸 –cn→ ℝ ) )
6 fdvnegge.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
7 fdvnegge.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ≤ 0 )
8 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐸 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
9 8 renegcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐸 ) → - ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
10 9 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐸 ↦ - ( 𝐹 ‘ 𝑦 ) ) : 𝐸 ⟶ ℝ )
11 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
12 11 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
13 ax-resscn ⊢ ℝ ⊆ ℂ
14 13 8 sselid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐸 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
15 fvexd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐸 ) → ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ V )
16 4 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 ‘ 𝑦 ) ) )
17 16 oveq2d ⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( ℝ D ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 ‘ 𝑦 ) ) ) )
18 cncff ⊢ ( ( ℝ D 𝐹 ) ∈ ( 𝐸 –cn→ ℝ ) → ( ℝ D 𝐹 ) : 𝐸 ⟶ ℝ )
19 5 18 syl ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : 𝐸 ⟶ ℝ )
20 19 feqmptd ⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( 𝑦 ∈ 𝐸 ↦ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) )
21 17 20 eqtr3d ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐸 ↦ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) )
22 12 14 15 21 dvmptneg ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ 𝐸 ↦ - ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐸 ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) )
23 19 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐸 ) → ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ℝ )
24 23 renegcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐸 ) → - ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ℝ )
25 24 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐸 ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) : 𝐸 ⟶ ℝ )
26 ssid ⊢ ℂ ⊆ ℂ
27 cncfss ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐸 –cn→ ℝ ) ⊆ ( 𝐸 –cn→ ℂ ) )
28 13 26 27 mp2an ⊢ ( 𝐸 –cn→ ℝ ) ⊆ ( 𝐸 –cn→ ℂ )
29 28 5 sselid ⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( 𝐸 –cn→ ℂ ) )
30 eqid ⊢ ( 𝑦 ∈ 𝐸 ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) = ( 𝑦 ∈ 𝐸 ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑦 ) )
31 30 negfcncf ⊢ ( ( ℝ D 𝐹 ) ∈ ( 𝐸 –cn→ ℂ ) → ( 𝑦 ∈ 𝐸 ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ∈ ( 𝐸 –cn→ ℂ ) )
32 29 31 syl ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐸 ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ∈ ( 𝐸 –cn→ ℂ ) )
33 cncfcdm ⊢ ( ( ℝ ⊆ ℂ ∧ ( 𝑦 ∈ 𝐸 ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ∈ ( 𝐸 –cn→ ℂ ) ) → ( ( 𝑦 ∈ 𝐸 ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ∈ ( 𝐸 –cn→ ℝ ) ↔ ( 𝑦 ∈ 𝐸 ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) : 𝐸 ⟶ ℝ ) )
34 13 32 33 sylancr ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐸 ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ∈ ( 𝐸 –cn→ ℝ ) ↔ ( 𝑦 ∈ 𝐸 ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) : 𝐸 ⟶ ℝ ) )
35 25 34 mpbird ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐸 ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ∈ ( 𝐸 –cn→ ℝ ) )
36 22 35 eqeltrd ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ 𝐸 ↦ - ( 𝐹 ‘ 𝑦 ) ) ) ∈ ( 𝐸 –cn→ ℝ ) )
37 19 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ℝ D 𝐹 ) : 𝐸 ⟶ ℝ )
38 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
39 38 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
40 1 2 3 fct2relem ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ 𝐸 )
41 39 40 sstrd ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐸 )
42 41 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ 𝐸 )
43 37 42 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℝ )
44 43 le0neg1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ≤ 0 ↔ 0 ≤ - ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
45 7 44 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ≤ - ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
46 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ℝ D ( 𝑦 ∈ 𝐸 ↦ - ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐸 ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) )
47 46 fveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D ( 𝑦 ∈ 𝐸 ↦ - ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐸 ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ‘ 𝑥 ) )
48 30 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑦 ∈ 𝐸 ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) = ( 𝑦 ∈ 𝐸 ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) )
49 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑦 = 𝑥 ) → 𝑦 = 𝑥 )
50 49 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑦 = 𝑥 ) → ( ( ℝ D 𝐹 ) ‘ 𝑦 ) = ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
51 50 negeqd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ 𝑦 = 𝑥 ) → - ( ( ℝ D 𝐹 ) ‘ 𝑦 ) = - ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
52 43 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → - ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℝ )
53 48 51 42 52 fvmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑦 ∈ 𝐸 ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ‘ 𝑥 ) = - ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
54 47 53 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D ( 𝑦 ∈ 𝐸 ↦ - ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑥 ) = - ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
55 45 54 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ≤ ( ( ℝ D ( 𝑦 ∈ 𝐸 ↦ - ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑥 ) )
56 1 2 3 10 36 6 55 fdvposle ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐸 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝐴 ) ≤ ( ( 𝑦 ∈ 𝐸 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝐵 ) )
57 eqidd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐸 ↦ - ( 𝐹 ‘ 𝑦 ) ) = ( 𝑦 ∈ 𝐸 ↦ - ( 𝐹 ‘ 𝑦 ) ) )
58 simpr ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → 𝑦 = 𝐴 )
59 58 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) )
60 59 negeqd ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → - ( 𝐹 ‘ 𝑦 ) = - ( 𝐹 ‘ 𝐴 ) )
61 4 2 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
62 61 renegcld ⊢ ( 𝜑 → - ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
63 57 60 2 62 fvmptd ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐸 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝐴 ) = - ( 𝐹 ‘ 𝐴 ) )
64 simpr ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
65 64 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐵 ) )
66 65 negeqd ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → - ( 𝐹 ‘ 𝑦 ) = - ( 𝐹 ‘ 𝐵 ) )
67 4 3 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ℝ )
68 67 renegcld ⊢ ( 𝜑 → - ( 𝐹 ‘ 𝐵 ) ∈ ℝ )
69 57 66 3 68 fvmptd ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐸 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝐵 ) = - ( 𝐹 ‘ 𝐵 ) )
70 56 63 69 3brtr3d ⊢ ( 𝜑 → - ( 𝐹 ‘ 𝐴 ) ≤ - ( 𝐹 ‘ 𝐵 ) )
71 67 61 lenegd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) ≤ ( 𝐹 ‘ 𝐴 ) ↔ - ( 𝐹 ‘ 𝐴 ) ≤ - ( 𝐹 ‘ 𝐵 ) ) )
72 70 71 mpbird ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ≤ ( 𝐹 ‘ 𝐴 ) )