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

Theorem expgrowth 29606
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 29604 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 29604 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 9373 . . . . . . . . . . . . . . . . . 18  |-  CC  e.  { RR ,  CC }
32a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  CC  e.  { RR ,  CC } )
4 expgrowth.k . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  K  e.  CC )
5 recnprss 21377 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
61, 5syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  S  C_  CC )
76sseld 3353 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( u  e.  S  ->  u  e.  CC ) )
8 mulcl 9364 . . . . . . . . . . . . . . . . . . . 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 9704 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  S )  ->  -u ( K  x.  u )  e.  CC )
124negcld 9704 . . . . . . . . . . . . . . . . . 18  |-  ( ph  -> 
-u K  e.  CC )
1312adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  S )  ->  -u K  e.  CC )
14 efcl 13366 . . . . . . . . . . . . . . . . . 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 9338 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  CC
1918a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  S )  ->  1  e.  CC )
201dvmptid 21429 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( S  _D  (
u  e.  S  |->  u ) )  =  ( u  e.  S  |->  1 ) )
211, 17, 19, 20, 4dvmptcmul 21436 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( S  _D  (
u  e.  S  |->  ( K  x.  u ) ) )  =  ( u  e.  S  |->  ( K  x.  1 ) ) )
224mulid1d 9401 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( K  x.  1 )  =  K )
2322mpteq2dv 4377 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( u  e.  S  |->  ( K  x.  1 ) )  =  ( u  e.  S  |->  K ) )
2421, 23eqtrd 2473 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( S  _D  (
u  e.  S  |->  ( K  x.  u ) ) )  =  ( u  e.  S  |->  K ) )
251, 10, 16, 24dvmptneg 21438 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( S  _D  (
u  e.  S  |->  -u ( K  x.  u
) ) )  =  ( u  e.  S  |-> 
-u K ) )
26 dvef 21450 . . . . . . . . . . . . . . . . . . 19  |-  ( CC 
_D  exp )  =  exp
27 eff 13365 . . . . . . . . . . . . . . . . . . . . . 22  |-  exp : CC
--> CC
28 ffn 5557 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( exp
: CC --> CC  ->  exp 
Fn  CC )
2927, 28ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21  |-  exp  Fn  CC
30 dffn5 5735 . . . . . . . . . . . . . . . . . . . . 21  |-  ( exp 
Fn  CC  <->  exp  =  ( y  e.  CC  |->  ( exp `  y ) ) )
3129, 30mpbi 208 . . . . . . . . . . . . . . . . . . . 20  |-  exp  =  ( y  e.  CC  |->  ( exp `  y ) )
3231oveq2i 6100 . . . . . . . . . . . . . . . . . . 19  |-  ( CC 
_D  exp )  =  ( CC  _D  ( y  e.  CC  |->  ( exp `  y ) ) )
3326, 32, 313eqtr3i 2469 . . . . . . . . . . . . . . . . . 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 5689 . . . . . . . . . . . . . . . . 17  |-  ( y  =  -u ( K  x.  u )  ->  ( exp `  y )  =  ( exp `  -u ( K  x.  u )
) )
361, 3, 11, 13, 15, 15, 25, 34, 35, 35dvmptco 21444 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( S  _D  (
u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u )
)  x.  -u K
) ) )
3736oveq2d 6105 . . . . . . . . . . . . . . 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 13366 . . . . . . . . . . . . . . . . . . . 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 9404 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  S )  ->  (
( exp `  -u ( K  x.  u )
)  x.  -u K
)  e.  CC )
42 eqid 2441 . . . . . . . . . . . . . . . . . 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 5865 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( u  e.  S  |->  ( ( exp `  -u ( K  x.  u )
)  x.  -u K
) ) : S --> CC )
4436feq1d 5544 . . . . . . . . . . . . . . . . 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 9366 . . . . . . . . . . . . . . . . 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 6350 . . . . . . . . . . . . . . 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 2475 . . . . . . . . . . . . . 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 6105 . . . . . . . . . . . . 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 5597 . . . . . . . . . . . . . . . . . 18  |-  ( -u K  e.  CC  ->  ( S  X.  { -u K } ) : S --> CC )
5212, 51syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( S  X.  { -u K } ) : S --> CC )
53 eqid 2441 . . . . . . . . . . . . . . . . . 18  |-  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) )  =  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) )
5440, 53fmptd 5865 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) : S --> CC )
551, 52, 54, 47caofcom 6350 . . . . . . . . . . . . . . . 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 2442 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) )  =  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )
57 fconstmpt 4880 . . . . . . . . . . . . . . . . . 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 6334 . . . . . . . . . . . . . . . 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 2473 . . . . . . . . . . . . . . 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 6105 . . . . . . . . . . . . . 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 6105 . . . . . . . . . . . . 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 5040 . . . . . . . . . . . . . . 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 5561 . . . . . . . . . . . . . . . 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 2473 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( S  _D  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  S )
681, 38, 54, 63, 67dvmulf 21415 . . . . . . . . . . . . 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 2484 . . . . . . . . . . . 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 29596 . . . . . . . . . . . . . 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 1219 . . . . . . . . . . . . 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 6105 . . . . . . . . . . . 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 2473 . . . . . . . . . . 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 6096 . . . . . . . . . . . 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 6104 . . . . . . . . . . 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 2493 . . . . . . . . . 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 9368 . . . . . . . . . . . . . . 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 6352 . . . . . . . . . . . . 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 6105 . . . . . . . . . . . 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 2452 . . . . . . . . . . 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 9364 . . . . . . . . . . . . . 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 5597 . . . . . . . . . . . . . 14  |-  ( K  e.  CC  ->  ( S  X.  { K }
) : S --> CC )
874, 86syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S  X.  { K } ) : S --> CC )
88 inidm 3557 . . . . . . . . . . . . 13  |-  ( S  i^i  S )  =  S
8985, 87, 38, 1, 1, 88off 6332 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S  X.  { K } )  oF  x.  Y ) : S --> CC )
9085, 52, 38, 1, 1, 88off 6332 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S  X.  { -u K } )  oF  x.  Y
) : S --> CC )
91 adddir 9375 . . . . . . . . . . . . 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 6355 . . . . . . . . . . 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 2452 . . . . . . . . . 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 10318 . . . . . . . . . . . . 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 1218 . . . . . . . . . . . 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 10423 . . . . . . . . . . . . . . . . 17  |-  -u 1  e.  CC
10099fconst6 5598 . . . . . . . . . . . . . . . 16  |-  ( S  X.  { -u 1 } ) : S --> CC
101100a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( S  X.  { -u 1 } ) : S --> CC )
1021, 101, 87, 38, 78caofass 6352 . . . . . . . . . . . . . 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 6343 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( S  X.  { -u 1 } )  oF  x.  ( S  X.  { K }
) )  =  ( S  X.  { (
-u 1  x.  K
) } ) )
1054mulm1d 9794 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( -u 1  x.  K )  =  -u K )
106105sneqd 3887 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  { ( -u 1  x.  K ) }  =  { -u K } )
107106xpeq2d 4862 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( S  X.  {
( -u 1  x.  K
) } )  =  ( S  X.  { -u K } ) )
108104, 107eqtrd 2473 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( S  X.  { -u 1 } )  oF  x.  ( S  X.  { K }
) )  =  ( S  X.  { -u K } ) )
109108oveq1d 6104 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( S  X.  { -u 1 } )  oF  x.  ( S  X.  { K } ) )  oF  x.  Y
)  =  ( ( S  X.  { -u K } )  oF  x.  Y ) )
110102, 109eqtr3d 2475 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S  X.  { -u 1 } )  oF  x.  (
( S  X.  { K } )  oF  x.  Y ) )  =  ( ( S  X.  { -u K } )  oF  x.  Y ) )
111110oveq2d 6105 . . . . . . . . . . . 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 29595 . . . . . . . . . . . . 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 2481 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( S  X.  { K }
)  oF  x.  Y )  oF  +  ( ( S  X.  { -u K } )  oF  x.  Y ) )  =  ( S  X.  { 0 } ) )
115114oveq1d 6104 . . . . . . . . . 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 2452 . . . . . . . . 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 9377 . . . . . . . . 9  |-  ( ph  ->  0  e.  CC )
120 mul02 9545 . . . . . . . . . 10  |-  ( x  e.  CC  ->  (
0  x.  x )  =  0 )
121120adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  CC )  ->  ( 0  x.  x )  =  0 )
1221, 54, 119, 119, 121caofid2 6349 . . . . . . . 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 2473 . . . . . 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 6332 . . . . . . . 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 5040 . . . . . . . 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 9376 . . . . . . . . . 10  |-  0  e.  CC
130129fconst6 5598 . . . . . . . . 9  |-  ( S  X.  { 0 } ) : S --> CC
131130fdmi 5562 . . . . . . . 8  |-  dom  ( S  X.  { 0 } )  =  S
132128, 131syl6eq 2489 . . . . . . 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 29605 . . . . . 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 6096 . . . . . . . . . 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 13379 . . . . . . . . . . . . . . 15  |-  ( -u ( K  x.  u
)  e.  CC  ->  ( exp `  -u ( K  x.  u )
)  =/=  0 )
137 eldifsn 3998 . . . . . . . . . . . . . . 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 5865 . . . . . . . . . . . 12  |-  ( ph  ->  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) : S --> ( CC  \  { 0 } ) )
141 ofdivcan4 29598 . . . . . . . . . . . 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 1218 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Y  oF  x.  ( u  e.  S  |->  ( exp `  -u ( K  x.  u ) ) ) )  oF  / 
( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) ) )  =  Y )
143142eqeq1d 2449 . . . . . . . . . 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 2973 . . . . . . . . . . . . 13  |-  x  e. 
_V
147146a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S )  ->  x  e.  _V )
148 ovex 6114 . . . . . . . . . . . . 13  |-  ( 1  /  ( exp `  ( K  x.  u )
) )  e.  _V
149148a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S )  ->  (
1  /  ( exp `  ( K  x.  u
) ) )  e. 
_V )
150 fconstmpt 4880 . . . . . . . . . . . . 13  |-  ( S  X.  { x }
)  =  ( u  e.  S  |->  x )
151150a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( S  X.  {
x } )  =  ( u  e.  S  |->  x ) )
152 efneg 13380 . . . . . . . . . . . . . 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 4376 . . . . . . . . . . . 12  |-  ( ph  ->  ( u  e.  S  |->  ( exp `  -u ( K  x.  u )
) )  =  ( u  e.  S  |->  ( 1  /  ( exp `  ( K  x.  u
) ) ) ) )
1551, 147, 149, 151, 154offval2 6334 . . . . . . . . . . 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 13366 . . . . . . . . . . . . . . . . 17  |-  ( ( K  x.  u )  e.  CC  ->  ( exp `  ( K  x.  u ) )  e.  CC )
158 efne0 13379 . . . . . . . . . . . . . . . . 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 9349 . . . . . . . . . . . . . . . . 17  |-  1  =/=  0
16218, 161pm3.2i 455 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  CC  /\  1  =/=  0 )
163 divdiv2 10041 . . . . . . . . . . . . . . . 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 1302 . . . . . . . . . . . . . . 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 9364 . . . . . . . . . . . . . . . 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 10097 . . . . . . . . . . . . . 14  |-  ( ( x  e.  CC  /\  ( ph  /\  u  e.  S ) )  -> 
( ( x  x.  ( exp `  ( K  x.  u )
) )  /  1
)  =  ( x  x.  ( exp `  ( K  x.  u )
) ) )
170165, 169eqtrd 2473 . . . . . . . . . . . . 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 4376 . . . . . . . . . 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 2473 . . . . . . . . 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 2452 . . . . . . . 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 2826 . . . . . 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 2441 . . . . . . 7  |-  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) )  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u ) ) ) )
185181, 182, 183, 184expgrowthi 29604 . . . . . 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 1183 . . . . 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 6097 . . . . . . 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 6097 . . . . . . 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 2455 . . . . . 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 1011 . . . . 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 2841 . . 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 6097 . . . . . . . 8  |-  ( u  =  t  ->  ( K  x.  u )  =  ( K  x.  t ) )
195194fveq2d 5693 . . . . . . 7  |-  ( u  =  t  ->  ( exp `  ( K  x.  u ) )  =  ( exp `  ( K  x.  t )
) )
196195oveq2d 6105 . . . . . 6  |-  ( u  =  t  ->  (
x  x.  ( exp `  ( K  x.  u
) ) )  =  ( x  x.  ( exp `  ( K  x.  t ) ) ) )
197196cbvmptv 4381 . . . . 5  |-  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) )  =  ( t  e.  S  |->  ( x  x.  ( exp `  ( K  x.  t ) ) ) )
198 oveq1 6096 . . . . . 6  |-  ( x  =  c  ->  (
x  x.  ( exp `  ( K  x.  t
) ) )  =  ( c  x.  ( exp `  ( K  x.  t ) ) ) )
199198mpteq2dv 4377 . . . . 5  |-  ( x  =  c  ->  (
t  e.  S  |->  ( x  x.  ( exp `  ( K  x.  t
) ) ) )  =  ( t  e.  S  |->  ( c  x.  ( exp `  ( K  x.  t )
) ) ) )
200197, 199syl5eq 2485 . . . 4  |-  ( x  =  c  ->  (
u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u
) ) ) )  =  ( t  e.  S  |->  ( c  x.  ( exp `  ( K  x.  t )
) ) ) )
201200eqeq2d 2452 . . 3  |-  ( x  =  c  ->  ( Y  =  ( u  e.  S  |->  ( x  x.  ( exp `  ( K  x.  u )
) ) )  <->  Y  =  ( t  e.  S  |->  ( c  x.  ( exp `  ( K  x.  t ) ) ) ) ) )
202201cbvrexv 2946 . 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 965    = wceq 1369    e. wcel 1756    =/= wne 2604   E.wrex 2714   _Vcvv 2970    \ cdif 3323    C_ wss 3326   {csn 3875   {cpr 3877    e. cmpt 4348    X. cxp 4836   dom cdm 4838    Fn wfn 5411   -->wf 5412   ` cfv 5416  (class class class)co 6089    oFcof 6316   CCcc 9278   RRcr 9279   0cc0 9280   1c1 9281    + caddc 9283    x. cmul 9285    - cmin 9593   -ucneg 9594    / cdiv 9991   expce 13345    _D cdv 21336
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422  ax-rep 4401  ax-sep 4411  ax-nul 4419  ax-pow 4468  ax-pr 4529  ax-un 6370  ax-inf2 7845  ax-cnex 9336  ax-resscn 9337  ax-1cn 9338  ax-icn 9339  ax-addcl 9340  ax-addrcl 9341  ax-mulcl 9342  ax-mulrcl 9343  ax-mulcom 9344  ax-addass 9345  ax-mulass 9346  ax-distr 9347  ax-i2m1 9348  ax-1ne0 9349  ax-1rid 9350  ax-rnegex 9351  ax-rrecex 9352  ax-cnre 9353  ax-pre-lttri 9354  ax-pre-lttrn 9355  ax-pre-ltadd 9356  ax-pre-mulgt0 9357  ax-pre-sup 9358  ax-addf 9359  ax-mulf 9360
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3185  df-csb 3287  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-pss 3342  df-nul 3636  df-if 3790  df-pw 3860  df-sn 3876  df-pr 3878  df-tp 3880  df-op 3882  df-uni 4090  df-int 4127  df-iun 4171  df-iin 4172  df-br 4291  df-opab 4349  df-mpt 4350  df-tr 4384  df-eprel 4630  df-id 4634  df-po 4639  df-so 4640  df-fr 4677  df-se 4678  df-we 4679  df-ord 4720  df-on 4721  df-lim 4722  df-suc 4723  df-xp 4844  df-rel 4845  df-cnv 4846  df-co 4847  df-dm 4848  df-rn 4849  df-res 4850  df-ima 4851  df-iota 5379  df-fun 5418  df-fn 5419  df-f 5420  df-f1 5421  df-fo 5422  df-f1o 5423  df-fv 5424  df-isom 5425  df-riota 6050  df-ov 6092  df-oprab 6093  df-mpt2 6094  df-of 6318  df-om 6475  df-1st 6575  df-2nd 6576  df-supp 6689  df-recs 6830  df-rdg 6864  df-1o 6918  df-2o 6919  df-oadd 6922  df-er 7099  df-map 7214  df-pm 7215  df-ixp 7262  df-en 7309  df-dom 7310  df-sdom 7311  df-fin 7312  df-fsupp 7619  df-fi 7659  df-sup 7689  df-oi 7722  df-card 8107  df-cda 8335  df-pnf 9418  df-mnf 9419  df-xr 9420  df-ltxr 9421  df-le 9422  df-sub 9595  df-neg 9596  df-div 9992  df-nn 10321  df-2 10378  df-3 10379  df-4 10380  df-5 10381  df-6 10382  df-7 10383  df-8 10384  df-9 10385  df-10 10386  df-n0 10578  df-z 10645  df-dec 10754  df-uz 10860  df-q 10952  df-rp 10990  df-xneg 11087  df-xadd 11088  df-xmul 11089  df-ioo 11302  df-ico 11304  df-icc 11305  df-fz 11436  df-fzo 11547  df-fl 11640  df-seq 11805  df-exp 11864  df-fac 12050  df-bc 12077  df-hash 12102  df-shft 12554  df-cj 12586  df-re 12587  df-im 12588  df-sqr 12722  df-abs 12723  df-limsup 12947  df-clim 12964  df-rlim 12965  df-sum 13162  df-ef 13351  df-struct 14174  df-ndx 14175  df-slot 14176  df-base 14177  df-sets 14178  df-ress 14179  df-plusg 14249  df-mulr 14250  df-starv 14251  df-sca 14252  df-vsca 14253  df-ip 14254  df-tset 14255  df-ple 14256  df-ds 14258  df-unif 14259  df-hom 14260  df-cco 14261  df-rest 14359  df-topn 14360  df-0g 14378  df-gsum 14379  df-topgen 14380  df-pt 14381  df-prds 14384  df-xrs 14438  df-qtop 14443  df-imas 14444  df-xps 14446  df-mre 14522  df-mrc 14523  df-acs 14525  df-mnd 15413  df-submnd 15463  df-mulg 15546  df-cntz 15833  df-cmn 16277  df-psmet 17807  df-xmet 17808  df-met 17809  df-bl 17810  df-mopn 17811  df-fbas 17812  df-fg 17813  df-cnfld 17817  df-top 18501  df-bases 18503  df-topon 18504  df-topsp 18505  df-cld 18621  df-ntr 18622  df-cls 18623  df-nei 18700  df-lp 18738  df-perf 18739  df-cn 18829  df-cnp 18830  df-haus 18917  df-cmp 18988  df-tx 19133  df-hmeo 19326  df-fil 19417  df-fm 19509  df-flim 19510  df-flf 19511  df-xms 19893  df-ms 19894  df-tms 19895  df-cncf 20452  df-limc 21339  df-dv 21340
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator