Metamath Proof Explorer


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 φ S
expgrowthi.k φ K
expgrowthi.y0 φ C
expgrowthi.yt Y = t S C e K t
Assertion expgrowthi φ S D Y = S × K × f Y

Proof

Step Hyp Ref Expression
1 expgrowthi.s φ S
2 expgrowthi.k φ K
3 expgrowthi.y0 φ C
4 expgrowthi.yt Y = t S C e K t
5 oveq2 t = y K t = K y
6 5 fveq2d t = y e K t = e K y
7 6 oveq2d t = y C e K t = C e K y
8 7 cbvmptv t S C e K t = y S C e K y
9 4 8 eqtri Y = y S C e K y
10 9 oveq2i S D Y = dy S C e K y dS y
11 elpri S S = S =
12 eleq2 S = y S y
13 recn y y
14 12 13 syl6bi S = y S y
15 eleq2 S = y S y
16 15 biimpd S = y S y
17 14 16 jaoi S = S = y S y
18 1 11 17 3syl φ y S y
19 18 imp φ y S y
20 mulcl K y K y
21 2 20 sylan φ y K y
22 efcl K y e K y
23 21 22 syl φ y e K y
24 19 23 syldan φ y S e K y
25 ovexd φ y S K e K y V
26 cnelprrecn
27 26 a1i φ
28 19 21 syldan φ y S K y
29 2 adantr φ y S K
30 efcl x e x
31 30 adantl φ x e x
32 1cnd φ y S 1
33 1 dvmptid φ dy S y dS y = y S 1
34 1 19 32 33 2 dvmptcmul φ dy S K y dS y = y S K 1
35 2 mulid1d φ K 1 = K
36 35 mpteq2dv φ y S K 1 = y S K
37 34 36 eqtrd φ dy S K y dS y = y S K
38 dvef D exp = exp
39 eff exp :
40 ffn exp : exp Fn
41 39 40 ax-mp exp Fn
42 dffn5 exp Fn exp = x e x
43 41 42 mpbi exp = x e x
44 43 oveq2i D exp = dx e x d x
45 38 44 43 3eqtr3i dx e x d x = x e x
46 45 a1i φ dx e x d x = x e x
47 fveq2 x = K y e x = e K y
48 1 27 28 29 31 31 37 46 47 47 dvmptco φ dy S e K y dS y = y S e K y K
49 mulcom e K y K e K y K = K e K y
50 24 2 49 syl2anr φ φ y S e K y K = K e K y
51 50 anabss5 φ y S e K y K = K e K y
52 51 mpteq2dva φ y S e K y K = y S K e K y
53 48 52 eqtrd φ dy S e K y dS y = y S K e K y
54 1 24 25 53 3 dvmptcmul φ dy S C e K y dS y = y S C K e K y
55 3 2 24 3anim123i φ φ φ y S C K e K y
56 55 3anidm12 φ φ y S C K e K y
57 56 anabss5 φ y S C K e K y
58 mul12 C K e K y C K e K y = K C e K y
59 57 58 syl φ y S C K e K y = K C e K y
60 59 mpteq2dva φ y S C K e K y = y S K C e K y
61 54 60 eqtrd φ dy S C e K y dS y = y S K C e K y
62 10 61 syl5eq φ S D Y = y S K C e K y
63 ovexd φ y S C e K y V
64 fconstmpt S × K = y S K
65 64 a1i φ S × K = y S K
66 9 a1i φ Y = y S C e K y
67 1 29 63 65 66 offval2 φ S × K × f Y = y S K C e K y
68 62 67 eqtr4d φ S D Y = S × K × f Y