ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dvmulxxbr Unicode version

Theorem dvmulxxbr 13066
Description: The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmulxx 13068. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.)
Hypotheses
Ref Expression
dvadd.f  |-  ( ph  ->  F : X --> CC )
dvadd.x  |-  ( ph  ->  X  C_  S )
dvaddxx.g  |-  ( ph  ->  G : X --> CC )
dvaddbr.s  |-  ( ph  ->  S  C_  CC )
dvadd.bf  |-  ( ph  ->  C ( S  _D  F ) K )
dvadd.bg  |-  ( ph  ->  C ( S  _D  G ) L )
dvaddcntop.j  |-  J  =  ( MetOpen `  ( abs  o. 
-  ) )
Assertion
Ref Expression
dvmulxxbr  |-  ( ph  ->  C ( S  _D  ( F  oF  x.  G ) ) ( ( K  x.  ( G `  C )
)  +  ( L  x.  ( F `  C ) ) ) )

Proof of Theorem dvmulxxbr
Dummy variables  y  z  x  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvadd.bf . . . 4  |-  ( ph  ->  C ( S  _D  F ) K )
2 eqid 2157 . . . . 5  |-  ( Jt  S )  =  ( Jt  S )
3 dvaddcntop.j . . . . 5  |-  J  =  ( MetOpen `  ( abs  o. 
-  ) )
4 eqid 2157 . . . . 5  |-  ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( F `  z )  -  ( F `  C ) )  / 
( z  -  C
) ) )  =  ( z  e.  {
w  e.  X  |  w #  C }  |->  ( ( ( F `  z
)  -  ( F `
 C ) )  /  ( z  -  C ) ) )
5 dvaddbr.s . . . . 5  |-  ( ph  ->  S  C_  CC )
6 dvadd.f . . . . 5  |-  ( ph  ->  F : X --> CC )
7 dvadd.x . . . . 5  |-  ( ph  ->  X  C_  S )
82, 3, 4, 5, 6, 7eldvap 13051 . . . 4  |-  ( ph  ->  ( C ( S  _D  F ) K  <-> 
( C  e.  ( ( int `  ( Jt  S ) ) `  X )  /\  K  e.  ( ( z  e. 
{ w  e.  X  |  w #  C }  |->  ( ( ( F `
 z )  -  ( F `  C ) )  /  ( z  -  C ) ) ) lim CC  C ) ) ) )
91, 8mpbid 146 . . 3  |-  ( ph  ->  ( C  e.  ( ( int `  ( Jt  S ) ) `  X )  /\  K  e.  ( ( z  e. 
{ w  e.  X  |  w #  C }  |->  ( ( ( F `
 z )  -  ( F `  C ) )  /  ( z  -  C ) ) ) lim CC  C ) ) )
109simpld 111 . 2  |-  ( ph  ->  C  e.  ( ( int `  ( Jt  S ) ) `  X
) )
117, 5sstrd 3138 . . . . . 6  |-  ( ph  ->  X  C_  CC )
123cntoptopon 12932 . . . . . . . . . 10  |-  J  e.  (TopOn `  CC )
13 resttopon 12571 . . . . . . . . . 10  |-  ( ( J  e.  (TopOn `  CC )  /\  S  C_  CC )  ->  ( Jt  S )  e.  (TopOn `  S ) )
1412, 5, 13sylancr 411 . . . . . . . . 9  |-  ( ph  ->  ( Jt  S )  e.  (TopOn `  S ) )
15 topontop 12412 . . . . . . . . 9  |-  ( ( Jt  S )  e.  (TopOn `  S )  ->  ( Jt  S )  e.  Top )
1614, 15syl 14 . . . . . . . 8  |-  ( ph  ->  ( Jt  S )  e.  Top )
17 toponuni 12413 . . . . . . . . . 10  |-  ( ( Jt  S )  e.  (TopOn `  S )  ->  S  =  U. ( Jt  S ) )
1814, 17syl 14 . . . . . . . . 9  |-  ( ph  ->  S  =  U. ( Jt  S ) )
197, 18sseqtrd 3166 . . . . . . . 8  |-  ( ph  ->  X  C_  U. ( Jt  S ) )
20 eqid 2157 . . . . . . . . 9  |-  U. ( Jt  S )  =  U. ( Jt  S )
2120ntrss2 12521 . . . . . . . 8  |-  ( ( ( Jt  S )  e.  Top  /\  X  C_  U. ( Jt  S ) )  -> 
( ( int `  ( Jt  S ) ) `  X )  C_  X
)
2216, 19, 21syl2anc 409 . . . . . . 7  |-  ( ph  ->  ( ( int `  ( Jt  S ) ) `  X )  C_  X
)
2322, 10sseldd 3129 . . . . . 6  |-  ( ph  ->  C  e.  X )
246, 11, 23dvlemap 13049 . . . . 5  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( F `
 z )  -  ( F `  C ) )  /  ( z  -  C ) )  e.  CC )
25 dvaddxx.g . . . . . . 7  |-  ( ph  ->  G : X --> CC )
2625adantr 274 . . . . . 6  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  ->  G : X --> CC )
27 elrabi 2865 . . . . . . 7  |-  ( z  e.  { w  e.  X  |  w #  C }  ->  z  e.  X
)
2827adantl 275 . . . . . 6  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
z  e.  X )
2926, 28ffvelrnd 5603 . . . . 5  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( G `  z
)  e.  CC )
3024, 29mulcld 7898 . . . 4  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( F `  z )  -  ( F `  C ) )  / 
( z  -  C
) )  x.  ( G `  z )
)  e.  CC )
3125, 11, 23dvlemap 13049 . . . . 5  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( G `
 z )  -  ( G `  C ) )  /  ( z  -  C ) )  e.  CC )
326, 23ffvelrnd 5603 . . . . . 6  |-  ( ph  ->  ( F `  C
)  e.  CC )
3332adantr 274 . . . . 5  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( F `  C
)  e.  CC )
3431, 33mulcld 7898 . . . 4  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( G `  z )  -  ( G `  C ) )  / 
( z  -  C
) )  x.  ( F `  C )
)  e.  CC )
35 ssidd 3149 . . . 4  |-  ( ph  ->  CC  C_  CC )
36 txtopon 12662 . . . . . 6  |-  ( ( J  e.  (TopOn `  CC )  /\  J  e.  (TopOn `  CC )
)  ->  ( J  tX  J )  e.  (TopOn `  ( CC  X.  CC ) ) )
3712, 12, 36mp2an 423 . . . . 5  |-  ( J 
tX  J )  e.  (TopOn `  ( CC  X.  CC ) )
3837toponrestid 12419 . . . 4  |-  ( J 
tX  J )  =  ( ( J  tX  J )t  ( CC  X.  CC ) )
399simprd 113 . . . . 5  |-  ( ph  ->  K  e.  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( F `  z
)  -  ( F `
 C ) )  /  ( z  -  C ) ) ) lim
