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	mulridd	|- ( 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	imbitrid	|- ( 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	eqtrid	|- ( 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 ) ) ) ) ) )