Metamath Proof Explorer

Theorem cmvth

Description: Cauchy's Mean Value Theorem. If F , G are real continuous functions on [ A , B ] differentiable on ( A , B ) , then there is some x e. ( A , B ) such that F ' ( x ) / G ' ( x ) = ( F ( A ) - F ( B ) ) / ( G ( A ) - G ( B ) ) . (We express the condition without division, so that we need no nonzero constraints.) (Contributed by Mario Carneiro, 29-Dec-2016) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypotheses cmvth.a 
|- ( ph -> A e. RR )
cmvth.b 
|- ( ph -> B e. RR )
cmvth.lt 
|- ( ph -> A < B )
cmvth.f 
|- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
cmvth.g 
|- ( ph -> G e. ( ( A [,] B ) -cn-> RR ) )
cmvth.df 
|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
cmvth.dg 
|- ( ph -> dom ( RR _D G ) = ( A (,) B ) )
Assertion cmvth 
|- ( ph -> E. x e. ( A (,) B ) ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` x ) ) = ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` x ) ) )

Proof

Step Hyp Ref Expression
1 cmvth.a 
 |-  ( ph -> A e. RR )
2 cmvth.b 
 |-  ( ph -> B e. RR )
3 cmvth.lt 
 |-  ( ph -> A < B )
4 cmvth.f 
 |-  ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
5 cmvth.g 
 |-  ( ph -> G e. ( ( A [,] B ) -cn-> RR ) )
6 cmvth.df 
 |-  ( ph -> dom ( RR _D F ) = ( A (,) B ) )
7 cmvth.dg 
 |-  ( ph -> dom ( RR _D G ) = ( A (,) B ) )
8 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
9 8 subcn 
 |-  - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
10 cncff 
 |-  ( F e. ( ( A [,] B ) -cn-> RR ) -> F : ( A [,] B ) --> RR )
11 4 10 syl 
 |-  ( ph -> F : ( A [,] B ) --> RR )
12 1 rexrd 
 |-  ( ph -> A e. RR* )
13 2 rexrd 
 |-  ( ph -> B e. RR* )
14 1 2 3 ltled 
 |-  ( ph -> A <_ B )
15 ubicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
16 12 13 14 15 syl3anc 
 |-  ( ph -> B e. ( A [,] B ) )
17 11 16 ffvelcdmd 
 |-  ( ph -> ( F ` B ) e. RR )
18 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
19 12 13 14 18 syl3anc 
 |-  ( ph -> A e. ( A [,] B ) )
20 11 19 ffvelcdmd 
 |-  ( ph -> ( F ` A ) e. RR )
21 17 20 resubcld 
 |-  ( ph -> ( ( F ` B ) - ( F ` A ) ) e. RR )
22 21 recnd 
 |-  ( ph -> ( ( F ` B ) - ( F ` A ) ) e. CC )
23 22 adantr 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( ( F ` B ) - ( F ` A ) ) e. CC )
24 cncff 
 |-  ( G e. ( ( A [,] B ) -cn-> RR ) -> G : ( A [,] B ) --> RR )
25 5 24 syl 
 |-  ( ph -> G : ( A [,] B ) --> RR )
