expgrowthi

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

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

Proof

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

Metamath Proof Explorer

Theorem expgrowthi

Proof