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 
|- ( ph -> A e. RR )
mvth.b 
|- ( ph -> B e. RR )
mvth.lt 
|- ( ph -> A < B )
mvth.f 
|- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
mvth.d 
|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
Assertion mvth 
|- ( ph -> E. x e. ( A (,) B ) ( ( RR _D F ) ` x ) = ( ( ( F ` B ) - ( F ` A ) ) / ( B - A ) ) )

Proof

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