26 25 ffvelcdmda 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( G ` z ) e. RR )
27 26 recnd 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( G ` z ) e. CC )
28 ovmpot 
 |-  ( ( ( ( F ` B ) - ( F ` A ) ) e. CC /\ ( G ` z ) e. CC ) -> ( ( ( F ` B ) - ( F ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( G ` z ) ) = ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) )
29 23 27 28 syl2anc 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( ( ( F ` B ) - ( F ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( G ` z ) ) = ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) )
30 29 eqeq2d 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( w = ( ( ( F ` B ) - ( F ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( G ` z ) ) <-> w = ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) ) )
31 30 pm5.32da 
 |-  ( ph -> ( ( z e. ( A [,] B ) /\ w = ( ( ( F ` B ) - ( F ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( G ` z ) ) ) <-> ( z e. ( A [,] B ) /\ w = ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) ) ) )
32 31 opabbidv 
 |-  ( ph -> { <. z , w >. | ( z e. ( A [,] B ) /\ w = ( ( ( F ` B ) - ( F ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( G ` z ) ) ) } = { <. z , w >. | ( z e. ( A [,] B ) /\ w = ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) ) } )
33 df-mpt 
 |-  ( z e. ( A [,] B ) |-> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) ) = { <. z , w >. | ( z e. ( A [,] B ) /\ w = ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) ) }
34 32 33 eqtr4di 
 |-  ( ph -> { <. z , w >. | ( z e. ( A [,] B ) /\ w = ( ( ( F ` B ) - ( F ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( G ` z ) ) ) } = ( z e. ( A [,] B ) |-> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) ) )
35 df-mpt 
 |-  ( z e. ( A [,] B ) |-> ( ( ( F ` B ) - ( F ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( G ` z ) ) ) = { <. z , w >. | ( z e. ( A [,] B ) /\ w = ( ( ( F ` B ) - ( F ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( G ` z ) ) ) }
36 8 mpomulcn 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
37 1 2 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
38 ax-resscn 
 |-  RR C_ CC
39 37 38 sstrdi 
 |-  ( ph -> ( A [,] B ) C_ CC )
40 38 a1i 
 |-  ( ph -> RR C_ CC )
41 cncfmptc 
 |-  ( ( ( ( F ` B ) - ( F ` A ) ) e. RR /\ ( A [,] B ) C_ CC /\ RR C_ CC ) -> ( z e. ( A [,] B ) |-> ( ( F ` B ) - ( F ` A ) ) ) e. ( ( A [,] B ) -cn-> RR ) )
42 21 39 40 41 syl3anc 
 |-  ( ph -> ( z e. ( A [,] B ) |-> ( ( F ` B ) - ( F ` A ) ) ) e. ( ( A [,] B ) -cn-> RR ) )
43 25 feqmptd 
 |-  ( ph -> G = ( z e. ( A [,] B ) |-> ( G ` z ) ) )
44 43 5 eqeltrrd 
 |-  ( ph -> ( z e. ( A [,] B ) |-> ( G ` z ) ) e. ( ( A [,] B ) -cn-> RR ) )
45 simpl 
 |-  ( ( ( ( F ` B ) - ( F ` A ) ) e. RR /\ ( G ` z ) e. RR ) -> ( ( F ` B ) - ( F ` A ) ) e. RR )
46 45 recnd 
 |-  ( ( ( ( F ` B ) - ( F ` A ) ) e. RR /\ ( G ` z ) e. RR ) -> ( ( F ` B ) - ( F ` A ) ) e. CC )
47 simpr 
 |-  ( ( ( ( F ` B ) - ( F ` A ) ) e. RR /\ ( G ` z ) e. RR ) -> ( G ` z ) e. RR )
48 47 recnd 
 |-  ( ( ( ( F ` B ) - ( F ` A ) ) e. RR /\ ( G ` z ) e. RR ) -> ( G ` z ) e. CC )
49 28 eqcomd 
 |-  ( ( ( ( F ` B ) - ( F ` A ) ) e. CC /\ ( G ` z ) e. CC ) -> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) = ( ( ( F ` B ) - ( F ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( G ` z ) ) )
50 46 48 49 syl2anc 
 |-  ( ( ( ( F ` B ) - ( F ` A ) ) e. RR /\ ( G ` z ) e. RR ) -> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) = ( ( ( F ` B ) - ( F ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( G ` z ) ) )
51 remulcl 
 |-  ( ( ( ( F ` B ) - ( F ` A ) ) e. RR /\ ( G ` z ) e. RR ) -> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) e. RR )
52 50 51 eqeltrrd 
 |-  ( ( ( ( F ` B ) - ( F ` A ) ) e. RR /\ ( G ` z ) e. RR ) -> ( ( ( F ` B ) - ( F ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( G ` z ) ) e. RR )
53 8 36 42 44 38 52 cncfmpt2ss 
 |-  ( ph -> ( z e. ( A [,] B ) |-> ( ( ( F ` B ) - ( F ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( G ` z ) ) ) e. ( ( A [,] B ) -cn-> RR ) )
54 35 53 eqeltrrid 
 |-  ( ph -> { <. z , w >. | ( z e. ( A [,] B ) /\ w = ( ( ( F ` B ) - ( F ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( G ` z ) ) ) } e. ( ( A [,] B ) -cn-> RR ) )
55 34 54 eqeltrrd 
 |-  ( ph -> ( z e. ( A [,] B ) |-> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) ) e. ( ( A [,] B ) -cn-> RR ) )
56 25 16 ffvelcdmd 
 |-  ( ph -> ( G ` B ) e. RR )
57 25 19 ffvelcdmd 
 |-  ( ph -> ( G ` A ) e. RR )
58 56 57 resubcld 
 |-  ( ph -> ( ( G ` B ) - ( G ` A ) ) e. RR )
59 58 adantr 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( ( G ` B ) - ( G ` A ) ) e. RR )
60 59 recnd 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( ( G ` B ) - ( G ` A ) ) e. CC )
61 11 ffvelcdmda 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( F ` z ) e. RR )
62 61 recnd 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( F ` z ) e. CC )
63 ovmpot 
 |-  ( ( ( ( G ` B ) - ( G ` A ) ) e. CC /\ ( F ` z ) e. CC ) -> ( ( ( G ` B ) - ( G ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( F ` z ) ) = ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) )
64 60 62 63 syl2anc 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( ( ( G ` B ) - ( G ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( F ` z ) ) = ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) )
65 64 eqeq2d 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( w = ( ( ( G ` B ) - ( G ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( F ` z ) ) <-> w = ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) )
66 65 pm5.32da 
 |-  ( ph -> ( ( z e. ( A [,] B ) /\ w = ( ( ( G ` B ) - ( G ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( F ` z ) ) ) <-> ( z e. ( A [,] B ) /\ w = ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) )
67 66 opabbidv 
 |-  ( ph -> { <. z , w >. | ( z e. ( A [,] B ) /\ w = ( ( ( G ` B ) - ( G ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( F ` z ) ) ) } = { <. z , w >. | ( z e. ( A [,] B ) /\ w = ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) } )
68 df-mpt 
 |-  ( z e. ( A [,] B ) |-> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) = { <. z , w >. | ( z e. ( A [,] B ) /\ w = ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) }
69 67 68 eqtr4di 
 |-  ( ph -> { <. z , w >. | ( z e. ( A [,] B ) /\ w = ( ( ( G ` B ) - ( G ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( F ` z ) ) ) } = ( z e. ( A [,] B ) |-> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) )
70 df-mpt 
 |-  ( z e. ( A [,] B ) |-> ( ( ( G ` B ) - ( G ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( F ` z ) ) ) = { <. z , w >. | ( z e. ( A [,] B ) /\ w = ( ( ( G ` B ) - ( G ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( F ` z ) ) ) }
71 cncfmptc 
 |-  ( ( ( ( G ` B ) - ( G ` A ) ) e. RR /\ ( A [,] B ) C_ CC /\ RR C_ CC ) -> ( z e. ( A [,] B ) |-> ( ( G ` B ) - ( G ` A ) ) ) e. ( ( A [,] B ) -cn-> RR ) )
72 58 39 40 71 syl3anc 
 |-  ( ph -> ( z e. ( A [,] B ) |-> ( ( G ` B ) - ( G ` A ) ) ) e. ( ( A [,] B ) -cn-> RR ) )
73 11 feqmptd 
 |-  ( ph -> F = ( z e. ( A [,] B ) |-> ( F ` z ) ) )
74 73 4 eqeltrrd 
 |-  ( ph -> ( z e. ( A [,] B ) |-> ( F ` z ) ) e. ( ( A [,] B ) -cn-> RR ) )
75 simpl 
 |-  ( ( ( ( G ` B ) - ( G ` A ) ) e. RR /\ ( F ` z ) e. RR ) -> ( ( G ` B ) - ( G ` A ) ) e. RR )
76 75 recnd 
 |-  ( ( ( ( G ` B ) - ( G ` A ) ) e. RR /\ ( F ` z ) e. RR ) -> ( ( G ` B ) - ( G ` A ) ) e. CC )
77 simpr 
 |-  ( ( ( ( G ` B ) - ( G ` A ) ) e. RR /\ ( F ` z ) e. RR ) -> ( F ` z ) e. RR )
78 77 recnd 
 |-  ( ( ( ( G ` B ) - ( G ` A ) ) e. RR /\ ( F ` z ) e. RR ) -> ( F ` z ) e. CC )
79 63 eqcomd 
 |-  ( ( ( ( G ` B ) - ( G ` A ) ) e. CC /\ ( F ` z ) e. CC ) -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) = ( ( ( G ` B ) - ( G ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( F ` z ) ) )
80 76 78 79 syl2anc 
 |-  ( ( ( ( G ` B ) - ( G ` A ) ) e. RR /\ ( F ` z ) e. RR ) -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) = ( ( ( G ` B ) - ( G ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( F ` z ) ) )
81 remulcl 
 |-  ( ( ( ( G ` B ) - ( G ` A ) ) e. RR /\ ( F ` z ) e. RR ) -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) e. RR )
82 80 81 eqeltrrd 
 |-  ( ( ( ( G ` B ) - ( G ` A ) ) e. RR /\ ( F ` z ) e. RR ) -> ( ( ( G ` B ) - ( G ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( F ` z ) ) e. RR )
83 8 36 72 74 38 82 cncfmpt2ss 
 |-  ( ph -> ( z e. ( A [,] B ) |-> ( ( ( G ` B ) - ( G ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( F ` z ) ) ) e. ( ( A [,] B ) -cn-> RR ) )
84 70 83 eqeltrrid 
 |-  ( ph -> { <. z , w >. | ( z e. ( A [,] B ) /\ w = ( ( ( G ` B ) - ( G ` A ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( F ` z ) ) ) } e. ( ( A [,] B ) -cn-> RR ) )
85 69 84 eqeltrrd 
 |-  ( ph -> ( z e. ( A [,] B ) |-> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) e. ( ( A [,] B ) -cn-> RR ) )
86 resubcl 
 |-  ( ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) e. RR /\ ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) e. RR ) -> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) e. RR )
87 8 9 55 85 38 86 cncfmpt2ss 
 |-  ( ph -> ( z e. ( A [,] B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) e. ( ( A [,] B ) -cn-> RR ) )
88 23 27 mulcld 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) e. CC )
89 59 61 remulcld 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) e. RR )
90 89 recnd 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) e. CC )
91 88 90 subcld 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) e. CC )
92 8 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
93 iccntr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
94 1 2 93 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
95 40 37 91 92 8 94 dvmptntr 
 |-  ( ph -> ( RR _D ( z e. ( A [,] B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) ) = ( RR _D ( z e. ( A (,) B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) ) )
96 reelprrecn 
 |-  RR e. { RR , CC }
97 96 a1i 
 |-  ( ph -> RR e. { RR , CC } )
98 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
99 98 sseli 
 |-  ( z e. ( A (,) B ) -> z e. ( A [,] B ) )
100 99 88 sylan2 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) e. CC )
101 ovexd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` z ) ) e. _V )
102 99 27 sylan2 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( G ` z ) e. CC )
103 fvexd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( RR _D G ) ` z ) e. _V )
104 43 oveq2d 
 |-  ( ph -> ( RR _D G ) = ( RR _D ( z e. ( A [,] B ) |-> ( G ` z ) ) ) )
105 dvf 
 |-  ( RR _D G ) : dom ( RR _D G ) --> CC
106 7 feq2d 
 |-  ( ph -> ( ( RR _D G ) : dom ( RR _D G ) --> CC <-> ( RR _D G ) : ( A (,) B ) --> CC ) )
107 105 106 mpbii 
 |-  ( ph -> ( RR _D G ) : ( A (,) B ) --> CC )
108 107 feqmptd 
 |-  ( ph -> ( RR _D G ) = ( z e. ( A (,) B ) |-> ( ( RR _D G ) ` z ) ) )
109 40 37 27 92 8 94 dvmptntr 
 |-  ( ph -> ( RR _D ( z e. ( A [,] B ) |-> ( G ` z ) ) ) = ( RR _D ( z e. ( A (,) B ) |-> ( G ` z ) ) ) )
110 104 108 109 3eqtr3rd 
 |-  ( ph -> ( RR _D ( z e. ( A (,) B ) |-> ( G ` z ) ) ) = ( z e. ( A (,) B ) |-> ( ( RR _D G ) ` z ) ) )
111 97 102 103 110 22 dvmptcmul 
 |-  ( ph -> ( RR _D ( z e. ( A (,) B ) |-> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) ) ) = ( z e. ( A (,) B ) |-> ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` z ) ) ) )
112 99 90 sylan2 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) e. CC )
113 ovexd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` z ) ) e. _V )
114 99 62 sylan2 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( F ` z ) e. CC )
115 fvexd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( RR _D F ) ` z ) e. _V )
116 73 oveq2d 
 |-  ( ph -> ( RR _D F ) = ( RR _D ( z e. ( A [,] B ) |-> ( F ` z ) ) ) )
117 dvf 
 |-  ( RR _D F ) : dom ( RR _D F ) --> CC
118 6 feq2d 
 |-  ( ph -> ( ( RR _D F ) : dom ( RR _D F ) --> CC <-> ( RR _D F ) : ( A (,) B ) --> CC ) )
119 117 118 mpbii 
 |-  ( ph -> ( RR _D F ) : ( A (,) B ) --> CC )
120 119 feqmptd 
 |-  ( ph -> ( RR _D F ) = ( z e. ( A (,) B ) |-> ( ( RR _D F ) ` z ) ) )
121 40 37 62 92 8 94 dvmptntr 
 |-  ( ph -> ( RR _D ( z e. ( A [,] B ) |-> ( F ` z ) ) ) = ( RR _D ( z e. ( A (,) B ) |-> ( F ` z ) ) ) )
122 116 120 121 3eqtr3rd 
 |-  ( ph -> ( RR _D ( z e. ( A (,) B ) |-> ( F ` z ) ) ) = ( z e. ( A (,) B ) |-> ( ( RR _D F ) ` z ) ) )
123 58 recnd 
 |-  ( ph -> ( ( G ` B ) - ( G ` A ) ) e. CC )
124 97 114 115 122 123 dvmptcmul 
 |-  ( ph -> ( RR _D ( z e. ( A (,) B ) |-> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) = ( z e. ( A (,) B ) |-> ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` z ) ) ) )
125 97 100 101 111 112 113 124 dvmptsub 
 |-  ( ph -> ( RR _D ( z e. ( A (,) B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) ) = ( z e. ( A (,) B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` z ) ) ) ) )
126 95 125 eqtrd 
 |-  ( ph -> ( RR _D ( z e. ( A [,] B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) ) = ( z e. ( A (,) B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` z ) ) ) ) )
127 126 dmeqd 
 |-  ( ph -> dom ( RR _D ( z e. ( A [,] B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) ) = dom ( z e. ( A (,) B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` z ) ) ) ) )
128 ovex 
 |-  ( ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` z ) ) ) e. _V
129 eqid 
 |-  ( z e. ( A (,) B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` z ) ) ) ) = ( z e. ( A (,) B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` z ) ) ) )
130 128 129 dmmpti 
 |-  dom ( z e. ( A (,) B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` z ) ) ) ) = ( A (,) B )
131 127 130 eqtrdi 
 |-  ( ph -> dom ( RR _D ( z e. ( A [,] B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) ) = ( A (,) B ) )
132 17 recnd 
 |-  ( ph -> ( F ` B ) e. CC )
133 57 recnd 
 |-  ( ph -> ( G ` A ) e. CC )
134 132 133 mulcld 
 |-  ( ph -> ( ( F ` B ) x. ( G ` A ) ) e. CC )
135 20 recnd 
 |-  ( ph -> ( F ` A ) e. CC )
136 56 recnd 
 |-  ( ph -> ( G ` B ) e. CC )
137 135 136 mulcld 
 |-  ( ph -> ( ( F ` A ) x. ( G ` B ) ) e. CC )
138 135 133 mulcld 
 |-  ( ph -> ( ( F ` A ) x. ( G ` A ) ) e. CC )
139 134 137 138 nnncan2d 
 |-  ( ph -> ( ( ( ( F ` B ) x. ( G ` A ) ) - ( ( F ` A ) x. ( G ` A ) ) ) - ( ( ( F ` A ) x. ( G ` B ) ) - ( ( F ` A ) x. ( G ` A ) ) ) ) = ( ( ( F ` B ) x. ( G ` A ) ) - ( ( F ` A ) x. ( G ` B ) ) ) )
140 132 136 mulcld 
 |-  ( ph -> ( ( F ` B ) x. ( G ` B ) ) e. CC )
141 140 137 134 nnncan1d 
 |-  ( ph -> ( ( ( ( F ` B ) x. ( G ` B ) ) - ( ( F ` A ) x. ( G ` B ) ) ) - ( ( ( F ` B ) x. ( G ` B ) ) - ( ( F ` B ) x. ( G ` A ) ) ) ) = ( ( ( F ` B ) x. ( G ` A ) ) - ( ( F ` A ) x. ( G ` B ) ) ) )
142 139 141 eqtr4d 
 |-  ( ph -> ( ( ( ( F ` B ) x. ( G ` A ) ) - ( ( F ` A ) x. ( G ` A ) ) ) - ( ( ( F ` A ) x. ( G ` B ) ) - ( ( F ` A ) x. ( G ` A ) ) ) ) = ( ( ( ( F ` B ) x. ( G ` B ) ) - ( ( F ` A ) x. ( G ` B ) ) ) - ( ( ( F ` B ) x. ( G ` B ) ) - ( ( F ` B ) x. ( G ` A ) ) ) ) )
143 132 135 133 subdird 
 |-  ( ph -> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` A ) ) = ( ( ( F ` B ) x. ( G ` A ) ) - ( ( F ` A ) x. ( G ` A ) ) ) )
144 123 135 mulcomd 
 |-  ( ph -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` A ) ) = ( ( F ` A ) x. ( ( G ` B ) - ( G ` A ) ) ) )
145 135 136 133 subdid 
 |-  ( ph -> ( ( F ` A ) x. ( ( G ` B ) - ( G ` A ) ) ) = ( ( ( F ` A ) x. ( G ` B ) ) - ( ( F ` A ) x. ( G ` A ) ) ) )
146 144 145 eqtrd 
 |-  ( ph -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` A ) ) = ( ( ( F ` A ) x. ( G ` B ) ) - ( ( F ` A ) x. ( G ` A ) ) ) )
147 143 146 oveq12d 
 |-  ( ph -> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` A ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` A ) ) ) = ( ( ( ( F ` B ) x. ( G ` A ) ) - ( ( F ` A ) x. ( G ` A ) ) ) - ( ( ( F ` A ) x. ( G ` B ) ) - ( ( F ` A ) x. ( G ` A ) ) ) ) )
148 132 135 136 subdird 
 |-  ( ph -> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` B ) ) = ( ( ( F ` B ) x. ( G ` B ) ) - ( ( F ` A ) x. ( G ` B ) ) ) )
149 123 132 mulcomd 
 |-  ( ph -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` B ) ) = ( ( F ` B ) x. ( ( G ` B ) - ( G ` A ) ) ) )
150 132 136 133 subdid 
 |-  ( ph -> ( ( F ` B ) x. ( ( G ` B ) - ( G ` A ) ) ) = ( ( ( F ` B ) x. ( G ` B ) ) - ( ( F ` B ) x. ( G ` A ) ) ) )
151 149 150 eqtrd 
 |-  ( ph -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` B ) ) = ( ( ( F ` B ) x. ( G ` B ) ) - ( ( F ` B ) x. ( G ` A ) ) ) )
152 148 151 oveq12d 
 |-  ( ph -> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` B ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` B ) ) ) = ( ( ( ( F ` B ) x. ( G ` B ) ) - ( ( F ` A ) x. ( G ` B ) ) ) - ( ( ( F ` B ) x. ( G ` B ) ) - ( ( F ` B ) x. ( G ` A ) ) ) ) )
153 142 147 152 3eqtr4d 
 |-  ( ph -> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` A ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` A ) ) ) = ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` B ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` B ) ) ) )
154 fveq2 
 |-  ( z = A -> ( G ` z ) = ( G ` A ) )
155 154 oveq2d 
 |-  ( z = A -> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) = ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` A ) ) )
156 fveq2 
 |-  ( z = A -> ( F ` z ) = ( F ` A ) )
157 156 oveq2d 
 |-  ( z = A -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) = ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` A ) ) )
158 155 157 oveq12d 
 |-  ( z = A -> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) = ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` A ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` A ) ) ) )
159 eqid 
 |-  ( z e. ( A [,] B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) = ( z e. ( A [,] B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) )
160 ovex 
 |-  ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) e. _V
161 158 159 160 fvmpt3i 
 |-  ( A e. ( A [,] B ) -> ( ( z e. ( A [,] B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) ` A ) = ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` A ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` A ) ) ) )
162 19 161 syl 
 |-  ( ph -> ( ( z e. ( A [,] B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) ` A ) = ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` A ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` A ) ) ) )
163 fveq2 
 |-  ( z = B -> ( G ` z ) = ( G ` B ) )
164 163 oveq2d 
 |-  ( z = B -> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) = ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` B ) ) )
165 fveq2 
 |-  ( z = B -> ( F ` z ) = ( F ` B ) )
166 165 oveq2d 
 |-  ( z = B -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) = ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` B ) ) )
167 164 166 oveq12d 
 |-  ( z = B -> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) = ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` B ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` B ) ) ) )
168 167 159 160 fvmpt3i 
 |-  ( B e. ( A [,] B ) -> ( ( z e. ( A [,] B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) ` B ) = ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` B ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` B ) ) ) )
169 16 168 syl 
 |-  ( ph -> ( ( z e. ( A [,] B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) ` B ) = ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` B ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` B ) ) ) )
170 153 162 169 3eqtr4d 
 |-  ( ph -> ( ( z e. ( A [,] B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) ` A ) = ( ( z e. ( A [,] B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) ` B ) )
171 1 2 3 87 131 170 rolle 
 |-  ( ph -> E. x e. ( A (,) B ) ( ( RR _D ( z e. ( A [,] B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) ) ` x ) = 0 )
172 126 fveq1d 
 |-  ( ph -> ( ( RR _D ( z e. ( A [,] B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) ) ` x ) = ( ( z e. ( A (,) B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` z ) ) ) ) ` x ) )
173 fveq2 
 |-  ( z = x -> ( ( RR _D G ) ` z ) = ( ( RR _D G ) ` x ) )
174 173 oveq2d 
 |-  ( z = x -> ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` z ) ) = ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` x ) ) )
175 fveq2 
 |-  ( z = x -> ( ( RR _D F ) ` z ) = ( ( RR _D F ) ` x ) )
176 175 oveq2d 
 |-  ( z = x -> ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` z ) ) = ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` x ) ) )
