dvle

Description: If A ( x ) , C ( x ) are differentiable functions and A<_ C` , then for x <_ y , A ( y ) - A ( x ) <_ C ( y ) - C ( x ) ` . (Contributed by Mario Carneiro, 16-May-2016)

	Ref	Expression
Hypotheses	dvle.m	$⊢ φ \to M \in ℝ$
	dvle.n	$⊢ φ \to N \in ℝ$
	dvle.a	$⊢ φ \to (x \in [M, N] ⟼ A) : [M, N] \underset{cn}{⟶} ℝ$
	dvle.b	$⊢ φ \to \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = (x \in (M, N) ⟼ B)$
	dvle.c	$⊢ φ \to (x \in [M, N] ⟼ C) : [M, N] \underset{cn}{⟶} ℝ$
	dvle.d	$⊢ φ \to \frac{d (x \in (M, N)⟼ C)}{d_{ℝ} x} = (x \in (M, N) ⟼ D)$
	dvle.f	$⊢ (φ \land x \in (M, N)) \to B \leq D$
	dvle.x	$⊢ φ \to X \in [M, N]$
	dvle.y	$⊢ φ \to Y \in [M, N]$
	dvle.l	$⊢ φ \to X \leq Y$
	dvle.p	$⊢ x = X \to A = P$
	dvle.q	$⊢ x = X \to C = Q$
	dvle.r	$⊢ x = Y \to A = R$
	dvle.s	$⊢ x = Y \to C = S$
Assertion	dvle	$⊢ φ \to R - P \leq S - Q$

Proof

