Metamath Proof Explorer


Theorem expgrowth

Description: Exponential growth and decay model. The derivative of a functiony of variablet equals a constantk timesy itself, iffy equals some constantC times the exponential ofkt. This theorem and expgrowthi 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 callsy' =ky "the most important differential equation in applied mathematics". In the field of population ecology it is known as theMalthusian growth model or exponential law, andC,k, andt 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 incontinuous compounding withC as the initial amount of money. Inexponential decay models, k is often expressed as the negative of a positive constant λ.

Herey' is given as ( SD Y ) , C_ as c , andky as ( ( S X. { K } ) oF x. Y ) . ( S X. { K } ) is the constant function that maps any real or complex input tok 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 theinitial value ofy, andk is theproportionality constant.Exponential growth occurs whenk > 0, andexponential decay occurs whenk < 0."); its proof here closely follows the proof ofy' =y in https://proofwiki.org/wiki/Exponential_Growth_Equation/Special_Case .

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

Ref Expression
Hypotheses 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 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 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 expgrowth.s
 |-  ( ph -> S e. { RR , CC } )
2 expgrowth.k
 |-  ( ph -> K e. CC )
3 expgrowth.y
 |-  ( ph -> Y : S --> CC )
4 expgrowth.dy
 |-  ( ph -> dom ( S _D Y ) = S )
5 cnelprrecn
 |-  CC e. { RR , CC }
6 5 a1i
 |-  ( ph -> CC e. { RR , CC } )
7 recnprss
 |-  ( S e. { RR , CC } -> S C_ CC )
8 1 7 syl
 |-  ( ph -> S C_ CC )
9 8 sseld
 |-  ( ph -> ( u e. S -> u e. CC ) )
10 mulcl
 |-  ( ( K e. CC /\ u e. CC ) -> ( K x. u ) e. CC )
11 2 9 10 syl6an
 |-  ( ph -> ( u e. S -> ( K x. u ) e. CC ) )
12 11 imp
 |-  ( ( ph /\ u e. S ) -> ( K x. u ) e. CC )
13 12 negcld
 |-  ( ( ph /\ u e. S ) -> -u ( K x. u ) e. CC )
14 2 negcld
 |-  ( ph -> -u K e. CC )
15 14 adantr
 |-  ( ( ph /\ u e. S ) -> -u K e. CC )
16 efcl
 |-  ( y e. CC -> ( exp ` y ) e. CC )
17 16 adantl
 |-  ( ( ph /\ y e. CC ) -> ( exp ` y ) e. CC )
18 2 adantr
 |-  ( ( ph /\ u e. S ) -> K e. CC )
19 9 imp
 |-  ( ( ph /\ u e. S ) -> u e. CC )
20 ax-1cn
 |-  1 e. CC
21 20 a1i
 |-  ( ( ph /\ u e. S ) -> 1 e. CC )
22 1 dvmptid
 |-  ( ph -> ( S _D ( u e. S |-> u ) ) = ( u e. S |-> 1 ) )
23 1 19 21 22 2 dvmptcmul
 |-  ( ph -> ( S _D ( u e. S |-> ( K x. u ) ) ) = ( u e. S |-> ( K x. 1 ) ) )
24 2 mulid1d
 |-  ( ph -> ( K x. 1 ) = K )
25 24 mpteq2dv
 |-  ( ph -> ( u e. S |-> ( K x. 1 ) ) = ( u e. S |-> K ) )
26 23 25 eqtrd
 |-  ( ph -> ( S _D ( u e. S |-> ( K x. u ) ) ) = ( u e. S |-> K ) )
27 1 12 18 26 dvmptneg
 |-  ( ph -> ( S _D ( u e. S |-> -u ( K x. u ) ) ) = ( u e. S |-> -u K ) )
28 dvef
 |-  ( CC _D exp ) = exp
29 eff
 |-  exp : CC --> CC
30 ffn
 |-  ( exp : CC --> CC -> exp Fn CC )
31 29 30 ax-mp
 |-  exp Fn CC
