Metamath Proof Explorer


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 ffvelrnd ( 𝜑 → ( 𝐹𝐵 ) ∈ ℝ )
55 53 41 ffvelrnd ( 𝜑 → ( 𝐹𝐴 ) ∈ ℝ )
56 54 55 resubcld ( 𝜑 → ( ( 𝐹𝐵 ) − ( 𝐹𝐴 ) ) ∈ ℝ )
57 56 recnd ( 𝜑 → ( ( 𝐹𝐵 ) − ( 𝐹𝐴 ) ) ∈ ℂ )
58 57 adantr ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹𝐵 ) − ( 𝐹𝐴 ) ) ∈ ℂ )
59 58 mulid1d ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝐹𝐵 ) − ( 𝐹𝐴 ) ) · 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 ffvelrnda ( ( 𝜑𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ 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 𝐹 ) ‘ 𝑥 ) = ( ( ( 𝐹𝐵 ) − ( 𝐹𝐴 ) ) / ( 𝐵𝐴 ) ) )