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

Theorem expgrowth 30795
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 30793 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 30793 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 9574 . . . . . . . . . . . . . . . . . 18  |-  CC  e.  { RR ,  CC }
32a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  CC  e.  { RR ,  CC } )
4 expgrowth.k . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  K  e.  CC )
5 recnprss 22036 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
61, 5syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  S  C_  CC )
76sseld 3496 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( u  e.  S  ->  u  e.  CC ) )
8 mulcl 9565 . . . . . . . . . . . . . . . . . . . 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 9906 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  S )  ->  -u ( K  x.  u )  e.  CC )
124negcld 9906 . . . . . . . . . . . . . . . . . 18  |-  ( ph  -> 
-u K  e.  CC )
1312adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  S )  ->  -u K  e.  CC )
14 efcl 13669 . . . . . . . . . . . . . . . . . 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 9539 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  CC
1918a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  S )  ->  1  e.  CC )
201dvmptid 22088 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( S  _D  (
u  e.  S  |->  u ) )  =  ( u  e.  S  |->  1 ) )
211, 17, 19, 20, 4dvmptcmul 22095 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( S  _D  (
u  e.  S  |->  ( K  x.  u ) ) )  =  ( u  e.  S  |->  ( K  x.  1 ) ) )
224mulid1d 9602 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( K  x.  1 )  =  K )
2322mpteq2dv 4527 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( u  e.  S  |->  ( K  x.  1 ) )  =  ( u  e.  S  |->  K ) )
2421, 23eqtrd 2501 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( S  _D  (
u  e.  S  |->  ( K  x.  u ) ) )  =  ( u  e.  S  |->  K ) )
251, 10, 16, 24dvmptneg 22097 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( S  _D  (
u  e.  S  |->  -u ( K  x.  u
) ) )  =  ( u  e.  S  |-> 
-u K ) )
26 dvef 22109 . . . . . . . . . . . . . . . . . . 19  |-  ( CC 
_D  exp )  =  exp
27 eff 13668 . . . . . . . . . . . . . . . . . . . . . 22  |-  exp : CC
--> CC
28 ffn 5722 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( exp
: CC --> CC  ->  exp 
Fn  CC )
2927, 28ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21  |-  exp  Fn  CC
30 dffn5 5904 . . . . . . . . . . . . . . . . . . . . 21  |-  ( exp 
Fn  CC  <->  exp  =  ( y  e.  CC  |->  ( exp `  y ) ) )
3129, 30mpbi 208 . . . . . . . . . . . . . . . . . . . 20  |-  exp  =  ( y  e.  CC  |->  ( exp `  y ) )
3231oveq2i 6286 . . . . . . . . . . . . . . . . . . 19  |-  ( CC 
_D  exp )  =  ( CC  _D  ( y  e.  CC  |->  ( exp `  y ) ) )
3326, 32, 313eqtr3i 2497 . . . . . . . . . . . . . . . . . 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 5857 . . . . . . . . . . . . . . . . 17  |-  ( y  =  -u ( K  x.  u )  ->  ( exp `  y )  =  ( exp `  -u ( K  x.  u )
) )
361, 3, 11, 13, 15, 15, 25, 34, 35, 35dvmptco 22103 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( S  _D  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u )
)  x.  -u K
) ) )
3736oveq2d 6291 . . . . . . . . . . . . . . 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 13669 . . . . . . . . . . . . . . . . . . . 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 9605 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  S )  ->  (
( exp `  -u ( K  x.  u )
)  x.  -u K
)  e.  CC )
42 eqid 2460 . . . . . . . . . . . . . . . . . 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 6036 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u )
)  x.  -u K
) ) : S --> CC )
4436feq1d 5708 . . . . . . . . . . . . . . . . 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 9567 . . . . . . . . . . . . . . . . 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 6547 . . . . . . . . . . . . . . 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 2503 . . . . . . . . . . . . . 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 6291 . . . . . . . . . . . . 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 5765 . . . . . . . . . . . . . . . . . 18  |-  ( -u K  e.  CC  ->  ( S  X.  { -u K } ) : S --> CC )
5212, 51syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( S  X.  { -u K } ) : S --> CC )
53 eqid 2460 . . . . . . . . . . . . . . . . . 18  |-  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) )  =  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) )
5440, 53fmptd 6036 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) : S --> CC )
551, 52, 54, 47caofcom 6547 . . . . . . . . . . . . . . . 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 2461 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) )  =  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )
57 fconstmpt 5035 . . . . . . . . . . . . . . . . . 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 6531 . . . . . . . . . . . . . . . 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 2501 . . . . . . . . . . . . . . 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 6291 . . . . . . . . . . . . . 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 6291 . . . . . . . . . . . . 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 5196 . . . . . . . . . . . . . . 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 ) ) )
65 fdm 5726 . . . . . . . . . . . . . . . 16  |-  ( ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u )
)  x.  -u K
) ) : S --> CC  ->  dom  ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u )
)  x.  -u K
) )  =  S )
6643, 65syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u ) )  x.  -u K ) )  =  S )
6764, 66eqtrd 2501 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( S  _D  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  S )
681, 38, 54, 63, 67dvmulf 22074 . . . . . . . . . . . . 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 ) ) )
6950, 62, 683eqtr4rd 2512 . . . . . . . . . . . 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 ) ) ) ) ) ) )
70 ofmul12 30785 . . . . . . . . . . . . . 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 )
) ) ) ) )
711, 38, 52, 54, 70syl22anc 1224 . . . . . . . . . . . . 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 ) ) ) ) ) )
7271oveq2d 6291 . . . . . . . . . . . 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 ) ) ) ) ) ) )
7369, 72eqtrd 2501 . . . . . . . . . . 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 ) ) ) ) ) ) )
74 oveq1 6282 . . . . . . . . . . . 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 )
) ) ) )
7574oveq1d 6290 . . . . . . . . . . 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 )
) ) ) ) ) )
7673, 75sylan9eq 2521 . . . . . . . . . 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 )
) ) ) ) ) )
77 mulass 9569 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  CC  /\  y  e.  CC  /\  z  e.  CC )  ->  (
( x  x.  y
)  x.  z )  =  ( x  x.  ( y  x.  z
) ) )
7877adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  CC  /\  y  e.  CC  /\  z  e.  CC ) )  -> 
( ( x  x.  y )  x.  z
)  =  ( x  x.  ( y  x.  z ) ) )
791, 52, 38, 54, 78caofass 6549 . . . . . . . . . . . . 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 ) ) ) ) ) )
8079oveq2d 6291 . . . . . . . . . . . 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 ) ) ) ) ) ) )
8180eqeq2d 2474 . . . . . . . . . . 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 )
) ) ) ) ) ) )
8281adantr 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 )
) ) ) ) ) ) )
8376, 82mpbird 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 ) ) ) ) ) )
84 mulcl 9565 . . . . . . . . . . . . . 14  |-  ( ( x  e.  CC  /\  y  e.  CC )  ->  ( x  x.  y
)  e.  CC )
8584adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  CC  /\  y  e.  CC ) )  -> 
( x  x.  y
)  e.  CC )
86 fconst6g 5765 . . . . . . . . . . . . . 14  |-  ( K  e.  CC  ->  ( S  X.  { K }
) : S --> CC )
874, 86syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S  X.  { K } ) : S --> CC )
88 inidm 3700 . . . . . . . . . . . . 13  |-  ( S  i^i  S )  =  S
8985, 87, 38, 1, 1, 88off 6529 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S  X.  { K } )  oF  x.  Y ) : S --> CC )
9085, 52, 38, 1, 1, 88off 6529 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S  X.  { -u K } )  oF  x.  Y
) : S --> CC )
91 adddir 9576 . . . . . . . . . . . . 13  |-  ( ( x  e.  CC  /\  y  e.  CC  /\  z  e.  CC )  ->  (
( x  +  y )  x.  z )  =  ( ( x  x.  z )  +  ( y  x.  z
) ) )
9291adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  CC  /\  y  e.  CC  /\  z  e.  CC ) )  -> 
( ( x  +  y )  x.  z
)  =  ( ( x  x.  z )  +  ( y  x.  z ) ) )
931, 54, 89, 90, 92caofdir 6552 . . . . . . . . . . 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 ) ) ) ) ) )
9493eqeq2d 2474 . . . . . . . . . 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 ) ) ) ) ) ) )
9594adantr 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 ) ) ) ) ) ) )
9683, 95mpbird 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 )
) ) ) )
97 ofnegsub 10523 . . . . . . . . . . . . 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 ) ) )
981, 89, 89, 97syl3anc 1223 . . . . . . . . . . . 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 ) ) )
99 neg1cn 10628 . . . . . . . . . . . . . . . . 17  |-  -u 1  e.  CC
10099fconst6 5766 . . . . . . . . . . . . . . . 16  |-  ( S  X.  { -u 1 } ) : S --> CC
101100a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( S  X.  { -u 1 } ) : S --> CC )
1021, 101, 87, 38, 78caofass 6549 . . . . . . . . . . . . . 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 ) ) )
10399a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  -> 
-u 1  e.  CC )
1041, 103, 4ofc12 6540 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( S  X.  { -u 1 } )  oF  x.  ( S  X.  { K }
) )  =  ( S  X.  { (
-u 1  x.  K
) } ) )
1054mulm1d 9997 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( -u 1  x.  K )  =  -u K )
106105sneqd 4032 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  { ( -u 1  x.  K ) }  =  { -u K } )
107106xpeq2d 5016 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( S  X.  {
( -u 1  x.  K
) } )  =  ( S  X.  { -u K } ) )
108104, 107eqtrd 2501 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( S  X.  { -u 1 } )  oF  x.  ( S  X.  { K }
) )  =  ( S  X.  { -u K } ) )
109108oveq1d 6290 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( S  X.  { -u 1 } )  oF  x.  ( S  X.  { K } ) )  oF  x.  Y
)  =  ( ( S  X.  { -u K } )  oF  x.  Y ) )
110102, 109eqtr3d 2503 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S  X.  { -u 1 } )  oF  x.  (
( S  X.  { K } )  oF  x.  Y ) )  =  ( ( S  X.  { -u K } )  oF  x.  Y ) )
111110oveq2d 6291 . . . . . . . . . . . 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 ) ) )
112 ofsubid 30784 . . . . . . . . . . . . 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 } ) )
1131, 89, 112syl2anc 661 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( S  X.  { K }
)  oF  x.  Y )  oF  -  ( ( S  X.  { K }
)  oF  x.  Y ) )  =  ( S  X.  {
0 } ) )
11498, 111, 1133eqtr3d 2509 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( S  X.  { K }
)  oF  x.  Y )  oF  +  ( ( S  X.  { -u K } )  oF  x.  Y ) )  =  ( S  X.  { 0 } ) )
115114oveq1d 6290 . . . . . . . . . 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 )
) ) ) )
116115eqeq2d 2474 . . . . . . . . 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 )
) ) ) ) )
117116adantr 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 )
) ) ) ) )
11896, 117mpbid 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 )
) ) ) )
119 0cnd 9578 . . . . . . . . 9  |-  ( ph  ->  0  e.  CC )
120 mul02 9746 . . . . . . . . . 10  |-  ( x  e.  CC  ->  (
0  x.  x )  =  0 )
121120adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  CC )  ->  ( 0  x.  x )  =  0 )
1221, 54, 119, 119, 121caofid2 6546 . . . . . . . 8  |-  ( ph  ->  ( ( S  X.  { 0 } )  oF  x.  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( S  X.  {
0 } ) )
123122adantr 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 } ) )
124118, 123eqtrd 2501 . . . . . 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 } ) )
1251adantr 465 . . . . . . 7  |-  ( (
ph  /\  ( S  _D  Y )  =  ( ( S  X.  { K } )  oF  x.  Y ) )  ->  S  e.  { RR ,  CC } )
12685, 38, 54, 1, 1, 88off 6529 . . . . . . . 8  |-  ( ph  ->  ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) ) : S --> CC )
127126adantr 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 )
128124dmeqd 5196 . . . . . . . 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 } ) )
129 0cn 9577 . . . . . . . . . 10  |-  0  e.  CC
130129fconst6 5766 . . . . . . . . 9  |-  ( S  X.  { 0 } ) : S --> CC
131130fdmi 5727 . . . . . . . 8  |-  dom  ( S  X.  { 0 } )  =  S
132128, 131syl6eq 2517 . . . . . . 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 )
133125, 127, 132dvconstbi 30794 . . . . . 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 }
) ) )
134124, 133mpbid 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 } ) )
135 oveq1 6282 . . . . . . . . . 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 )
) ) ) )
136 efne0 13682 . . . . . . . . . . . . . . 15  |-  ( -u ( K  x.  u
)  e.  CC  ->  ( exp `  -u ( K  x.  u )
)  =/=  0 )
137 eldifsn 4145 . . . . . . . . . . . . . . 15  |-  ( ( exp `  -u ( K  x.  u )
)  e.  ( CC 
\  { 0 } )  <->  ( ( exp `  -u ( K  x.  u ) )  e.  CC  /\  ( exp `  -u ( K  x.  u ) )  =/=  0 ) )
13839, 136, 137sylanbrc 664 . . . . . . . . . . . . . 14  |-  ( -u ( K  x.  u
)  e.  CC  ->  ( exp `  -u ( K  x.  u )
)  e.  ( CC 
\  { 0 } ) )
13911, 138syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  S )  ->  ( exp `  -u ( K  x.  u ) )  e.  ( CC  \  {
0 } ) )
140139, 53fmptd 6036 . . . . . . . . . . . 12  |-  ( ph  ->  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) : S --> ( CC  \  { 0 } ) )
141 ofdivcan4 30787 . . . . . . . . . . . 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 )
1421, 38, 140, 141syl3anc 1223 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  / 
( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  Y )
143142eqeq1d 2462 . . . . . . . . . 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 )
) ) ) ) )
144135, 143syl5ib 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 )
) ) ) ) )
145144adantr 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 )
) ) ) ) )
146 vex 3109 . . . . . . . . . . . . 13  |-  x  e. 
_V
147146a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S )  ->  x  e.  _V )
148 ovex 6300 . . . . . . . . . . . . 13  |-  ( 1  /  ( exp `  ( K  x.  u )
) )  e.  _V
149148a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S )  ->  (
1  /  ( exp `  ( K  x.  u
) ) )  e. 
_V )
150 fconstmpt 5035 . . . . . . . . . . . . 13  |-  ( S  X.  { x }
)  =  ( u  e.  S  |->  x )
151150a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( S  X.  {
x } )  =  ( u  e.  S  |->  x ) )
152 efneg 13683 . . . . . . . . . . . . . 14  |-  ( ( K  x.  u )  e.  CC  ->  ( exp `  -u ( K  x.  u ) )  =  ( 1  /  ( exp `  ( K  x.  u ) ) ) )
15310, 152syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  S )  ->  ( exp `  -u ( K  x.  u ) )  =  ( 1  /  ( exp `  ( K  x.  u ) ) ) )
154153mpteq2dva 4526 . . . . . . . . . . . 12  |-  ( ph  ->  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) )  =  ( u  e.  S  |->  ( 1  /  ( exp `  ( K  x.  u
) ) ) ) )
1551, 147, 149, 151, 154offval2 6531 . . . . . . . . . . 11  |-  ( ph  ->  ( ( S  X.  { x } )  oF  /  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( u  e.  S  |->  ( x  /  (
1  /  ( exp `  ( K  x.  u
) ) ) ) ) )
156155adantr 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
) ) ) ) ) )
157 efcl 13669 . . . . . . . . . . . . . . . . 17  |-  ( ( K  x.  u )  e.  CC  ->  ( exp `  ( K  x.  u ) )  e.  CC )
158 efne0 13682 . . . . . . . . . . . . . . . . 17  |-  ( ( K  x.  u )  e.  CC  ->  ( exp `  ( K  x.  u ) )  =/=  0 )
159157, 158jca 532 . . . . . . . . . . . . . . . 16  |-  ( ( K  x.  u )  e.  CC  ->  (
( exp `  ( K  x.  u )
)  e.  CC  /\  ( exp `  ( K  x.  u ) )  =/=  0 ) )
16010, 159syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  S )  ->  (
( exp `  ( K  x.  u )
)  e.  CC  /\  ( exp `  ( K  x.  u ) )  =/=  0 ) )
161 ax-1ne0 9550 . . . . . . . . . . . . . . . . 17  |-  1  =/=  0
16218, 161pm3.2i 455 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  CC  /\  1  =/=  0 )
163 divdiv2 10245 . . . . . . . . . . . . . . . 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
) )
164162, 163mp3an2 1307 . . . . . . . . . . . . . . 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 ) )
165160, 164sylan2 474 . . . . . . . . . . . . . 14  |-  ( ( x  e.  CC  /\  ( ph  /\  u  e.  S ) )  -> 
( x  /  (
1  /  ( exp `  ( K  x.  u
) ) ) )  =  ( ( x  x.  ( exp `  ( K  x.  u )
) )  /  1
) )
16610, 157syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  S )  ->  ( exp `  ( K  x.  u ) )  e.  CC )
167 mulcl 9565 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  CC  /\  ( exp `  ( K  x.  u ) )  e.  CC )  -> 
( x  x.  ( exp `  ( K  x.  u ) ) )  e.  CC )
168166, 167sylan2 474 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  CC  /\  ( ph  /\  u  e.  S ) )  -> 
( x  x.  ( exp `  ( K  x.  u ) ) )  e.  CC )
169168div1d 10301 . . . . . . . . . . . . . 14  |-  ( ( x  e.  CC  /\  ( ph  /\  u  e.  S ) )  -> 
( ( x  x.  ( exp `  ( K  x.  u )
) )  /  1
)  =  ( x  x.  ( exp `  ( K  x.  u )
) ) )
170165, 169eqtrd 2501 . . . . . . . . . . . . 13  |-  ( ( x  e.  CC  /\  ( ph  /\  u  e.  S ) )  -> 
( x  /  (
1  /  ( exp `  ( K  x.  u
) ) ) )  =  ( x  x.  ( exp `  ( K  x.  u )
) ) )
171170ancoms 453 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  u  e.  S )  /\  x  e.  CC )  ->  (
x  /  ( 1  /  ( exp `  ( K  x.  u )
) ) )  =  ( x  x.  ( exp `  ( K  x.  u ) ) ) )
172171an32s 802 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  CC )  /\  u  e.  S )  ->  (
x  /  ( 1  /  ( exp `  ( K  x.  u )
) ) )  =  ( x  x.  ( exp `  ( K  x.  u ) ) ) )
173172mpteq2dva 4526 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  CC )  ->  ( u  e.  S  |->  ( x  /  ( 1  / 
( exp `  ( K  x.  u )
) ) ) )  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) ) )
174156, 173eqtrd 2501 . . . . . . . . 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 ) ) ) ) )
175174eqeq2d 2474 . . . . . . . 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 ) ) ) ) ) )
176145, 175sylibd 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 )
) ) ) ) )
177176reximdva 2931 . . . . . 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
) ) ) ) ) )
178177adantr 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
) ) ) ) ) )
179134, 178mpd 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 )
) ) ) )
180179ex 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 )
) ) ) ) )
1811adantr 465 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  CC  /\  Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u ) ) ) ) ) )  ->  S  e.  { RR ,  CC } )
1824adantr 465 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  CC  /\  Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u ) ) ) ) ) )  ->  K  e.  CC )
183 simprl 755 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  CC  /\  Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u ) ) ) ) ) )  ->  x  e.  CC )
184 eqid 2460 . . . . . . 7  |-  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) )  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u ) ) ) )
185181, 182, 183, 184expgrowthi 30793 . . . . . 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 )
) ) ) ) )
1861853impb 1187 . . . . 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 )
) ) ) ) )
187 oveq2 6283 . . . . . . 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 )
) ) ) ) )
188 oveq2 6283 . . . . . . 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 ) ) ) ) ) )
189187, 188eqeq12d 2482 . . . . . 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 )
) ) ) ) ) )
1901893ad2ant3 1014 . . . . 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 )
) ) ) ) ) )
191186, 190mpbird 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 ) )
192191rexlimdv3a 2950 . . 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 ) ) )
193180, 192impbid 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
) ) ) ) ) )
194 oveq2 6283 . . . . . . . 8  |-  ( u  =  t  ->  ( K  x.  u )  =  ( K  x.  t ) )
195194fveq2d 5861 . . . . . . 7  |-  ( u  =  t  ->  ( exp `  ( K  x.  u ) )  =  ( exp `  ( K  x.  t )
) )
196195oveq2d 6291 . . . . . 6  |-  ( u  =  t  ->  (
x  x.  ( exp `  ( K  x.  u
) ) )  =  ( x  x.  ( exp `  ( K  x.  t ) ) ) )
197196cbvmptv 4531 . . . . 5  |-  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) )  =  ( t  e.  S  |->  ( x  x.  ( exp `  ( K  x.  t ) ) ) )
198 oveq1 6282 . . . . . 6  |-  ( x  =  c  ->  (
x  x.  ( exp `  ( K  x.  t
) ) )  =  ( c  x.  ( exp `  ( K  x.  t ) ) ) )
199198mpteq2dv 4527 . . . . 5  |-  ( x  =  c  ->  (
t  e.  S  |->  ( x  x.  ( exp `  ( K  x.  t
) ) ) )  =  ( t  e.  S  |->  ( c  x.  ( exp `  ( K  x.  t )
) ) ) )
200197, 199syl5eq 2513 . . . 4  |-  ( x  =  c  ->  (
u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u
) ) ) )  =  ( t  e.  S  |->  ( c  x.  ( exp `  ( K  x.  t )
) ) ) )
201200eqeq2d 2474 . . 3  |-  ( x  =  c  ->  ( Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) )  <->  Y  =  ( t  e.  S  |->  ( c  x.  ( exp `  ( K  x.  t ) ) ) ) ) )
202201cbvrexv 3082 . 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
) ) ) ) )
203193, 202syl6bb 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 968    = wceq 1374    e. wcel 1762    =/= wne 2655   E.wrex 2808   _Vcvv 3106    \ cdif 3466    C_ wss 3469   {csn 4020   {cpr 4022    |-> cmpt 4498    X. cxp 4990   dom cdm 4992    Fn wfn 5574   -->wf 5575   ` cfv 5579  (class class class)co 6275    oFcof 6513   CCcc 9479   RRcr 9480   0cc0 9481   1c1 9482    + caddc 9484    x. cmul 9486    - cmin 9794   -ucneg 9795    / cdiv 10195   expce 13648    _D cdv 21995
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-rep 4551  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567  ax-inf2 8047  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558  ax-pre-sup 9559  ax-addf 9560  ax-mulf 9561
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-fal 1380  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-nel 2658  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-pss 3485  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-tp 4025  df-op 4027  df-uni 4239  df-int 4276  df-iun 4320  df-iin 4321  df-br 4441  df-opab 4499  df-mpt 4500  df-tr 4534  df-eprel 4784  df-id 4788  df-po 4793  df-so 4794  df-fr 4831  df-se 4832  df-we 4833  df-ord 4874  df-on 4875  df-lim 4876  df-suc 4877  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587  df-isom 5588  df-riota 6236  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-of 6515  df-om 6672  df-1st 6774  df-2nd 6775  df-supp 6892  df-recs 7032  df-rdg 7066  df-1o 7120  df-2o 7121  df-oadd 7124  df-er 7301  df-map 7412  df-pm 7413  df-ixp 7460  df-en 7507  df-dom 7508  df-sdom 7509  df-fin 7510  df-fsupp 7819  df-fi 7860  df-sup 7890  df-oi 7924  df-card 8309  df-cda 8537  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9796  df-neg 9797  df-div 10196  df-nn 10526  df-2 10583  df-3 10584  df-4 10585  df-5 10586  df-6 10587  df-7 10588  df-8 10589  df-9 10590  df-10 10591  df-n0 10785  df-z 10854  df-dec 10966  df-uz 11072  df-q 11172  df-rp 11210  df-xneg 11307  df-xadd 11308  df-xmul 11309  df-ioo 11522  df-ico 11524  df-icc 11525  df-fz 11662  df-fzo 11782  df-fl 11886  df-seq 12064  df-exp 12123  df-fac 12309  df-bc 12336  df-hash 12361  df-shft 12850  df-cj 12882  df-re 12883  df-im 12884  df-sqr 13018  df-abs 13019  df-limsup 13243  df-clim 13260  df-rlim 13261  df-sum 13458  df-ef 13654  df-struct 14481  df-ndx 14482  df-slot 14483  df-base 14484  df-sets 14485  df-ress 14486  df-plusg 14557  df-mulr 14558  df-starv 14559  df-sca 14560  df-vsca 14561  df-ip 14562  df-tset 14563  df-ple 14564  df-ds 14566  df-unif 14567  df-hom 14568  df-cco 14569  df-rest 14667  df-topn 14668  df-0g 14686  df-gsum 14687  df-topgen 14688  df-pt 14689  df-prds 14692  df-xrs 14746  df-qtop 14751  df-imas 14752  df-xps 14754  df-mre 14830  df-mrc 14831  df-acs 14833  df-mnd 15721  df-submnd 15771  df-mulg 15854  df-cntz 16143  df-cmn 16589  df-psmet 18175  df-xmet 18176  df-met 18177  df-bl 18178  df-mopn 18179  df-fbas 18180  df-fg 18181  df-cnfld 18185  df-top 19159  df-bases 19161  df-topon 19162  df-topsp 19163  df-cld 19279  df-ntr 19280  df-cls 19281  df-nei 19358  df-lp 19396  df-perf 19397  df-cn 19487  df-cnp 19488  df-haus 19575  df-cmp 19646  df-tx 19791  df-hmeo 19984  df-fil 20075  df-fm 20167  df-flim 20168  df-flf 20169  df-xms 20551  df-ms 20552  df-tms 20553  df-cncf 21110  df-limc 21998  df-dv 21999
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator