Users' Mathboxes Mathbox for Steve Rodriguez < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  expgrowth Structured version   Unicode version

Theorem expgrowth 31216
Description: Exponential growth and decay model. The derivative of a function y of variable t equals a constant k times y itself, iff y equals some constant C times the exponential of kt. This theorem and expgrowthi 31214 illustrate one of the simplest and most crucial classes of differential equations, equations that relate functions to their derivatives.

Section 6.3 of [Strang] p. 242 calls y' = ky "the most important differential equation in applied mathematics". In the field of population ecology it is known as the Malthusian growth model or exponential law, and C, k, and t correspond to initial population size, growth rate, and time respectively (https://en.wikipedia.org/wiki/Malthusian_growth_model); and in finance, the model appears in a similar role in continuous compounding with C as the initial amount of money. In exponential decay models, k is often expressed as the negative of a positive constant λ.

Here y' is given as  ( S  _D  Y
), C as  c, and ky as  ( ( S  X.  { K }
)  oF  x.  Y ).  ( S  X.  { K }
) is the constant function that maps any real or complex input to k and  oF  x. is multiplication as a function operation.

The leftward direction of the biconditional is as given in http://www.saylor.org/site/wp-content/uploads/2011/06/MA221-2.1.1.pdf pp. 1-2, which also notes the reverse direction ("While we will not prove this here, it turns out that these are the only functions that satisfy this equation."). The rightward direction is Theorem 5.1 of [LarsonHostetlerEdwards] p. 375 (which notes " C is the initial value of y, and k is the proportionality constant. Exponential growth occurs when k > 0, and exponential decay occurs when k < 0."); its proof here closely follows the proof of y' = y in https://proofwiki.org/wiki/Exponential_Growth_Equation/Special_Case.

Statements for this and expgrowthi 31214 formulated by Mario Carneiro. (Contributed by Steve Rodriguez, 24-Nov-2015.)

Hypotheses
Ref Expression
expgrowth.s  |-  ( ph  ->  S  e.  { RR ,  CC } )
expgrowth.k  |-  ( ph  ->  K  e.  CC )
expgrowth.y  |-  ( ph  ->  Y : S --> CC )
expgrowth.dy  |-  ( ph  ->  dom  ( S  _D  Y )  =  S )
Assertion
Ref Expression
expgrowth  |-  ( ph  ->  ( ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y )  <->  E. c  e.  CC  Y  =  ( t  e.  S  |->  ( c  x.  ( exp `  ( K  x.  t
) ) ) ) ) )
Distinct variable groups:    t, c, K    S, c, t    Y, c
Allowed substitution hints:    ph( t, c)    Y( t)

Proof of Theorem expgrowth
Dummy variables  u  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 expgrowth.s . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  S  e.  { RR ,  CC } )
2 cnelprrecn 9588 . . . . . . . . . . . . . . . . . 18  |-  CC  e.  { RR ,  CC }
32a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  CC  e.  { RR ,  CC } )
4 expgrowth.k . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  K  e.  CC )
5 recnprss 22285 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
61, 5syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  S  C_  CC )
76sseld 3488 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( u  e.  S  ->  u  e.  CC ) )
8 mulcl 9579 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( K  e.  CC  /\  u  e.  CC )  ->  ( K  x.  u
)  e.  CC )
94, 7, 8syl6an 545 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( u  e.  S  ->  ( K  x.  u
)  e.  CC ) )
109imp 429 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  S )  ->  ( K  x.  u )  e.  CC )
1110negcld 9923 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  S )  ->  -u ( K  x.  u )  e.  CC )
124negcld 9923 . . . . . . . . . . . . . . . . . 18  |-  ( ph  -> 
-u K  e.  CC )
1312adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  S )  ->  -u K  e.  CC )
14 efcl 13799 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  CC  ->  ( exp `  y )  e.  CC )
1514adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  CC )  ->  ( exp `  y )  e.  CC )
164adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  S )  ->  K  e.  CC )
177imp 429 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  S )  ->  u  e.  CC )
18 ax-1cn 9553 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  CC
1918a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  S )  ->  1  e.  CC )
201dvmptid 22337 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( S  _D  (
u  e.  S  |->  u ) )  =  ( u  e.  S  |->  1 ) )
211, 17, 19, 20, 4dvmptcmul 22344 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( S  _D  (
u  e.  S  |->  ( K  x.  u ) ) )  =  ( u  e.  S  |->  ( K  x.  1 ) ) )
224mulid1d 9616 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( K  x.  1 )  =  K )
2322mpteq2dv 4524 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( u  e.  S  |->  ( K  x.  1 ) )  =  ( u  e.  S  |->  K ) )
2421, 23eqtrd 2484 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( S  _D  (
u  e.  S  |->  ( K  x.  u ) ) )  =  ( u  e.  S  |->  K ) )
251, 10, 16, 24dvmptneg 22346 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( S  _D  (
u  e.  S  |->  -u ( K  x.  u
) ) )  =  ( u  e.  S  |-> 
-u K ) )
26 dvef 22358 . . . . . . . . . . . . . . . . . . 19  |-  ( CC 
_D  exp )  =  exp
27 eff 13798 . . . . . . . . . . . . . . . . . . . . . 22  |-  exp : CC
--> CC
28 ffn 5721 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( exp
: CC --> CC  ->  exp 
Fn  CC )
2927, 28ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21  |-  exp  Fn  CC
30 dffn5 5903 . . . . . . . . . . . . . . . . . . . . 21  |-  ( exp 
Fn  CC  <->  exp  =  ( y  e.  CC  |->  ( exp `  y ) ) )
3129, 30mpbi 208 . . . . . . . . . . . . . . . . . . . 20  |-  exp  =  ( y  e.  CC  |->  ( exp `  y ) )
3231oveq2i 6292 . . . . . . . . . . . . . . . . . . 19  |-  ( CC 
_D  exp )  =  ( CC  _D  ( y  e.  CC  |->  ( exp `  y ) ) )
3326, 32, 313eqtr3i 2480 . . . . . . . . . . . . . . . . . 18  |-  ( CC 
_D  ( y  e.  CC  |->  ( exp `  y
) ) )  =  ( y  e.  CC  |->  ( exp `  y ) )
3433a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( CC  _D  (
y  e.  CC  |->  ( exp `  y ) ) )  =  ( y  e.  CC  |->  ( exp `  y ) ) )
35 fveq2 5856 . . . . . . . . . . . . . . . . 17  |-  ( y  =  -u ( K  x.  u )  ->  ( exp `  y )  =  ( exp `  -u ( K  x.  u )
) )
361, 3, 11, 13, 15, 15, 25, 34, 35, 35dvmptco 22352 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( S  _D  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u )
)  x.  -u K
) ) )
3736oveq2d 6297 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( Y  oF  x.  ( S  _D  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( Y  oF  x.  ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u )
)  x.  -u K
) ) ) )
38 expgrowth.y . . . . . . . . . . . . . . . 16  |-  ( ph  ->  Y : S --> CC )
39 efcl 13799 . . . . . . . . . . . . . . . . . . . 20  |-  ( -u ( K  x.  u
)  e.  CC  ->  ( exp `  -u ( K  x.  u )
)  e.  CC )
4011, 39syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  S )  ->  ( exp `  -u ( K  x.  u ) )  e.  CC )
4140, 13mulcld 9619 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  S )  ->  (
( exp `  -u ( K  x.  u )
)  x.  -u K
)  e.  CC )
42 eqid 2443 . . . . . . . . . . . . . . . . . 18  |-  ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u )
)  x.  -u K
) )  =  ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u )
)  x.  -u K
) )
4341, 42fmptd 6040 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u )
)  x.  -u K
) ) : S --> CC )
4436feq1d 5707 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( S  _D  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) : S --> CC  <->  ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u )
)  x.  -u K
) ) : S --> CC ) )
4543, 44mpbird 232 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( S  _D  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) : S --> CC )
46 mulcom 9581 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  CC  /\  y  e.  CC )  ->  ( x  x.  y
)  =  ( y  x.  x ) )
4746adantl 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  CC  /\  y  e.  CC ) )  -> 
( x  x.  y
)  =  ( y  x.  x ) )
481, 38, 45, 47caofcom 6557 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( Y  oF  x.  ( S  _D  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( ( S  _D  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  oF  x.  Y ) )
4937, 48eqtr3d 2486 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Y  oF  x.  ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u ) )  x.  -u K ) ) )  =  ( ( S  _D  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  oF  x.  Y ) )
5049oveq2d 6297 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( S  _D  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  +  ( Y  oF  x.  ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u )
)  x.  -u K
) ) ) )  =  ( ( ( S  _D  Y )  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  oF  +  ( ( S  _D  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  x.  Y ) ) )
51 fconst6g 5764 . . . . . . . . . . . . . . . . . 18  |-  ( -u K  e.  CC  ->  ( S  X.  { -u K } ) : S --> CC )
5212, 51syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( S  X.  { -u K } ) : S --> CC )
53 eqid 2443 . . . . . . . . . . . . . . . . . 18  |-  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) )  =  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) )
5440, 53fmptd 6040 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) : S --> CC )
551, 52, 54, 47caofcom 6557 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( S  X.  { -u K } )  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) )  oF  x.  ( S  X.  { -u K } ) ) )
56 eqidd 2444 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) )  =  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )
57 fconstmpt 5033 . . . . . . . . . . . . . . . . . 18  |-  ( S  X.  { -u K } )  =  ( u  e.  S  |->  -u K )
5857a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( S  X.  { -u K } )  =  ( u  e.  S  |-> 
-u K ) )
591, 40, 13, 56, 58offval2 6541 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) )  oF  x.  ( S  X.  { -u K } ) )  =  ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u )
)  x.  -u K
) ) )
6055, 59eqtrd 2484 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( S  X.  { -u K } )  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u )
)  x.  -u K
) ) )
6160oveq2d 6297 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Y  oF  x.  ( ( S  X.  { -u K } )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( Y  oF  x.  ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u )
)  x.  -u K
) ) ) )
6261oveq2d 6297 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( S  _D  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  +  ( Y  oF  x.  ( ( S  X.  { -u K } )  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) ) )  =  ( ( ( S  _D  Y
)  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  oF  +  ( Y  oF  x.  (
u  e.  S  |->  ( ( exp `  -u ( K  x.  u )
)  x.  -u K
) ) ) ) )
63 expgrowth.dy . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( S  _D  Y )  =  S )
6436dmeqd 5195 . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  ( S  _D  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  dom  ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u ) )  x.  -u K ) ) )
6542, 41dmmptd 5701 . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u ) )  x.  -u K ) )  =  S )
6664, 65eqtrd 2484 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( S  _D  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  S )
671, 38, 54, 63, 66dvmulf 22323 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S  _D  ( Y  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( ( ( S  _D  Y )  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  oF  +  ( ( S  _D  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  x.  Y ) ) )
6850, 62, 673eqtr4rd 2495 . . . . . . . . . . . 12  |-  ( ph  ->  ( S  _D  ( Y  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( ( ( S  _D  Y )  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  oF  +  ( Y  oF  x.  (
( S  X.  { -u K } )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) ) ) ) )
69 ofmul12 31206 . . . . . . . . . . . . . 14  |-  ( ( ( S  e.  { RR ,  CC }  /\  Y : S --> CC )  /\  ( ( S  X.  { -u K } ) : S --> CC  /\  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) : S --> CC ) )  ->  ( Y  oF  x.  (
( S  X.  { -u K } )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) ) )  =  ( ( S  X.  { -u K } )  oF  x.  ( Y  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) ) )
701, 38, 52, 54, 69syl22anc 1230 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Y  oF  x.  ( ( S  X.  { -u K } )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( ( S  X.  { -u K } )  oF  x.  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) ) ) )
7170oveq2d 6297 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( S  _D  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  +  ( Y  oF  x.  ( ( S  X.  { -u K } )  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) ) )  =  ( ( ( S  _D  Y
)  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  oF  +  ( ( S  X.  { -u K } )  oF  x.  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) ) ) ) )
7268, 71eqtrd 2484 . . . . . . . . . . 11  |-  ( ph  ->  ( S  _D  ( Y  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( ( ( S  _D  Y )  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  oF  +  ( ( S  X.  { -u K } )  oF  x.  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) ) ) ) )
73 oveq1 6288 . . . . . . . . . . . 12  |-  ( ( S  _D  Y )  =  ( ( S  X.  { K }
)  oF  x.  Y )  ->  (
( S  _D  Y
)  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( ( ( S  X.  { K }
)  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )
7473oveq1d 6296 . . . . . . . . . . 11  |-  ( ( S  _D  Y )  =  ( ( S  X.  { K }
)  oF  x.  Y )  ->  (
( ( S  _D  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  oF  +  ( ( S  X.  { -u K } )  oF  x.  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) ) ) )  =  ( ( ( ( S  X.  { K } )  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  +  ( ( S  X.  { -u K } )  oF  x.  ( Y  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) ) ) )
7572, 74sylan9eq 2504 . . . . . . . . . 10  |-  ( (
ph  /\  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) )  ->  ( S  _D  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( ( ( ( S  X.  { K } )  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  +  ( ( S  X.  { -u K } )  oF  x.  ( Y  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) ) ) )
76 mulass 9583 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  CC  /\  y  e.  CC  /\  z  e.  CC )  ->  (
( x  x.  y
)  x.  z )  =  ( x  x.  ( y  x.  z
) ) )
7776adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  CC  /\  y  e.  CC  /\  z  e.  CC ) )  -> 
( ( x  x.  y )  x.  z
)  =  ( x  x.  ( y  x.  z ) ) )
781, 52, 38, 54, 77caofass 6559 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( S  X.  { -u K } )  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  =  ( ( S  X.  { -u K } )  oF  x.  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) ) ) )
7978oveq2d 6297 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( S  X.  { K } )  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  +  ( ( ( S  X.  { -u K } )  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) ) )  =  ( ( ( ( S  X.  { K }
)  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  oF  +  ( ( S  X.  { -u K } )  oF  x.  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) ) ) ) )
8079eqeq2d 2457 . . . . . . . . . . 11  |-  ( ph  ->  ( ( S  _D  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( ( ( ( S  X.  { K } )  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  +  ( ( ( S  X.  { -u K } )  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) ) )  <->  ( S  _D  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( ( ( ( S  X.  { K } )  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  +  ( ( S  X.  { -u K } )  oF  x.  ( Y  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) ) ) ) )
8180adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) )  ->  ( ( S  _D  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) ) )  =  ( ( ( ( S  X.  { K }
)  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  oF  +  ( ( ( S  X.  { -u K } )  oF  x.  Y )  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  <-> 
( S  _D  ( Y  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( ( ( ( S  X.  { K } )  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  +  ( ( S  X.  { -u K } )  oF  x.  ( Y  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) ) ) ) )
8275, 81mpbird 232 . . . . . . . . 9  |-  ( (
ph  /\  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) )  ->  ( S  _D  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( ( ( ( S  X.  { K } )  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  +  ( ( ( S  X.  { -u K } )  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) ) ) )
83 mulcl 9579 . . . . . . . . . . . . . 14  |-  ( ( x  e.  CC  /\  y  e.  CC )  ->  ( x  x.  y
)  e.  CC )
8483adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  CC  /\  y  e.  CC ) )  -> 
( x  x.  y
)  e.  CC )
85 fconst6g 5764 . . . . . . . . . . . . . 14  |-  ( K  e.  CC  ->  ( S  X.  { K }
) : S --> CC )
864, 85syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S  X.  { K } ) : S --> CC )
87 inidm 3692 . . . . . . . . . . . . 13  |-  ( S  i^i  S )  =  S
8884, 86, 38, 1, 1, 87off 6539 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S  X.  { K } )  oF  x.  Y ) : S --> CC )
8984, 52, 38, 1, 1, 87off 6539 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S  X.  { -u K } )  oF  x.  Y
) : S --> CC )
90 adddir 9590 . . . . . . . . . . . . 13  |-  ( ( x  e.  CC  /\  y  e.  CC  /\  z  e.  CC )  ->  (
( x  +  y )  x.  z )  =  ( ( x  x.  z )  +  ( y  x.  z
) ) )
9190adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  CC  /\  y  e.  CC  /\  z  e.  CC ) )  -> 
( ( x  +  y )  x.  z
)  =  ( ( x  x.  z )  +  ( y  x.  z ) ) )
921, 54, 88, 89, 91caofdir 6562 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( S  X.  { K } )  oF  x.  Y )  oF  +  ( ( S  X.  { -u K } )  oF  x.  Y ) )  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( ( ( ( S  X.  { K } )  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  +  ( ( ( S  X.  { -u K } )  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) ) ) )
9392eqeq2d 2457 . . . . . . . . . 10  |-  ( ph  ->  ( ( S  _D  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( ( ( ( S  X.  { K } )  oF  x.  Y )  oF  +  ( ( S  X.  { -u K } )  oF  x.  Y ) )  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  <->  ( S  _D  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( ( ( ( S  X.  { K } )  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  +  ( ( ( S  X.  { -u K } )  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) ) ) ) )
9493adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) )  ->  ( ( S  _D  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) ) )  =  ( ( ( ( S  X.  { K }
)  oF  x.  Y )  oF  +  ( ( S  X.  { -u K } )  oF  x.  Y ) )  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  <->  ( S  _D  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( ( ( ( S  X.  { K } )  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  +  ( ( ( S  X.  { -u K } )  oF  x.  Y )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) ) ) ) )
9582, 94mpbird 232 . . . . . . . 8  |-  ( (
ph  /\  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) )  ->  ( S  _D  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( ( ( ( S  X.  { K } )  oF  x.  Y )  oF  +  ( ( S  X.  { -u K } )  oF  x.  Y ) )  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )
96 ofnegsub 10541 . . . . . . . . . . . . 13  |-  ( ( S  e.  { RR ,  CC }  /\  (
( S  X.  { K } )  oF  x.  Y ) : S --> CC  /\  (
( S  X.  { K } )  oF  x.  Y ) : S --> CC )  -> 
( ( ( S  X.  { K }
)  oF  x.  Y )  oF  +  ( ( S  X.  { -u 1 } )  oF  x.  ( ( S  X.  { K }
)  oF  x.  Y ) ) )  =  ( ( ( S  X.  { K } )  oF  x.  Y )  oF  -  ( ( S  X.  { K } )  oF  x.  Y ) ) )
971, 88, 88, 96syl3anc 1229 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( S  X.  { K }
)  oF  x.  Y )  oF  +  ( ( S  X.  { -u 1 } )  oF  x.  ( ( S  X.  { K }
)  oF  x.  Y ) ) )  =  ( ( ( S  X.  { K } )  oF  x.  Y )  oF  -  ( ( S  X.  { K } )  oF  x.  Y ) ) )
98 neg1cn 10646 . . . . . . . . . . . . . . . . 17  |-  -u 1  e.  CC
9998fconst6 5765 . . . . . . . . . . . . . . . 16  |-  ( S  X.  { -u 1 } ) : S --> CC
10099a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( S  X.  { -u 1 } ) : S --> CC )
1011, 100, 86, 38, 77caofass 6559 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( S  X.  { -u 1 } )  oF  x.  ( S  X.  { K } ) )  oF  x.  Y
)  =  ( ( S  X.  { -u
1 } )  oF  x.  ( ( S  X.  { K } )  oF  x.  Y ) ) )
10298a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  -> 
-u 1  e.  CC )
1031, 102, 4ofc12 6550 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( S  X.  { -u 1 } )  oF  x.  ( S  X.  { K }
) )  =  ( S  X.  { (
-u 1  x.  K
) } ) )
1044mulm1d 10015 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( -u 1  x.  K )  =  -u K )
105104sneqd 4026 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  { ( -u 1  x.  K ) }  =  { -u K } )
106105xpeq2d 5013 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( S  X.  {
( -u 1  x.  K
) } )  =  ( S  X.  { -u K } ) )
107103, 106eqtrd 2484 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( S  X.  { -u 1 } )  oF  x.  ( S  X.  { K }
) )  =  ( S  X.  { -u K } ) )
108107oveq1d 6296 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( S  X.  { -u 1 } )  oF  x.  ( S  X.  { K } ) )  oF  x.  Y
)  =  ( ( S  X.  { -u K } )  oF  x.  Y ) )
109101, 108eqtr3d 2486 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S  X.  { -u 1 } )  oF  x.  (
( S  X.  { K } )  oF  x.  Y ) )  =  ( ( S  X.  { -u K } )  oF  x.  Y ) )
110109oveq2d 6297 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( S  X.  { K }
)  oF  x.  Y )  oF  +  ( ( S  X.  { -u 1 } )  oF  x.  ( ( S  X.  { K }
)  oF  x.  Y ) ) )  =  ( ( ( S  X.  { K } )  oF  x.  Y )  oF  +  ( ( S  X.  { -u K } )  oF  x.  Y ) ) )
111 ofsubid 31205 . . . . . . . . . . . . 13  |-  ( ( S  e.  { RR ,  CC }  /\  (
( S  X.  { K } )  oF  x.  Y ) : S --> CC )  -> 
( ( ( S  X.  { K }
)  oF  x.  Y )  oF  -  ( ( S  X.  { K }
)  oF  x.  Y ) )  =  ( S  X.  {
0 } ) )
1121, 88, 111syl2anc 661 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( S  X.  { K }
)  oF  x.  Y )  oF  -  ( ( S  X.  { K }
)  oF  x.  Y ) )  =  ( S  X.  {
0 } ) )
11397, 110, 1123eqtr3d 2492 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( S  X.  { K }
)  oF  x.  Y )  oF  +  ( ( S  X.  { -u K } )  oF  x.  Y ) )  =  ( S  X.  { 0 } ) )
114113oveq1d 6296 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( S  X.  { K } )  oF  x.  Y )  oF  +  ( ( S  X.  { -u K } )  oF  x.  Y ) )  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( ( S  X.  { 0 } )  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )
115114eqeq2d 2457 . . . . . . . . 9  |-  ( ph  ->  ( ( S  _D  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( ( ( ( S  X.  { K } )  oF  x.  Y )  oF  +  ( ( S  X.  { -u K } )  oF  x.  Y ) )  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  <->  ( S  _D  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( ( S  X.  { 0 } )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) ) )
116115adantr 465 . . . . . . . 8  |-  ( (
ph  /\  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) )  ->  ( ( S  _D  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) ) )  =  ( ( ( ( S  X.  { K }
)  oF  x.  Y )  oF  +  ( ( S  X.  { -u K } )  oF  x.  Y ) )  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  <->  ( S  _D  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( ( S  X.  { 0 } )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) ) )
11795, 116mpbid 210 . . . . . . 7  |-  ( (
ph  /\  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) )  ->  ( S  _D  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( ( S  X.  { 0 } )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )
118 0cnd 9592 . . . . . . . . 9  |-  ( ph  ->  0  e.  CC )
119 mul02 9761 . . . . . . . . . 10  |-  ( x  e.  CC  ->  (
0  x.  x )  =  0 )
120119adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  CC )  ->  ( 0  x.  x )  =  0 )
1211, 54, 118, 118, 120caofid2 6556 . . . . . . . 8  |-  ( ph  ->  ( ( S  X.  { 0 } )  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( S  X.  {
0 } ) )
122121adantr 465 . . . . . . 7  |-  ( (
ph  /\  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) )  ->  ( ( S  X.  { 0 } )  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( S  X.  {
0 } ) )
123117, 122eqtrd 2484 . . . . . 6  |-  ( (
ph  /\  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) )  ->  ( S  _D  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  ( S  X.  { 0 } ) )
1241adantr 465 . . . . . . 7  |-  ( (
ph  /\  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) )  ->  S  e.  { RR ,  CC } )
12584, 38, 54, 1, 1, 87off 6539 . . . . . . . 8  |-  ( ph  ->  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) : S --> CC )
126125adantr 465 . . . . . . 7  |-  ( (
ph  /\  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) )  ->  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) ) : S --> CC )
127123dmeqd 5195 . . . . . . . 8  |-  ( (
ph  /\  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) )  ->  dom  ( S  _D  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  dom  ( S  X.  { 0 } ) )
128 0cn 9591 . . . . . . . . . 10  |-  0  e.  CC
129128fconst6 5765 . . . . . . . . 9  |-  ( S  X.  { 0 } ) : S --> CC
130129fdmi 5726 . . . . . . . 8  |-  dom  ( S  X.  { 0 } )  =  S
131127, 130syl6eq 2500 . . . . . . 7  |-  ( (
ph  /\  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) )  ->  dom  ( S  _D  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )  =  S )
132124, 126, 131dvconstbi 31215 . . . . . 6  |-  ( (
ph  /\  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) )  ->  ( ( S  _D  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) ) )  =  ( S  X.  { 0 } )  <->  E. x  e.  CC  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  =  ( S  X.  { x }
) ) )
133123, 132mpbid 210 . . . . 5  |-  ( (
ph  /\  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) )  ->  E. x  e.  CC  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( S  X.  {
x } ) )
134 oveq1 6288 . . . . . . . . . 10  |-  ( ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( S  X.  {
x } )  -> 
( ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  / 
( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( ( S  X.  { x } )  oF  /  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) )
135 efne0 13813 . . . . . . . . . . . . . . 15  |-  ( -u ( K  x.  u
)  e.  CC  ->  ( exp `  -u ( K  x.  u )
)  =/=  0 )
136 eldifsn 4140 . . . . . . . . . . . . . . 15  |-  ( ( exp `  -u ( K  x.  u )
)  e.  ( CC 
\  { 0 } )  <->  ( ( exp `  -u ( K  x.  u ) )  e.  CC  /\  ( exp `  -u ( K  x.  u ) )  =/=  0 ) )
13739, 135, 136sylanbrc 664 . . . . . . . . . . . . . 14  |-  ( -u ( K  x.  u
)  e.  CC  ->  ( exp `  -u ( K  x.  u )
)  e.  ( CC 
\  { 0 } ) )
13811, 137syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  S )  ->  ( exp `  -u ( K  x.  u ) )  e.  ( CC  \  {
0 } ) )
139138, 53fmptd 6040 . . . . . . . . . . . 12  |-  ( ph  ->  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) : S --> ( CC  \  { 0 } ) )
140 ofdivcan4 31208 . . . . . . . . . . . 12  |-  ( ( S  e.  { RR ,  CC }  /\  Y : S --> CC  /\  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) : S --> ( CC  \  { 0 } ) )  -> 
( ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  / 
( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  Y )
1411, 38, 139, 140syl3anc 1229 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  / 
( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  Y )
142141eqeq1d 2445 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( Y  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  oF  /  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  =  ( ( S  X.  { x } )  oF  /  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  <->  Y  =  ( ( S  X.  { x } )  oF  /  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) ) )
143134, 142syl5ib 219 . . . . . . . . 9  |-  ( ph  ->  ( ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  =  ( S  X.  { x }
)  ->  Y  =  ( ( S  X.  { x } )  oF  /  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) ) )
144143adantr 465 . . . . . . . 8  |-  ( (
ph  /\  x  e.  CC )  ->  ( ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( S  X.  {
x } )  ->  Y  =  ( ( S  X.  { x }
)  oF  / 
( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) ) )
145 vex 3098 . . . . . . . . . . . . 13  |-  x  e. 
_V
146145a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S )  ->  x  e.  _V )
147 ovex 6309 . . . . . . . . . . . . 13  |-  ( 1  /  ( exp `  ( K  x.  u )
) )  e.  _V
148147a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S )  ->  (
1  /  ( exp `  ( K  x.  u
) ) )  e. 
_V )
149 fconstmpt 5033 . . . . . . . . . . . . 13  |-  ( S  X.  { x }
)  =  ( u  e.  S  |->  x )
150149a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( S  X.  {
x } )  =  ( u  e.  S  |->  x ) )
151 efneg 13814 . . . . . . . . . . . . . 14  |-  ( ( K  x.  u )  e.  CC  ->  ( exp `  -u ( K  x.  u ) )  =  ( 1  /  ( exp `  ( K  x.  u ) ) ) )
15210, 151syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  S )  ->  ( exp `  -u ( K  x.  u ) )  =  ( 1  /  ( exp `  ( K  x.  u ) ) ) )
153152mpteq2dva 4523 . . . . . . . . . . . 12  |-  ( ph  ->  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) )  =  ( u  e.  S  |->  ( 1  /  ( exp `  ( K  x.  u
) ) ) ) )
1541, 146, 148, 150, 153offval2 6541 . . . . . . . . . . 11  |-  ( ph  ->  ( ( S  X.  { x } )  oF  /  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( u  e.  S  |->  ( x  /  (
1  /  ( exp `  ( K  x.  u
) ) ) ) ) )
155154adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  CC )  ->  ( ( S  X.  { x } )  oF  /  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( u  e.  S  |->  ( x  /  (
1  /  ( exp `  ( K  x.  u
) ) ) ) ) )
156 efcl 13799 . . . . . . . . . . . . . . . . 17  |-  ( ( K  x.  u )  e.  CC  ->  ( exp `  ( K  x.  u ) )  e.  CC )
157 efne0 13813 . . . . . . . . . . . . . . . . 17  |-  ( ( K  x.  u )  e.  CC  ->  ( exp `  ( K  x.  u ) )  =/=  0 )
158156, 157jca 532 . . . . . . . . . . . . . . . 16  |-  ( ( K  x.  u )  e.  CC  ->  (
( exp `  ( K  x.  u )
)  e.  CC  /\  ( exp `  ( K  x.  u ) )  =/=  0 ) )
15910, 158syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  S )  ->  (
( exp `  ( K  x.  u )
)  e.  CC  /\  ( exp `  ( K  x.  u ) )  =/=  0 ) )
160 ax-1ne0 9564 . . . . . . . . . . . . . . . . 17  |-  1  =/=  0
16118, 160pm3.2i 455 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  CC  /\  1  =/=  0 )
162 divdiv2 10263 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  CC  /\  ( 1  e.  CC  /\  1  =/=  0 )  /\  ( ( exp `  ( K  x.  u
) )  e.  CC  /\  ( exp `  ( K  x.  u )
)  =/=  0 ) )  ->  ( x  /  ( 1  / 
( exp `  ( K  x.  u )
) ) )  =  ( ( x  x.  ( exp `  ( K  x.  u )
) )  /  1
) )
163161, 162mp3an2 1313 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  CC  /\  ( ( exp `  ( K  x.  u )
)  e.  CC  /\  ( exp `  ( K  x.  u ) )  =/=  0 ) )  ->  ( x  / 
( 1  /  ( exp `  ( K  x.  u ) ) ) )  =  ( ( x  x.  ( exp `  ( K  x.  u
) ) )  / 
1 ) )
164159, 163sylan2 474 . . . . . . . . . . . . . 14  |-  ( ( x  e.  CC  /\  ( ph  /\  u  e.  S ) )  -> 
( x  /  (
1  /  ( exp `  ( K  x.  u
) ) ) )  =  ( ( x  x.  ( exp `  ( K  x.  u )
) )  /  1
) )
16510, 156syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  S )  ->  ( exp `  ( K  x.  u ) )  e.  CC )
166 mulcl 9579 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  CC  /\  ( exp `  ( K  x.  u ) )  e.  CC )  -> 
( x  x.  ( exp `  ( K  x.  u ) ) )  e.  CC )
167165, 166sylan2 474 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  CC  /\  ( ph  /\  u  e.  S ) )  -> 
( x  x.  ( exp `  ( K  x.  u ) ) )  e.  CC )
168167div1d 10319 . . . . . . . . . . . . . 14  |-  ( ( x  e.  CC  /\  ( ph  /\  u  e.  S ) )  -> 
( ( x  x.  ( exp `  ( K  x.  u )
) )  /  1
)  =  ( x  x.  ( exp `  ( K  x.  u )
) ) )
169164, 168eqtrd 2484 . . . . . . . . . . . . 13  |-  ( ( x  e.  CC  /\  ( ph  /\  u  e.  S ) )  -> 
( x  /  (
1  /  ( exp `  ( K  x.  u
) ) ) )  =  ( x  x.  ( exp `  ( K  x.  u )
) ) )
170169ancoms 453 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  u  e.  S )  /\  x  e.  CC )  ->  (
x  /  ( 1  /  ( exp `  ( K  x.  u )
) ) )  =  ( x  x.  ( exp `  ( K  x.  u ) ) ) )
171170an32s 804 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  CC )  /\  u  e.  S )  ->  (
x  /  ( 1  /  ( exp `  ( K  x.  u )
) ) )  =  ( x  x.  ( exp `  ( K  x.  u ) ) ) )
172171mpteq2dva 4523 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  CC )  ->  ( u  e.  S  |->  ( x  /  ( 1  / 
( exp `  ( K  x.  u )
) ) ) )  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) ) )
173155, 172eqtrd 2484 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  CC )  ->  ( ( S  X.  { x } )  oF  /  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u ) ) ) ) )
174173eqeq2d 2457 . . . . . . . 8  |-  ( (
ph  /\  x  e.  CC )  ->  ( Y  =  ( ( S  X.  { x }
)  oF  / 
( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  <->  Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u ) ) ) ) ) )
175144, 174sylibd 214 . . . . . . 7  |-  ( (
ph  /\  x  e.  CC )  ->  ( ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( S  X.  {
x } )  ->  Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) ) ) )
176175reximdva 2918 . . . . . 6  |-  ( ph  ->  ( E. x  e.  CC  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  =  ( S  X.  { x }
)  ->  E. x  e.  CC  Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u
) ) ) ) ) )
177176adantr 465 . . . . 5  |-  ( (
ph  /\  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) )  ->  ( E. x  e.  CC  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  =  ( S  X.  { x }
)  ->  E. x  e.  CC  Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u
) ) ) ) ) )
178133, 177mpd 15 . . . 4  |-  ( (
ph  /\  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) )  ->  E. x  e.  CC  Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) ) )
179178ex 434 . . 3  |-  ( ph  ->  ( ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y )  ->  E. x  e.  CC  Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) ) ) )
1801adantr 465 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  CC  /\  Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u ) ) ) ) ) )  ->  S  e.  { RR ,  CC } )
1814adantr 465 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  CC  /\  Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u ) ) ) ) ) )  ->  K  e.  CC )
182 simprl 756 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  CC  /\  Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u ) ) ) ) ) )  ->  x  e.  CC )
183 eqid 2443 . . . . . . 7  |-  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) )  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u ) ) ) )
184180, 181, 182, 183expgrowthi 31214 . . . . . 6  |-  ( (
ph  /\  ( x  e.  CC  /\  Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u ) ) ) ) ) )  -> 
( S  _D  (
u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u
) ) ) ) )  =  ( ( S  X.  { K } )  oF  x.  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) ) ) )
1851843impb 1193 . . . . 5  |-  ( (
ph  /\  x  e.  CC  /\  Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u
) ) ) ) )  ->  ( S  _D  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u ) ) ) ) )  =  ( ( S  X.  { K } )  oF  x.  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) ) ) )
186 oveq2 6289 . . . . . . 7  |-  ( Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) )  -> 
( S  _D  Y
)  =  ( S  _D  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) ) ) )
187 oveq2 6289 . . . . . . 7  |-  ( Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) )  -> 
( ( S  X.  { K } )  oF  x.  Y )  =  ( ( S  X.  { K }
)  oF  x.  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u ) ) ) ) ) )
188186, 187eqeq12d 2465 . . . . . 6  |-  ( Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) )  -> 
( ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y )  <->  ( S  _D  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u ) ) ) ) )  =  ( ( S  X.  { K } )  oF  x.  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) ) ) ) )
1891883ad2ant3 1020 . . . . 5  |-  ( (
ph  /\  x  e.  CC  /\  Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u
) ) ) ) )  ->  ( ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y )  <-> 
( S  _D  (
u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u
) ) ) ) )  =  ( ( S  X.  { K } )  oF  x.  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) ) ) ) )
190185, 189mpbird 232 . . . 4  |-  ( (
ph  /\  x  e.  CC  /\  Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u
) ) ) ) )  ->  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) )
191190rexlimdv3a 2937 . . 3  |-  ( ph  ->  ( E. x  e.  CC  Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u
) ) ) )  ->  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) ) )
192179, 191impbid 191 . 2  |-  ( ph  ->  ( ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y )  <->  E. x  e.  CC  Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u
) ) ) ) ) )
193 oveq2 6289 . . . . . . . 8  |-  ( u  =  t  ->  ( K  x.  u )  =  ( K  x.  t ) )
194193fveq2d 5860 . . . . . . 7  |-  ( u  =  t  ->  ( exp `  ( K  x.  u ) )  =  ( exp `  ( K  x.  t )
) )
195194oveq2d 6297 . . . . . 6  |-  ( u  =  t  ->  (
x  x.  ( exp `  ( K  x.  u
) ) )  =  ( x  x.  ( exp `  ( K  x.  t ) ) ) )
196195cbvmptv 4528 . . . . 5  |-  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) )  =  ( t  e.  S  |->  ( x  x.  ( exp `  ( K  x.  t ) ) ) )
197 oveq1 6288 . . . . . 6  |-  ( x  =  c  ->  (
x  x.  ( exp `  ( K  x.  t
) ) )  =  ( c  x.  ( exp `  ( K  x.  t ) ) ) )
198197mpteq2dv 4524 . . . . 5  |-  ( x  =  c  ->  (
t  e.  S  |->  ( x  x.  ( exp `  ( K  x.  t
) ) ) )  =  ( t  e.  S  |->  ( c  x.  ( exp `  ( K  x.  t )
) ) ) )
199196, 198syl5eq 2496 . . . 4  |-  ( x  =  c  ->  (
u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u
) ) ) )  =  ( t  e.  S  |->  ( c  x.  ( exp `  ( K  x.  t )
) ) ) )
200199eqeq2d 2457 . . 3  |-  ( x  =  c  ->  ( Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) )  <->  Y  =  ( t  e.  S  |->  ( c  x.  ( exp `  ( K  x.  t ) ) ) ) ) )
201200cbvrexv 3071 . 2  |-  ( E. x  e.  CC  Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) )  <->  E. c  e.  CC  Y  =  ( t  e.  S  |->  ( c  x.  ( exp `  ( K  x.  t
) ) ) ) )
202192, 201syl6bb 261 1  |-  ( ph  ->  ( ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y )  <->  E. c  e.  CC  Y  =  ( t  e.  S  |->  ( c  x.  ( exp `  ( K  x.  t
) ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 974    = wceq 1383    e. wcel 1804    =/= wne 2638   E.wrex 2794   _Vcvv 3095    \ cdif 3458    C_ wss 3461   {csn 4014   {cpr 4016    |-> cmpt 4495    X. cxp 4987   dom cdm 4989    Fn wfn 5573   -->wf 5574   ` cfv 5578  (class class class)co 6281    oFcof 6523   CCcc 9493   RRcr 9494   0cc0 9495   1c1 9496    + caddc 9498    x. cmul 9500    - cmin 9810   -ucneg 9811    / cdiv 10213   expce 13778    _D cdv 22244
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-inf2 8061  ax-cnex 9551  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571  ax-pre-mulgt0 9572  ax-pre-sup 9573  ax-addf 9574  ax-mulf 9575
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-fal 1389  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rmo 2801  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-int 4272  df-iun 4317  df-iin 4318  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-se 4829  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-isom 5587  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-of 6525  df-om 6686  df-1st 6785  df-2nd 6786  df-supp 6904  df-recs 7044  df-rdg 7078  df-1o 7132  df-2o 7133  df-oadd 7136  df-er 7313  df-map 7424  df-pm 7425  df-ixp 7472  df-en 7519  df-dom 7520  df-sdom 7521  df-fin 7522  df-fsupp 7832  df-fi 7873  df-sup 7903  df-oi 7938  df-card 8323  df-cda 8551  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-sub 9812  df-neg 9813  df-div 10214  df-nn 10544  df-2 10601  df-3 10602  df-4 10603  df-5 10604  df-6 10605  df-7 10606  df-8 10607  df-9 10608  df-10 10609  df-n0 10803  df-z 10872  df-dec 10986  df-uz 11092  df-q 11193  df-rp 11231  df-xneg 11328  df-xadd 11329  df-xmul 11330  df-ioo 11543  df-ico 11545  df-icc 11546  df-fz 11683  df-fzo 11806  df-fl 11910  df-seq 12089  df-exp 12148  df-fac 12335  df-bc 12362  df-hash 12387  df-shft 12881  df-cj 12913  df-re 12914  df-im 12915  df-sqrt 13049  df-abs 13050  df-limsup 13275  df-clim 13292  df-rlim 13293  df-sum 13490  df-ef 13784  df-struct 14615  df-ndx 14616  df-slot 14617  df-base 14618  df-sets 14619  df-ress 14620  df-plusg 14691  df-mulr 14692  df-starv 14693  df-sca 14694  df-vsca 14695  df-ip 14696  df-tset 14697  df-ple 14698  df-ds 14700  df-unif 14701  df-hom 14702  df-cco 14703  df-rest 14801  df-topn 14802  df-0g 14820  df-gsum 14821  df-topgen 14822  df-pt 14823  df-prds 14826  df-xrs 14880  df-qtop 14885  df-imas 14886  df-xps 14888  df-mre 14964  df-mrc 14965  df-acs 14967  df-mgm 15850  df-sgrp 15889  df-mnd 15899  df-submnd 15945  df-mulg 16038  df-cntz 16333  df-cmn 16778  df-psmet 18389  df-xmet 18390  df-met 18391  df-bl 18392  df-mopn 18393  df-fbas 18394  df-fg 18395  df-cnfld 18399  df-top 19376  df-bases 19378  df-topon 19379  df-topsp 19380  df-cld 19497  df-ntr 19498  df-cls 19499  df-nei 19576  df-lp 19614  df-perf 19615  df-cn 19705  df-cnp 19706  df-haus 19793  df-cmp 19864  df-tx 20040  df-hmeo 20233  df-fil 20324  df-fm 20416  df-flim 20417  df-flf 20418  df-xms 20800  df-ms 20801  df-tms 20802  df-cncf 21359  df-limc 22247  df-dv 22248
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator