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 E = C D
fdvposlt.a φ A E
fdvposlt.b φ B E
fdvposlt.f φ F : E
fdvposlt.c φ F : E cn
fdvnegge.le φ A B
fdvnegge.1 φ x A B F x 0
Assertion fdvnegge φ F B F A

Proof

Step Hyp Ref Expression
1 fdvposlt.d E = C D
2 fdvposlt.a φ A E
3 fdvposlt.b φ B E
4 fdvposlt.f φ F : E
5 fdvposlt.c φ F : E cn
6 fdvnegge.le φ A B
7 fdvnegge.1 φ x A B F x 0
8 4 ffvelrnda φ y E F y
9 8 renegcld φ y E F y
10 9 fmpttd φ y E F y : E
11 reelprrecn
12 11 a1i φ
13 ax-resscn
14 13 8 sseldi φ y E F y
15 fvexd φ y E F y V
16 4 feqmptd φ F = y E F y
17 16 oveq2d φ D F = dy E F y d y
18 cncff F : E cn F : E
19 5 18 syl φ F : E
20 19 feqmptd φ D F = y E F y
21 17 20 eqtr3d φ dy E F y d y = y E F y
22 12 14 15 21 dvmptneg φ dy E F y d y = y E F y
23 19 ffvelrnda φ y E F y
24 23 renegcld φ y E F y
25 24 fmpttd φ y E F y : E
26 ssid
27 cncfss E cn E cn
28 13 26 27 mp2an E cn E cn
29 28 5 sseldi φ F : E cn
30 eqid y E F y = y E F y
31 30 negfcncf F : E cn y E F y : E cn
32 29 31 syl φ y E F y : E cn
33 cncffvrn y E F y : E cn y E F y : E cn y E F y : E
34 13 32 33 sylancr φ y E F y : E cn y E F y : E
35 25 34 mpbird φ y E F y : E cn
36 22 35 eqeltrd φ dy E F y d y : E cn
37 19 adantr φ x A B F : E
38 ioossicc A B A B
39 38 a1i φ A B A B
40 1 2 3 fct2relem φ A B E
41 39 40 sstrd φ A B E
42 41 sselda φ x A B x E
43 37 42 ffvelrnd φ x A B F x
44 43 le0neg1d φ x A B F x 0 0 F x
45 7 44 mpbid φ x A B 0 F x
46 22 adantr φ x A B dy E F y d y = y E F y
47 46 fveq1d φ x A B dy E F y d y x = y E F y x
48 30 a1i φ x A B y E F y = y E F y
49 simpr φ x A B y = x y = x
50 49 fveq2d φ x A B y = x F y = F x
51 50 negeqd φ x A B y = x F y = F x
52 43 renegcld φ x A B F x
53 48 51 42 52 fvmptd φ x A B y E F y x = F x
54 47 53 eqtrd φ x A B dy E F y d y x = F x
55 45 54 breqtrrd φ x A B 0 dy E F y d y x
56 1 2 3 10 36 6 55 fdvposle φ y E F y A y E F y B
57 eqidd φ y E F y = y E F y
58 simpr φ y = A y = A
59 58 fveq2d φ y = A F y = F A
60 59 negeqd φ y = A F y = F A
61 4 2 ffvelrnd φ F A
62 61 renegcld φ F A
63 57 60 2 62 fvmptd φ y E F y A = F A
64 simpr φ y = B y = B
65 64 fveq2d φ y = B F y = F B
66 65 negeqd φ y = B F y = F B
67 4 3 ffvelrnd φ F B
68 67 renegcld φ F B
69 57 66 3 68 fvmptd φ y E F y B = F B
70 56 63 69 3brtr3d φ F A F B
71 67 61 lenegd φ F B F A F A F B
72 70 71 mpbird φ F B F A