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 
|- ( ph -> S e. { RR , CC } )
expgrowthi.k 
|- ( ph -> K e. CC )
expgrowthi.y0 
|- ( ph -> C e. CC )
expgrowthi.yt 
|- Y = ( t e. S |-> ( C x. ( exp ` ( K x. t ) ) ) )
Assertion expgrowthi 
|- ( ph -> ( S _D Y ) = ( ( S X. { K } ) oF x. Y ) )

Proof

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