CC  C ) )
40 cnex 7856 . . . . . . . . . . . . 13  |-  CC  e.  _V
4140a1i 9 . . . . . . . . . . . 12  |-  ( ph  ->  CC  e.  _V )
4241, 5ssexd 4104 . . . . . . . . . . . 12  |-  ( ph  ->  S  e.  _V )
43 elpm2r 6611 . . . . . . . . . . . 12  |-  ( ( ( CC  e.  _V  /\  S  e.  _V )  /\  ( G : X --> CC  /\  X  C_  S
) )  ->  G  e.  ( CC  ^pm  S
) )
4441, 42, 25, 7, 43syl22anc 1221 . . . . . . . . . . 11  |-  ( ph  ->  G  e.  ( CC 
^pm  S ) )
45 reldvg 13048 . . . . . . . . . . 11  |-  ( ( S  C_  CC  /\  G  e.  ( CC  ^pm  S
) )  ->  Rel  ( S  _D  G
) )
465, 44, 45syl2anc 409 . . . . . . . . . 10  |-  ( ph  ->  Rel  ( S  _D  G ) )
47 dvadd.bg . . . . . . . . . 10  |-  ( ph  ->  C ( S  _D  G ) L )
48 releldm 4821 . . . . . . . . . 10  |-  ( ( Rel  ( S  _D  G )  /\  C
( S  _D  G
) L )  ->  C  e.  dom  ( S  _D  G ) )
4946, 47, 48syl2anc 409 . . . . . . . . 9  |-  ( ph  ->  C  e.  dom  ( S  _D  G ) )
50 eqid 2157 . . . . . . . . . 10  |-  ( Jt  X )  =  ( Jt  X )
5150, 3dvcnp2cntop 13063 . . . . . . . . 9  |-  ( ( ( S  C_  CC  /\  G : X --> CC  /\  X  C_  S )  /\  C  e.  dom  ( S  _D  G ) )  ->  G  e.  ( ( ( Jt  X )  CnP  J ) `  C ) )
525, 25, 7, 49, 51syl31anc 1223 . . . . . . . 8  |-  ( ph  ->  G  e.  ( ( ( Jt  X )  CnP  J
) `  C )
)
533, 50cnplimccntop 13039 . . . . . . . . 9  |-  ( ( X  C_  CC  /\  C  e.  X )  ->  ( G  e.  ( (
( Jt  X )  CnP  J
) `  C )  <->  ( G : X --> CC  /\  ( G `  C )  e.  ( G lim CC  C ) ) ) )
5411, 23, 53syl2anc 409 . . . . . . . 8  |-  ( ph  ->  ( G  e.  ( ( ( Jt  X )  CnP  J ) `  C )  <->  ( G : X --> CC  /\  ( G `  C )  e.  ( G lim CC  C
) ) ) )
5552, 54mpbid 146 . . . . . . 7  |-  ( ph  ->  ( G : X --> CC  /\  ( G `  C )  e.  ( G lim CC  C ) ) )
5655simprd 113 . . . . . 6  |-  ( ph  ->  ( G `  C
)  e.  ( G lim
CC  C ) )
5725, 11limcdifap 13031 . . . . . . 7  |-  ( ph  ->  ( G lim CC  C
)  =  ( ( G  |`  { w  e.  X  |  w #  C } ) lim CC  C
) )
58 ssrab2 3213 . . . . . . . . . 10  |-  { w  e.  X  |  w #  C }  C_  X
5958a1i 9 . . . . . . . . 9  |-  ( ph  ->  { w  e.  X  |  w #  C }  C_  X )
6025, 59feqresmpt 5522 . . . . . . . 8  |-  ( ph  ->  ( G  |`  { w  e.  X  |  w #  C } )  =  ( z  e.  { w  e.  X  |  w #  C }  |->  ( G `
 z ) ) )
6160oveq1d 5839 . . . . . . 7  |-  ( ph  ->  ( ( G  |`  { w  e.  X  |  w #  C }
) lim CC  C )  =  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( G `  z ) ) lim CC  C ) )
6257, 61eqtrd 2190 . . . . . 6  |-  ( ph  ->  ( G lim CC  C
)  =  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( G `
 z ) ) lim
CC  C ) )
6356, 62eleqtrd 2236 . . . . 5  |-  ( ph  ->  ( G `  C
)  e.  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( G `
 z ) ) lim
CC  C ) )
643mulcncntop 12954 . . . . . 6  |-  x.  e.  ( ( J  tX  J )  Cn  J
)
655, 6, 7dvcl 13052 . . . . . . . 8  |-  ( (
ph  /\  C ( S  _D  F ) K )  ->  K  e.  CC )
661, 65mpdan 418 . . . . . . 7  |-  ( ph  ->  K  e.  CC )
6725, 23ffvelrnd 5603 . . . . . . 7  |-  ( ph  ->  ( G `  C
)  e.  CC )
6866, 67opelxpd 4619 . . . . . 6  |-  ( ph  -> 
<. K ,  ( G `
 C ) >.  e.  ( CC  X.  CC ) )
6937toponunii 12415 . . . . . . 7  |-  ( CC 
X.  CC )  = 
U. ( J  tX  J )
7069cncnpi 12628 . . . . . 6  |-  ( (  x.  e.  ( ( J  tX  J )  Cn  J )  /\  <. K ,  ( G `  C ) >.  e.  ( CC  X.  CC ) )  ->  x.  e.  ( ( ( J 
tX  J )  CnP 
J ) `  <. K ,  ( G `  C ) >. )
)
7164, 68, 70sylancr 411 . . . . 5  |-  ( ph  ->  x.  e.  ( ( ( J  tX  J
)  CnP  J ) `  <. K ,  ( G `  C )
>. ) )
7224, 29, 35, 35, 3, 38, 39, 63, 71limccnp2cntop 13046 . . . 4  |-  ( ph  ->  ( K  x.  ( G `  C )
)  e.  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( ( F `  z )  -  ( F `  C )
)  /  ( z  -  C ) )  x.  ( G `  z ) ) ) lim
CC  C ) )
73 eqid 2157 . . . . . . . 8  |-  ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( G `  z )  -  ( G `  C ) )  / 
( z  -  C
) ) )  =  ( z  e.  {
w  e.  X  |  w #  C }  |->  ( ( ( G `  z
)  -  ( G `
 C ) )  /  ( z  -  C ) ) )
742, 3, 73, 5, 25, 7eldvap 13051 . . . . . . 7  |-  ( ph  ->  ( C ( S  _D  G ) L  <-> 
( C  e.  ( ( int `  ( Jt  S ) ) `  X )  /\  L  e.  ( ( z  e. 
{ w  e.  X  |  w #  C }  |->  ( ( ( G `
 z )  -  ( G `  C ) )  /  ( z  -  C ) ) ) lim CC  C ) ) ) )
7547, 74mpbid 146 . . . . . 6  |-  ( ph  ->  ( C  e.  ( ( int `  ( Jt  S ) ) `  X )  /\  L  e.  ( ( z  e. 
{ w  e.  X  |  w #  C }  |->  ( ( ( G `
 z )  -  ( G `  C ) )  /  ( z  -  C ) ) ) lim CC  C ) ) )
7675simprd 113 . . . . 5  |-  ( ph  ->  L  e.  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( G `  z
)  -  ( G `
 C ) )  /  ( z  -  C ) ) ) lim
CC  C ) )
77 cncfmptc 12982 . . . . . . . 8  |-  ( ( ( F `  C
)  e.  CC  /\  X  C_  CC  /\  CC  C_  CC )  ->  (
z  e.  X  |->  ( F `  C ) )  e.  ( X
-cn-> CC ) )
7832, 11, 35, 77syl3anc 1220 . . . . . . 7  |-  ( ph  ->  ( z  e.  X  |->  ( F `  C
) )  e.  ( X -cn-> CC ) )
79 eqidd 2158 . . . . . . 7  |-  ( z  =  C  ->  ( F `  C )  =  ( F `  C ) )
8078, 23, 79cnmptlimc 13043 . . . . . 6  |-  ( ph  ->  ( F `  C
)  e.  ( ( z  e.  X  |->  ( F `  C ) ) lim CC  C ) )
8132adantr 274 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  X )  ->  ( F `  C )  e.  CC )
8281fmpttd 5622 . . . . . . . 8  |-  ( ph  ->  ( z  e.  X  |->  ( F `  C
) ) : X --> CC )
8382, 11limcdifap 13031 . . . . . . 7  |-  ( ph  ->  ( ( z  e.  X  |->  ( F `  C ) ) lim CC  C )  =  ( ( ( z  e.  X  |->  ( F `  C ) )  |`  { w  e.  X  |  w #  C }
) lim CC  C )
)
84 resmpt 4914 . . . . . . . . 9  |-  ( { w  e.  X  |  w #  C }  C_  X  ->  ( ( z  e.  X  |->  ( F `  C ) )  |`  { w  e.  X  |  w #  C }
)  =  ( z  e.  { w  e.  X  |  w #  C }  |->  ( F `  C ) ) )
8558, 84mp1i 10 . . . . . . . 8  |-  ( ph  ->  ( ( z  e.  X  |->  ( F `  C ) )  |`  { w  e.  X  |  w #  C }
)  =  ( z  e.  { w  e.  X  |  w #  C }  |->  ( F `  C ) ) )
8685oveq1d 5839 . . . . . . 7  |-  ( ph  ->  ( ( ( z  e.  X  |->  ( F `
 C ) )  |`  { w  e.  X  |  w #  C }
) lim CC  C )  =  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( F `  C ) ) lim CC  C ) )
8783, 86eqtrd 2190 . . . . . 6  |-  ( ph  ->  ( ( z  e.  X  |->  ( F `  C ) ) lim CC  C )  =  ( ( z  e.  {
w  e.  X  |  w #  C }  |->  ( F `
 C ) ) lim
CC  C ) )
8880, 87eleqtrd 2236 . . . . 5  |-  ( ph  ->  ( F `  C
)  e.  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( F `
 C ) ) lim
CC  C ) )
895, 25, 7dvcl 13052 . . . . . . . 8  |-  ( (
ph  /\  C ( S  _D  G ) L )  ->  L  e.  CC )
9047, 89mpdan 418 . . . . . . 7  |-  ( ph  ->  L  e.  CC )
9190, 32opelxpd 4619 . . . . . 6  |-  ( ph  -> 
<. L ,  ( F `
 C ) >.  e.  ( CC  X.  CC ) )
9269cncnpi 12628 . . . . . 6  |-  ( (  x.  e.  ( ( J  tX  J )  Cn  J )  /\  <. L ,  ( F `  C ) >.  e.  ( CC  X.  CC ) )  ->  x.  e.  ( ( ( J 
tX  J )  CnP 
J ) `  <. L ,  ( F `  C ) >. )
)
9364, 91, 92sylancr 411 . . . . 5  |-  ( ph  ->  x.  e.  ( ( ( J  tX  J
)  CnP  J ) `  <. L ,  ( F `  C )
>. ) )
9431, 33, 35, 35, 3, 38, 76, 88, 93limccnp2cntop 13046 . . . 4  |-  ( ph  ->  ( L  x.  ( F `  C )
)  e.  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( ( G `  z )  -  ( G `  C )
)  /  ( z  -  C ) )  x.  ( F `  C ) ) ) lim
CC  C ) )
953addcncntop 12952 . . . . 5  |-  +  e.  ( ( J  tX  J )  Cn  J
)
9666, 67mulcld 7898 . . . . . 6  |-  ( ph  ->  ( K  x.  ( G `  C )
)  e.  CC )
9790, 32mulcld 7898 . . . . . 6  |-  ( ph  ->  ( L  x.  ( F `  C )
)  e.  CC )
9896, 97opelxpd 4619 . . . . 5  |-  ( ph  -> 
<. ( K  x.  ( G `  C )
) ,  ( L  x.  ( F `  C ) ) >.  e.  ( CC  X.  CC ) )
9969cncnpi 12628 . . . . 5  |-  ( (  +  e.  ( ( J  tX  J )  Cn  J )  /\  <.
( K  x.  ( G `  C )
) ,  ( L  x.  ( F `  C ) ) >.  e.  ( CC  X.  CC ) )  ->  +  e.  ( ( ( J 
tX  J )  CnP 
J ) `  <. ( K  x.  ( G `
 C ) ) ,  ( L  x.  ( F `  C ) ) >. ) )
10095, 98, 99sylancr 411 . . . 4  |-  ( ph  ->  +  e.  ( ( ( J  tX  J
)  CnP  J ) `  <. ( K  x.  ( G `  C ) ) ,  ( L  x.  ( F `  C ) ) >.
) )
10130, 34, 35, 35, 3, 38, 72, 94, 100limccnp2cntop 13046 . . 3  |-  ( ph  ->  ( ( K  x.  ( G `  C ) )  +  ( L  x.  ( F `  C ) ) )  e.  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( ( ( F `  z )  -  ( F `  C )
)  /  ( z  -  C ) )  x.  ( G `  z ) )  +  ( ( ( ( G `  z )  -  ( G `  C ) )  / 
( z  -  C
) )  x.  ( F `  C )
) ) ) lim CC  C ) )
1026adantr 274 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  ->  F : X --> CC )
103102, 28ffvelrnd 5603 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( F `  z
)  e.  CC )
104103, 33subcld 8186 . . . . . . . 8  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( F `  z )  -  ( F `  C )
)  e.  CC )
105104, 29mulcld 7898 . . . . . . 7  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( F `
 z )  -  ( F `  C ) )  x.  ( G `
 z ) )  e.  CC )
