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	$⊢ φ \to A \in E$
	fdvposlt.b	$⊢ φ \to B \in E$
	fdvposlt.f	$⊢ φ \to F : E ⟶ ℝ$
	fdvposlt.c	$⊢ φ \to F_{ℝ}^{'} : E \underset{cn}{⟶} ℝ$
	fdvnegge.le	$⊢ φ \to A \leq B$
	fdvnegge.1	$⊢ (φ \land x \in (A, B)) \to F_{ℝ}^{'} (x) \leq 0$
Assertion	fdvnegge	$⊢ φ \to F (B) \leq F (A)$

Proof

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

Metamath Proof Explorer

Theorem fdvnegge

Proof