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	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	expgrowthi.k	⊢ ( 𝜑 → 𝐾 ∈ ℂ )
	expgrowthi.y0	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	expgrowthi.yt	⊢ 𝑌 = ( 𝑡 ∈ 𝑆 ↦ ( 𝐶 · ( exp ‘ ( 𝐾 · 𝑡 ) ) ) )
Assertion	expgrowthi	⊢ ( 𝜑 → ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		expgrowthi.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		expgrowthi.k	⊢ ( 𝜑 → 𝐾 ∈ ℂ )
3		expgrowthi.y0	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4		expgrowthi.yt	⊢ 𝑌 = ( 𝑡 ∈ 𝑆 ↦ ( 𝐶 · ( exp ‘ ( 𝐾 · 𝑡 ) ) ) )
5		oveq2	⊢ ( 𝑡 = 𝑦 → ( 𝐾 · 𝑡 ) = ( 𝐾 · 𝑦 ) )
6	5	fveq2d	⊢ ( 𝑡 = 𝑦 → ( exp ‘ ( 𝐾 · 𝑡 ) ) = ( exp ‘ ( 𝐾 · 𝑦 ) ) )
7	6	oveq2d	⊢ ( 𝑡 = 𝑦 → ( 𝐶 · ( exp ‘ ( 𝐾 · 𝑡 ) ) ) = ( 𝐶 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) )
8	7	cbvmptv	⊢ ( 𝑡 ∈ 𝑆 ↦ ( 𝐶 · ( exp ‘ ( 𝐾 · 𝑡 ) ) ) ) = ( 𝑦 ∈ 𝑆 ↦ ( 𝐶 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) )
9	4 8	eqtri	⊢ 𝑌 = ( 𝑦 ∈ 𝑆 ↦ ( 𝐶 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) )
10	9	oveq2i	⊢ ( 𝑆 D 𝑌 ) = ( 𝑆 D ( 𝑦 ∈ 𝑆 ↦ ( 𝐶 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ) )
11		elpri	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) )
12		eleq2	⊢ ( 𝑆 = ℝ → ( 𝑦 ∈ 𝑆 ↔ 𝑦 ∈ ℝ ) )
13		recn	⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
14	12 13	syl6bi	⊢ ( 𝑆 = ℝ → ( 𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ ) )
15		eleq2	⊢ ( 𝑆 = ℂ → ( 𝑦 ∈ 𝑆 ↔ 𝑦 ∈ ℂ ) )
16	15	biimpd	⊢ ( 𝑆 = ℂ → ( 𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ ) )
17	14 16	jaoi	⊢ ( ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) → ( 𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ ) )
18	1 11 17	3syl	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ ) )
19	18	imp	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ ℂ )
20		mulcl	⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝐾 · 𝑦 ) ∈ ℂ )
21	2 20	sylan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝐾 · 𝑦 ) ∈ ℂ )
22		efcl	⊢ ( ( 𝐾 · 𝑦 ) ∈ ℂ → ( exp ‘ ( 𝐾 · 𝑦 ) ) ∈ ℂ )
23	21 22	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( exp ‘ ( 𝐾 · 𝑦 ) ) ∈ ℂ )
24	19 23	syldan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( exp ‘ ( 𝐾 · 𝑦 ) ) ∈ ℂ )
25		ovexd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝐾 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ∈ V )
26		cnelprrecn	⊢ ℂ ∈ { ℝ , ℂ }
27	26	a1i	⊢ ( 𝜑 → ℂ ∈ { ℝ , ℂ } )
28	19 21	syldan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝐾 · 𝑦 ) ∈ ℂ )
29	2	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝐾 ∈ ℂ )
30		efcl	⊢ ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) ∈ ℂ )
31	30	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( exp ‘ 𝑥 ) ∈ ℂ )
32		1cnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 1 ∈ ℂ )
33	1	dvmptid	⊢ ( 𝜑 → ( 𝑆 D ( 𝑦 ∈ 𝑆 ↦ 𝑦 ) ) = ( 𝑦 ∈ 𝑆 ↦ 1 ) )
34	1 19 32 33 2	dvmptcmul	⊢ ( 𝜑 → ( 𝑆 D ( 𝑦 ∈ 𝑆 ↦ ( 𝐾 · 𝑦 ) ) ) = ( 𝑦 ∈ 𝑆 ↦ ( 𝐾 · 1 ) ) )
35	2	mulid1d	⊢ ( 𝜑 → ( 𝐾 · 1 ) = 𝐾 )
36	35	mpteq2dv	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑆 ↦ ( 𝐾 · 1 ) ) = ( 𝑦 ∈ 𝑆 ↦ 𝐾 ) )
37	34 36	eqtrd	⊢ ( 𝜑 → ( 𝑆 D ( 𝑦 ∈ 𝑆 ↦ ( 𝐾 · 𝑦 ) ) ) = ( 𝑦 ∈ 𝑆 ↦ 𝐾 ) )
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 = ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) ) )
43	41 42	mpbi	⊢ exp = ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) )
44	43	oveq2i	⊢ ( ℂ D exp ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) ) )
45	38 44 43	3eqtr3i	⊢ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) )
46	45	a1i	⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) ) )
47		fveq2	⊢ ( 𝑥 = ( 𝐾 · 𝑦 ) → ( exp ‘ 𝑥 ) = ( exp ‘ ( 𝐾 · 𝑦 ) ) )
48	1 27 28 29 31 31 37 46 47 47	dvmptco	⊢ ( 𝜑 → ( 𝑆 D ( 𝑦 ∈ 𝑆 ↦ ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ) = ( 𝑦 ∈ 𝑆 ↦ ( ( exp ‘ ( 𝐾 · 𝑦 ) ) · 𝐾 ) ) )
49		mulcom	⊢ ( ( ( exp ‘ ( 𝐾 · 𝑦 ) ) ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( ( exp ‘ ( 𝐾 · 𝑦 ) ) · 𝐾 ) = ( 𝐾 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) )
50	24 2 49	syl2anr	⊢ ( ( 𝜑 ∧ ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( exp ‘ ( 𝐾 · 𝑦 ) ) · 𝐾 ) = ( 𝐾 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) )
51	50	anabss5	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( exp ‘ ( 𝐾 · 𝑦 ) ) · 𝐾 ) = ( 𝐾 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) )
52	51	mpteq2dva	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑆 ↦ ( ( exp ‘ ( 𝐾 · 𝑦 ) ) · 𝐾 ) ) = ( 𝑦 ∈ 𝑆 ↦ ( 𝐾 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ) )
53	48 52	eqtrd	⊢ ( 𝜑 → ( 𝑆 D ( 𝑦 ∈ 𝑆 ↦ ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ) = ( 𝑦 ∈ 𝑆 ↦ ( 𝐾 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ) )
54	1 24 25 53 3	dvmptcmul	⊢ ( 𝜑 → ( 𝑆 D ( 𝑦 ∈ 𝑆 ↦ ( 𝐶 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ) ) = ( 𝑦 ∈ 𝑆 ↦ ( 𝐶 · ( 𝐾 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ) ) )
55	3 2 24	3anim123i	⊢ ( ( 𝜑 ∧ 𝜑 ∧ ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝐶 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ ( exp ‘ ( 𝐾 · 𝑦 ) ) ∈ ℂ ) )
56	55	3anidm12	⊢ ( ( 𝜑 ∧ ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝐶 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ ( exp ‘ ( 𝐾 · 𝑦 ) ) ∈ ℂ ) )
57	56	anabss5	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝐶 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ ( exp ‘ ( 𝐾 · 𝑦 ) ) ∈ ℂ ) )
58		mul12	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ ( exp ‘ ( 𝐾 · 𝑦 ) ) ∈ ℂ ) → ( 𝐶 · ( 𝐾 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ) = ( 𝐾 · ( 𝐶 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ) )
59	57 58	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝐶 · ( 𝐾 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ) = ( 𝐾 · ( 𝐶 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ) )
60	59	mpteq2dva	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑆 ↦ ( 𝐶 · ( 𝐾 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ) ) = ( 𝑦 ∈ 𝑆 ↦ ( 𝐾 · ( 𝐶 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ) ) )
61	54 60	eqtrd	⊢ ( 𝜑 → ( 𝑆 D ( 𝑦 ∈ 𝑆 ↦ ( 𝐶 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ) ) = ( 𝑦 ∈ 𝑆 ↦ ( 𝐾 · ( 𝐶 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ) ) )
62	10 61	syl5eq	⊢ ( 𝜑 → ( 𝑆 D 𝑌 ) = ( 𝑦 ∈ 𝑆 ↦ ( 𝐾 · ( 𝐶 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ) ) )
63		ovexd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝐶 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ∈ V )
64		fconstmpt	⊢ ( 𝑆 × { 𝐾 } ) = ( 𝑦 ∈ 𝑆 ↦ 𝐾 )
65	64	a1i	⊢ ( 𝜑 → ( 𝑆 × { 𝐾 } ) = ( 𝑦 ∈ 𝑆 ↦ 𝐾 ) )
66	9	a1i	⊢ ( 𝜑 → 𝑌 = ( 𝑦 ∈ 𝑆 ↦ ( 𝐶 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ) )
67	1 29 63 65 66	offval2	⊢ ( 𝜑 → ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) = ( 𝑦 ∈ 𝑆 ↦ ( 𝐾 · ( 𝐶 · ( exp ‘ ( 𝐾 · 𝑦 ) ) ) ) ) )
68	62 67	eqtr4d	⊢ ( 𝜑 → ( 𝑆 D 𝑌 ) = ( ( 𝑆 × { 𝐾 } ) ∘f · 𝑌 ) )