10667adantr 274 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( G `  C
)  e.  CC )
10729, 106subcld 8186 . . . . . . . 8  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( G `  z )  -  ( G `  C )
)  e.  CC )
108107, 33mulcld 7898 . . . . . . 7  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( G `
 z )  -  ( G `  C ) )  x.  ( F `
 C ) )  e.  CC )
10911adantr 274 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  ->  X  C_  CC )
110109, 28sseldd 3129 . . . . . . . 8  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
z  e.  CC )
11111, 23sseldd 3129 . . . . . . . . 9  |-  ( ph  ->  C  e.  CC )
112111adantr 274 . . . . . . . 8  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  ->  C  e.  CC )
113110, 112subcld 8186 . . . . . . 7  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( z  -  C
)  e.  CC )
114 breq1 3968 . . . . . . . . . . 11  |-  ( w  =  z  ->  (
w #  C  <->  z #  C
) )
115114elrab 2868 . . . . . . . . . 10  |-  ( z  e.  { w  e.  X  |  w #  C } 
<->  ( z  e.  X  /\  z #  C )
)
116115simprbi 273 . . . . . . . . 9  |-  ( z  e.  { w  e.  X  |  w #  C }  ->  z #  C )
117116adantl 275 . . . . . . . 8  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
z #  C )
118110, 112, 117subap0d 8519 . . . . . . 7  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( z  -  C
) #  0 )
119105, 108, 113, 118divdirapd 8702 . . . . . 6  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( ( F `  z
)  -  ( F `
 C ) )  x.  ( G `  z ) )  +  ( ( ( G `
 z )  -  ( G `  C ) )  x.  ( F `
 C ) ) )  /  ( z  -  C ) )  =  ( ( ( ( ( F `  z )  -  ( F `  C )
)  x.  ( G `
 z ) )  /  ( z  -  C ) )  +  ( ( ( ( G `  z )  -  ( G `  C ) )  x.  ( F `  C
) )  /  (
z  -  C ) ) ) )
120103, 29mulcld 7898 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( F `  z )  x.  ( G `  z )
)  e.  CC )
12133, 29mulcld 7898 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( F `  C )  x.  ( G `  z )
)  e.  CC )
12233, 106mulcld 7898 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( F `  C )  x.  ( G `  C )
)  e.  CC )
123120, 121, 122npncand 8210 . . . . . . . 8  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( F `  z )  x.  ( G `  z ) )  -  ( ( F `  C )  x.  ( G `  z )
) )  +  ( ( ( F `  C )  x.  ( G `  z )
)  -  ( ( F `  C )  x.  ( G `  C ) ) ) )  =  ( ( ( F `  z
)  x.  ( G `
 z ) )  -  ( ( F `
 C )  x.  ( G `  C
) ) ) )
124103, 33, 29subdird 8290 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( F `
 z )  -  ( F `  C ) )  x.  ( G `
 z ) )  =  ( ( ( F `  z )  x.  ( G `  z ) )  -  ( ( F `  C )  x.  ( G `  z )
) ) )
125107, 33mulcomd 7899 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( G `
 z )  -  ( G `  C ) )  x.  ( F `
 C ) )  =  ( ( F `
 C )  x.  ( ( G `  z )  -  ( G `  C )
) ) )
12633, 29, 106subdid 8289 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( F `  C )  x.  (
( G `  z
)  -  ( G `
 C ) ) )  =  ( ( ( F `  C
)  x.  ( G `
 z ) )  -  ( ( F `
 C )  x.  ( G `  C
) ) ) )
127125, 126eqtrd 2190 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( G `
 z )  -  ( G `  C ) )  x.  ( F `
 C ) )  =  ( ( ( F `  C )  x.  ( G `  z ) )  -  ( ( F `  C )  x.  ( G `  C )
) ) )
128124, 127oveq12d 5842 . . . . . . . 8  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( F `  z )  -  ( F `  C ) )  x.  ( G `  z
) )  +  ( ( ( G `  z )  -  ( G `  C )
)  x.  ( F `
 C ) ) )  =  ( ( ( ( F `  z )  x.  ( G `  z )
)  -  ( ( F `  C )  x.  ( G `  z ) ) )  +  ( ( ( F `  C )  x.  ( G `  z ) )  -  ( ( F `  C )  x.  ( G `  C )
) ) ) )
12928, 28elind 3292 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
z  e.  ( X  i^i  X ) )
1306ffnd 5320 . . . . . . . . . . . 12  |-  ( ph  ->  F  Fn  X )
131130adantr 274 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  ->  F  Fn  X )
13225ffnd 5320 . . . . . . . . . . . 12  |-  ( ph  ->  G  Fn  X )
133132adantr 274 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  ->  G  Fn  X )
134 ssexg 4103 . . . . . . . . . . . . 13  |-  ( ( X  C_  CC  /\  CC  e.  _V )  ->  X  e.  _V )
13511, 40, 134sylancl 410 . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  _V )
136135adantr 274 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  ->  X  e.  _V )
137 eqid 2157 . . . . . . . . . . 11  |-  ( X  i^i  X )  =  ( X  i^i  X
)
138 eqidd 2158 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  { w  e.  X  |  w #  C }
)  /\  z  e.  X )  ->  ( F `  z )  =  ( F `  z ) )
139 eqidd 2158 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  { w  e.  X  |  w #  C }
)  /\  z  e.  X )  ->  ( G `  z )  =  ( G `  z ) )
140120adantr 274 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  { w  e.  X  |  w #  C }
)  /\  z  e.  ( X  i^i  X ) )  ->  ( ( F `  z )  x.  ( G `  z
) )  e.  CC )
141131, 133, 136, 136, 137, 138, 139, 140ofvalg 6041 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  { w  e.  X  |  w #  C }
)  /\  z  e.  ( X  i^i  X ) )  ->  ( ( F  oF  x.  G
) `  z )  =  ( ( F `
 z )  x.  ( G `  z
) ) )
142129, 141mpdan 418 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( F  oF  x.  G ) `  z )  =  ( ( F `  z
)  x.  ( G `
 z ) ) )
14323, 23elind 3292 . . . . . . . . . 10  |-  ( ph  ->  C  e.  ( X  i^i  X ) )
144 eqidd 2158 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  { w  e.  X  |  w #  C }
)  /\  C  e.  X )  ->  ( F `  C )  =  ( F `  C ) )
145 eqidd 2158 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  { w  e.  X  |  w #  C }
)  /\  C  e.  X )  ->  ( G `  C )  =  ( G `  C ) )
146122adantr 274 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  { w  e.  X  |  w #  C }
)  /\  C  e.  ( X  i^i  X ) )  ->  ( ( F `  C )  x.  ( G `  C
) )  e.  CC )
147131, 133, 136, 136, 137, 144, 145, 146ofvalg 6041 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  { w  e.  X  |  w #  C }
)  /\  C  e.  ( X  i^i  X ) )  ->  ( ( F  oF  x.  G
) `  C )  =  ( ( F `
 C )  x.  ( G `  C
) ) )
148143, 147mpidan 420 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( F  oF  x.  G ) `  C )  =  ( ( F `  C
)  x.  ( G `
 C ) ) )
149142, 148oveq12d 5842 . . . . . . . 8  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( F  oF  x.  G
) `  z )  -  ( ( F  oF  x.  G
) `  C )
)  =  ( ( ( F `  z
)  x.  ( G `
 z ) )  -  ( ( F `
 C )  x.  ( G `  C
) ) ) )
150123, 128, 1493eqtr4d 2200 . . . . . . 7  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( F `  z )  -  ( F `  C ) )  x.  ( G `  z
) )  +  ( ( ( G `  z )  -  ( G `  C )
)  x.  ( F `
 C ) ) )  =  ( ( ( F  oF  x.  G ) `  z )  -  (
( F  oF  x.  G ) `  C ) ) )
151150oveq1d 5839 . . . . . 6  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( ( F `  z
)  -  ( F `
 C ) )  x.  ( G `  z ) )  +  ( ( ( G `
 z )  -  ( G `  C ) )  x.  ( F `
 C ) ) )  /  ( z  -  C ) )  =  ( ( ( ( F  oF  x.  G ) `  z )  -  (
( F  oF  x.  G ) `  C ) )  / 
( z  -  C
) ) )
152104, 29, 113, 118div23apd 8701 . . . . . . 7  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( F `  z )  -  ( F `  C ) )  x.  ( G `  z
) )  /  (
z  -  C ) )  =  ( ( ( ( F `  z )  -  ( F `  C )
)  /  ( z  -  C ) )  x.  ( G `  z ) ) )
153107, 33, 113, 118div23apd 8701 . . . . . . 7  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( G `  z )  -  ( G `  C ) )  x.  ( F `  C
) )  /  (
z  -  C ) )  =  ( ( ( ( G `  z )  -  ( G `  C )
)  /  ( z  -  C ) )  x.  ( F `  C ) ) )
154152, 153oveq12d 5842 . . . . . 6  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( ( F `  z
)  -  ( F `
 C ) )  x.  ( G `  z ) )  / 
