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	ffvelcdmda	\|- ( ( 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	ffvelcdmda	\|- ( ( 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		cncfcdm	\|- ( ( 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	ffvelcdmd	\|- ( ( 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	ffvelcdmd	\|- ( 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	ffvelcdmd	\|- ( 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 ) )

Metamath Proof Explorer

Theorem fdvneggt

Proof