Metamath Proof Explorer

Theorem fdvneggt

Description: Functions with a negative derivative, i.e. monotonously decreasing functions, inverse strict ordering. (Contributed by Thierry Arnoux, 20-Dec-2021)

Ref Expression
Hypotheses fdvposlt.d 
|- E = ( C (,) D )
fdvposlt.a 
|- ( ph -> A e. E )
fdvposlt.b 
|- ( ph -> B e. E )
fdvposlt.f 
|- ( ph -> F : E --> RR )
fdvposlt.c 
|- ( ph -> ( RR _D F ) e. ( E -cn-> RR ) )
fdvneggt.lt 
|- ( ph -> A < B )
fdvneggt.1 
|- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) < 0 )
Assertion fdvneggt 
|- ( ph -> ( F ` B ) < ( F ` A ) )

Proof

Step Hyp Ref Expression
1 fdvposlt.d 
 |-  E = ( C (,) D )
2 fdvposlt.a 
 |-  ( ph -> A e. E )
3 fdvposlt.b 
 |-  ( ph -> B e. E )
4 fdvposlt.f 
 |-  ( ph -> F : E --> RR )
5 fdvposlt.c 
 |-  ( ph -> ( RR _D F ) e. ( E -cn-> RR ) )
6 fdvneggt.lt 
 |-  ( ph -> A < B )
7 fdvneggt.1 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) < 0 )
8 4 ffvelrnda 
 |-  ( ( ph /\ y e. E ) -> ( F ` y ) e. RR )
9 8 renegcld 
 |-  ( ( ph /\ y e. E ) -> -u ( F ` y ) e. RR )
10 9 fmpttd 
 |-  ( ph -> ( y e. E |-> -u ( F ` y ) ) : E --> RR )
11 reelprrecn 
 |-  RR e. { RR , CC }
12 11 a1i 
 |-  ( ph -> RR e. { RR , CC } )
13 ax-resscn 
 |-  RR C_ CC
14 13 8 sselid 
 |-  ( ( ph /\ y e. E ) -> ( F ` y ) e. CC )
15 fvexd 
 |-  ( ( ph /\ y e. E ) -> ( ( RR _D F ) ` y ) e. _V )
16 4 feqmptd 
 |-  ( ph -> F = ( y e. E |-> ( F ` y ) ) )
17 16 oveq2d 
 |-  ( ph -> ( RR _D F ) = ( RR _D ( y e. E |-> ( F ` y ) ) ) )
18 cncff 
 |-  ( ( RR _D F ) e. ( E -cn-> RR ) -> ( RR _D F ) : E --> RR )
19 5 18 syl 
 |-  ( ph -> ( RR _D F ) : E --> RR )
20 19 feqmptd 
 |-  ( ph -> ( RR _D F ) = ( y e. E |-> ( ( RR _D F ) ` y ) ) )
21 17 20 eqtr3d 
 |-  ( ph -> ( RR _D ( y e. E |-> ( F ` y ) ) ) = ( y e. E |-> ( ( RR _D F ) ` y ) ) )
22 12 14 15 21 dvmptneg 
 |-  ( ph -> ( RR _D ( y e. E |-> -u ( F ` y ) ) ) = ( y e. E |-> -u ( ( RR _D F ) ` y ) ) )
23 19 ffvelrnda 
 |-  ( ( ph /\ y e. E ) -> ( ( RR _D F ) ` y ) e. RR )
24 23 renegcld 
 |-  ( ( ph /\ y e. E ) -> -u ( ( RR _D F ) ` y ) e. RR )
25 24 fmpttd 
 |-  ( ph -> ( y e. E |-> -u ( ( RR _D F ) ` y ) ) : E --> RR )
26 ssid 
 |-  CC C_ CC
27 cncfss 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( E -cn-> RR ) C_ ( E -cn-> CC ) )
28 13 26 27 mp2an 
 |-  ( E -cn-> RR ) C_ ( E -cn-> CC )
29 28 5 sselid 
 |-  ( ph -> ( RR _D F ) e. ( E -cn-> CC ) )
30 eqid 
 |-  ( y e. E |-> -u ( ( RR _D F ) ` y ) ) = ( y e. E |-> -u ( ( RR _D F ) ` y ) )
31 30 negfcncf 
 |-  ( ( RR _D F ) e. ( E -cn-> CC ) -> ( y e. E |-> -u ( ( RR _D F ) ` y ) ) e. ( E -cn-> CC ) )
32 29 31 syl 
 |-  ( ph -> ( y e. E |-> -u ( ( RR _D F ) ` y ) ) e. ( E -cn-> CC ) )
33 cncffvrn 
 |-  ( ( RR C_ CC /\ ( y e. E |-> -u ( ( RR _D F ) ` y ) ) e. ( E -cn-> CC ) ) -> ( ( y e. E |-> -u ( ( RR _D F ) ` y ) ) e. ( E -cn-> RR ) <-> ( y e. E |-> -u ( ( RR _D F ) ` y ) ) : E --> RR ) )
34 13 32 33 sylancr 
 |-  ( ph -> ( ( y e. E |-> -u ( ( RR _D F ) ` y ) ) e. ( E -cn-> RR ) <-> ( y e. E |-> -u ( ( RR _D F ) ` y ) ) : E --> RR ) )
35 25 34 mpbird 
 |-  ( ph -> ( y e. E |-> -u ( ( RR _D F ) ` y ) ) e. ( E -cn-> RR ) )
36 22 35 eqeltrd 
 |-  ( ph -> ( RR _D ( y e. E |-> -u ( F ` y ) ) ) e. ( E -cn-> RR ) )
37 19 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( RR _D F ) : E --> RR )
38 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
39 38 a1i 
 |-  ( ph -> ( A (,) B ) C_ ( A [,] B ) )
