Step | Hyp | Ref
| Expression |
1 | | expgrowthi.yt |
. . . . 5
⊢ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑡)))) |
2 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑡 = 𝑦 → (𝐾 · 𝑡) = (𝐾 · 𝑦)) |
3 | 2 | fveq2d 6911 |
. . . . . . 7
⊢ (𝑡 = 𝑦 → (exp‘(𝐾 · 𝑡)) = (exp‘(𝐾 · 𝑦))) |
4 | 3 | oveq2d 7447 |
. . . . . 6
⊢ (𝑡 = 𝑦 → (𝐶 · (exp‘(𝐾 · 𝑡))) = (𝐶 · (exp‘(𝐾 · 𝑦)))) |
5 | 4 | cbvmptv 5261 |
. . . . 5
⊢ (𝑡 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑡)))) = (𝑦 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑦)))) |
6 | 1, 5 | eqtri 2763 |
. . . 4
⊢ 𝑌 = (𝑦 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑦)))) |
7 | 6 | oveq2i 7442 |
. . 3
⊢ (𝑆 D 𝑌) = (𝑆 D (𝑦 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑦))))) |
8 | | expgrowthi.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
9 | | elpri 4654 |
. . . . . . . 8
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝑆 = ℝ ∨
𝑆 =
ℂ)) |
10 | | eleq2 2828 |
. . . . . . . . . 10
⊢ (𝑆 = ℝ → (𝑦 ∈ 𝑆 ↔ 𝑦 ∈ ℝ)) |
11 | | recn 11243 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
12 | 10, 11 | biimtrdi 253 |
. . . . . . . . 9
⊢ (𝑆 = ℝ → (𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ)) |
13 | | eleq2 2828 |
. . . . . . . . . 10
⊢ (𝑆 = ℂ → (𝑦 ∈ 𝑆 ↔ 𝑦 ∈ ℂ)) |
14 | 13 | biimpd 229 |
. . . . . . . . 9
⊢ (𝑆 = ℂ → (𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ)) |
15 | 12, 14 | jaoi 857 |
. . . . . . . 8
⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → (𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ)) |
16 | 8, 9, 15 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ)) |
17 | 16 | imp 406 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ ℂ) |
18 | | expgrowthi.k |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ℂ) |
19 | | mulcl 11237 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐾 · 𝑦) ∈ ℂ) |
20 | 18, 19 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝐾 · 𝑦) ∈ ℂ) |
21 | | efcl 16115 |
. . . . . . 7
⊢ ((𝐾 · 𝑦) ∈ ℂ → (exp‘(𝐾 · 𝑦)) ∈ ℂ) |
22 | 20, 21 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (exp‘(𝐾 · 𝑦)) ∈ ℂ) |
23 | 17, 22 | syldan 591 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘(𝐾 · 𝑦)) ∈ ℂ) |
24 | | ovexd 7466 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐾 · (exp‘(𝐾 · 𝑦))) ∈ V) |
25 | | cnelprrecn 11246 |
. . . . . . . 8
⊢ ℂ
∈ {ℝ, ℂ} |
26 | 25 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℂ ∈ {ℝ,
ℂ}) |
27 | 17, 20 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐾 · 𝑦) ∈ ℂ) |
28 | 18 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝐾 ∈ ℂ) |
29 | | efcl 16115 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ∈
ℂ) |
30 | 29 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (exp‘𝑥) ∈
ℂ) |
31 | | 1cnd 11254 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 1 ∈ ℂ) |
32 | 8 | dvmptid 26010 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ 𝑦)) = (𝑦 ∈ 𝑆 ↦ 1)) |
33 | 8, 17, 31, 32, 18 | dvmptcmul 26017 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (𝐾 · 𝑦))) = (𝑦 ∈ 𝑆 ↦ (𝐾 · 1))) |
34 | 18 | mulridd 11276 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 · 1) = 𝐾) |
35 | 34 | mpteq2dv 5250 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝑆 ↦ (𝐾 · 1)) = (𝑦 ∈ 𝑆 ↦ 𝐾)) |
36 | 33, 35 | eqtrd 2775 |
. . . . . . 7
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (𝐾 · 𝑦))) = (𝑦 ∈ 𝑆 ↦ 𝐾)) |
37 | | dvef 26033 |
. . . . . . . . 9
⊢ (ℂ
D exp) = exp |
38 | | eff 16114 |
. . . . . . . . . . . 12
⊢
exp:ℂ⟶ℂ |
39 | | ffn 6737 |
. . . . . . . . . . . 12
⊢
(exp:ℂ⟶ℂ → exp Fn ℂ) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . 11
⊢ exp Fn
ℂ |
41 | | dffn5 6967 |
. . . . . . . . . . 11
⊢ (exp Fn
ℂ ↔ exp = (𝑥
∈ ℂ ↦ (exp‘𝑥))) |
42 | 40, 41 | mpbi 230 |
. . . . . . . . . 10
⊢ exp =
(𝑥 ∈ ℂ ↦
(exp‘𝑥)) |
43 | 42 | oveq2i 7442 |
. . . . . . . . 9
⊢ (ℂ
D exp) = (ℂ D (𝑥
∈ ℂ ↦ (exp‘𝑥))) |
44 | 37, 43, 42 | 3eqtr3i 2771 |
. . . . . . . 8
⊢ (ℂ
D (𝑥 ∈ ℂ ↦
(exp‘𝑥))) = (𝑥 ∈ ℂ ↦
(exp‘𝑥)) |
45 | 44 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦
(exp‘𝑥))) = (𝑥 ∈ ℂ ↦
(exp‘𝑥))) |
46 | | fveq2 6907 |
. . . . . . 7
⊢ (𝑥 = (𝐾 · 𝑦) → (exp‘𝑥) = (exp‘(𝐾 · 𝑦))) |
47 | 8, 26, 27, 28, 30, 30, 36, 45, 46, 46 | dvmptco 26025 |
. . . . . 6
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (exp‘(𝐾 · 𝑦)))) = (𝑦 ∈ 𝑆 ↦ ((exp‘(𝐾 · 𝑦)) · 𝐾))) |
48 | | mulcom 11239 |
. . . . . . . . 9
⊢
(((exp‘(𝐾
· 𝑦)) ∈ ℂ
∧ 𝐾 ∈ ℂ)
→ ((exp‘(𝐾
· 𝑦)) · 𝐾) = (𝐾 · (exp‘(𝐾 · 𝑦)))) |
49 | 23, 18, 48 | syl2anr 597 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝜑 ∧ 𝑦 ∈ 𝑆)) → ((exp‘(𝐾 · 𝑦)) · 𝐾) = (𝐾 · (exp‘(𝐾 · 𝑦)))) |
50 | 49 | anabss5 668 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((exp‘(𝐾 · 𝑦)) · 𝐾) = (𝐾 · (exp‘(𝐾 · 𝑦)))) |
51 | 50 | mpteq2dva 5248 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝑆 ↦ ((exp‘(𝐾 · 𝑦)) · 𝐾)) = (𝑦 ∈ 𝑆 ↦ (𝐾 · (exp‘(𝐾 · 𝑦))))) |
52 | 47, 51 | eqtrd 2775 |
. . . . 5
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (exp‘(𝐾 · 𝑦)))) = (𝑦 ∈ 𝑆 ↦ (𝐾 · (exp‘(𝐾 · 𝑦))))) |
53 | | expgrowthi.y0 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℂ) |
54 | 8, 23, 24, 52, 53 | dvmptcmul 26017 |
. . . 4
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑦))))) = (𝑦 ∈ 𝑆 ↦ (𝐶 · (𝐾 · (exp‘(𝐾 · 𝑦)))))) |
55 | 53, 18, 23 | 3anim123i 1150 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜑 ∧ (𝜑 ∧ 𝑦 ∈ 𝑆)) → (𝐶 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ (exp‘(𝐾 · 𝑦)) ∈ ℂ)) |
56 | 55 | 3anidm12 1418 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝜑 ∧ 𝑦 ∈ 𝑆)) → (𝐶 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ (exp‘(𝐾 · 𝑦)) ∈ ℂ)) |
57 | 56 | anabss5 668 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐶 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ (exp‘(𝐾 · 𝑦)) ∈ ℂ)) |
58 | | mul12 11424 |
. . . . . 6
⊢ ((𝐶 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧
(exp‘(𝐾 ·
𝑦)) ∈ ℂ) →
(𝐶 · (𝐾 · (exp‘(𝐾 · 𝑦)))) = (𝐾 · (𝐶 · (exp‘(𝐾 · 𝑦))))) |
59 | 57, 58 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐶 · (𝐾 · (exp‘(𝐾 · 𝑦)))) = (𝐾 · (𝐶 · (exp‘(𝐾 · 𝑦))))) |
60 | 59 | mpteq2dva 5248 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝑆 ↦ (𝐶 · (𝐾 · (exp‘(𝐾 · 𝑦))))) = (𝑦 ∈ 𝑆 ↦ (𝐾 · (𝐶 · (exp‘(𝐾 · 𝑦)))))) |
61 | 54, 60 | eqtrd 2775 |
. . 3
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑦))))) = (𝑦 ∈ 𝑆 ↦ (𝐾 · (𝐶 · (exp‘(𝐾 · 𝑦)))))) |
62 | 7, 61 | eqtrid 2787 |
. 2
⊢ (𝜑 → (𝑆 D 𝑌) = (𝑦 ∈ 𝑆 ↦ (𝐾 · (𝐶 · (exp‘(𝐾 · 𝑦)))))) |
63 | | ovexd 7466 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐶 · (exp‘(𝐾 · 𝑦))) ∈ V) |
64 | | fconstmpt 5751 |
. . . 4
⊢ (𝑆 × {𝐾}) = (𝑦 ∈ 𝑆 ↦ 𝐾) |
65 | 64 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑆 × {𝐾}) = (𝑦 ∈ 𝑆 ↦ 𝐾)) |
66 | 6 | a1i 11 |
. . 3
⊢ (𝜑 → 𝑌 = (𝑦 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑦))))) |
67 | 8, 28, 63, 65, 66 | offval2 7717 |
. 2
⊢ (𝜑 → ((𝑆 × {𝐾}) ∘f · 𝑌) = (𝑦 ∈ 𝑆 ↦ (𝐾 · (𝐶 · (exp‘(𝐾 · 𝑦)))))) |
68 | 62, 67 | eqtr4d 2778 |
1
⊢ (𝜑 → (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) |