mvth

Description: The Mean Value Theorem. If F is a real continuous function on [ A , B ] which is differentiable on ( A , B ) , then there is some x e. ( A , B ) such that ( RR _D F )x is equal to the average slope over [ A , B ] . This is Metamath 100 proof #75. (Contributed by Mario Carneiro, 1-Sep-2014) (Proof shortened by Mario Carneiro, 29-Dec-2016)

	Ref	Expression
Hypotheses	mvth.a	$⊢ φ \to A \in ℝ$
	mvth.b	$⊢ φ \to B \in ℝ$
	mvth.lt	$⊢ φ \to A < B$
	mvth.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
	mvth.d	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
Assertion	mvth	$⊢ φ \to \exists x \in (A, B) F_{ℝ}^{'} (x) = \frac{F (B) - F (A)}{B - A}$

Proof

Step	Hyp	Ref	Expression
1		mvth.a	$⊢ φ \to A \in ℝ$
2		mvth.b	$⊢ φ \to B \in ℝ$
3		mvth.lt	$⊢ φ \to A < B$
4		mvth.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
5		mvth.d	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
6		mptresid	$⊢ {I ↾}_{[A, B]} = (z \in [A, B] ⟼ z)$
7		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
8	1 2 7	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
9		ax-resscn	$⊢ ℝ \subseteq ℂ$
10		cncfmptid	$⊢ ([A, B] \subseteq ℝ \land ℝ \subseteq ℂ) \to (z \in [A, B] ⟼ z) : [A, B] \underset{cn}{⟶} ℝ$
11	8 9 10	sylancl	$⊢ φ \to (z \in [A, B] ⟼ z) : [A, B] \underset{cn}{⟶} ℝ$
12	6 11	eqeltrid	$⊢ φ \to ({I ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℝ$
13	6	eqcomi	$⊢ (z \in [A, B] ⟼ z) = {I ↾}_{[A, B]}$
14	13	oveq2i	$⊢ \frac{d (z \in [A, B]⟼ z)}{d_{ℝ} z} = ℝ D ({I ↾}_{[A, B]})$
15		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
16	15	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
17		simpr	$⊢ (φ \land z \in ℝ) \to z \in ℝ$
18	17	recnd	$⊢ (φ \land z \in ℝ) \to z \in ℂ$
19		1red	$⊢ (φ \land z \in ℝ) \to 1 \in ℝ$
20	16	dvmptid	$⊢ φ \to \frac{d (z \in ℝ⟼ z)}{d_{ℝ} z} = (z \in ℝ ⟼ 1)$
21		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
22	21	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
23		iccntr	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) = (A, B)$
24	1 2 23	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([A, B]) = (A, B)$
25	16 18 19 20 8 22 21 24	dvmptres2	$⊢ φ \to \frac{d (z \in [A, B]⟼ z)}{d_{ℝ} z} = (z \in (A, B) ⟼ 1)$
26	14 25	eqtr3id	$⊢ φ \to ℝ D ({I ↾}_{[A, B]}) = (z \in (A, B) ⟼ 1)$
27	26	dmeqd	$⊢ φ \to dom {({I ↾}_{[A, B]})}_{ℝ}^{'} = dom (z \in (A, B) ⟼ 1)$
28		1ex	$⊢ 1 \in V$
29		eqid	$⊢ (z \in (A, B) ⟼ 1) = (z \in (A, B) ⟼ 1)$
30	28 29	dmmpti	$⊢ dom (z \in (A, B) ⟼ 1) = (A, B)$
31	27 30	eqtrdi	$⊢ φ \to dom {({I ↾}_{[A, B]})}_{ℝ}^{'} = (A, B)$
32	1 2 3 4 12 5 31	cmvth	$⊢ φ \to \exists x \in (A, B) (F (B) - F (A)) {({I ↾}_{[A, B]})}_{ℝ}^{'} (x) = (({I ↾}_{[A, B]}) (B) - ({I ↾}_{[A, B]}) (A)) F_{ℝ}^{'} (x)$
33	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
34	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
35	1 2 3	ltled	$⊢ φ \to A \leq B$
36		ubicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to B \in [A, B]$
37	33 34 35 36	syl3anc	$⊢ φ \to B \in [A, B]$
38		fvresi	$⊢ B \in [A, B] \to ({I ↾}_{[A, B]}) (B) = B$
39	37 38	syl	$⊢ φ \to ({I ↾}_{[A, B]}) (B) = B$
40		lbicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in [A, B]$
41	33 34 35 40	syl3anc	$⊢ φ \to A \in [A, B]$
42		fvresi	$⊢ A \in [A, B] \to ({I ↾}_{[A, B]}) (A) = A$
43	41 42	syl	$⊢ φ \to ({I ↾}_{[A, B]}) (A) = A$
44	39 43	oveq12d	$⊢ φ \to ({I ↾}_{[A, B]}) (B) - ({I ↾}_{[A, B]}) (A) = B - A$
45	44	adantr	$⊢ (φ \land x \in (A, B)) \to ({I ↾}_{[A, B]}) (B) - ({I ↾}_{[A, B]}) (A) = B - A$
46	45	oveq1d	$⊢ (φ \land x \in (A, B)) \to (({I ↾}_{[A, B]}) (B) - ({I ↾}_{[A, B]}) (A)) F_{ℝ}^{'} (x) = (B - A) F_{ℝ}^{'} (x)$
47	26	fveq1d	$⊢ φ \to {({I ↾}_{[A, B]})}_{ℝ}^{'} (x) = (z \in (A, B) ⟼ 1) (x)$
48		eqidd	$⊢ z = x \to 1 = 1$
49	48 29 28	fvmpt3i	$⊢ x \in (A, B) \to (z \in (A, B) ⟼ 1) (x) = 1$
50	47 49	sylan9eq	$⊢ (φ \land x \in (A, B)) \to {({I ↾}_{[A, B]})}_{ℝ}^{'} (x) = 1$
51	50	oveq2d	$⊢ (φ \land x \in (A, B)) \to (F (B) - F (A)) {({I ↾}_{[A, B]})}_{ℝ}^{'} (x) = (F (B) - F (A)) \cdot 1$
52		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℝ \to F : [A, B] ⟶ ℝ$
53	4 52	syl	$⊢ φ \to F : [A, B] ⟶ ℝ$
54	53 37	ffvelrnd	$⊢ φ \to F (B) \in ℝ$
55	53 41	ffvelrnd	$⊢ φ \to F (A) \in ℝ$
56	54 55	resubcld	$⊢ φ \to F (B) - F (A) \in ℝ$
57	56	recnd	$⊢ φ \to F (B) - F (A) \in ℂ$
58	57	adantr	$⊢ (φ \land x \in (A, B)) \to F (B) - F (A) \in ℂ$
59	58	mulid1d	$⊢ (φ \land x \in (A, B)) \to (F (B) - F (A)) \cdot 1 = F (B) - F (A)$
60	51 59	eqtrd	$⊢ (φ \land x \in (A, B)) \to (F (B) - F (A)) {({I ↾}_{[A, B]})}_{ℝ}^{'} (x) = F (B) - F (A)$
61	46 60	eqeq12d	$⊢ (φ \land x \in (A, B)) \to ((({I ↾}_{[A, B]}) (B) - ({I ↾}_{[A, B]}) (A)) F_{ℝ}^{'} (x) = (F (B) - F (A)) {({I ↾}_{[A, B]})}_{ℝ}^{'} (x) \leftrightarrow (B - A) F_{ℝ}^{'} (x) = F (B) - F (A))$
62	2 1	resubcld	$⊢ φ \to B - A \in ℝ$
63	62	recnd	$⊢ φ \to B - A \in ℂ$
64	63	adantr	$⊢ (φ \land x \in (A, B)) \to B - A \in ℂ$
65		dvf	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ$
66	5	feq2d	$⊢ φ \to (F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ \leftrightarrow F_{ℝ}^{'} : (A, B) ⟶ ℂ)$
67	65 66	mpbii	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ ℂ$
68	67	ffvelrnda	$⊢ (φ \land x \in (A, B)) \to F_{ℝ}^{'} (x) \in ℂ$
69	1 2	posdifd	$⊢ φ \to (A < B \leftrightarrow 0 < B - A)$
70	3 69	mpbid	$⊢ φ \to 0 < B - A$
71	70	gt0ne0d	$⊢ φ \to B - A \neq 0$
72	71	adantr	$⊢ (φ \land x \in (A, B)) \to B - A \neq 0$
73	58 64 68 72	divmuld	$⊢ (φ \land x \in (A, B)) \to (\frac{F (B) - F (A)}{B - A} = F_{ℝ}^{'} (x) \leftrightarrow (B - A) F_{ℝ}^{'} (x) = F (B) - F (A))$
74	61 73	bitr4d	$⊢ (φ \land x \in (A, B)) \to ((({I ↾}_{[A, B]}) (B) - ({I ↾}_{[A, B]}) (A)) F_{ℝ}^{'} (x) = (F (B) - F (A)) {({I ↾}_{[A, B]})}_{ℝ}^{'} (x) \leftrightarrow \frac{F (B) - F (A)}{B - A} = F_{ℝ}^{'} (x))$
75		eqcom	$⊢ (F (B) - F (A)) {({I ↾}_{[A, B]})}_{ℝ}^{'} (x) = (({I ↾}_{[A, B]}) (B) - ({I ↾}_{[A, B]}) (A)) F_{ℝ}^{'} (x) \leftrightarrow (({I ↾}_{[A, B]}) (B) - ({I ↾}_{[A, B]}) (A)) F_{ℝ}^{'} (x) = (F (B) - F (A)) {({I ↾}_{[A, B]})}_{ℝ}^{'} (x)$
76		eqcom	$⊢ F_{ℝ}^{'} (x) = \frac{F (B) - F (A)}{B - A} \leftrightarrow \frac{F (B) - F (A)}{B - A} = F_{ℝ}^{'} (x)$
77	74 75 76	3bitr4g	$⊢ (φ \land x \in (A, B)) \to ((F (B) - F (A)) {({I ↾}_{[A, B]})}_{ℝ}^{'} (x) = (({I ↾}_{[A, B]}) (B) - ({I ↾}_{[A, B]}) (A)) F_{ℝ}^{'} (x) \leftrightarrow F_{ℝ}^{'} (x) = \frac{F (B) - F (A)}{B - A})$
78	77	rexbidva	$⊢ φ \to (\exists x \in (A, B) (F (B) - F (A)) {({I ↾}_{[A, B]})}_{ℝ}^{'} (x) = (({I ↾}_{[A, B]}) (B) - ({I ↾}_{[A, B]}) (A)) F_{ℝ}^{'} (x) \leftrightarrow \exists x \in (A, B) F_{ℝ}^{'} (x) = \frac{F (B) - F (A)}{B - A})$
79	32 78	mpbid	$⊢ φ \to \exists x \in (A, B) F_{ℝ}^{'} (x) = \frac{F (B) - F (A)}{B - A}$

Metamath Proof Explorer

Theorem mvth

Proof