dvgt0lem1

	Ref	Expression
Hypotheses	dvgt0.a	$⊢ φ \to A \in ℝ$
	dvgt0.b	$⊢ φ \to B \in ℝ$
	dvgt0.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
	dvgt0lem.d	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ S$
Assertion	dvgt0lem1	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to \frac{F (Y) - F (X)}{Y - X} \in S$

Proof

Step	Hyp	Ref	Expression
1		dvgt0.a	$⊢ φ \to A \in ℝ$
2		dvgt0.b	$⊢ φ \to B \in ℝ$
3		dvgt0.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
4		dvgt0lem.d	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ S$
5		iccssxr	$⊢ [A, B] \subseteq ℝ^{*}$
6		simplrl	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to X \in [A, B]$
7	5 6	sselid	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to X \in ℝ^{*}$
8		simplrr	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to Y \in [A, B]$
9	5 8	sselid	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to Y \in ℝ^{*}$
10		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
11	1 2 10	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
12	11	ad2antrr	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to [A, B] \subseteq ℝ$
13	12 6	sseldd	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to X \in ℝ$
14	12 8	sseldd	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to Y \in ℝ$
15		simpr	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to X < Y$
16	13 14 15	ltled	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to X \leq Y$
17		ubicc2	$⊢ (X \in ℝ^{} \land Y \in ℝ^{} \land X \leq Y) \to Y \in [X, Y]$
18	7 9 16 17	syl3anc	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to Y \in [X, Y]$
19	18	fvresd	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to ({F ↾}_{[X, Y]}) (Y) = F (Y)$
20		lbicc2	$⊢ (X \in ℝ^{} \land Y \in ℝ^{} \land X \leq Y) \to X \in [X, Y]$
21	7 9 16 20	syl3anc	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to X \in [X, Y]$
22	21	fvresd	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to ({F ↾}_{[X, Y]}) (X) = F (X)$
23	19 22	oveq12d	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to ({F ↾}_{[X, Y]}) (Y) - ({F ↾}_{[X, Y]}) (X) = F (Y) - F (X)$
24	23	oveq1d	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to \frac{({F ↾}_{[X, Y]}) (Y) - ({F ↾}_{[X, Y]}) (X)}{Y - X} = \frac{F (Y) - F (X)}{Y - X}$
25		iccss2	$⊢ (X \in [A, B] \land Y \in [A, B]) \to [X, Y] \subseteq [A, B]$
26	25	ad2antlr	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to [X, Y] \subseteq [A, B]$
27	3	ad2antrr	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to F : [A, B] \underset{cn}{⟶} ℝ$
28		rescncf	$⊢ [X, Y] \subseteq [A, B] \to (F : [A, B] \underset{cn}{⟶} ℝ \to ({F ↾}_{[X, Y]}) : [X, Y] \underset{cn}{⟶} ℝ)$
29	26 27 28	sylc	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to ({F ↾}_{[X, Y]}) : [X, Y] \underset{cn}{⟶} ℝ$
30	4	ad2antrr	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to F_{ℝ}^{'} : (A, B) ⟶ S$
31	1	ad2antrr	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to A \in ℝ$
32	31	rexrd	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to A \in ℝ^{*}$
33	2	ad2antrr	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to B \in ℝ$
34		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (X \in [A, B] \leftrightarrow (X \in ℝ \land A \leq X \land X \leq B))$
35	31 33 34	syl2anc	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to (X \in [A, B] \leftrightarrow (X \in ℝ \land A \leq X \land X \leq B))$
36	6 35	mpbid	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to (X \in ℝ \land A \leq X \land X \leq B)$
37	36	simp2d	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to A \leq X$
38		iooss1	$⊢ (A \in ℝ^{*} \land A \leq X) \to (X, Y) \subseteq (A, Y)$
39	32 37 38	syl2anc	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to (X, Y) \subseteq (A, Y)$
40	33	rexrd	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to B \in ℝ^{*}$
41		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (Y \in [A, B] \leftrightarrow (Y \in ℝ \land A \leq Y \land Y \leq B))$
42	31 33 41	syl2anc	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to (Y \in [A, B] \leftrightarrow (Y \in ℝ \land A \leq Y \land Y \leq B))$
43	8 42	mpbid	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to (Y \in ℝ \land A \leq Y \land Y \leq B)$
44	43	simp3d	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to Y \leq B$
45		iooss2	$⊢ (B \in ℝ^{*} \land Y \leq B) \to (A, Y) \subseteq (A, B)$
46	40 44 45	syl2anc	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to (A, Y) \subseteq (A, B)$
47	39 46	sstrd	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to (X, Y) \subseteq (A, B)$
48	30 47	fssresd	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to ({F_{ℝ}^{'} ↾}_{(X, Y)}) : (X, Y) ⟶ S$
49		ax-resscn	$⊢ ℝ \subseteq ℂ$
50	49	a1i	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to ℝ \subseteq ℂ$
51		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℝ \to F : [A, B] ⟶ ℝ$
52	3 51	syl	$⊢ φ \to F : [A, B] ⟶ ℝ$
53	52	ad2antrr	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to F : [A, B] ⟶ ℝ$
54		fss	$⊢ (F : [A, B] ⟶ ℝ \land ℝ \subseteq ℂ) \to F : [A, B] ⟶ ℂ$
55	53 49 54	sylancl	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to F : [A, B] ⟶ ℂ$
56		iccssre	$⊢ (X \in ℝ \land Y \in ℝ) \to [X, Y] \subseteq ℝ$
57	13 14 56	syl2anc	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to [X, Y] \subseteq ℝ$
58		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
59		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
60	58 59	dvres	$⊢ ((ℝ \subseteq ℂ \land F : [A, B] ⟶ ℂ) \land ([A, B] \subseteq ℝ \land [X, Y] \subseteq ℝ)) \to ℝ D ({F ↾}_{[X, Y]}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([X, Y])}$
61	50 55 12 57 60	syl22anc	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to ℝ D ({F ↾}_{[X, Y]}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([X, Y])}$
62		iccntr	$⊢ (X \in ℝ \land Y \in ℝ) \to int (topGen (ran (.))) ([X, Y]) = (X, Y)$
63	13 14 62	syl2anc	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to int (topGen (ran (.))) ([X, Y]) = (X, Y)$
64	63	reseq2d	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([X, Y])} = {F_{ℝ}^{'} ↾}_{(X, Y)}$
65	61 64	eqtrd	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to ℝ D ({F ↾}_{[X, Y]}) = {F_{ℝ}^{'} ↾}_{(X, Y)}$
66	65	feq1d	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to ({({F ↾}_{[X, Y]})}_{ℝ}^{'} : (X, Y) ⟶ S \leftrightarrow ({F_{ℝ}^{'} ↾}_{(X, Y)}) : (X, Y) ⟶ S)$
67	48 66	mpbird	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to {({F ↾}_{[X, Y]})}_{ℝ}^{'} : (X, Y) ⟶ S$
68	67	fdmd	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to dom {({F ↾}_{[X, Y]})}_{ℝ}^{'} = (X, Y)$
69	13 14 15 29 68	mvth	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to \exists z \in (X, Y) {({F ↾}_{[X, Y]})}_{ℝ}^{'} (z) = \frac{({F ↾}_{[X, Y]}) (Y) - ({F ↾}_{[X, Y]}) (X)}{Y - X}$
70	67	ffvelcdmda	$⊢ (((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \land z \in (X, Y)) \to {({F ↾}_{[X, Y]})}_{ℝ}^{'} (z) \in S$
71		eleq1	$⊢ {({F ↾}_{[X, Y]})}_{ℝ}^{'} (z) = \frac{({F ↾}_{[X, Y]}) (Y) - ({F ↾}_{[X, Y]}) (X)}{Y - X} \to ({({F ↾}_{[X, Y]})}_{ℝ}^{'} (z) \in S \leftrightarrow \frac{({F ↾}_{[X, Y]}) (Y) - ({F ↾}_{[X, Y]}) (X)}{Y - X} \in S)$
72	70 71	syl5ibcom	$⊢ (((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \land z \in (X, Y)) \to ({({F ↾}_{[X, Y]})}_{ℝ}^{'} (z) = \frac{({F ↾}_{[X, Y]}) (Y) - ({F ↾}_{[X, Y]}) (X)}{Y - X} \to \frac{({F ↾}_{[X, Y]}) (Y) - ({F ↾}_{[X, Y]}) (X)}{Y - X} \in S)$
73	72	rexlimdva	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to (\exists z \in (X, Y) {({F ↾}_{[X, Y]})}_{ℝ}^{'} (z) = \frac{({F ↾}_{[X, Y]}) (Y) - ({F ↾}_{[X, Y]}) (X)}{Y - X} \to \frac{({F ↾}_{[X, Y]}) (Y) - ({F ↾}_{[X, Y]}) (X)}{Y - X} \in S)$
74	69 73	mpd	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to \frac{({F ↾}_{[X, Y]}) (Y) - ({F ↾}_{[X, Y]}) (X)}{Y - X} \in S$
75	24 74	eqeltrrd	$⊢ ((φ \land (X \in [A, B] \land Y \in [A, B])) \land X < Y) \to \frac{F (Y) - F (X)}{Y - X} \in S$

Metamath Proof Explorer

Theorem dvgt0lem1

Proof