Step | Hyp | Ref
| Expression |
1 | | expgrowthi.yt |
. . . . 5
⊢ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑡)))) |
2 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑡 = 𝑦 → (𝐾 · 𝑡) = (𝐾 · 𝑦)) |
3 | 2 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑡 = 𝑦 → (exp‘(𝐾 · 𝑡)) = (exp‘(𝐾 · 𝑦))) |
4 | 3 | oveq2d 6565 |
. . . . . 6
⊢ (𝑡 = 𝑦 → (𝐶 · (exp‘(𝐾 · 𝑡))) = (𝐶 · (exp‘(𝐾 · 𝑦)))) |
5 | 4 | cbvmptv 4678 |
. . . . 5
⊢ (𝑡 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑡)))) = (𝑦 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑦)))) |
6 | 1, 5 | eqtri 2632 |
. . . 4
⊢ 𝑌 = (𝑦 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑦)))) |
7 | 6 | oveq2i 6560 |
. . 3
⊢ (𝑆 D 𝑌) = (𝑆 D (𝑦 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑦))))) |
8 | | expgrowthi.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
9 | | elpri 4145 |
. . . . . . . 8
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝑆 = ℝ ∨
𝑆 =
ℂ)) |
10 | | eleq2 2677 |
. . . . . . . . . 10
⊢ (𝑆 = ℝ → (𝑦 ∈ 𝑆 ↔ 𝑦 ∈ ℝ)) |
11 | | recn 9905 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
12 | 10, 11 | syl6bi 242 |
. . . . . . . . 9
⊢ (𝑆 = ℝ → (𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ)) |
13 | | eleq2 2677 |
. . . . . . . . . 10
⊢ (𝑆 = ℂ → (𝑦 ∈ 𝑆 ↔ 𝑦 ∈ ℂ)) |
14 | 13 | biimpd 218 |
. . . . . . . . 9
⊢ (𝑆 = ℂ → (𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ)) |
15 | 12, 14 | jaoi 393 |
. . . . . . . 8
⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → (𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ)) |
16 | 8, 9, 15 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ)) |
17 | 16 | imp 444 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ ℂ) |
18 | | expgrowthi.k |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ℂ) |
19 | | mulcl 9899 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐾 · 𝑦) ∈ ℂ) |
20 | 18, 19 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝐾 · 𝑦) ∈ ℂ) |
21 | | efcl 14652 |
. . . . . . 7
⊢ ((𝐾 · 𝑦) ∈ ℂ → (exp‘(𝐾 · 𝑦)) ∈ ℂ) |
22 | 20, 21 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (exp‘(𝐾 · 𝑦)) ∈ ℂ) |
23 | 17, 22 | syldan 486 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘(𝐾 · 𝑦)) ∈ ℂ) |
24 | | ovex 6577 |
. . . . . 6
⊢ (𝐾 · (exp‘(𝐾 · 𝑦))) ∈ V |
25 | 24 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐾 · (exp‘(𝐾 · 𝑦))) ∈ V) |
26 | | cnelprrecn 9908 |
. . . . . . . 8
⊢ ℂ
∈ {ℝ, ℂ} |
27 | 26 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℂ ∈ {ℝ,
ℂ}) |
28 | 17, 20 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐾 · 𝑦) ∈ ℂ) |
29 | 18 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝐾 ∈ ℂ) |
30 | | efcl 14652 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ∈
ℂ) |
31 | 30 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (exp‘𝑥) ∈
ℂ) |
32 | | 1cnd 9935 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 1 ∈ ℂ) |
33 | 8 | dvmptid 23526 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ 𝑦)) = (𝑦 ∈ 𝑆 ↦ 1)) |
34 | 8, 17, 32, 33, 18 | dvmptcmul 23533 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (𝐾 · 𝑦))) = (𝑦 ∈ 𝑆 ↦ (𝐾 · 1))) |
35 | 18 | mulid1d 9936 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 · 1) = 𝐾) |
36 | 35 | mpteq2dv 4673 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝑆 ↦ (𝐾 · 1)) = (𝑦 ∈ 𝑆 ↦ 𝐾)) |
37 | 34, 36 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (𝐾 · 𝑦))) = (𝑦 ∈ 𝑆 ↦ 𝐾)) |
38 | | dvef 23547 |
. . . . . . . . 9
⊢ (ℂ
D exp) = exp |
39 | | eff 14651 |
. . . . . . . . . . . 12
⊢
exp:ℂ⟶ℂ |
40 | | ffn 5958 |
. . . . . . . . . . . 12
⊢
(exp:ℂ⟶ℂ → exp Fn ℂ) |
41 | 39, 40 | ax-mp 5 |
. . . . . . . . . . 11
⊢ exp Fn
ℂ |
42 | | dffn5 6151 |
. . . . . . . . . . 11
⊢ (exp Fn
ℂ ↔ exp = (𝑥
∈ ℂ ↦ (exp‘𝑥))) |
43 | 41, 42 | mpbi 219 |
. . . . . . . . . 10
⊢ exp =
(𝑥 ∈ ℂ ↦
(exp‘𝑥)) |
44 | 43 | oveq2i 6560 |
. . . . . . . . 9
⊢ (ℂ
D exp) = (ℂ D (𝑥
∈ ℂ ↦ (exp‘𝑥))) |
45 | 38, 44, 43 | 3eqtr3i 2640 |
. . . . . . . 8
⊢ (ℂ
D (𝑥 ∈ ℂ ↦
(exp‘𝑥))) = (𝑥 ∈ ℂ ↦
(exp‘𝑥)) |
46 | 45 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦
(exp‘𝑥))) = (𝑥 ∈ ℂ ↦
(exp‘𝑥))) |
47 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = (𝐾 · 𝑦) → (exp‘𝑥) = (exp‘(𝐾 · 𝑦))) |
48 | 8, 27, 28, 29, 31, 31, 37, 46, 47, 47 | dvmptco 23541 |
. . . . . 6
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (exp‘(𝐾 · 𝑦)))) = (𝑦 ∈ 𝑆 ↦ ((exp‘(𝐾 · 𝑦)) · 𝐾))) |
49 | | mulcom 9901 |
. . . . . . . . 9
⊢
(((exp‘(𝐾
· 𝑦)) ∈ ℂ
∧ 𝐾 ∈ ℂ)
→ ((exp‘(𝐾
· 𝑦)) · 𝐾) = (𝐾 · (exp‘(𝐾 · 𝑦)))) |
50 | 23, 18, 49 | syl2anr 494 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝜑 ∧ 𝑦 ∈ 𝑆)) → ((exp‘(𝐾 · 𝑦)) · 𝐾) = (𝐾 · (exp‘(𝐾 · 𝑦)))) |
51 | 50 | anabss5 853 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((exp‘(𝐾 · 𝑦)) · 𝐾) = (𝐾 · (exp‘(𝐾 · 𝑦)))) |
52 | 51 | mpteq2dva 4672 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝑆 ↦ ((exp‘(𝐾 · 𝑦)) · 𝐾)) = (𝑦 ∈ 𝑆 ↦ (𝐾 · (exp‘(𝐾 · 𝑦))))) |
53 | 48, 52 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (exp‘(𝐾 · 𝑦)))) = (𝑦 ∈ 𝑆 ↦ (𝐾 · (exp‘(𝐾 · 𝑦))))) |
54 | | expgrowthi.y0 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℂ) |
55 | 8, 23, 25, 53, 54 | dvmptcmul 23533 |
. . . 4
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑦))))) = (𝑦 ∈ 𝑆 ↦ (𝐶 · (𝐾 · (exp‘(𝐾 · 𝑦)))))) |
56 | 54, 18, 23 | 3anim123i 1240 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜑 ∧ (𝜑 ∧ 𝑦 ∈ 𝑆)) → (𝐶 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ (exp‘(𝐾 · 𝑦)) ∈ ℂ)) |
57 | 56 | 3anidm12 1375 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝜑 ∧ 𝑦 ∈ 𝑆)) → (𝐶 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ (exp‘(𝐾 · 𝑦)) ∈ ℂ)) |
58 | 57 | anabss5 853 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐶 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ (exp‘(𝐾 · 𝑦)) ∈ ℂ)) |
59 | | mul12 10081 |
. . . . . 6
⊢ ((𝐶 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧
(exp‘(𝐾 ·
𝑦)) ∈ ℂ) →
(𝐶 · (𝐾 · (exp‘(𝐾 · 𝑦)))) = (𝐾 · (𝐶 · (exp‘(𝐾 · 𝑦))))) |
60 | 58, 59 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐶 · (𝐾 · (exp‘(𝐾 · 𝑦)))) = (𝐾 · (𝐶 · (exp‘(𝐾 · 𝑦))))) |
61 | 60 | mpteq2dva 4672 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝑆 ↦ (𝐶 · (𝐾 · (exp‘(𝐾 · 𝑦))))) = (𝑦 ∈ 𝑆 ↦ (𝐾 · (𝐶 · (exp‘(𝐾 · 𝑦)))))) |
62 | 55, 61 | eqtrd 2644 |
. . 3
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑦))))) = (𝑦 ∈ 𝑆 ↦ (𝐾 · (𝐶 · (exp‘(𝐾 · 𝑦)))))) |
63 | 7, 62 | syl5eq 2656 |
. 2
⊢ (𝜑 → (𝑆 D 𝑌) = (𝑦 ∈ 𝑆 ↦ (𝐾 · (𝐶 · (exp‘(𝐾 · 𝑦)))))) |
64 | | ovex 6577 |
. . . 4
⊢ (𝐶 · (exp‘(𝐾 · 𝑦))) ∈ V |
65 | 64 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐶 · (exp‘(𝐾 · 𝑦))) ∈ V) |
66 | | fconstmpt 5085 |
. . . 4
⊢ (𝑆 × {𝐾}) = (𝑦 ∈ 𝑆 ↦ 𝐾) |
67 | 66 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑆 × {𝐾}) = (𝑦 ∈ 𝑆 ↦ 𝐾)) |
68 | 6 | a1i 11 |
. . 3
⊢ (𝜑 → 𝑌 = (𝑦 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑦))))) |
69 | 8, 29, 65, 67, 68 | offval2 6812 |
. 2
⊢ (𝜑 → ((𝑆 × {𝐾}) ∘𝑓 ·
𝑌) = (𝑦 ∈ 𝑆 ↦ (𝐾 · (𝐶 · (exp‘(𝐾 · 𝑦)))))) |
70 | 63, 69 | eqtr4d 2647 |
1
⊢ (𝜑 → (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘𝑓 ·
𝑌)) |