Theorem expgrowthi

Description: Exponential growth and decay model. See expgrowth for more information. (Contributed by Steve Rodriguez, 4-Nov-2015)

	Ref	Expression
Hypotheses	expgrowthi.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	expgrowthi.k	$$⊢\phi \to K\in ℂ$$
	expgrowthi.y0	$$⊢\phi \to C\in ℂ$$
	expgrowthi.yt	$$⊢Y=\left(t\in S⟼C{\mathrm{e}}^{Kt}\right)$$
Assertion	expgrowthi	$$⊢\phi \to S\mathrm{D}Y=\left(S\times \left\{K\right\}\right){\times }_{f}Y$$

Proof

Step	Hyp	Ref	Expression
1		expgrowthi.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		expgrowthi.k	$$⊢\phi \to K\in ℂ$$
3		expgrowthi.y0	$$⊢\phi \to C\in ℂ$$
4		expgrowthi.yt	$$⊢Y=\left(t\in S⟼C{\mathrm{e}}^{Kt}\right)$$
5		oveq2	$$⊢t=y\to Kt=Ky$$
6	5	fveq2d	$$⊢t=y\to {\mathrm{e}}^{Kt}={\mathrm{e}}^{Ky}$$
7	6	oveq2d	$$⊢t=y\to C{\mathrm{e}}^{Kt}=C{\mathrm{e}}^{Ky}$$
8	7	cbvmptv	$$⊢\left(t\in S⟼C{\mathrm{e}}^{Kt}\right)=\left(y\in S⟼C{\mathrm{e}}^{Ky}\right)$$
9	4 8	eqtri	$$⊢Y=\left(y\in S⟼C{\mathrm{e}}^{Ky}\right)$$
10	9	oveq2i	$$⊢S\mathrm{D}Y=\frac{d\left(y\in S⟼C{\mathrm{e}}^{Ky}\right)}{d_{S}y}$$
11		elpri	$$⊢S\in \left\{ℝ,ℂ\right\}\to \left(S=ℝ\vee S=ℂ\right)$$
12		eleq2	$$⊢S=ℝ\to \left(y\in S\leftrightarrow y\in ℝ\right)$$
13		recn	$$⊢y\in ℝ\to y\in ℂ$$
14	12 13	biimtrdi	$$⊢S=ℝ\to \left(y\in S\to y\in ℂ\right)$$
15		eleq2	$$⊢S=ℂ\to \left(y\in S\leftrightarrow y\in ℂ\right)$$
16	15	biimpd	$$⊢S=ℂ\to \left(y\in S\to y\in ℂ\right)$$
17	14 16	jaoi	$$⊢\left(S=ℝ\vee S=ℂ\right)\to \left(y\in S\to y\in ℂ\right)$$
18	1 11 17	3syl	$$⊢\phi \to \left(y\in S\to y\in ℂ\right)$$
19	18	imp	$$⊢\left(\phi \wedge y\in S\right)\to y\in ℂ$$
20		mulcl	$$⊢\left(K\in ℂ\wedge y\in ℂ\right)\to Ky\in ℂ$$
21	2 20	sylan	$$⊢\left(\phi \wedge y\in ℂ\right)\to Ky\in ℂ$$
22		efcl	$$⊢Ky\in ℂ\to {\mathrm{e}}^{Ky}\in ℂ$$
23	21 22	syl	$$⊢\left(\phi \wedge y\in ℂ\right)\to {\mathrm{e}}^{Ky}\in ℂ$$
24	19 23	syldan	$$⊢\left(\phi \wedge y\in S\right)\to {\mathrm{e}}^{Ky}\in ℂ$$
25		ovexd	$$⊢\left(\phi \wedge y\in S\right)\to K{\mathrm{e}}^{Ky}\in \mathrm{V}$$
26		cnelprrecn	$$⊢ℂ\in \left\{ℝ,ℂ\right\}$$
27	26	a1i	$$⊢\phi \to ℂ\in \left\{ℝ,ℂ\right\}$$
28	19 21	syldan	$$⊢\left(\phi \wedge y\in S\right)\to Ky\in ℂ$$
29	2	adantr	$$⊢\left(\phi \wedge y\in S\right)\to K\in ℂ$$
30		efcl	$$⊢x\in ℂ\to {\mathrm{e}}^x\in ℂ$$
31	30	adantl	$$⊢\left(\phi \wedge x\in ℂ\right)\to {\mathrm{e}}^x\in ℂ$$
32		1cnd	$$⊢\left(\phi \wedge y\in S\right)\to 1\in ℂ$$
33	1	dvmptid	$$⊢\phi \to \frac{d\left(y\in S⟼y\right)}{d_{S}y}=\left(y\in S⟼1\right)$$
34	1 19 32 33 2	dvmptcmul	$$⊢\phi \to \frac{d\left(y\in S⟼Ky\right)}{d_{S}y}=\left(y\in S⟼K\cdot 1\right)$$
35	2	mulridd	$$⊢\phi \to K\cdot 1=K$$
36	35	mpteq2dv	$$⊢\phi \to \left(y\in S⟼K\cdot 1\right)=\left(y\in S⟼K\right)$$
37	34 36	eqtrd	$$⊢\phi \to \frac{d\left(y\in S⟼Ky\right)}{d_{S}y}=\left(y\in S⟼K\right)$$
38		dvef	$$⊢ℂ\mathrm{D}\exp =\exp$$
39		eff	$$⊢\exp :ℂ⟶ℂ$$
40		ffn	$$⊢\exp :ℂ⟶ℂ\to \exp Fnℂ$$
41	39 40	ax-mp	$$⊢\exp Fnℂ$$
42		dffn5	$$⊢\exp Fnℂ\leftrightarrow \exp =\left(x\in ℂ⟼{\mathrm{e}}^x\right)$$
43	41 42	mpbi	$$⊢\exp =\left(x\in ℂ⟼{\mathrm{e}}^x\right)$$
44	43	oveq2i	$$⊢ℂ\mathrm{D}\exp =\frac{d\left(x\in ℂ⟼{\mathrm{e}}^x\right)}{d_{ℂ}x}$$
45	38 44 43	3eqtr3i	$$⊢\frac{d\left(x\in ℂ⟼{\mathrm{e}}^x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼{\mathrm{e}}^x\right)$$
46	45	a1i	$$⊢\phi \to \frac{d\left(x\in ℂ⟼{\mathrm{e}}^x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼{\mathrm{e}}^x\right)$$
47		fveq2	$$⊢x=Ky\to {\mathrm{e}}^x={\mathrm{e}}^{Ky}$$
48	1 27 28 29 31 31 37 46 47 47	dvmptco	$$⊢\phi \to \frac{d\left(y\in S⟼{\mathrm{e}}^{Ky}\right)}{d_{S}y}=\left(y\in S⟼{\mathrm{e}}^{Ky}K\right)$$
49		mulcom	$$⊢\left({\mathrm{e}}^{Ky}\in ℂ\wedge K\in ℂ\right)\to {\mathrm{e}}^{Ky}K=K{\mathrm{e}}^{Ky}$$
50	24 2 49	syl2anr	$$⊢\left(\phi \wedge \left(\phi \wedge y\in S\right)\right)\to {\mathrm{e}}^{Ky}K=K{\mathrm{e}}^{Ky}$$
51	50	anabss5	$$⊢\left(\phi \wedge y\in S\right)\to {\mathrm{e}}^{Ky}K=K{\mathrm{e}}^{Ky}$$
52	51	mpteq2dva	$$⊢\phi \to \left(y\in S⟼{\mathrm{e}}^{Ky}K\right)=\left(y\in S⟼K{\mathrm{e}}^{Ky}\right)$$
53	48 52	eqtrd	$$⊢\phi \to \frac{d\left(y\in S⟼{\mathrm{e}}^{Ky}\right)}{d_{S}y}=\left(y\in S⟼K{\mathrm{e}}^{Ky}\right)$$
54	1 24 25 53 3	dvmptcmul	$$⊢\phi \to \frac{d\left(y\in S⟼C{\mathrm{e}}^{Ky}\right)}{d_{S}y}=\left(y\in S⟼CK{\mathrm{e}}^{Ky}\right)$$
55	3 2 24	3anim123i	$$⊢\left(\phi \wedge \phi \wedge \left(\phi \wedge y\in S\right)\right)\to \left(C\in ℂ\wedge K\in ℂ\wedge {\mathrm{e}}^{Ky}\in ℂ\right)$$
56	55	3anidm12	$$⊢\left(\phi \wedge \left(\phi \wedge y\in S\right)\right)\to \left(C\in ℂ\wedge K\in ℂ\wedge {\mathrm{e}}^{Ky}\in ℂ\right)$$
57	56	anabss5	$$⊢\left(\phi \wedge y\in S\right)\to \left(C\in ℂ\wedge K\in ℂ\wedge {\mathrm{e}}^{Ky}\in ℂ\right)$$
58		mul12	$$⊢\left(C\in ℂ\wedge K\in ℂ\wedge {\mathrm{e}}^{Ky}\in ℂ\right)\to CK{\mathrm{e}}^{Ky}=KC{\mathrm{e}}^{Ky}$$
59	57 58	syl	$$⊢\left(\phi \wedge y\in S\right)\to CK{\mathrm{e}}^{Ky}=KC{\mathrm{e}}^{Ky}$$
60	59	mpteq2dva	$$⊢\phi \to \left(y\in S⟼CK{\mathrm{e}}^{Ky}\right)=\left(y\in S⟼KC{\mathrm{e}}^{Ky}\right)$$
61	54 60	eqtrd	$$⊢\phi \to \frac{d\left(y\in S⟼C{\mathrm{e}}^{Ky}\right)}{d_{S}y}=\left(y\in S⟼KC{\mathrm{e}}^{Ky}\right)$$
62	10 61	eqtrid	$$⊢\phi \to S\mathrm{D}Y=\left(y\in S⟼KC{\mathrm{e}}^{Ky}\right)$$
63		ovexd	$$⊢\left(\phi \wedge y\in S\right)\to C{\mathrm{e}}^{Ky}\in \mathrm{V}$$
64		fconstmpt	$$⊢S\times \left\{K\right\}=\left(y\in S⟼K\right)$$
65	64	a1i	$$⊢\phi \to S\times \left\{K\right\}=\left(y\in S⟼K\right)$$
66	9	a1i	$$⊢\phi \to Y=\left(y\in S⟼C{\mathrm{e}}^{Ky}\right)$$
67	1 29 63 65 66	offval2	$$⊢\phi \to \left(S\times \left\{K\right\}\right){\times }_{f}Y=\left(y\in S⟼KC{\mathrm{e}}^{Ky}\right)$$
68	62 67	eqtr4d	$$⊢\phi \to S\mathrm{D}Y=\left(S\times \left\{K\right\}\right){\times }_{f}Y$$