32 dffn5
 |-  ( exp Fn CC <-> exp = ( y e. CC |-> ( exp ` y ) ) )
33 31 32 mpbi
 |-  exp = ( y e. CC |-> ( exp ` y ) )
34 33 oveq2i
 |-  ( CC _D exp ) = ( CC _D ( y e. CC |-> ( exp ` y ) ) )
35 28 34 33 3eqtr3i
 |-  ( CC _D ( y e. CC |-> ( exp ` y ) ) ) = ( y e. CC |-> ( exp ` y ) )
36 35 a1i
 |-  ( ph -> ( CC _D ( y e. CC |-> ( exp ` y ) ) ) = ( y e. CC |-> ( exp ` y ) ) )
37 fveq2
 |-  ( y = -u ( K x. u ) -> ( exp ` y ) = ( exp ` -u ( K x. u ) ) )
38 1 6 13 15 17 17 27 36 37 37 dvmptco
 |-  ( ph -> ( S _D ( u e. S |-> ( exp ` -u ( K x. u ) ) ) ) = ( u e. S |-> ( ( exp ` -u ( K x. u ) ) x. -u K ) ) )
39 38 oveq2d
 |-  ( 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 ) ) ) )
40 efcl
 |-  ( -u ( K x. u ) e. CC -> ( exp ` -u ( K x. u ) ) e. CC )
41 13 40 syl
 |-  ( ( ph /\ u e. S ) -> ( exp ` -u ( K x. u ) ) e. CC )
42 41 15 mulcld
 |-  ( ( ph /\ u e. S ) -> ( ( exp ` -u ( K x. u ) ) x. -u K ) e. CC )
43 42 fmpttd
 |-  ( ph -> ( u e. S |-> ( ( exp ` -u ( K x. u ) ) x. -u K ) ) : S --> CC )
44 38 feq1d
 |-  ( 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 ) )
45 43 44 mpbird
 |-  ( ph -> ( S _D ( u e. S |-> ( exp ` -u ( K x. u ) ) ) ) : S --> CC )
46 mulcom
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) = ( y x. x ) )
47 46 adantl
 |-  ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x x. y ) = ( y x. x ) )
48 1 3 45 47 caofcom
 |-  ( 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 ) )
49 39 48 eqtr3d
 |-  ( 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 ) )
50 49 oveq2d
 |-  ( 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
 |-  ( -u K e. CC -> ( S X. { -u K } ) : S --> CC )
52 14 51 syl
 |-  ( ph -> ( S X. { -u K } ) : S --> CC )
53 41 fmpttd
 |-  ( ph -> ( u e. S |-> ( exp ` -u ( K x. u ) ) ) : S --> CC )
54 1 52 53 47 caofcom
 |-  ( 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 } ) ) )
55 eqidd
 |-  ( ph -> ( u e. S |-> ( exp ` -u ( K x. u ) ) ) = ( u e. S |-> ( exp ` -u ( K x. u ) ) ) )
56 fconstmpt
 |-  ( S X. { -u K } ) = ( u e. S |-> -u K )
57 56 a1i
 |-  ( ph -> ( S X. { -u K } ) = ( u e. S |-> -u K ) )
58 1 41 15 55 57 offval2
 |-  ( 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 ) ) )
59 54 58 eqtrd
 |-  ( 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 ) ) )
60 59 oveq2d
 |-  ( 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 ) ) ) )
61 60 oveq2d
 |-  ( 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 ) ) ) ) )
62 38 dmeqd
 |-  ( ph -> dom ( S _D ( u e. S |-> ( exp ` -u ( K x. u ) ) ) ) = dom ( u e. S |-> ( ( exp ` -u ( K x. u ) ) x. -u K ) ) )
63 eqid
 |-  ( u e. S |-> ( ( exp ` -u ( K x. u ) ) x. -u K ) ) = ( u e. S |-> ( ( exp ` -u ( K x. u ) ) x. -u K ) )
64 63 42 dmmptd
 |-  ( ph -> dom ( u e. S |-> ( ( exp ` -u ( K x. u ) ) x. -u K ) ) = S )