( z  -  C
) )  +  ( ( ( ( G `
 z )  -  ( G `  C ) )  x.  ( F `
 C ) )  /  ( z  -  C ) ) )  =  ( ( ( ( ( F `  z )  -  ( F `  C )
)  /  ( z  -  C ) )  x.  ( G `  z ) )  +  ( ( ( ( G `  z )  -  ( G `  C ) )  / 
( z  -  C
) )  x.  ( F `  C )
) ) )
155119, 151, 1543eqtr3d 2198 . . . . 5  |-  ( (
ph  /\  z  e.  { w  e.  X  |  w #  C } )  -> 
( ( ( ( F  oF  x.  G ) `  z
)  -  ( ( F  oF  x.  G ) `  C
) )  /  (
z  -  C ) )  =  ( ( ( ( ( F `
 z )  -  ( F `  C ) )  /  ( z  -  C ) )  x.  ( G `  z ) )  +  ( ( ( ( G `  z )  -  ( G `  C ) )  / 
( z  -  C
) )  x.  ( F `  C )
) ) )
156155mpteq2dva 4054 . . . 4  |-  ( ph  ->  ( z  e.  {
w  e.  X  |  w #  C }  |->  ( ( ( ( F  oF  x.  G ) `  z )  -  (
( F  oF  x.  G ) `  C ) )  / 
( z  -  C
) ) )  =  ( z  e.  {
w  e.  X  |  w #  C }  |->  ( ( ( ( ( F `
 z )  -  ( F `  C ) )  /  ( z  -  C ) )  x.  ( G `  z ) )  +  ( ( ( ( G `  z )  -  ( G `  C ) )  / 
( z  -  C
) )  x.  ( F `  C )
) ) ) )
157156oveq1d 5839 . . 3  |-  ( ph  ->  ( ( z  e. 
{ w  e.  X  |  w #  C }  |->  ( ( ( ( F  oF  x.  G ) `  z
)  -  ( ( F  oF  x.  G ) `  C
) )  /  (
z  -  C ) ) ) lim CC  C
)  =  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( ( ( F `
 z )  -  ( F `  C ) )  /  ( z  -  C ) )  x.  ( G `  z ) )  +  ( ( ( ( G `  z )  -  ( G `  C ) )  / 
( z  -  C
) )  x.  ( F `  C )
) ) ) lim CC  C ) )
158101, 157eleqtrrd 2237 . 2  |-  ( ph  ->  ( ( K  x.  ( G `  C ) )  +  ( L  x.  ( F `  C ) ) )  e.  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( ( F  oF  x.  G ) `  z )  -  (
( F  oF  x.  G ) `  C ) )  / 
( z  -  C
) ) ) lim CC  C ) )
159 eqid 2157 . . 3  |-  ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( ( F  oF  x.  G ) `  z )  -  (
( F  oF  x.  G ) `  C ) )  / 
( z  -  C
) ) )  =  ( z  e.  {
w  e.  X  |  w #  C }  |->  ( ( ( ( F  oF  x.  G ) `  z )  -  (
( F  oF  x.  G ) `  C ) )  / 
( z  -  C
) ) )
160 mulcl 7859 . . . . 5  |-  ( ( x  e.  CC  /\  y  e.  CC )  ->  ( x  x.  y
)  e.  CC )
161160adantl 275 . . . 4  |-  ( (
ph  /\  ( x  e.  CC  /\  y  e.  CC ) )  -> 
( x  x.  y
)  e.  CC )
162 inidm 3316 . . . 4  |-  ( X  i^i  X )  =  X
163161, 6, 25, 135, 135, 162off 6044 . . 3  |-  ( ph  ->  ( F  oF  x.  G ) : X --> CC )
1642, 3, 159, 5, 163, 7eldvap 13051 . 2  |-  ( ph  ->  ( C ( S  _D  ( F  oF  x.  G )
) ( ( K  x.  ( G `  C ) )  +  ( L  x.  ( F `  C )
) )  <->  ( C  e.  ( ( int `  ( Jt  S ) ) `  X )  /\  (
( K  x.  ( G `  C )
)  +  ( L  x.  ( F `  C ) ) )  e.  ( ( z  e.  { w  e.  X  |  w #  C }  |->  ( ( ( ( F  oF  x.  G ) `  z )  -  (
( F  oF  x.  G ) `  C ) )  / 
( z  -  C
) ) ) lim CC  C ) ) ) )
16510, 158, 164mpbir2and 929 1  |-  ( ph  ->  C ( S  _D  ( F  oF  x.  G ) ) ( ( K  x.  ( G `  C )
)  +  ( L  x.  ( F `  C ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    = wceq 1335    e. wcel 2128   {crab 2439   _Vcvv 2712    i^i cin 3101    C_ wss 3102   <.cop 3563   U.cuni 3772   class class class wbr 3965    |-> cmpt 4025    X. cxp 4584   dom cdm 4586    |` cres 4588    o. ccom 4590   Rel wrel 4591    Fn wfn 5165   -->wf 5166   ` cfv 5170  (class class class)co 5824    oFcof 6030    ^pm cpm 6594   CCcc 7730    + caddc 7735    x. cmul 7737    - cmin 8046   # cap 8456    / cdiv 8545   abscabs 10897   ↾t crest 12351   MetOpencmopn 12385   Topctop 12395  TopOnctopon 12408   intcnt 12493    Cn ccn 12585    CnP ccnp 12586    tX ctx 12652   -cn->ccncf 12957   lim CC climc 13023    _D cdv 13024
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4079  ax-sep 4082  ax-nul 4090  ax-pow 4135  ax-pr 4169  ax-un 4393  ax-setind 4496  ax-iinf 4547  ax-cnex 7823  ax-resscn 7824  ax-1cn 7825  ax-1re 7826  ax-icn 7827  ax-addcl 7828  ax-addrcl 7829  ax-mulcl 7830  ax-mulrcl 7831  ax-addcom 7832  ax-mulcom 7833  ax-addass 7834  ax-mulass 7835  ax-distr 7836  ax-i2m1 7837  ax-0lt1 7838  ax-1rid 7839  ax-0id 7840  ax-rnegex 7841  ax-precex 7842  ax-cnre 7843  ax-pre-ltirr 7844  ax-pre-ltwlin 7845  ax-pre-lttrn 7846  ax-pre-apti 7847  ax-pre-ltadd 7848  ax-pre-mulgt0 7849  ax-pre-mulext 7850  ax-arch 7851  ax-caucvg 7852  ax-addf 7854  ax-mulf 7855
This theorem depends on definitions:  df-bi 116  df-stab 817  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-reu 2442  df-rmo 2443  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-if 3506  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-iun 3851  df-br 3966  df-opab 4026  df-mpt 4027  df-tr 4063  df-id 4253  df-po 4256  df-iso 4257  df-iord 4326  df-on 4328  df-ilim 4329  df-suc 4331  df-iom 4550  df-xp 4592  df-rel 4593  df-cnv 4594  df-co 4595  df-dm 4596  df-rn 4597  df-res 4598  df-ima 4599  df-iota 5135  df-fun 5172  df-fn 5173  df-f 5174  df-f1 5175  df-fo 5176  df-f1o 5177  df-fv 5178  df-isom 5179  df-riota 5780  df-ov 5827  df-oprab 5828  df-mpo 5829  df-of 6032  df-1st 6088  df-2nd 6089  df-recs 6252  df-frec 6338  df-map 6595  df-pm 6596  df-sup 6928  df-inf 6929  df-pnf 7914  df-mnf 7915  df-xr 7916  df-ltxr 7917  df-le 7918  df-sub 8048  df-neg 8049  df-reap 8450  df-ap 8457  df-div 8546  df-inn 8834  df-2 8892  df-3 8893  df-4 8894  df-n0 9091  df-z 9168  df-uz 9440  df-q 9529  df-rp 9561  df-xneg 9679  df-xadd 9680  df-seqfrec 10345  df-exp 10419  df-cj 10742  df-re 10743  df-im 10744  df-rsqrt 10898  df-abs 10899  df-rest 12353  df-topgen 12372  df-psmet 12387  df-xmet 12388  df-met 12389  df-bl 12390  df-mopn 12391  df-top 12396  df-topon 12409  df-bases 12441  df-ntr 12496  df-cn 12588  df-cnp 12589  df-tx 12653  df-cncf 12958  df-limced 13025  df-dvap 13026
This theorem is referenced by:  dvmulxx  13068  dvimulf  13070  dvef  13088
  Copyright terms: Public domain W3C validator