dvlip

Description: A function with derivative bounded by M is M-Lipschitz continuous. (Contributed by Mario Carneiro, 3-Mar-2015)

	Ref	Expression
Hypotheses	dvlip.a	$⊢ φ \to A \in ℝ$
	dvlip.b	$⊢ φ \to B \in ℝ$
	dvlip.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℂ$
	dvlip.d	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
	dvlip.m	$⊢ φ \to M \in ℝ$
	dvlip.l	$⊢ (φ \land x \in (A, B)) \to \|F_{ℝ}^{'} (x)\| \leq M$
Assertion	dvlip	$⊢ (φ \land (X \in [A, B] \land Y \in [A, B])) \to \|F (X) - F (Y)\| \leq M \|X - Y\|$

Proof

Step	Hyp	Ref	Expression
1		dvlip.a	$⊢ φ \to A \in ℝ$
2		dvlip.b	$⊢ φ \to B \in ℝ$
3		dvlip.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℂ$
4		dvlip.d	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
5		dvlip.m	$⊢ φ \to M \in ℝ$
6		dvlip.l	$⊢ (φ \land x \in (A, B)) \to \|F_{ℝ}^{'} (x)\| \leq M$
7		fveq2	$⊢ a = Y \to F (a) = F (Y)$
8	7	oveq2d	$⊢ a = Y \to F (b) - F (a) = F (b) - F (Y)$
9	8	fveq2d	$⊢ a = Y \to \|F (b) - F (a)\| = \|F (b) - F (Y)\|$
10		oveq2	$⊢ a = Y \to b - a = b - Y$
11	10	fveq2d	$⊢ a = Y \to \|b - a\| = \|b - Y\|$
12	11	oveq2d	$⊢ a = Y \to M \|b - a\| = M \|b - Y\|$
13	9 12	breq12d	$⊢ a = Y \to (\|F (b) - F (a)\| \leq M \|b - a\| \leftrightarrow \|F (b) - F (Y)\| \leq M \|b - Y\|)$
14	13	imbi2d	$⊢ a = Y \to ((φ \to \|F (b) - F (a)\| \leq M \|b - a\|) \leftrightarrow (φ \to \|F (b) - F (Y)\| \leq M \|b - Y\|))$
15		fveq2	$⊢ b = X \to F (b) = F (X)$
16	15	fvoveq1d	$⊢ b = X \to \|F (b) - F (Y)\| = \|F (X) - F (Y)\|$
17		fvoveq1	$⊢ b = X \to \|b - Y\| = \|X - Y\|$
18	17	oveq2d	$⊢ b = X \to M \|b - Y\| = M \|X - Y\|$
19	16 18	breq12d	$⊢ b = X \to (\|F (b) - F (Y)\| \leq M \|b - Y\| \leftrightarrow \|F (X) - F (Y)\| \leq M \|X - Y\|)$
20	19	imbi2d	$⊢ b = X \to ((φ \to \|F (b) - F (Y)\| \leq M \|b - Y\|) \leftrightarrow (φ \to \|F (X) - F (Y)\| \leq M \|X - Y\|))$
21		fveq2	$⊢ y = b \to F (y) = F (b)$
22		fveq2	$⊢ x = a \to F (x) = F (a)$
23	21 22	oveqan12d	$⊢ (y = b \land x = a) \to F (y) - F (x) = F (b) - F (a)$
24	23	fveq2d	$⊢ (y = b \land x = a) \to \|F (y) - F (x)\| = \|F (b) - F (a)\|$
25		oveq12	$⊢ (y = b \land x = a) \to y - x = b - a$
26	25	fveq2d	$⊢ (y = b \land x = a) \to \|y - x\| = \|b - a\|$
27	26	oveq2d	$⊢ (y = b \land x = a) \to M \|y - x\| = M \|b - a\|$
28	24 27	breq12d	$⊢ (y = b \land x = a) \to (\|F (y) - F (x)\| \leq M \|y - x\| \leftrightarrow \|F (b) - F (a)\| \leq M \|b - a\|)$
29	28	ancoms	$⊢ (x = a \land y = b) \to (\|F (y) - F (x)\| \leq M \|y - x\| \leftrightarrow \|F (b) - F (a)\| \leq M \|b - a\|)$
30		fveq2	$⊢ y = a \to F (y) = F (a)$
31		fveq2	$⊢ x = b \to F (x) = F (b)$
32	30 31	oveqan12d	$⊢ (y = a \land x = b) \to F (y) - F (x) = F (a) - F (b)$
33	32	fveq2d	$⊢ (y = a \land x = b) \to \|F (y) - F (x)\| = \|F (a) - F (b)\|$
34		oveq12	$⊢ (y = a \land x = b) \to y - x = a - b$
35	34	fveq2d	$⊢ (y = a \land x = b) \to \|y - x\| = \|a - b\|$
36	35	oveq2d	$⊢ (y = a \land x = b) \to M \|y - x\| = M \|a - b\|$
37	33 36	breq12d	$⊢ (y = a \land x = b) \to (\|F (y) - F (x)\| \leq M \|y - x\| \leftrightarrow \|F (a) - F (b)\| \leq M \|a - b\|)$
38	37	ancoms	$⊢ (x = b \land y = a) \to (\|F (y) - F (x)\| \leq M \|y - x\| \leftrightarrow \|F (a) - F (b)\| \leq M \|a - b\|)$
39		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
40	1 2 39	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
41		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℂ \to F : [A, B] ⟶ ℂ$
42	3 41	syl	$⊢ φ \to F : [A, B] ⟶ ℂ$
43		ffvelcdm	$⊢ (F : [A, B] ⟶ ℂ \land a \in [A, B]) \to F (a) \in ℂ$
44		ffvelcdm	$⊢ (F : [A, B] ⟶ ℂ \land b \in [A, B]) \to F (b) \in ℂ$
45	43 44	anim12dan	$⊢ (F : [A, B] ⟶ ℂ \land (a \in [A, B] \land b \in [A, B])) \to (F (a) \in ℂ \land F (b) \in ℂ)$
46	42 45	sylan	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to (F (a) \in ℂ \land F (b) \in ℂ)$
47	46	simprd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to F (b) \in ℂ$
48	46	simpld	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to F (a) \in ℂ$
49	47 48	abssubd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to \|F (b) - F (a)\| = \|F (a) - F (b)\|$
50		ax-resscn	$⊢ ℝ \subseteq ℂ$
51	40 50	sstrdi	$⊢ φ \to [A, B] \subseteq ℂ$
52	51	sselda	$⊢ (φ \land b \in [A, B]) \to b \in ℂ$
53	52	adantrl	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to b \in ℂ$
54	51	sselda	$⊢ (φ \land a \in [A, B]) \to a \in ℂ$
55	54	adantrr	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to a \in ℂ$
56	53 55	abssubd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to \|b - a\| = \|a - b\|$
57	56	oveq2d	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to M \|b - a\| = M \|a - b\|$
58	49 57	breq12d	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to (\|F (b) - F (a)\| \leq M \|b - a\| \leftrightarrow \|F (a) - F (b)\| \leq M \|a - b\|)$
59	42	adantr	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to F : [A, B] ⟶ ℂ$
60		simpr2	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to b \in [A, B]$
61	59 60	ffvelcdmd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to F (b) \in ℂ$
62		simpr1	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to a \in [A, B]$
63	59 62	ffvelcdmd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to F (a) \in ℂ$
64	61 63	subeq0ad	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (F (b) - F (a) = 0 \leftrightarrow F (b) = F (a))$
65	64	biimpar	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) = F (a)) \to F (b) - F (a) = 0$
66	65	abs00bd	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) = F (a)) \to \|F (b) - F (a)\| = 0$
67	40	adantr	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to [A, B] \subseteq ℝ$
68	67 62	sseldd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to a \in ℝ$
69	68	rexrd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to a \in ℝ^{*}$
70	67 60	sseldd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to b \in ℝ$
71	70	rexrd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to b \in ℝ^{*}$
72		ioon0	$⊢ (a \in ℝ^{} \land b \in ℝ^{}) \to ((a, b) \neq \emptyset \leftrightarrow a < b)$
73	69 71 72	syl2anc	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to ((a, b) \neq \emptyset \leftrightarrow a < b)$
74	5	ad2antrr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land (a, b) \neq \emptyset) \to M \in ℝ$
75	70 68	resubcld	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to b - a \in ℝ$
76	75	adantr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land (a, b) \neq \emptyset) \to b - a \in ℝ$
77	1	adantr	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to A \in ℝ$
78	77	rexrd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to A \in ℝ^{*}$
79	2	adantr	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to B \in ℝ$
80		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (a \in [A, B] \leftrightarrow (a \in ℝ \land A \leq a \land a \leq B))$
81	77 79 80	syl2anc	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (a \in [A, B] \leftrightarrow (a \in ℝ \land A \leq a \land a \leq B))$
82	62 81	mpbid	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (a \in ℝ \land A \leq a \land a \leq B)$
83	82	simp2d	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to A \leq a$
84		iooss1	$⊢ (A \in ℝ^{*} \land A \leq a) \to (a, b) \subseteq (A, b)$
85	78 83 84	syl2anc	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (a, b) \subseteq (A, b)$
86	79	rexrd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to B \in ℝ^{*}$
87		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (b \in [A, B] \leftrightarrow (b \in ℝ \land A \leq b \land b \leq B))$
88	77 79 87	syl2anc	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (b \in [A, B] \leftrightarrow (b \in ℝ \land A \leq b \land b \leq B))$
89	60 88	mpbid	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (b \in ℝ \land A \leq b \land b \leq B)$
90	89	simp3d	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to b \leq B$
91		iooss2	$⊢ (B \in ℝ^{*} \land b \leq B) \to (A, b) \subseteq (A, B)$
92	86 90 91	syl2anc	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (A, b) \subseteq (A, B)$
93	85 92	sstrd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (a, b) \subseteq (A, B)$
94		ssn0	$⊢ ((a, b) \subseteq (A, B) \land (a, b) \neq \emptyset) \to (A, B) \neq \emptyset$
95	93 94	sylan	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land (a, b) \neq \emptyset) \to (A, B) \neq \emptyset$
96		n0	$⊢ (A, B) \neq \emptyset \leftrightarrow \exists x x \in (A, B)$
97		0red	$⊢ (φ \land x \in (A, B)) \to 0 \in ℝ$
98		dvf	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ$
99	4	feq2d	$⊢ φ \to (F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ \leftrightarrow F_{ℝ}^{'} : (A, B) ⟶ ℂ)$
100	98 99	mpbii	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ ℂ$
101	100	ffvelcdmda	$⊢ (φ \land x \in (A, B)) \to F_{ℝ}^{'} (x) \in ℂ$
102	101	abscld	$⊢ (φ \land x \in (A, B)) \to \|F_{ℝ}^{'} (x)\| \in ℝ$
103	5	adantr	$⊢ (φ \land x \in (A, B)) \to M \in ℝ$
104	101	absge0d	$⊢ (φ \land x \in (A, B)) \to 0 \leq \|F_{ℝ}^{'} (x)\|$
105	97 102 103 104 6	letrd	$⊢ (φ \land x \in (A, B)) \to 0 \leq M$
106	105	ex	$⊢ φ \to (x \in (A, B) \to 0 \leq M)$
107	106	exlimdv	$⊢ φ \to (\exists x x \in (A, B) \to 0 \leq M)$
108	107	imp	$⊢ (φ \land \exists x x \in (A, B)) \to 0 \leq M$
109	96 108	sylan2b	$⊢ (φ \land (A, B) \neq \emptyset) \to 0 \leq M$
110	109	adantlr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land (A, B) \neq \emptyset) \to 0 \leq M$
111	95 110	syldan	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land (a, b) \neq \emptyset) \to 0 \leq M$
112		simpr3	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to a \leq b$
113	70 68	subge0d	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (0 \leq b - a \leftrightarrow a \leq b)$
114	112 113	mpbird	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to 0 \leq b - a$
115	114	adantr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land (a, b) \neq \emptyset) \to 0 \leq b - a$
116	74 76 111 115	mulge0d	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land (a, b) \neq \emptyset) \to 0 \leq M (b - a)$
117	116	ex	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to ((a, b) \neq \emptyset \to 0 \leq M (b - a))$
118	73 117	sylbird	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (a < b \to 0 \leq M (b - a))$
119	70	recnd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to b \in ℂ$
120	68	recnd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to a \in ℂ$
121	119 120	subeq0ad	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (b - a = 0 \leftrightarrow b = a)$
122		equcom	$⊢ b = a \leftrightarrow a = b$
123	121 122	bitrdi	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (b - a = 0 \leftrightarrow a = b)$
124		0re	$⊢ 0 \in ℝ$
125	5	adantr	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to M \in ℝ$
126	125	recnd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to M \in ℂ$
127	126	mul01d	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to M \cdot 0 = 0$
128	127	eqcomd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to 0 = M \cdot 0$
129		eqle	$⊢ (0 \in ℝ \land 0 = M \cdot 0) \to 0 \leq M \cdot 0$
130	124 128 129	sylancr	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to 0 \leq M \cdot 0$
131		oveq2	$⊢ b - a = 0 \to M (b - a) = M \cdot 0$
132	131	breq2d	$⊢ b - a = 0 \to (0 \leq M (b - a) \leftrightarrow 0 \leq M \cdot 0)$
133	130 132	syl5ibrcom	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (b - a = 0 \to 0 \leq M (b - a))$
134	123 133	sylbird	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (a = b \to 0 \leq M (b - a))$
135	68 70	leloed	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (a \leq b \leftrightarrow (a < b \lor a = b))$
136	112 135	mpbid	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (a < b \lor a = b)$
137	118 134 136	mpjaod	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to 0 \leq M (b - a)$
138	137	adantr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) = F (a)) \to 0 \leq M (b - a)$
139	66 138	eqbrtrd	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) = F (a)) \to \|F (b) - F (a)\| \leq M (b - a)$
140	61 63	subcld	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to F (b) - F (a) \in ℂ$
141	140	adantr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to F (b) - F (a) \in ℂ$
142	141	abscld	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to \|F (b) - F (a)\| \in ℝ$
143	142	recnd	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to \|F (b) - F (a)\| \in ℂ$
144	75	adantr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to b - a \in ℝ$
145	144	recnd	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to b - a \in ℂ$
146	136	ord	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (\neg a < b \to a = b)$
147		fveq2	$⊢ a = b \to F (a) = F (b)$
148	147	eqcomd	$⊢ a = b \to F (b) = F (a)$
149	146 148	syl6	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (\neg a < b \to F (b) = F (a))$
150	149	necon1ad	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (F (b) \neq F (a) \to a < b)$
151	150	imp	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to a < b$
152	68	adantr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to a \in ℝ$
153	70	adantr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to b \in ℝ$
154	152 153	posdifd	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to (a < b \leftrightarrow 0 < b - a)$
155	151 154	mpbid	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to 0 < b - a$
156	155	gt0ne0d	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to b - a \neq 0$
157	143 145 156	divrec2d	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to \frac{\|F (b) - F (a)\|}{b - a} = (\frac{1}{b - a}) \|F (b) - F (a)\|$
158		iccss2	$⊢ (a \in [A, B] \land b \in [A, B]) \to [a, b] \subseteq [A, B]$
159	62 60 158	syl2anc	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to [a, b] \subseteq [A, B]$
160	159	adantr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to [a, b] \subseteq [A, B]$
161	160	sselda	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land y \in [a, b]) \to y \in [A, B]$
162	42	ad2antrr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to F : [A, B] ⟶ ℂ$
163	162	ffvelcdmda	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land y \in [A, B]) \to F (y) \in ℂ$
164	161 163	syldan	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land y \in [a, b]) \to F (y) \in ℂ$
165	140	ad2antrr	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land y \in [a, b]) \to F (b) - F (a) \in ℂ$
166	64	necon3bid	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to (F (b) - F (a) \neq 0 \leftrightarrow F (b) \neq F (a))$
167	166	biimpar	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to F (b) - F (a) \neq 0$
168	167	adantr	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land y \in [a, b]) \to F (b) - F (a) \neq 0$
169	164 165 168	divcld	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land y \in [a, b]) \to \frac{F (y)}{F (b) - F (a)} \in ℂ$
170	162 160	feqresmpt	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to {F ↾}_{[a, b]} = (y \in [a, b] ⟼ F (y))$
171		eqidd	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to (x \in ℂ ⟼ \frac{x}{F (b) - F (a)}) = (x \in ℂ ⟼ \frac{x}{F (b) - F (a)})$
172		oveq1	$⊢ x = F (y) \to \frac{x}{F (b) - F (a)} = \frac{F (y)}{F (b) - F (a)}$
173	164 170 171 172	fmptco	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to (x \in ℂ ⟼ \frac{x}{F (b) - F (a)}) \circ ({F ↾}_{[a, b]}) = (y \in [a, b] ⟼ \frac{F (y)}{F (b) - F (a)})$
174		ref	$⊢ ℜ : ℂ ⟶ ℝ$
175	174	a1i	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to ℜ : ℂ ⟶ ℝ$
176	175	feqmptd	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to ℜ = (x \in ℂ ⟼ ℜ (x))$
177		fveq2	$⊢ x = \frac{F (y)}{F (b) - F (a)} \to ℜ (x) = ℜ (\frac{F (y)}{F (b) - F (a)})$
178	169 173 176 177	fmptco	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to ℜ \circ ((x \in ℂ ⟼ \frac{x}{F (b) - F (a)}) \circ ({F ↾}_{[a, b]})) = (y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)}))$
179	3	adantr	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to F : [A, B] \underset{cn}{⟶} ℂ$
180		rescncf	$⊢ [a, b] \subseteq [A, B] \to (F : [A, B] \underset{cn}{⟶} ℂ \to ({F ↾}_{[a, b]}) : [a, b] \underset{cn}{⟶} ℂ)$
181	159 179 180	sylc	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to ({F ↾}_{[a, b]}) : [a, b] \underset{cn}{⟶} ℂ$
182	181	adantr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to ({F ↾}_{[a, b]}) : [a, b] \underset{cn}{⟶} ℂ$
183		eqid	$⊢ (x \in ℂ ⟼ \frac{x}{F (b) - F (a)}) = (x \in ℂ ⟼ \frac{x}{F (b) - F (a)})$
184	183	divccncf	$⊢ (F (b) - F (a) \in ℂ \land F (b) - F (a) \neq 0) \to (x \in ℂ ⟼ \frac{x}{F (b) - F (a)}) : ℂ \underset{cn}{⟶} ℂ$
185	141 167 184	syl2anc	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to (x \in ℂ ⟼ \frac{x}{F (b) - F (a)}) : ℂ \underset{cn}{⟶} ℂ$
186	182 185	cncfco	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to ((x \in ℂ ⟼ \frac{x}{F (b) - F (a)}) \circ ({F ↾}_{[a, b]})) : [a, b] \underset{cn}{⟶} ℂ$
187		recncf	$⊢ ℜ : ℂ \underset{cn}{⟶} ℝ$
188	187	a1i	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to ℜ : ℂ \underset{cn}{⟶} ℝ$
189	186 188	cncfco	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to (ℜ \circ ((x \in ℂ ⟼ \frac{x}{F (b) - F (a)}) \circ ({F ↾}_{[a, b]}))) : [a, b] \underset{cn}{⟶} ℝ$
190	178 189	eqeltrrd	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to (y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)})) : [a, b] \underset{cn}{⟶} ℝ$
191	50	a1i	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to ℝ \subseteq ℂ$
192		iccssre	$⊢ (a \in ℝ \land b \in ℝ) \to [a, b] \subseteq ℝ$
193	152 153 192	syl2anc	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to [a, b] \subseteq ℝ$
194	169	recld	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land y \in [a, b]) \to ℜ (\frac{F (y)}{F (b) - F (a)}) \in ℝ$
195	194	recnd	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land y \in [a, b]) \to ℜ (\frac{F (y)}{F (b) - F (a)}) \in ℂ$
196		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
197	196	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
198		iccntr	$⊢ (a \in ℝ \land b \in ℝ) \to int (topGen (ran (.))) ([a, b]) = (a, b)$
199	68 70 198	syl2anc	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to int (topGen (ran (.))) ([a, b]) = (a, b)$
200	199	adantr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to int (topGen (ran (.))) ([a, b]) = (a, b)$
201	191 193 195 197 196 200	dvmptntr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to \frac{d (y \in [a, b]⟼ ℜ (\frac{F (y)}{F (b) - F (a)}))}{d_{ℝ} y} = \frac{d (y \in (a, b)⟼ ℜ (\frac{F (y)}{F (b) - F (a)}))}{d_{ℝ} y}$
202		ioossicc	$⊢ (a, b) \subseteq [a, b]$
203	202	sseli	$⊢ y \in (a, b) \to y \in [a, b]$
204	203 169	sylan2	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land y \in (a, b)) \to \frac{F (y)}{F (b) - F (a)} \in ℂ$
205		ovexd	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land y \in (a, b)) \to \frac{F_{ℝ}^{'} (y)}{F (b) - F (a)} \in V$
206		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
207	206	a1i	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to ℝ \in \{ℝ, ℂ\}$
208	203 164	sylan2	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land y \in (a, b)) \to F (y) \in ℂ$
209	93	adantr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to (a, b) \subseteq (A, B)$
210	209	sselda	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land y \in (a, b)) \to y \in (A, B)$
211	100	ad2antrr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to F_{ℝ}^{'} : (A, B) ⟶ ℂ$
212	211	ffvelcdmda	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land y \in (A, B)) \to F_{ℝ}^{'} (y) \in ℂ$
213	210 212	syldan	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land y \in (a, b)) \to F_{ℝ}^{'} (y) \in ℂ$
214	40	ad2antrr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to [A, B] \subseteq ℝ$
215		ioossre	$⊢ (a, b) \subseteq ℝ$
216	215	a1i	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to (a, b) \subseteq ℝ$
217	196 197	dvres	$⊢ ((ℝ \subseteq ℂ \land F : [A, B] ⟶ ℂ) \land ([A, B] \subseteq ℝ \land (a, b) \subseteq ℝ)) \to ℝ D ({F ↾}_{(a, b)}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((a, b))}$
218	191 162 214 216 217	syl22anc	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to ℝ D ({F ↾}_{(a, b)}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((a, b))}$
219		retop	$⊢ topGen (ran (.)) \in Top$
220		iooretop	$⊢ (a, b) \in topGen (ran (.))$
221		isopn3i	$⊢ (topGen (ran (.)) \in Top \land (a, b) \in topGen (ran (.))) \to int (topGen (ran (.))) ((a, b)) = (a, b)$
222	219 220 221	mp2an	$⊢ int (topGen (ran (.))) ((a, b)) = (a, b)$
223	222	reseq2i	$⊢ {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((a, b))} = {F_{ℝ}^{'} ↾}_{(a, b)}$
224	218 223	eqtrdi	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to ℝ D ({F ↾}_{(a, b)}) = {F_{ℝ}^{'} ↾}_{(a, b)}$
225	202 160	sstrid	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to (a, b) \subseteq [A, B]$
226	162 225	feqresmpt	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to {F ↾}_{(a, b)} = (y \in (a, b) ⟼ F (y))$
227	226	oveq2d	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to ℝ D ({F ↾}_{(a, b)}) = \frac{d (y \in (a, b)⟼ F (y))}{d_{ℝ} y}$
228	100	adantr	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to F_{ℝ}^{'} : (A, B) ⟶ ℂ$
229	228 93	fssresd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to ({F_{ℝ}^{'} ↾}_{(a, b)}) : (a, b) ⟶ ℂ$
230	229	feqmptd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to {F_{ℝ}^{'} ↾}_{(a, b)} = (y \in (a, b) ⟼ ({F_{ℝ}^{'} ↾}_{(a, b)}) (y))$
231	230	adantr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to {F_{ℝ}^{'} ↾}_{(a, b)} = (y \in (a, b) ⟼ ({F_{ℝ}^{'} ↾}_{(a, b)}) (y))$
232		fvres	$⊢ y \in (a, b) \to ({F_{ℝ}^{'} ↾}_{(a, b)}) (y) = F_{ℝ}^{'} (y)$
233	232	mpteq2ia	$⊢ (y \in (a, b) ⟼ ({F_{ℝ}^{'} ↾}_{(a, b)}) (y)) = (y \in (a, b) ⟼ F_{ℝ}^{'} (y))$
234	231 233	eqtrdi	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to {F_{ℝ}^{'} ↾}_{(a, b)} = (y \in (a, b) ⟼ F_{ℝ}^{'} (y))$
235	224 227 234	3eqtr3d	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to \frac{d (y \in (a, b)⟼ F (y))}{d_{ℝ} y} = (y \in (a, b) ⟼ F_{ℝ}^{'} (y))$
236	207 208 213 235 141 167	dvmptdivc	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to \frac{d (y \in (a, b)⟼ \frac{F (y)}{F (b) - F (a)})}{d_{ℝ} y} = (y \in (a, b) ⟼ \frac{F_{ℝ}^{'} (y)}{F (b) - F (a)})$
237	204 205 236	dvmptre	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to \frac{d (y \in (a, b)⟼ ℜ (\frac{F (y)}{F (b) - F (a)}))}{d_{ℝ} y} = (y \in (a, b) ⟼ ℜ (\frac{F_{ℝ}^{'} (y)}{F (b) - F (a)}))$
238	201 237	eqtrd	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to \frac{d (y \in [a, b]⟼ ℜ (\frac{F (y)}{F (b) - F (a)}))}{d_{ℝ} y} = (y \in (a, b) ⟼ ℜ (\frac{F_{ℝ}^{'} (y)}{F (b) - F (a)}))$
239	238	dmeqd	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to dom \frac{d (y \in [a, b]⟼ ℜ (\frac{F (y)}{F (b) - F (a)}))}{d_{ℝ} y} = dom (y \in (a, b) ⟼ ℜ (\frac{F_{ℝ}^{'} (y)}{F (b) - F (a)}))$
240		dmmptg	$⊢ \forall y \in (a, b) ℜ (\frac{F_{ℝ}^{'} (y)}{F (b) - F (a)}) \in V \to dom (y \in (a, b) ⟼ ℜ (\frac{F_{ℝ}^{'} (y)}{F (b) - F (a)})) = (a, b)$
241		fvex	$⊢ ℜ (\frac{F_{ℝ}^{'} (y)}{F (b) - F (a)}) \in V$
242	241	a1i	$⊢ y \in (a, b) \to ℜ (\frac{F_{ℝ}^{'} (y)}{F (b) - F (a)}) \in V$
243	240 242	mprg	$⊢ dom (y \in (a, b) ⟼ ℜ (\frac{F_{ℝ}^{'} (y)}{F (b) - F (a)})) = (a, b)$
244	239 243	eqtrdi	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to dom \frac{d (y \in [a, b]⟼ ℜ (\frac{F (y)}{F (b) - F (a)}))}{d_{ℝ} y} = (a, b)$
245	152 153 151 190 244	mvth	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to \exists x \in (a, b) \frac{d (y \in [a, b]⟼ ℜ (\frac{F (y)}{F (b) - F (a)}))}{d_{ℝ} y} (x) = \frac{(y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)})) (b) - (y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)})) (a)}{b - a}$
246	238	fveq1d	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to \frac{d (y \in [a, b]⟼ ℜ (\frac{F (y)}{F (b) - F (a)}))}{d_{ℝ} y} (x) = (y \in (a, b) ⟼ ℜ (\frac{F_{ℝ}^{'} (y)}{F (b) - F (a)})) (x)$
247		fveq2	$⊢ y = x \to F_{ℝ}^{'} (y) = F_{ℝ}^{'} (x)$
248	247	fvoveq1d	$⊢ y = x \to ℜ (\frac{F_{ℝ}^{'} (y)}{F (b) - F (a)}) = ℜ (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)})$
249		eqid	$⊢ (y \in (a, b) ⟼ ℜ (\frac{F_{ℝ}^{'} (y)}{F (b) - F (a)})) = (y \in (a, b) ⟼ ℜ (\frac{F_{ℝ}^{'} (y)}{F (b) - F (a)}))$
250		fvex	$⊢ ℜ (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}) \in V$
251	248 249 250	fvmpt	$⊢ x \in (a, b) \to (y \in (a, b) ⟼ ℜ (\frac{F_{ℝ}^{'} (y)}{F (b) - F (a)})) (x) = ℜ (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)})$
252	246 251	sylan9eq	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to \frac{d (y \in [a, b]⟼ ℜ (\frac{F (y)}{F (b) - F (a)}))}{d_{ℝ} y} (x) = ℜ (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)})$
253		ubicc2	$⊢ (a \in ℝ^{} \land b \in ℝ^{} \land a \leq b) \to b \in [a, b]$
254	69 71 112 253	syl3anc	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to b \in [a, b]$
255	254	ad2antrr	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to b \in [a, b]$
256	21	fvoveq1d	$⊢ y = b \to ℜ (\frac{F (y)}{F (b) - F (a)}) = ℜ (\frac{F (b)}{F (b) - F (a)})$
257		eqid	$⊢ (y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)})) = (y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)}))$
258		fvex	$⊢ ℜ (\frac{F (b)}{F (b) - F (a)}) \in V$
259	256 257 258	fvmpt	$⊢ b \in [a, b] \to (y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)})) (b) = ℜ (\frac{F (b)}{F (b) - F (a)})$
260	255 259	syl	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to (y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)})) (b) = ℜ (\frac{F (b)}{F (b) - F (a)})$
261		lbicc2	$⊢ (a \in ℝ^{} \land b \in ℝ^{} \land a \leq b) \to a \in [a, b]$
262	69 71 112 261	syl3anc	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to a \in [a, b]$
263	262	ad2antrr	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to a \in [a, b]$
264	30	fvoveq1d	$⊢ y = a \to ℜ (\frac{F (y)}{F (b) - F (a)}) = ℜ (\frac{F (a)}{F (b) - F (a)})$
265		fvex	$⊢ ℜ (\frac{F (a)}{F (b) - F (a)}) \in V$
266	264 257 265	fvmpt	$⊢ a \in [a, b] \to (y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)})) (a) = ℜ (\frac{F (a)}{F (b) - F (a)})$
267	263 266	syl	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to (y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)})) (a) = ℜ (\frac{F (a)}{F (b) - F (a)})$
268	260 267	oveq12d	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to (y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)})) (b) - (y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)})) (a) = ℜ (\frac{F (b)}{F (b) - F (a)}) - ℜ (\frac{F (a)}{F (b) - F (a)})$
269	61	adantr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to F (b) \in ℂ$
270	269 141 167	divcld	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to \frac{F (b)}{F (b) - F (a)} \in ℂ$
271	63	adantr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to F (a) \in ℂ$
272	271 141 167	divcld	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to \frac{F (a)}{F (b) - F (a)} \in ℂ$
273	270 272	resubd	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to ℜ ((\frac{F (b)}{F (b) - F (a)}) - (\frac{F (a)}{F (b) - F (a)})) = ℜ (\frac{F (b)}{F (b) - F (a)}) - ℜ (\frac{F (a)}{F (b) - F (a)})$
274	269 271 141 167	divsubdird	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to \frac{F (b) - F (a)}{F (b) - F (a)} = (\frac{F (b)}{F (b) - F (a)}) - (\frac{F (a)}{F (b) - F (a)})$
275	141 167	dividd	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to \frac{F (b) - F (a)}{F (b) - F (a)} = 1$
276	274 275	eqtr3d	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to (\frac{F (b)}{F (b) - F (a)}) - (\frac{F (a)}{F (b) - F (a)}) = 1$
277	276	fveq2d	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to ℜ ((\frac{F (b)}{F (b) - F (a)}) - (\frac{F (a)}{F (b) - F (a)})) = ℜ (1)$
278		re1	$⊢ ℜ (1) = 1$
279	277 278	eqtrdi	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to ℜ ((\frac{F (b)}{F (b) - F (a)}) - (\frac{F (a)}{F (b) - F (a)})) = 1$
280	273 279	eqtr3d	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to ℜ (\frac{F (b)}{F (b) - F (a)}) - ℜ (\frac{F (a)}{F (b) - F (a)}) = 1$
281	280	adantr	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to ℜ (\frac{F (b)}{F (b) - F (a)}) - ℜ (\frac{F (a)}{F (b) - F (a)}) = 1$
282	268 281	eqtrd	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to (y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)})) (b) - (y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)})) (a) = 1$
283	282	oveq1d	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to \frac{(y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)})) (b) - (y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)})) (a)}{b - a} = \frac{1}{b - a}$
284	252 283	eqeq12d	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to (\frac{d (y \in [a, b]⟼ ℜ (\frac{F (y)}{F (b) - F (a)}))}{d_{ℝ} y} (x) = \frac{(y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)})) (b) - (y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)})) (a)}{b - a} \leftrightarrow ℜ (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}) = \frac{1}{b - a})$
285	284	rexbidva	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to (\exists x \in (a, b) \frac{d (y \in [a, b]⟼ ℜ (\frac{F (y)}{F (b) - F (a)}))}{d_{ℝ} y} (x) = \frac{(y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)})) (b) - (y \in [a, b] ⟼ ℜ (\frac{F (y)}{F (b) - F (a)})) (a)}{b - a} \leftrightarrow \exists x \in (a, b) ℜ (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}) = \frac{1}{b - a})$
286	245 285	mpbid	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to \exists x \in (a, b) ℜ (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}) = \frac{1}{b - a}$
287	209	sselda	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to x \in (A, B)$
288	211	ffvelcdmda	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (A, B)) \to F_{ℝ}^{'} (x) \in ℂ$
289	287 288	syldan	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to F_{ℝ}^{'} (x) \in ℂ$
290	140	ad2antrr	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to F (b) - F (a) \in ℂ$
291	167	adantr	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to F (b) - F (a) \neq 0$
292	289 290 291	divcld	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to \frac{F_{ℝ}^{'} (x)}{F (b) - F (a)} \in ℂ$
293	292	recld	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to ℜ (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}) \in ℝ$
294	142	adantr	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to \|F (b) - F (a)\| \in ℝ$
295	293 294	remulcld	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to ℜ (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}) \|F (b) - F (a)\| \in ℝ$
296	289	abscld	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to \|F_{ℝ}^{'} (x)\| \in ℝ$
297	125	ad2antrr	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to M \in ℝ$
298	292	abscld	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to \|\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}\| \in ℝ$
299	141	absge0d	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to 0 \leq \|F (b) - F (a)\|$
300	299	adantr	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to 0 \leq \|F (b) - F (a)\|$
301	292	releabsd	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to ℜ (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}) \leq \|\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}\|$
302	293 298 294 300 301	lemul1ad	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to ℜ (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}) \|F (b) - F (a)\| \leq \|\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}\| \|F (b) - F (a)\|$
303	292 290	absmuld	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to \|(\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}) (F (b) - F (a))\| = \|\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}\| \|F (b) - F (a)\|$
304	289 290 291	divcan1d	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}) (F (b) - F (a)) = F_{ℝ}^{'} (x)$
305	304	fveq2d	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to \|(\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}) (F (b) - F (a))\| = \|F_{ℝ}^{'} (x)\|$
306	303 305	eqtr3d	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to \|\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}\| \|F (b) - F (a)\| = \|F_{ℝ}^{'} (x)\|$
307	302 306	breqtrd	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to ℜ (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}) \|F (b) - F (a)\| \leq \|F_{ℝ}^{'} (x)\|$
308	6	ad4ant14	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (A, B)) \to \|F_{ℝ}^{'} (x)\| \leq M$
309	287 308	syldan	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to \|F_{ℝ}^{'} (x)\| \leq M$
310	295 296 297 307 309	letrd	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to ℜ (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}) \|F (b) - F (a)\| \leq M$
311		oveq1	$⊢ ℜ (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}) = \frac{1}{b - a} \to ℜ (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}) \|F (b) - F (a)\| = (\frac{1}{b - a}) \|F (b) - F (a)\|$
312	311	breq1d	$⊢ ℜ (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}) = \frac{1}{b - a} \to (ℜ (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}) \|F (b) - F (a)\| \leq M \leftrightarrow (\frac{1}{b - a}) \|F (b) - F (a)\| \leq M)$
313	310 312	syl5ibcom	$⊢ (((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \land x \in (a, b)) \to (ℜ (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}) = \frac{1}{b - a} \to (\frac{1}{b - a}) \|F (b) - F (a)\| \leq M)$
314	313	rexlimdva	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to (\exists x \in (a, b) ℜ (\frac{F_{ℝ}^{'} (x)}{F (b) - F (a)}) = \frac{1}{b - a} \to (\frac{1}{b - a}) \|F (b) - F (a)\| \leq M)$
315	286 314	mpd	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to (\frac{1}{b - a}) \|F (b) - F (a)\| \leq M$
316	157 315	eqbrtrd	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to \frac{\|F (b) - F (a)\|}{b - a} \leq M$
317	5	ad2antrr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to M \in ℝ$
318		ledivmul2	$⊢ (\|F (b) - F (a)\| \in ℝ \land M \in ℝ \land (b - a \in ℝ \land 0 < b - a)) \to (\frac{\|F (b) - F (a)\|}{b - a} \leq M \leftrightarrow \|F (b) - F (a)\| \leq M (b - a))$
319	142 317 144 155 318	syl112anc	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to (\frac{\|F (b) - F (a)\|}{b - a} \leq M \leftrightarrow \|F (b) - F (a)\| \leq M (b - a))$
320	316 319	mpbid	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \land F (b) \neq F (a)) \to \|F (b) - F (a)\| \leq M (b - a)$
321	139 320	pm2.61dane	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to \|F (b) - F (a)\| \leq M (b - a)$
322	68 70 112	abssubge0d	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to \|b - a\| = b - a$
323	322	oveq2d	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to M \|b - a\| = M (b - a)$
324	321 323	breqtrrd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B] \land a \leq b)) \to \|F (b) - F (a)\| \leq M \|b - a\|$
325	29 38 40 58 324	wlogle	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to \|F (b) - F (a)\| \leq M \|b - a\|$
326	325	expcom	$⊢ (a \in [A, B] \land b \in [A, B]) \to (φ \to \|F (b) - F (a)\| \leq M \|b - a\|)$
327	14 20 326	vtocl2ga	$⊢ (Y \in [A, B] \land X \in [A, B]) \to (φ \to \|F (X) - F (Y)\| \leq M \|X - Y\|)$
328	327	ancoms	$⊢ (X \in [A, B] \land Y \in [A, B]) \to (φ \to \|F (X) - F (Y)\| \leq M \|X - Y\|)$
329	328	impcom	$⊢ (φ \land (X \in [A, B] \land Y \in [A, B])) \to \|F (X) - F (Y)\| \leq M \|X - Y\|$

Metamath Proof Explorer

Theorem dvlip

Proof