40 1 2 3 fct2relem 
 |-  ( ph -> ( A [,] B ) C_ E )
41 39 40 sstrd 
 |-  ( ph -> ( A (,) B ) C_ E )
42 41 sselda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. E )
43 37 42 ffvelrnd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. RR )
44 43 lt0neg1d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( RR _D F ) ` x ) < 0 <-> 0 < -u ( ( RR _D F ) ` x ) ) )
45 7 44 mpbid 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 0 < -u ( ( RR _D F ) ` x ) )
46 22 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( RR _D ( y e. E |-> -u ( F ` y ) ) ) = ( y e. E |-> -u ( ( RR _D F ) ` y ) ) )
47 46 fveq1d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D ( y e. E |-> -u ( F ` y ) ) ) ` x ) = ( ( y e. E |-> -u ( ( RR _D F ) ` y ) ) ` x ) )
48 30 a1i 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( y e. E |-> -u ( ( RR _D F ) ` y ) ) = ( y e. E |-> -u ( ( RR _D F ) ` y ) ) )
49 simpr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ y = x ) -> y = x )
50 49 fveq2d 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ y = x ) -> ( ( RR _D F ) ` y ) = ( ( RR _D F ) ` x ) )
51 50 negeqd 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ y = x ) -> -u ( ( RR _D F ) ` y ) = -u ( ( RR _D F ) ` x ) )
52 43 renegcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> -u ( ( RR _D F ) ` x ) e. RR )
53 48 51 42 52 fvmptd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( y e. E |-> -u ( ( RR _D F ) ` y ) ) ` x ) = -u ( ( RR _D F ) ` x ) )
54 47 53 eqtrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D ( y e. E |-> -u ( F ` y ) ) ) ` x ) = -u ( ( RR _D F ) ` x ) )
55 45 54 breqtrrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> 0 < ( ( RR _D ( y e. E |-> -u ( F ` y ) ) ) ` x ) )
56 1 2 3 10 36 6 55 fdvposlt 
 |-  ( ph -> ( ( y e. E |-> -u ( F ` y ) ) ` A ) < ( ( y e. E |-> -u ( F ` y ) ) ` B ) )
57 eqidd 
 |-  ( ph -> ( y e. E |-> -u ( F ` y ) ) = ( y e. E |-> -u ( F ` y ) ) )
58 simpr 
 |-  ( ( ph /\ y = A ) -> y = A )
59 58 fveq2d 
 |-  ( ( ph /\ y = A ) -> ( F ` y ) = ( F ` A ) )
60 59 negeqd 
 |-  ( ( ph /\ y = A ) -> -u ( F ` y ) = -u ( F ` A ) )
61 4 2 ffvelrnd 
 |-  ( ph -> ( F ` A ) e. RR )
62 61 renegcld 
 |-  ( ph -> -u ( F ` A ) e. RR )
63 57 60 2 62 fvmptd 
 |-  ( ph -> ( ( y e. E |-> -u ( F ` y ) ) ` A ) = -u ( F ` A ) )
64 simpr 
 |-  ( ( ph /\ y = B ) -> y = B )
65 64 fveq2d 
 |-  ( ( ph /\ y = B ) -> ( F ` y ) = ( F ` B ) )
66 65 negeqd 
 |-  ( ( ph /\ y = B ) -> -u ( F ` y ) = -u ( F ` B ) )
67 4 3 ffvelrnd 
 |-  ( ph -> ( F ` B ) e. RR )
68 67 renegcld 
 |-  ( ph -> -u ( F ` B ) e. RR )
69 57 66 3 68 fvmptd 
 |-  ( ph -> ( ( y e. E |-> -u ( F ` y ) ) ` B ) = -u ( F ` B ) )
70 56 63 69 3brtr3d 
 |-  ( ph -> -u ( F ` A ) < -u ( F ` B ) )
71 67 61 ltnegd 
 |-  ( ph -> ( ( F ` B ) < ( F ` A ) <-> -u ( F ` A ) < -u ( F ` B ) ) )
72 70 71 mpbird 
 |-  ( ph -> ( F ` B ) < ( F ` A ) )