| Step | Hyp | Ref
| Expression |
| 1 | | expgrowthi.yt |
. . . . 5
⊢ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑡)))) |
| 2 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑡 = 𝑦 → (𝐾 · 𝑡) = (𝐾 · 𝑦)) |
| 3 | 2 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑡 = 𝑦 → (exp‘(𝐾 · 𝑡)) = (exp‘(𝐾 · 𝑦))) |
| 4 | 3 | oveq2d 7447 |
. . . . . 6
⊢ (𝑡 = 𝑦 → (𝐶 · (exp‘(𝐾 · 𝑡))) = (𝐶 · (exp‘(𝐾 · 𝑦)))) |
| 5 | 4 | cbvmptv 5255 |
. . . . 5
⊢ (𝑡 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑡)))) = (𝑦 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑦)))) |
| 6 | 1, 5 | eqtri 2765 |
. . . 4
⊢ 𝑌 = (𝑦 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑦)))) |
| 7 | 6 | oveq2i 7442 |
. . 3
⊢ (𝑆 D 𝑌) = (𝑆 D (𝑦 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑦))))) |
| 8 | | expgrowthi.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
| 9 | | elpri 4649 |
. . . . . . . 8
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝑆 = ℝ ∨
𝑆 =
ℂ)) |
| 10 | | eleq2 2830 |
. . . . . . . . . 10
⊢ (𝑆 = ℝ → (𝑦 ∈ 𝑆 ↔ 𝑦 ∈ ℝ)) |
| 11 | | recn 11245 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
| 12 | 10, 11 | biimtrdi 253 |
. . . . . . . . 9
⊢ (𝑆 = ℝ → (𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ)) |
| 13 | | eleq2 2830 |
. . . . . . . . . 10
⊢ (𝑆 = ℂ → (𝑦 ∈ 𝑆 ↔ 𝑦 ∈ ℂ)) |
| 14 | 13 | biimpd 229 |
. . . . . . . . 9
⊢ (𝑆 = ℂ → (𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ)) |
| 15 | 12, 14 | jaoi 858 |
. . . . . . . 8
⊢ ((𝑆 = ℝ ∨ 𝑆 = ℂ) → (𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ)) |
| 16 | 8, 9, 15 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ)) |
| 17 | 16 | imp 406 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ ℂ) |
| 18 | | expgrowthi.k |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ℂ) |
| 19 | | mulcl 11239 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐾 · 𝑦) ∈ ℂ) |
| 20 | 18, 19 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝐾 · 𝑦) ∈ ℂ) |
| 21 | | efcl 16118 |
. . . . . . 7
⊢ ((𝐾 · 𝑦) ∈ ℂ → (exp‘(𝐾 · 𝑦)) ∈ ℂ) |
| 22 | 20, 21 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (exp‘(𝐾 · 𝑦)) ∈ ℂ) |
| 23 | 17, 22 | syldan 591 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (exp‘(𝐾 · 𝑦)) ∈ ℂ) |
| 24 | | ovexd 7466 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐾 · (exp‘(𝐾 · 𝑦))) ∈ V) |
| 25 | | cnelprrecn 11248 |
. . . . . . . 8
⊢ ℂ
∈ {ℝ, ℂ} |
| 26 | 25 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℂ ∈ {ℝ,
ℂ}) |
| 27 | 17, 20 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐾 · 𝑦) ∈ ℂ) |
| 28 | 18 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝐾 ∈ ℂ) |
| 29 | | efcl 16118 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ∈
ℂ) |
| 30 | 29 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (exp‘𝑥) ∈
ℂ) |
| 31 | | 1cnd 11256 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 1 ∈ ℂ) |
| 32 | 8 | dvmptid 25995 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ 𝑦)) = (𝑦 ∈ 𝑆 ↦ 1)) |
| 33 | 8, 17, 31, 32, 18 | dvmptcmul 26002 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (𝐾 · 𝑦))) = (𝑦 ∈ 𝑆 ↦ (𝐾 · 1))) |
| 34 | 18 | mulridd 11278 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 · 1) = 𝐾) |
| 35 | 34 | mpteq2dv 5244 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝑆 ↦ (𝐾 · 1)) = (𝑦 ∈ 𝑆 ↦ 𝐾)) |
| 36 | 33, 35 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (𝐾 · 𝑦))) = (𝑦 ∈ 𝑆 ↦ 𝐾)) |
| 37 | | dvef 26018 |
. . . . . . . . 9
⊢ (ℂ
D exp) = exp |
| 38 | | eff 16117 |
. . . . . . . . . . . 12
⊢
exp:ℂ⟶ℂ |
| 39 | | ffn 6736 |
. . . . . . . . . . . 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 2773 |
. . . . . . . 8
⊢ (ℂ
D (𝑥 ∈ ℂ ↦
(exp‘𝑥))) = (𝑥 ∈ ℂ ↦
(exp‘𝑥)) |
| 45 | 44 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦
(exp‘𝑥))) = (𝑥 ∈ ℂ ↦
(exp‘𝑥))) |
| 46 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑥 = (𝐾 · 𝑦) → (exp‘𝑥) = (exp‘(𝐾 · 𝑦))) |
| 47 | 8, 26, 27, 28, 30, 30, 36, 45, 46, 46 | dvmptco 26010 |
. . . . . 6
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (exp‘(𝐾 · 𝑦)))) = (𝑦 ∈ 𝑆 ↦ ((exp‘(𝐾 · 𝑦)) · 𝐾))) |
| 48 | | mulcom 11241 |
. . . . . . . . 9
⊢
(((exp‘(𝐾
· 𝑦)) ∈ ℂ
∧ 𝐾 ∈ ℂ)
→ ((exp‘(𝐾
· 𝑦)) · 𝐾) = (𝐾 · (exp‘(𝐾 · 𝑦)))) |
| 49 | 23, 18, 48 | syl2anr 597 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝜑 ∧ 𝑦 ∈ 𝑆)) → ((exp‘(𝐾 · 𝑦)) · 𝐾) = (𝐾 · (exp‘(𝐾 · 𝑦)))) |
| 50 | 49 | anabss5 668 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((exp‘(𝐾 · 𝑦)) · 𝐾) = (𝐾 · (exp‘(𝐾 · 𝑦)))) |
| 51 | 50 | mpteq2dva 5242 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝑆 ↦ ((exp‘(𝐾 · 𝑦)) · 𝐾)) = (𝑦 ∈ 𝑆 ↦ (𝐾 · (exp‘(𝐾 · 𝑦))))) |
| 52 | 47, 51 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (exp‘(𝐾 · 𝑦)))) = (𝑦 ∈ 𝑆 ↦ (𝐾 · (exp‘(𝐾 · 𝑦))))) |
| 53 | | expgrowthi.y0 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℂ) |
| 54 | 8, 23, 24, 52, 53 | dvmptcmul 26002 |
. . . 4
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑦))))) = (𝑦 ∈ 𝑆 ↦ (𝐶 · (𝐾 · (exp‘(𝐾 · 𝑦)))))) |
| 55 | 53, 18, 23 | 3anim123i 1152 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜑 ∧ (𝜑 ∧ 𝑦 ∈ 𝑆)) → (𝐶 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ (exp‘(𝐾 · 𝑦)) ∈ ℂ)) |
| 56 | 55 | 3anidm12 1421 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝜑 ∧ 𝑦 ∈ 𝑆)) → (𝐶 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ (exp‘(𝐾 · 𝑦)) ∈ ℂ)) |
| 57 | 56 | anabss5 668 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐶 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ (exp‘(𝐾 · 𝑦)) ∈ ℂ)) |
| 58 | | mul12 11426 |
. . . . . 6
⊢ ((𝐶 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧
(exp‘(𝐾 ·
𝑦)) ∈ ℂ) →
(𝐶 · (𝐾 · (exp‘(𝐾 · 𝑦)))) = (𝐾 · (𝐶 · (exp‘(𝐾 · 𝑦))))) |
| 59 | 57, 58 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐶 · (𝐾 · (exp‘(𝐾 · 𝑦)))) = (𝐾 · (𝐶 · (exp‘(𝐾 · 𝑦))))) |
| 60 | 59 | mpteq2dva 5242 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝑆 ↦ (𝐶 · (𝐾 · (exp‘(𝐾 · 𝑦))))) = (𝑦 ∈ 𝑆 ↦ (𝐾 · (𝐶 · (exp‘(𝐾 · 𝑦)))))) |
| 61 | 54, 60 | eqtrd 2777 |
. . 3
⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑦))))) = (𝑦 ∈ 𝑆 ↦ (𝐾 · (𝐶 · (exp‘(𝐾 · 𝑦)))))) |
| 62 | 7, 61 | eqtrid 2789 |
. 2
⊢ (𝜑 → (𝑆 D 𝑌) = (𝑦 ∈ 𝑆 ↦ (𝐾 · (𝐶 · (exp‘(𝐾 · 𝑦)))))) |
| 63 | | ovexd 7466 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐶 · (exp‘(𝐾 · 𝑦))) ∈ V) |
| 64 | | fconstmpt 5747 |
. . . 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 2780 |
1
⊢ (𝜑 → (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) |