65 62 64 eqtrd
 |-  ( ph -> dom ( S _D ( u e. S |-> ( exp ` -u ( K x. u ) ) ) ) = S )
66 1 3 53 4 65 dvmulf
 |-  ( 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 ) ) )
67 50 61 66 3eqtr4rd
 |-  ( 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 ) ) ) ) ) ) )
68 ofmul12
 |-  ( ( ( 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 ) ) ) ) ) )
69 1 3 52 53 68 syl22anc
 |-  ( 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 ) ) ) ) ) )
70 69 oveq2d
 |-  ( 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 ) ) ) ) ) ) )
71 67 70 eqtrd
 |-  ( 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 ) ) ) ) ) ) )
72 oveq1
 |-  ( ( 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 ) ) ) ) )
73 72 oveq1d
 |-  ( ( 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 ) ) ) ) ) ) )
74 71 73 sylan9eq
 |-  ( ( 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 ) ) ) ) ) ) )
75 mulass
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x x. y ) x. z ) = ( x x. ( y x. z ) ) )
76 75 adantl
 |-  ( ( ph /\ ( x e. CC /\ y e. CC /\ z e. CC ) ) -> ( ( x x. y ) x. z ) = ( x x. ( y x. z ) ) )
77 1 52 3 53 76 caofass
 |-  ( 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 ) ) ) ) ) )
78 77 oveq2d
 |-  ( 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 ) ) ) ) ) ) )
79 78 eqeq2d
 |-  ( 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 ) ) ) ) ) ) ) )
80 79 adantr
 |-  ( ( 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 ) ) ) ) ) ) ) )
81 74 80 mpbird
 |-  ( ( 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 ) ) ) ) ) )
82 mulcl
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
83 82 adantl
 |-  ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x x. y ) e. CC )
84 fconst6g
 |-  ( K e. CC -> ( S X. { K } ) : S --> CC )
85 2 84 syl
 |-  ( ph -> ( S X. { K } ) : S --> CC )
86 inidm
 |-  ( S i^i S ) = S
87 83 85 3 1 1 86 off
 |-  ( ph -> ( ( S X. { K } ) oF x. Y ) : S --> CC )
88 83 52 3 1 1 86 off
 |-  ( ph -> ( ( S X. { -u K } ) oF x. Y ) : S --> CC )
89 adddir
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x + y ) x. z ) = ( ( x x. z ) + ( y x. z ) ) )
90 89 adantl
 |-  ( ( ph /\ ( x e. CC /\ y e. CC /\ z e. CC ) ) -> ( ( x + y ) x. z ) = ( ( x x. z ) + ( y x. z ) ) )
91 1 53 87 88 90 caofdir
 |-  ( 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 ) ) ) ) ) )
92 91 eqeq2d
 |-  ( 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 ) ) ) ) ) ) )
93 92 adantr
 |-  ( ( 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 ) ) ) ) ) ) )
94 81 93 mpbird
 |-  ( ( 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 ) ) ) ) )
95 ofnegsub
 |-  ( ( 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 ) ) )
96 1 87 87 95 syl3anc
 |-  ( 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 ) ) )
97 neg1cn
 |-  -u 1 e. CC
98 97 fconst6
 |-  ( S X. { -u 1 } ) : S --> CC
99 98 a1i
 |-  ( ph -> ( S X. { -u 1 } ) : S --> CC )
100 1 99 85 3 76 caofass
 |-  ( 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 ) ) )
101 97 a1i
 |-  ( ph -> -u 1 e. CC )
102 1 101 2 ofc12
 |-  ( ph -> ( ( S X. { -u 1 } ) oF x. ( S X. { K } ) ) = ( S X. { ( -u 1 x. K ) } ) )
103 2 mulm1d
 |-  ( ph -> ( -u 1 x. K ) = -u K )
104 103 sneqd
 |-  ( ph -> { ( -u 1 x. K ) } = { -u K } )
105 104 xpeq2d
 |-  ( ph -> ( S X. { ( -u 1 x. K ) } ) = ( S X. { -u K } ) )
106 102 105 eqtrd
 |-  ( ph -> ( ( S X. { -u 1 } ) oF x. ( S X. { K } ) ) = ( S X. { -u K } ) )
107 106 oveq1d
 |-  ( ph -> ( ( ( S X. { -u 1 } ) oF x. ( S X. { K } ) ) oF x. Y ) = ( ( S X. { -u K } ) oF x. Y ) )
108 100 107 eqtr3d
 |-  ( ph -> ( ( S X. { -u 1 } ) oF x. ( ( S X. { K } ) oF x. Y ) ) = ( ( S X. { -u K } ) oF x. Y ) )
109 108 oveq2d
 |-  ( 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 ) ) )
110 ofsubid
 |-  ( ( 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 } ) )
111 1 87 110 syl2anc
 |-  ( ph -> ( ( ( S X. { K } ) oF x. Y ) oF - ( ( S X. { K } ) oF x. Y ) ) = ( S X. { 0 } ) )
112 96 109 111 3eqtr3d
 |-  ( ph -> ( ( ( S X. { K } ) oF x. Y ) oF + ( ( S X. { -u K } ) oF x. Y ) ) = ( S X. { 0 } ) )
113 112 oveq1d
 |-  ( 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 ) ) ) ) )
114 113 eqeq2d
 |-  ( 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 ) ) ) ) ) )
115 114 adantr
 |-  ( ( 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 ) ) ) ) ) )
116 94 115 mpbid
 |-  ( ( 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 ) ) ) ) )
117 0cnd
 |-  ( ph -> 0 e. CC )
118 mul02
 |-  ( x e. CC -> ( 0 x. x ) = 0 )
119 118 adantl
 |-  ( ( ph /\ x e. CC ) -> ( 0 x. x ) = 0 )
120 1 53 117 117 119 caofid2
 |-  ( ph -> ( ( S X. { 0 } ) oF x. ( u e. S |-> ( exp ` -u ( K x. u ) ) ) ) = ( S X. { 0 } ) )
121 120 adantr
 |-  ( ( 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 } ) )
122 116 121 eqtrd
 |-  ( ( 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 } ) )
123 1 adantr
 |-  ( ( ph /\ ( S _D Y ) = ( ( S X. { K } ) oF x. Y ) ) -> S e. { RR , CC } )
124 83 3 53 1 1 86 off
 |-  ( ph -> ( Y oF x. ( u e. S |-> ( exp ` -u ( K x. u ) ) ) ) : S --> CC )
125 124 adantr
 |-  ( ( ph /\ ( S _D Y ) = ( ( S X. { K } ) oF x. Y ) ) -> ( Y oF x. ( u e. S |-> ( exp ` -u ( K x. u ) ) ) ) : S --> CC )
126 122 dmeqd
 |-  ( ( 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 } ) )
127 0cn
 |-  0 e. CC
128 127 fconst6
 |-  ( S X. { 0 } ) : S --> CC
129 128 fdmi
 |-  dom ( S X. { 0 } ) = S
130 126 129 eqtrdi
 |-  ( ( 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 )
131 123 125 130 dvconstbi
 |-  ( ( 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 } ) ) )
132 122 131 mpbid
 |-  ( ( 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 } ) )
133 oveq1
 |-  ( ( 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 ) ) ) ) )
134 efne0
 |-  ( -u ( K x. u ) e. CC -> ( exp ` -u ( K x. u ) ) =/= 0 )
135 eldifsn
 |-  ( ( exp ` -u ( K x. u ) ) e. ( CC \ { 0 } ) <-> ( ( exp ` -u ( K x. u ) ) e. CC /\ ( exp ` -u ( K x. u ) ) =/= 0 ) )
136 40 134 135 sylanbrc
 |-  ( -u ( K x. u ) e. CC -> ( exp ` -u ( K x. u ) ) e. ( CC \ { 0 } ) )
137 13 136 syl
 |-  ( ( ph /\ u e. S ) -> ( exp ` -u ( K x. u ) ) e. ( CC \ { 0 } ) )
138 137 fmpttd
 |-  ( ph -> ( u e. S |-> ( exp ` -u ( K x. u ) ) ) : S --> ( CC \ { 0 } ) )
139 ofdivcan4
 |-  ( ( 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 )
140 1 3 138 139 syl3anc
 |-  ( ph -> ( ( Y oF x. ( u e. S |-> ( exp ` -u ( K x. u ) ) ) ) oF / ( u e. S |-> ( exp ` -u ( K x. u ) ) ) ) = Y )
141 140 eqeq1d
 |-  ( 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 ) ) ) ) ) )
142 133 141 syl5ib
 |-  ( 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 ) ) ) ) ) )
143 142 adantr
 |-  ( ( 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 ) ) ) ) ) )
144 vex
 |-  x e. _V
145 144 a1i
 |-  ( ( ph /\ u e. S ) -> x e. _V )
146 ovexd
 |-  ( ( ph /\ u e. S ) -> ( 1 / ( exp ` ( K x. u ) ) ) e. _V )
147 fconstmpt
 |-  ( S X. { x } ) = ( u e. S |-> x )
148 147 a1i
 |-  ( ph -> ( S X. { x } ) = ( u e. S |-> x ) )
149 efneg
 |-  ( ( K x. u ) e. CC -> ( exp ` -u ( K x. u ) ) = ( 1 / ( exp ` ( K x. u ) ) ) )
150 12 149 syl
 |-  ( ( ph /\ u e. S ) -> ( exp ` -u ( K x. u ) ) = ( 1 / ( exp ` ( K x. u ) ) ) )
151 150 mpteq2dva
 |-  ( ph -> ( u e. S |-> ( exp ` -u ( K x. u ) ) ) = ( u e. S |-> ( 1 / ( exp ` ( K x. u ) ) ) ) )
152 1 145 146 148 151 offval2
 |-  ( ph -> ( ( S X. { x } ) oF / ( u e. S |-> ( exp ` -u ( K x. u ) ) ) ) = ( u e. S |-> ( x / ( 1 / ( exp ` ( K x. u ) ) ) ) ) )
153 152 adantr
 |-  ( ( 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 ) ) ) ) ) )
154 efcl
 |-  ( ( K x. u ) e. CC -> ( exp ` ( K x. u ) ) e. CC )
155 efne0
 |-  ( ( K x. u ) e. CC -> ( exp ` ( K x. u ) ) =/= 0 )
156 154 155 jca
 |-  ( ( K x. u ) e. CC -> ( ( exp ` ( K x. u ) ) e. CC /\ ( exp ` ( K x. u ) ) =/= 0 ) )
157 12 156 syl
 |-  ( ( ph /\ u e. S ) -> ( ( exp ` ( K x. u ) ) e. CC /\ ( exp ` ( K x. u ) ) =/= 0 ) )
158 ax-1ne0
 |-  1 =/= 0
159 20 158 pm3.2i
 |-  ( 1 e. CC /\ 1 =/= 0 )
160 divdiv2
 |-  ( ( 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 ) )
161 159 160 mp3an2
 |-  ( ( 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 ) )
162 157 161 sylan2
 |-  ( ( x e. CC /\ ( ph /\ u e. S ) ) -> ( x / ( 1 / ( exp ` ( K x. u ) ) ) ) = ( ( x x. ( exp ` ( K x. u ) ) ) / 1 ) )
163 12 154 syl
 |-  ( ( ph /\ u e. S ) -> ( exp ` ( K x. u ) ) e. CC )
164 mulcl
 |-  ( ( x e. CC /\ ( exp ` ( K x. u ) ) e. CC ) -> ( x x. ( exp ` ( K x. u ) ) ) e. CC )
165 163 164 sylan2
 |-  ( ( x e. CC /\ ( ph /\ u e. S ) ) -> ( x x. ( exp ` ( K x. u ) ) ) e. CC )
166 165 div1d
 |-  ( ( x e. CC /\ ( ph /\ u e. S ) ) -> ( ( x x. ( exp ` ( K x. u ) ) ) / 1 ) = ( x x. ( exp ` ( K x. u ) ) ) )
167 162 166 eqtrd
 |-  ( ( x e. CC /\ ( ph /\ u e. S ) ) -> ( x / ( 1 / ( exp ` ( K x. u ) ) ) ) = ( x x. ( exp ` ( K x. u ) ) ) )
168 167 ancoms
 |-  ( ( ( ph /\ u e. S ) /\ x e. CC ) -> ( x / ( 1 / ( exp ` ( K x. u ) ) ) ) = ( x x. ( exp ` ( K x. u ) ) ) )
169 168 an32s
 |-  ( ( ( ph /\ x e. CC ) /\ u e. S ) -> ( x / ( 1 / ( exp ` ( K x. u ) ) ) ) = ( x x. ( exp ` ( K x. u ) ) ) )
170 169 mpteq2dva
 |-  ( ( ph /\ x e. CC ) -> ( u e. S |-> ( x / ( 1 / ( exp ` ( K x. u ) ) ) ) ) = ( u e. S |-> ( x x. ( exp ` ( K x. u ) ) ) ) )
171 153 170 eqtrd
 |-  ( ( 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 ) ) ) ) )
172 171 eqeq2d
 |-  ( ( 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 ) ) ) ) ) )
173 143 172 sylibd
 |-  ( ( 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 ) ) ) ) ) )
174 173 reximdva
 |-  ( 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 ) ) ) ) ) )
175 174 adantr
 |-  ( ( 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 ) ) ) ) ) )
176 132 175 mpd
 |-  ( ( ph /\ ( S _D Y ) = ( ( S X. { K } ) oF x. Y ) ) -> E. x e. CC Y = ( u e. S |-> ( x x. ( exp ` ( K x. u ) ) ) ) )
177 176 ex
 |-  ( ph -> ( ( S _D Y ) = ( ( S X. { K } ) oF x. Y ) -> E. x e. CC Y = ( u e. S |-> ( x x. ( exp ` ( K x. u ) ) ) ) ) )
