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)

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 8 mulcn 
 |-  x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
11 cncff 
 |-  ( F e. ( ( A [,] B ) -cn-> RR ) -> F : ( A [,] B ) --> RR )
12 4 11 syl 
 |-  ( ph -> F : ( A [,] B ) --> RR )
13 1 rexrd 
 |-  ( ph -> A e. RR* )
14 2 rexrd 
 |-  ( ph -> B e. RR* )
15 1 2 3 ltled 
 |-  ( ph -> A <_ B )
16 ubicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
17 13 14 15 16 syl3anc 
 |-  ( ph -> B e. ( A [,] B ) )
18 12 17 ffvelcdmd 
 |-  ( ph -> ( F ` B ) e. RR )
19 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
20 13 14 15 19 syl3anc 
 |-  ( ph -> A e. ( A [,] B ) )
21 12 20 ffvelcdmd 
 |-  ( ph -> ( F ` A ) e. RR )
22 18 21 resubcld 
 |-  ( ph -> ( ( F ` B ) - ( F ` A ) ) e. RR )
23 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
24 1 2 23 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
25 ax-resscn 
 |-  RR C_ CC
26 24 25 sstrdi 
 |-  ( ph -> ( A [,] B ) C_ CC )
27 25 a1i 
 |-  ( ph -> RR C_ CC )
28 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 ) )
29 22 26 27 28 syl3anc 
 |-  ( ph -> ( z e. ( A [,] B ) |-> ( ( F ` B ) - ( F ` A ) ) ) e. ( ( A [,] B ) -cn-> RR ) )
30 cncff 
 |-  ( G e. ( ( A [,] B ) -cn-> RR ) -> G : ( A [,] B ) --> RR )
31 5 30 syl 
 |-  ( ph -> G : ( A [,] B ) --> RR )
32 31 feqmptd 
 |-  ( ph -> G = ( z e. ( A [,] B ) |-> ( G ` z ) ) )
33 32 5 eqeltrrd 
 |-  ( ph -> ( z e. ( A [,] B ) |-> ( G ` z ) ) e. ( ( A [,] B ) -cn-> RR ) )
34 remulcl 
 |-  ( ( ( ( F ` B ) - ( F ` A ) ) e. RR /\ ( G ` z ) e. RR ) -> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) e. RR )
35 8 10 29 33 25 34 cncfmpt2ss 
 |-  ( ph -> ( z e. ( A [,] B ) |-> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) ) e. ( ( A [,] B ) -cn-> RR ) )
36 31 17 ffvelcdmd 
 |-  ( ph -> ( G ` B ) e. RR )
37 31 20 ffvelcdmd 
 |-  ( ph -> ( G ` A ) e. RR )
38 36 37 resubcld 
 |-  ( ph -> ( ( G ` B ) - ( G ` A ) ) e. RR )
39 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 ) )
40 38 26 27 39 syl3anc 
 |-  ( ph -> ( z e. ( A [,] B ) |-> ( ( G ` B ) - ( G ` A ) ) ) e. ( ( A [,] B ) -cn-> RR ) )
41 12 feqmptd 
 |-  ( ph -> F = ( z e. ( A [,] B ) |-> ( F ` z ) ) )
42 41 4 eqeltrrd 
 |-  ( ph -> ( z e. ( A [,] B ) |-> ( F ` z ) ) e. ( ( A [,] B ) -cn-> RR ) )
43 remulcl 
 |-  ( ( ( ( G ` B ) - ( G ` A ) ) e. RR /\ ( F ` z ) e. RR ) -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) e. RR )
44 8 10 40 42 25 43 cncfmpt2ss 
 |-  ( ph -> ( z e. ( A [,] B ) |-> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) e. ( ( A [,] B ) -cn-> RR ) )
45 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 )
46 8 9 35 44 25 45 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 ) )
47 22 recnd 
 |-  ( ph -> ( ( F ` B ) - ( F ` A ) ) e. CC )
48 47 adantr 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( ( F ` B ) - ( F ` A ) ) e. CC )
49 31 ffvelcdmda 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( G ` z ) e. RR )
50 49 recnd 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( G ` z ) e. CC )
51 48 50 mulcld 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) e. CC )
52 38 adantr 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( ( G ` B ) - ( G ` A ) ) e. RR )
53 12 ffvelcdmda 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( F ` z ) e. RR )
54 52 53 remulcld 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) e. RR )
55 54 recnd 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) e. CC )
56 51 55 subcld 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) e. CC )
57 8 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
58 iccntr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
59 1 2 58 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
60 27 24 56 57 8 59 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 ) ) ) ) ) )
61 reelprrecn 
 |-  RR e. { RR , CC }
62 61 a1i 
 |-  ( ph -> RR e. { RR , CC } )
63 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
64 63 sseli 
 |-  ( z e. ( A (,) B ) -> z e. ( A [,] B ) )
65 64 51 sylan2 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) e. CC )
66 ovex 
 |-  ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` z ) ) e. _V
67 66 a1i 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` z ) ) e. _V )
68 64 50 sylan2 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( G ` z ) e. CC )
69 fvexd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( RR _D G ) ` z ) e. _V )
70 32 oveq2d 
 |-  ( ph -> ( RR _D G ) = ( RR _D ( z e. ( A [,] B ) |-> ( G ` z ) ) ) )
71 dvf 
 |-  ( RR _D G ) : dom ( RR _D G ) --> CC
72 7 feq2d 
 |-  ( ph -> ( ( RR _D G ) : dom ( RR _D G ) --> CC <-> ( RR _D G ) : ( A (,) B ) --> CC ) )
73 71 72 mpbii 
 |-  ( ph -> ( RR _D G ) : ( A (,) B ) --> CC )
74 73 feqmptd 
 |-  ( ph -> ( RR _D G ) = ( z e. ( A (,) B ) |-> ( ( RR _D G ) ` z ) ) )
75 27 24 50 57 8 59 dvmptntr 
 |-  ( ph -> ( RR _D ( z e. ( A [,] B ) |-> ( G ` z ) ) ) = ( RR _D ( z e. ( A (,) B ) |-> ( G ` z ) ) ) )
76 70 74 75 3eqtr3rd 
 |-  ( ph -> ( RR _D ( z e. ( A (,) B ) |-> ( G ` z ) ) ) = ( z e. ( A (,) B ) |-> ( ( RR _D G ) ` z ) ) )
77 62 68 69 76 47 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 ) ) ) )
78 64 55 sylan2 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) e. CC )
79 ovex 
 |-  ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` z ) ) e. _V
80 79 a1i 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` z ) ) e. _V )
81 53 recnd 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( F ` z ) e. CC )
82 64 81 sylan2 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( F ` z ) e. CC )
83 fvexd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( ( RR _D F ) ` z ) e. _V )
84 41 oveq2d 
 |-  ( ph -> ( RR _D F ) = ( RR _D ( z e. ( A [,] B ) |-> ( F ` z ) ) ) )
85 dvf 
 |-  ( RR _D F ) : dom ( RR _D F ) --> CC
86 6 feq2d 
 |-  ( ph -> ( ( RR _D F ) : dom ( RR _D F ) --> CC <-> ( RR _D F ) : ( A (,) B ) --> CC ) )
87 85 86 mpbii 
 |-  ( ph -> ( RR _D F ) : ( A (,) B ) --> CC )
88 87 feqmptd 
 |-  ( ph -> ( RR _D F ) = ( z e. ( A (,) B ) |-> ( ( RR _D F ) ` z ) ) )
89 27 24 81 57 8 59 dvmptntr 
 |-  ( ph -> ( RR _D ( z e. ( A [,] B ) |-> ( F ` z ) ) ) = ( RR _D ( z e. ( A (,) B ) |-> ( F ` z ) ) ) )
90 84 88 89 3eqtr3rd 
 |-  ( ph -> ( RR _D ( z e. ( A (,) B ) |-> ( F ` z ) ) ) = ( z e. ( A (,) B ) |-> ( ( RR _D F ) ` z ) ) )
91 38 recnd 
 |-  ( ph -> ( ( G ` B ) - ( G ` A ) ) e. CC )
92 62 82 83 90 91 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 ) ) ) )
93 62 65 67 77 78 80 92 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 ) ) ) ) )
94 60 93 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 ) ) ) ) )
95 94 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 ) ) ) ) )
96 ovex 
 |-  ( ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` z ) ) ) e. _V
97 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 ) ) ) )
98 96 97 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 )
99 95 98 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 ) )
100 18 recnd 
 |-  ( ph -> ( F ` B ) e. CC )
101 37 recnd 
 |-  ( ph -> ( G ` A ) e. CC )
102 100 101 mulcld 
 |-  ( ph -> ( ( F ` B ) x. ( G ` A ) ) e. CC )
103 21 recnd 
 |-  ( ph -> ( F ` A ) e. CC )
104 36 recnd 
 |-  ( ph -> ( G ` B ) e. CC )
105 103 104 mulcld 
 |-  ( ph -> ( ( F ` A ) x. ( G ` B ) ) e. CC )
106 103 101 mulcld 
 |-  ( ph -> ( ( F ` A ) x. ( G ` A ) ) e. CC )
107 102 105 106 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 ) ) ) )
108 100 104 mulcld 
 |-  ( ph -> ( ( F ` B ) x. ( G ` B ) ) e. CC )
109 108 105 102 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 ) ) ) )
110 107 109 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 ) ) ) ) )
111 100 103 101 subdird 
 |-  ( ph -> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` A ) ) = ( ( ( F ` B ) x. ( G ` A ) ) - ( ( F ` A ) x. ( G ` A ) ) ) )
112 91 103 mulcomd 
 |-  ( ph -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` A ) ) = ( ( F ` A ) x. ( ( G ` B ) - ( G ` A ) ) ) )
113 103 104 101 subdid 
 |-  ( ph -> ( ( F ` A ) x. ( ( G ` B ) - ( G ` A ) ) ) = ( ( ( F ` A ) x. ( G ` B ) ) - ( ( F ` A ) x. ( G ` A ) ) ) )
114 112 113 eqtrd 
 |-  ( ph -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` A ) ) = ( ( ( F ` A ) x. ( G ` B ) ) - ( ( F ` A ) x. ( G ` A ) ) ) )
115 111 114 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 ) ) ) ) )
116 100 103 104 subdird 
 |-  ( ph -> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` B ) ) = ( ( ( F ` B ) x. ( G ` B ) ) - ( ( F ` A ) x. ( G ` B ) ) ) )
117 91 100 mulcomd 
 |-  ( ph -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` B ) ) = ( ( F ` B ) x. ( ( G ` B ) - ( G ` A ) ) ) )
118 100 104 101 subdid 
 |-  ( ph -> ( ( F ` B ) x. ( ( G ` B ) - ( G ` A ) ) ) = ( ( ( F ` B ) x. ( G ` B ) ) - ( ( F ` B ) x. ( G ` A ) ) ) )
119 117 118 eqtrd 
 |-  ( ph -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` B ) ) = ( ( ( F ` B ) x. ( G ` B ) ) - ( ( F ` B ) x. ( G ` A ) ) ) )
120 116 119 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 ) ) ) ) )
121 110 115 120 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 ) ) ) )
122 fveq2 
 |-  ( z = A -> ( G ` z ) = ( G ` A ) )
123 122 oveq2d 
 |-  ( z = A -> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) = ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` A ) ) )
124 fveq2 
 |-  ( z = A -> ( F ` z ) = ( F ` A ) )
125 124 oveq2d 
 |-  ( z = A -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) = ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` A ) ) )
126 123 125 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 ) ) ) )
127 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 ) ) ) )
128 ovex 
 |-  ( ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) - ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) ) e. _V
129 126 127 128 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 ) ) ) )
130 20 129 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 ) ) ) )
131 fveq2 
 |-  ( z = B -> ( G ` z ) = ( G ` B ) )
132 131 oveq2d 
 |-  ( z = B -> ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` z ) ) = ( ( ( F ` B ) - ( F ` A ) ) x. ( G ` B ) ) )
133 fveq2 
 |-  ( z = B -> ( F ` z ) = ( F ` B ) )
134 133 oveq2d 
 |-  ( z = B -> ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` z ) ) = ( ( ( G ` B ) - ( G ` A ) ) x. ( F ` B ) ) )
135 132 134 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 ) ) ) )
136 135 127 128 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 ) ) ) )
137 17 136 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 ) ) ) )
138 121 130 137 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 ) )
139 1 2 3 46 99 138 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 )
140 94 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 ) )
141 fveq2 
 |-  ( z = x -> ( ( RR _D G ) ` z ) = ( ( RR _D G ) ` x ) )
142 141 oveq2d 
 |-  ( z = x -> ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` z ) ) = ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` x ) ) )
143 fveq2 
 |-  ( z = x -> ( ( RR _D F ) ` z ) = ( ( RR _D F ) ` x ) )
144 143 oveq2d 
 |-  ( z = x -> ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` z ) ) = ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` x ) ) )
145 142 144 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 ) ) ) )
146 145 97 96 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 ) ) ) )
147 140 146 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 ) ) ) )
148 147 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 ) )
149 47 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( F ` B ) - ( F ` A ) ) e. CC )
150 73 ffvelcdmda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D G ) ` x ) e. CC )
151 149 150 mulcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( F ` B ) - ( F ` A ) ) x. ( ( RR _D G ) ` x ) ) e. CC )
152 91 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( G ` B ) - ( G ` A ) ) e. CC )
153 87 ffvelcdmda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. CC )
154 152 153 mulcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( G ` B ) - ( G ` A ) ) x. ( ( RR _D F ) ` x ) ) e. CC )
155 151 154 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 ) ) ) )
156 148 155 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 ) ) ) )
157 156 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 ) ) ) )
158 139 157 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 ) ) )