Step	Hyp	Ref	Expression
1		dvle.m	$⊢ φ \to M \in ℝ$
2		dvle.n	$⊢ φ \to N \in ℝ$
3		dvle.a	$⊢ φ \to (x \in [M, N] ⟼ A) : [M, N] \underset{cn}{⟶} ℝ$
4		dvle.b	$⊢ φ \to \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = (x \in (M, N) ⟼ B)$
5		dvle.c	$⊢ φ \to (x \in [M, N] ⟼ C) : [M, N] \underset{cn}{⟶} ℝ$
6		dvle.d	$⊢ φ \to \frac{d (x \in (M, N)⟼ C)}{d_{ℝ} x} = (x \in (M, N) ⟼ D)$
7		dvle.f	$⊢ (φ \land x \in (M, N)) \to B \leq D$
8		dvle.x	$⊢ φ \to X \in [M, N]$
9		dvle.y	$⊢ φ \to Y \in [M, N]$
10		dvle.l	$⊢ φ \to X \leq Y$
11		dvle.p	$⊢ x = X \to A = P$
12		dvle.q	$⊢ x = X \to C = Q$
13		dvle.r	$⊢ x = Y \to A = R$
14		dvle.s	$⊢ x = Y \to C = S$
15	13	eleq1d	$⊢ x = Y \to (A \in ℝ \leftrightarrow R \in ℝ)$
16		cncff	$⊢ (x \in [M, N] ⟼ A) : [M, N] \underset{cn}{⟶} ℝ \to (x \in [M, N] ⟼ A) : [M, N] ⟶ ℝ$
17	3 16	syl	$⊢ φ \to (x \in [M, N] ⟼ A) : [M, N] ⟶ ℝ$
18		eqid	$⊢ (x \in [M, N] ⟼ A) = (x \in [M, N] ⟼ A)$
19	18	fmpt	$⊢ \forall x \in [M, N] A \in ℝ \leftrightarrow (x \in [M, N] ⟼ A) : [M, N] ⟶ ℝ$
20	17 19	sylibr	$⊢ φ \to \forall x \in [M, N] A \in ℝ$
21	15 20 9	rspcdva	$⊢ φ \to R \in ℝ$
22	14	eleq1d	$⊢ x = Y \to (C \in ℝ \leftrightarrow S \in ℝ)$
23		cncff	$⊢ (x \in [M, N] ⟼ C) : [M, N] \underset{cn}{⟶} ℝ \to (x \in [M, N] ⟼ C) : [M, N] ⟶ ℝ$
24	5 23	syl	$⊢ φ \to (x \in [M, N] ⟼ C) : [M, N] ⟶ ℝ$
25		eqid	$⊢ (x \in [M, N] ⟼ C) = (x \in [M, N] ⟼ C)$
26	25	fmpt	$⊢ \forall x \in [M, N] C \in ℝ \leftrightarrow (x \in [M, N] ⟼ C) : [M, N] ⟶ ℝ$
27	24 26	sylibr	$⊢ φ \to \forall x \in [M, N] C \in ℝ$
28	22 27 9	rspcdva	$⊢ φ \to S \in ℝ$
29	12	eleq1d	$⊢ x = X \to (C \in ℝ \leftrightarrow Q \in ℝ)$
30	29 27 8	rspcdva	$⊢ φ \to Q \in ℝ$
31	28 30	resubcld	$⊢ φ \to S - Q \in ℝ$
32	11	eleq1d	$⊢ x = X \to (A \in ℝ \leftrightarrow P \in ℝ)$
33	32 20 8	rspcdva	$⊢ φ \to P \in ℝ$
34	21	recnd	$⊢ φ \to R \in ℂ$
35	30	recnd	$⊢ φ \to Q \in ℂ$
36	28	recnd	$⊢ φ \to S \in ℂ$
37	35 36	subcld	$⊢ φ \to Q - S \in ℂ$
38	34 37	addcomd	$⊢ φ \to R + Q - S = Q - S + R$
39	34 36 35	subsub2d	$⊢ φ \to R - (S - Q) = R + Q - S$
40	35 36 34	subsubd	$⊢ φ \to Q - (S - R) = Q - S + R$
41	38 39 40	3eqtr4d	$⊢ φ \to R - (S - Q) = Q - (S - R)$
42	28 21	resubcld	$⊢ φ \to S - R \in ℝ$
43		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
44	43	subcn	$⊢ - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
45		ax-resscn	$⊢ ℝ \subseteq ℂ$
46		resubcl	$⊢ (C \in ℝ \land A \in ℝ) \to C - A \in ℝ$
47	43 44 5 3 45 46	cncfmpt2ss	$⊢ φ \to (x \in [M, N] ⟼ C - A) : [M, N] \underset{cn}{⟶} ℝ$
48	45	a1i	$⊢ φ \to ℝ \subseteq ℂ$
49		iccssre	$⊢ (M \in ℝ \land N \in ℝ) \to [M, N] \subseteq ℝ$
50	1 2 49	syl2anc	$⊢ φ \to [M, N] \subseteq ℝ$
51	24	fvmptelcdm	$⊢ (φ \land x \in [M, N]) \to C \in ℝ$
52	17	fvmptelcdm	$⊢ (φ \land x \in [M, N]) \to A \in ℝ$
53	51 52	resubcld	$⊢ (φ \land x \in [M, N]) \to C - A \in ℝ$
54	53	recnd	$⊢ (φ \land x \in [M, N]) \to C - A \in ℂ$
55	43	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
56		iccntr	$⊢ (M \in ℝ \land N \in ℝ) \to int (topGen (ran (.))) ([M, N]) = (M, N)$
57	1 2 56	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([M, N]) = (M, N)$
58	48 50 54 55 43 57	dvmptntr	$⊢ φ \to \frac{d (x \in [M, N]⟼ C - A)}{d_{ℝ} x} = \frac{d (x \in (M, N)⟼ C - A)}{d_{ℝ} x}$
59		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
60	59	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
61		ioossicc	$⊢ (M, N) \subseteq [M, N]$
62	61	sseli	$⊢ x \in (M, N) \to x \in [M, N]$
63	51	recnd	$⊢ (φ \land x \in [M, N]) \to C \in ℂ$
64	62 63	sylan2	$⊢ (φ \land x \in (M, N)) \to C \in ℂ$
65		lerel	$⊢ Rel \leq$
66	65	brrelex2i	$⊢ B \leq D \to D \in V$
67	7 66	syl	$⊢ (φ \land x \in (M, N)) \to D \in V$
68	52	recnd	$⊢ (φ \land x \in [M, N]) \to A \in ℂ$
69	62 68	sylan2	$⊢ (φ \land x \in (M, N)) \to A \in ℂ$
70	65	brrelex1i	$⊢ B \leq D \to B \in V$
71	7 70	syl	$⊢ (φ \land x \in (M, N)) \to B \in V$
72	60 64 67 6 69 71 4	dvmptsub	$⊢ φ \to \frac{d (x \in (M, N)⟼ C - A)}{d_{ℝ} x} = (x \in (M, N) ⟼ D - B)$
73	58 72	eqtrd	$⊢ φ \to \frac{d (x \in [M, N]⟼ C - A)}{d_{ℝ} x} = (x \in (M, N) ⟼ D - B)$
74	62 51	sylan2	$⊢ (φ \land x \in (M, N)) \to C \in ℝ$
75	74	fmpttd	$⊢ φ \to (x \in (M, N) ⟼ C) : (M, N) ⟶ ℝ$
76		ioossre	$⊢ (M, N) \subseteq ℝ$
77		dvfre	$⊢ ((x \in (M, N) ⟼ C) : (M, N) ⟶ ℝ \land (M, N) \subseteq ℝ) \to \frac{d (x \in (M, N)⟼ C)}{d_{ℝ} x} : dom \frac{d (x \in (M, N)⟼ C)}{d_{ℝ} x} ⟶ ℝ$
78	75 76 77	sylancl	$⊢ φ \to \frac{d (x \in (M, N)⟼ C)}{d_{ℝ} x} : dom \frac{d (x \in (M, N)⟼ C)}{d_{ℝ} x} ⟶ ℝ$
79	6	dmeqd	$⊢ φ \to dom \frac{d (x \in (M, N)⟼ C)}{d_{ℝ} x} = dom (x \in (M, N) ⟼ D)$
80	67	ralrimiva	$⊢ φ \to \forall x \in (M, N) D \in V$
81		dmmptg	$⊢ \forall x \in (M, N) D \in V \to dom (x \in (M, N) ⟼ D) = (M, N)$
82	80 81	syl	$⊢ φ \to dom (x \in (M, N) ⟼ D) = (M, N)$
83	79 82	eqtrd	$⊢ φ \to dom \frac{d (x \in (M, N)⟼ C)}{d_{ℝ} x} = (M, N)$
84	6 83	feq12d	$⊢ φ \to (\frac{d (x \in (M, N)⟼ C)}{d_{ℝ} x} : dom \frac{d (x \in (M, N)⟼ C)}{d_{ℝ} x} ⟶ ℝ \leftrightarrow (x \in (M, N) ⟼ D) : (M, N) ⟶ ℝ)$
85	78 84	mpbid	$⊢ φ \to (x \in (M, N) ⟼ D) : (M, N) ⟶ ℝ$
86	85	fvmptelcdm	$⊢ (φ \land x \in (M, N)) \to D \in ℝ$
87	62 52	sylan2	$⊢ (φ \land x \in (M, N)) \to A \in ℝ$
88	87	fmpttd	$⊢ φ \to (x \in (M, N) ⟼ A) : (M, N) ⟶ ℝ$
89		dvfre	$⊢ ((x \in (M, N) ⟼ A) : (M, N) ⟶ ℝ \land (M, N) \subseteq ℝ) \to \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} : dom \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} ⟶ ℝ$
90	88 76 89	sylancl	$⊢ φ \to \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} : dom \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} ⟶ ℝ$
91	4	dmeqd	$⊢ φ \to dom \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = dom (x \in (M, N) ⟼ B)$
92	71	ralrimiva	$⊢ φ \to \forall x \in (M, N) B \in V$
93		dmmptg	$⊢ \forall x \in (M, N) B \in V \to dom (x \in (M, N) ⟼ B) = (M, N)$
94	92 93	syl	$⊢ φ \to dom (x \in (M, N) ⟼ B) = (M, N)$
95	91 94	eqtrd	$⊢ φ \to dom \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = (M, N)$
96	4 95	feq12d	$⊢ φ \to (\frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} : dom \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} ⟶ ℝ \leftrightarrow (x \in (M, N) ⟼ B) : (M, N) ⟶ ℝ)$
97	90 96	mpbid	$⊢ φ \to (x \in (M, N) ⟼ B) : (M, N) ⟶ ℝ$
98	97	fvmptelcdm	$⊢ (φ \land x \in (M, N)) \to B \in ℝ$
99	86 98	resubcld	$⊢ (φ \land x \in (M, N)) \to D - B \in ℝ$
100	86 98	subge0d	$⊢ (φ \land x \in (M, N)) \to (0 \leq D - B \leftrightarrow B \leq D)$
101	7 100	mpbird	$⊢ (φ \land x \in (M, N)) \to 0 \leq D - B$
102		elrege0	$⊢ D - B \in [0, +∞) \leftrightarrow (D - B \in ℝ \land 0 \leq D - B)$
103	99 101 102	sylanbrc	$⊢ (φ \land x \in (M, N)) \to D - B \in [0, +∞)$
104	73 103	fmpt3d	$⊢ φ \to \frac{d (x \in [M, N]⟼ C - A)}{d_{ℝ} x} : (M, N) ⟶ [0, +∞)$
105	1 2 47 104 8 9 10	dvge0	$⊢ φ \to (x \in [M, N] ⟼ C - A) (X) \leq (x \in [M, N] ⟼ C - A) (Y)$
106	12 11	oveq12d	$⊢ x = X \to C - A = Q - P$
107		eqid	$⊢ (x \in [M, N] ⟼ C - A) = (x \in [M, N] ⟼ C - A)$
108		ovex	$⊢ C - A \in V$
109	106 107 108	fvmpt3i	$⊢ X \in [M, N] \to (x \in [M, N] ⟼ C - A) (X) = Q - P$
110	8 109	syl	$⊢ φ \to (x \in [M, N] ⟼ C - A) (X) = Q - P$
111	14 13	oveq12d	$⊢ x = Y \to C - A = S - R$
112	111 107 108	fvmpt3i	$⊢ Y \in [M, N] \to (x \in [M, N] ⟼ C - A) (Y) = S - R$
113	9 112	syl	$⊢ φ \to (x \in [M, N] ⟼ C - A) (Y) = S - R$
114	105 110 113	3brtr3d	$⊢ φ \to Q - P \leq S - R$
115	30 33 42 114	subled	$⊢ φ \to Q - (S - R) \leq P$
116	41 115	eqbrtrd	$⊢ φ \to R - (S - Q) \leq P$
117	21 31 33 116	subled	$⊢ φ \to R - P \leq S - Q$

Metamath Proof Explorer

Theorem dvle

Proof