178 1 adantr
 |-  ( ( ph /\ ( x e. CC /\ Y = ( u e. S |-> ( x x. ( exp ` ( K x. u ) ) ) ) ) ) -> S e. { RR , CC } )
179 2 adantr
 |-  ( ( ph /\ ( x e. CC /\ Y = ( u e. S |-> ( x x. ( exp ` ( K x. u ) ) ) ) ) ) -> K e. CC )
180 simprl
 |-  ( ( ph /\ ( x e. CC /\ Y = ( u e. S |-> ( x x. ( exp ` ( K x. u ) ) ) ) ) ) -> x e. CC )
181 eqid
 |-  ( u e. S |-> ( x x. ( exp ` ( K x. u ) ) ) ) = ( u e. S |-> ( x x. ( exp ` ( K x. u ) ) ) )
182 178 179 180 181 expgrowthi
 |-  ( ( 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 ) ) ) ) ) )
183 182 3impb
 |-  ( ( 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 ) ) ) ) ) )
184 oveq2
 |-  ( Y = ( u e. S |-> ( x x. ( exp ` ( K x. u ) ) ) ) -> ( S _D Y ) = ( S _D ( u e. S |-> ( x x. ( exp ` ( K x. u ) ) ) ) ) )
185 oveq2
 |-  ( 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 ) ) ) ) ) )
186 184 185 eqeq12d
 |-  ( 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 ) ) ) ) ) ) )
187 186 3ad2ant3
 |-  ( ( 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 ) ) ) ) ) ) )
188 183 187 mpbird
 |-  ( ( ph /\ x e. CC /\ Y = ( u e. S |-> ( x x. ( exp ` ( K x. u ) ) ) ) ) -> ( S _D Y ) = ( ( S X. { K } ) oF x. Y ) )
189 188 rexlimdv3a
 |-  ( ph -> ( E. x e. CC Y = ( u e. S |-> ( x x. ( exp ` ( K x. u ) ) ) ) -> ( S _D Y ) = ( ( S X. { K } ) oF x. Y ) ) )
190 177 189 impbid
 |-  ( ph -> ( ( S _D Y ) = ( ( S X. { K } ) oF x. Y ) <-> E. x e. CC Y = ( u e. S |-> ( x x. ( exp ` ( K x. u ) ) ) ) ) )
191 oveq2
 |-  ( u = t -> ( K x. u ) = ( K x. t ) )
192 191 fveq2d
 |-  ( u = t -> ( exp ` ( K x. u ) ) = ( exp ` ( K x. t ) ) )
193 192 oveq2d
 |-  ( u = t -> ( x x. ( exp ` ( K x. u ) ) ) = ( x x. ( exp ` ( K x. t ) ) ) )
194 193 cbvmptv
 |-  ( u e. S |-> ( x x. ( exp ` ( K x. u ) ) ) ) = ( t e. S |-> ( x x. ( exp ` ( K x. t ) ) ) )
195 oveq1
 |-  ( x = c -> ( x x. ( exp ` ( K x. t ) ) ) = ( c x. ( exp ` ( K x. t ) ) ) )
196 195 mpteq2dv
 |-  ( x = c -> ( t e. S |-> ( x x. ( exp ` ( K x. t ) ) ) ) = ( t e. S |-> ( c x. ( exp ` ( K x. t ) ) ) ) )
197 194 196 syl5eq
 |-  ( x = c -> ( u e. S |-> ( x x. ( exp ` ( K x. u ) ) ) ) = ( t e. S |-> ( c x. ( exp ` ( K x. t ) ) ) ) )
198 197 eqeq2d
 |-  ( x = c -> ( Y = ( u e. S |-> ( x x. ( exp ` ( K x. u ) ) ) ) <-> Y = ( t e. S |-> ( c x. ( exp ` ( K x. t ) ) ) ) ) )
199 198 cbvrexvw
 |-  ( 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 ) ) ) ) )
200 190 199 bitrdi
 |-  ( ph -> ( ( S _D Y ) = ( ( S X. { K } ) oF x. Y ) <-> E. c e. CC Y = ( t e. S |-> ( c x. ( exp ` ( K x. t ) ) ) ) ) )