177 174 176 oveq12d 
 |-  ( z = x -> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` z ) ) ) = ( ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` x ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` x ) ) ) )
178 177 129 128 fvmpt3i 
 |-  ( x e. ( A (,) B ) -> ( ( z e. ( A (,) B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` z ) ) ) ) ` x ) = ( ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` x ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` x ) ) ) )
179 172 178 sylan9eq 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D ( z e. ( A [,] B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) ) ` x ) = ( ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` x ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` x ) ) ) )
180 179 eqeq1d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( RR _D ( z e. ( A [,] B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) ) ` x ) = 0 <-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` x ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` x ) ) ) = 0 ) )
181 22 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( F ` B ) - ( F ` A ) ) e. CC )
182 107 ffvelcdmda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D G ) ` x ) e. CC )
183 181 182 mulcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` x ) ) e. CC )
184 123 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( G ` B ) - ( G ` A ) ) e. CC )
185 119 ffvelcdmda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. CC )
186 184 185 mulcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` x ) ) e. CC )
187 183 186 subeq0ad 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` x ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` x ) ) ) = 0 <-> ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` x ) ) = ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` x ) ) ) )
188 180 187 bitrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( RR _D ( z e. ( A [,] B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) ) ` x ) = 0 <-> ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` x ) ) = ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` x ) ) ) )
189 188 rexbidva 
 |-  ( ph -> ( E. x e. ( A (,) B ) ( ( RR _D ( z e. ( A [,] B ) |-> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) ) ) ` x ) = 0 <-> E. x e. ( A (,) B ) ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` x ) ) = ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` x ) ) ) )
190 171 189 mpbid 
 |-  ( ph -> E. x e. ( A (,) B ) ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` x ) ) = ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` x ) ) )