dvle2

	Ref	Expression
Hypotheses	dvle2.1	$⊢ φ \to A \in ℝ$
	dvle2.2	$⊢ φ \to B \in ℝ$
	dvle2.3	$⊢ φ \to (x \in [A, B] ⟼ E) : [A, B] \underset{cn}{⟶} ℝ$
	dvle2.4	$⊢ φ \to (x \in [A, B] ⟼ G) : [A, B] \underset{cn}{⟶} ℝ$
	dvle2.5	$⊢ φ \to \frac{d (x \in (A, B)⟼ E)}{d_{ℝ} x} = (x \in (A, B) ⟼ F)$
	dvle2.6	$⊢ φ \to \frac{d (x \in (A, B)⟼ G)}{d_{ℝ} x} = (x \in (A, B) ⟼ H)$
	dvle2.7	$⊢ (φ \land x \in (A, B)) \to F \leq H$
	dvle2.8	$⊢ x = A \to E = P$
	dvle2.9	$⊢ x = A \to G = Q$
	dvle2.10	$⊢ x = B \to E = R$
	dvle2.11	$⊢ x = B \to G = S$
	dvle2.12	$⊢ φ \to P \leq Q$
	dvle2.13	$⊢ φ \to A \leq B$
Assertion	dvle2	$⊢ φ \to R \leq S$

Proof

Step	Hyp	Ref	Expression
1		dvle2.1	$⊢ φ \to A \in ℝ$
2		dvle2.2	$⊢ φ \to B \in ℝ$
3		dvle2.3	$⊢ φ \to (x \in [A, B] ⟼ E) : [A, B] \underset{cn}{⟶} ℝ$
4		dvle2.4	$⊢ φ \to (x \in [A, B] ⟼ G) : [A, B] \underset{cn}{⟶} ℝ$
5		dvle2.5	$⊢ φ \to \frac{d (x \in (A, B)⟼ E)}{d_{ℝ} x} = (x \in (A, B) ⟼ F)$
6		dvle2.6	$⊢ φ \to \frac{d (x \in (A, B)⟼ G)}{d_{ℝ} x} = (x \in (A, B) ⟼ H)$
7		dvle2.7	$⊢ (φ \land x \in (A, B)) \to F \leq H$
8		dvle2.8	$⊢ x = A \to E = P$
9		dvle2.9	$⊢ x = A \to G = Q$
10		dvle2.10	$⊢ x = B \to E = R$
11		dvle2.11	$⊢ x = B \to G = S$
12		dvle2.12	$⊢ φ \to P \leq Q$
13		dvle2.13	$⊢ φ \to A \leq B$
14	10	eleq1d	$⊢ x = B \to (E \in ℝ \leftrightarrow R \in ℝ)$
15		cncff	$⊢ (x \in [A, B] ⟼ E) : [A, B] \underset{cn}{⟶} ℝ \to (x \in [A, B] ⟼ E) : [A, B] ⟶ ℝ$
16	3 15	syl	$⊢ φ \to (x \in [A, B] ⟼ E) : [A, B] ⟶ ℝ$
17		eqid	$⊢ (x \in [A, B] ⟼ E) = (x \in [A, B] ⟼ E)$
18	17	fmpt	$⊢ \forall x \in [A, B] E \in ℝ \leftrightarrow (x \in [A, B] ⟼ E) : [A, B] ⟶ ℝ$
19	16 18	sylibr	$⊢ φ \to \forall x \in [A, B] E \in ℝ$
20	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
21	2	leidd	$⊢ φ \to B \leq B$
22	20 13 21	3jca	$⊢ φ \to (B \in ℝ^{*} \land A \leq B \land B \leq B)$
23	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
24		elicc1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (B \in [A, B] \leftrightarrow (B \in ℝ^{*} \land A \leq B \land B \leq B))$
25	23 20 24	syl2anc	$⊢ φ \to (B \in [A, B] \leftrightarrow (B \in ℝ^{*} \land A \leq B \land B \leq B))$
26	22 25	mpbird	$⊢ φ \to B \in [A, B]$
27	14 19 26	rspcdva	$⊢ φ \to R \in ℝ$
28	8	eleq1d	$⊢ x = A \to (E \in ℝ \leftrightarrow P \in ℝ)$
29	1	leidd	$⊢ φ \to A \leq A$
30	23 29 13	3jca	$⊢ φ \to (A \in ℝ^{*} \land A \leq A \land A \leq B)$
31		elicc1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A \in [A, B] \leftrightarrow (A \in ℝ^{*} \land A \leq A \land A \leq B))$
32	23 20 31	syl2anc	$⊢ φ \to (A \in [A, B] \leftrightarrow (A \in ℝ^{*} \land A \leq A \land A \leq B))$
33	30 32	mpbird	$⊢ φ \to A \in [A, B]$
34	28 19 33	rspcdva	$⊢ φ \to P \in ℝ$
35	27 34	resubcld	$⊢ φ \to R - P \in ℝ$
36	11	eleq1d	$⊢ x = B \to (G \in ℝ \leftrightarrow S \in ℝ)$
37		cncff	$⊢ (x \in [A, B] ⟼ G) : [A, B] \underset{cn}{⟶} ℝ \to (x \in [A, B] ⟼ G) : [A, B] ⟶ ℝ$
38	4 37	syl	$⊢ φ \to (x \in [A, B] ⟼ G) : [A, B] ⟶ ℝ$
39		eqid	$⊢ (x \in [A, B] ⟼ G) = (x \in [A, B] ⟼ G)$
40	39	fmpt	$⊢ \forall x \in [A, B] G \in ℝ \leftrightarrow (x \in [A, B] ⟼ G) : [A, B] ⟶ ℝ$
41	38 40	sylibr	$⊢ φ \to \forall x \in [A, B] G \in ℝ$
42	36 41 26	rspcdva	$⊢ φ \to S \in ℝ$
43	9	eleq1d	$⊢ x = A \to (G \in ℝ \leftrightarrow Q \in ℝ)$
44	43 41 33	rspcdva	$⊢ φ \to Q \in ℝ$
45	42 44	resubcld	$⊢ φ \to S - Q \in ℝ$
46	1 2 3 5 4 6 7 33 26 13 8 9 10 11	dvle	$⊢ φ \to R - P \leq S - Q$
47	35 34 45 44 46 12	le2addd	$⊢ φ \to R - P + P \leq S - Q + Q$
48	27	recnd	$⊢ φ \to R \in ℂ$
49	34	recnd	$⊢ φ \to P \in ℂ$
50	48 49	npcand	$⊢ φ \to R - P + P = R$
51	42	recnd	$⊢ φ \to S \in ℂ$
52	44	recnd	$⊢ φ \to Q \in ℂ$
53	51 52	npcand	$⊢ φ \to S - Q + Q = S$
54	50 53	breq12d	$⊢ φ \to (R - P + P \leq S - Q + Q \leftrightarrow R \leq S)$
55	47 54	mpbid	$⊢ φ \to R \leq S$

Metamath Proof Explorer

Theorem dvle2

Proof