Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	mvth.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	mvth.lt	⊢ ( 𝜑 → 𝐴 < 𝐵 )
	mvth.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
	mvth.d	⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
Assertion	mvth	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝐵 − 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mvth.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		mvth.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		mvth.lt	⊢ ( 𝜑 → 𝐴 < 𝐵 )
4		mvth.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
5		mvth.d	⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
6		mptresid	⊢ ( I ↾ ( 𝐴 [,] 𝐵 ) ) = ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑧 )
7		iccssre	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
8	1 2 7	syl2anc	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
9		ax-resscn	⊢ ℝ ⊆ ℂ
10		cncfmptid	⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑧 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
11	8 9 10	sylancl	⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑧 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
12	6 11	eqeltrid	⊢ ( 𝜑 → ( I ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
13	6	eqcomi	⊢ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑧 ) = ( I ↾ ( 𝐴 [,] 𝐵 ) )
14	13	oveq2i	⊢ ( ℝ D ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑧 ) ) = ( ℝ D ( I ↾ ( 𝐴 [,] 𝐵 ) ) )
15		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
16	15	a1i	⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
17		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → 𝑧 ∈ ℝ )
18	17	recnd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → 𝑧 ∈ ℂ )
19		1red	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → 1 ∈ ℝ )
20	16	dvmptid	⊢ ( 𝜑 → ( ℝ D ( 𝑧 ∈ ℝ ↦ 𝑧 ) ) = ( 𝑧 ∈ ℝ ↦ 1 ) )
21		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
22	21	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
23		iccntr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
24	1 2 23	syl2anc	⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
25	16 18 19 20 8 22 21 24	dvmptres2	⊢ ( 𝜑 → ( ℝ D ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑧 ) ) = ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) )
26	14 25	eqtr3id	⊢ ( 𝜑 → ( ℝ D ( I ↾ ( 𝐴 [,] 𝐵 ) ) ) = ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) )
27	26	dmeqd	⊢ ( 𝜑 → dom ( ℝ D ( I ↾ ( 𝐴 [,] 𝐵 ) ) ) = dom ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) )
28		1ex	⊢ 1 ∈ V
29		eqid	⊢ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) = ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 )
30	28 29	dmmpti	⊢ dom ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) = ( 𝐴 (,) 𝐵 )
31	27 30	eqtrdi	⊢ ( 𝜑 → dom ( ℝ D ( I ↾ ( 𝐴 [,] 𝐵 ) ) ) = ( 𝐴 (,) 𝐵 ) )
32	1 2 3 4 12 5 31	cmvth	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D ( I ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑥 ) ) = ( ( ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) − ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
33	1	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
34	2	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
35	1 2 3	ltled	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
36		ubicc2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
37	33 34 35 36	syl3anc	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
38		fvresi	⊢ ( 𝐵 ∈ ( 𝐴 [,] 𝐵 ) → ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) = 𝐵 )
39	37 38	syl	⊢ ( 𝜑 → ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) = 𝐵 )
40		lbicc2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
41	33 34 35 40	syl3anc	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
42		fvresi	⊢ ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) → ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) = 𝐴 )
43	41 42	syl	⊢ ( 𝜑 → ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) = 𝐴 )
44	39 43	oveq12d	⊢ ( 𝜑 → ( ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) − ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) ) = ( 𝐵 − 𝐴 ) )
45	44	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) − ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) ) = ( 𝐵 − 𝐴 ) )
46	45	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) − ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) = ( ( 𝐵 − 𝐴 ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
47	26	fveq1d	⊢ ( 𝜑 → ( ( ℝ D ( I ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑥 ) = ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) ‘ 𝑥 ) )
48		eqidd	⊢ ( 𝑧 = 𝑥 → 1 = 1 )
49	48 29 28	fvmpt3i	⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) ‘ 𝑥 ) = 1 )
50	47 49	sylan9eq	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D ( I ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑥 ) = 1 )
51	50	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D ( I ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑥 ) ) = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · 1 ) )
52		cncff	⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
53	4 52	syl	⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
54	53 37	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ℝ )
55	53 41	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
56	54 55	resubcld	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ )
57	56	recnd	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℂ )
58	57	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℂ )
59	58	mulridd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · 1 ) = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )
60	51 59	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D ( I ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )
61	46 60	eqeq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) − ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D ( I ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑥 ) ) ↔ ( ( 𝐵 − 𝐴 ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ) )
62	2 1	resubcld	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
63	62	recnd	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℂ )
64	63	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐵 − 𝐴 ) ∈ ℂ )
65		dvf	⊢ ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ
66	5	feq2d	⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ ↔ ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) )
67	65 66	mpbii	⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
68	67	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
69	1 2	posdifd	⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
70	3 69	mpbid	⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
71	70	gt0ne0d	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≠ 0 )
72	71	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐵 − 𝐴 ) ≠ 0 )
73	58 64 68 72	divmuld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝐵 − 𝐴 ) ) = ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ↔ ( ( 𝐵 − 𝐴 ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ) )
74	61 73	bitr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) − ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D ( I ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑥 ) ) ↔ ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝐵 − 𝐴 ) ) = ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
75		eqcom	⊢ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D ( I ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑥 ) ) = ( ( ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) − ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ↔ ( ( ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) − ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D ( I ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑥 ) ) )
76		eqcom	⊢ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝐵 − 𝐴 ) ) ↔ ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝐵 − 𝐴 ) ) = ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
77	74 75 76	3bitr4g	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D ( I ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑥 ) ) = ( ( ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) − ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ↔ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝐵 − 𝐴 ) ) ) )
78	77	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D ( I ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑥 ) ) = ( ( ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) − ( ( I ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝐵 − 𝐴 ) ) ) )
79	32 78	mpbid	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) / ( 𝐵 − 𝐴 ) ) )