| Step | Hyp | Ref
| Expression |
| 1 | | expgrowth.s |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
| 2 | | cnelprrecn 11248 |
. . . . . . . . . . . . . . . . . 18
⊢ ℂ
∈ {ℝ, ℂ} |
| 3 | 2 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ℂ ∈ {ℝ,
ℂ}) |
| 4 | | expgrowth.k |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐾 ∈ ℂ) |
| 5 | | recnprss 25939 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
| 6 | 1, 5 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
| 7 | 6 | sseld 3982 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑢 ∈ 𝑆 → 𝑢 ∈ ℂ)) |
| 8 | | mulcl 11239 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (𝐾 · 𝑢) ∈ ℂ) |
| 9 | 4, 7, 8 | syl6an 684 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑢 ∈ 𝑆 → (𝐾 · 𝑢) ∈ ℂ)) |
| 10 | 9 | imp 406 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (𝐾 · 𝑢) ∈ ℂ) |
| 11 | 10 | negcld 11607 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → -(𝐾 · 𝑢) ∈ ℂ) |
| 12 | 4 | negcld 11607 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → -𝐾 ∈ ℂ) |
| 13 | 12 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → -𝐾 ∈ ℂ) |
| 14 | | efcl 16118 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℂ →
(exp‘𝑦) ∈
ℂ) |
| 15 | 14 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (exp‘𝑦) ∈
ℂ) |
| 16 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝐾 ∈ ℂ) |
| 17 | 7 | imp 406 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ ℂ) |
| 18 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℂ |
| 19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 1 ∈ ℂ) |
| 20 | 1 | dvmptid 25995 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ 𝑢)) = (𝑢 ∈ 𝑆 ↦ 1)) |
| 21 | 1, 17, 19, 20, 4 | dvmptcmul 26002 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ (𝐾 · 1))) |
| 22 | 4 | mulridd 11278 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐾 · 1) = 𝐾) |
| 23 | 22 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (𝐾 · 1)) = (𝑢 ∈ 𝑆 ↦ 𝐾)) |
| 24 | 21, 23 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ 𝐾)) |
| 25 | 1, 10, 16, 24 | dvmptneg 26004 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ -(𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ -𝐾)) |
| 26 | | dvef 26018 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℂ
D exp) = exp |
| 27 | | eff 16117 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
exp:ℂ⟶ℂ |
| 28 | | ffn 6736 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(exp:ℂ⟶ℂ → exp Fn ℂ) |
| 29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ exp Fn
ℂ |
| 30 | | dffn5 6967 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (exp Fn
ℂ ↔ exp = (𝑦
∈ ℂ ↦ (exp‘𝑦))) |
| 31 | 29, 30 | mpbi 230 |
. . . . . . . . . . . . . . . . . . . 20
⊢ exp =
(𝑦 ∈ ℂ ↦
(exp‘𝑦)) |
| 32 | 31 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℂ
D exp) = (ℂ D (𝑦
∈ ℂ ↦ (exp‘𝑦))) |
| 33 | 26, 32, 31 | 3eqtr3i 2773 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℂ
D (𝑦 ∈ ℂ ↦
(exp‘𝑦))) = (𝑦 ∈ ℂ ↦
(exp‘𝑦)) |
| 34 | 33 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦
(exp‘𝑦))) = (𝑦 ∈ ℂ ↦
(exp‘𝑦))) |
| 35 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = -(𝐾 · 𝑢) → (exp‘𝑦) = (exp‘-(𝐾 · 𝑢))) |
| 36 | 1, 3, 11, 13, 15, 15, 25, 34, 35, 35 | dvmptco 26010 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))) |
| 37 | 36 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑌 ∘f · (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))) |
| 38 | | expgrowth.y |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑌:𝑆⟶ℂ) |
| 39 | | efcl 16118 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (-(𝐾 · 𝑢) ∈ ℂ → (exp‘-(𝐾 · 𝑢)) ∈ ℂ) |
| 40 | 11, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (exp‘-(𝐾 · 𝑢)) ∈ ℂ) |
| 41 | 40, 13 | mulcld 11281 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((exp‘-(𝐾 · 𝑢)) · -𝐾) ∈ ℂ) |
| 42 | 41 | fmpttd 7135 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)):𝑆⟶ℂ) |
| 43 | 36 | feq1d 6720 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ ↔ (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)):𝑆⟶ℂ)) |
| 44 | 42, 43 | mpbird 257 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ) |
| 45 | | mulcom 11241 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) |
| 46 | 45 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) |
| 47 | 1, 38, 44, 46 | caofcom 7734 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑌 ∘f · (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌)) |
| 48 | 37, 47 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))) = ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌)) |
| 49 | 48 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌))) |
| 50 | | fconst6g 6797 |
. . . . . . . . . . . . . . . . . 18
⊢ (-𝐾 ∈ ℂ → (𝑆 × {-𝐾}):𝑆⟶ℂ) |
| 51 | 12, 50 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑆 × {-𝐾}):𝑆⟶ℂ) |
| 52 | 40 | fmpttd 7135 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))):𝑆⟶ℂ) |
| 53 | 1, 51, 52, 46 | caofcom 7734 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))) ∘f · (𝑆 × {-𝐾}))) |
| 54 | | eqidd 2738 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) |
| 55 | | fconstmpt 5747 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆 × {-𝐾}) = (𝑢 ∈ 𝑆 ↦ -𝐾) |
| 56 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑆 × {-𝐾}) = (𝑢 ∈ 𝑆 ↦ -𝐾)) |
| 57 | 1, 40, 13, 54, 56 | offval2 7717 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))) ∘f · (𝑆 × {-𝐾})) = (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))) |
| 58 | 53, 57 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))) |
| 59 | 58 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))) |
| 60 | 59 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))))) |
| 61 | | expgrowth.dy |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (𝑆 D 𝑌) = 𝑆) |
| 62 | 36 | dmeqd 5916 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = dom (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))) |
| 63 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)) = (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)) |
| 64 | 63, 41 | dmmptd 6713 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)) = 𝑆) |
| 65 | 62, 64 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = 𝑆) |
| 66 | 1, 38, 52, 61, 65 | dvmulf 25980 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌))) |
| 67 | 49, 60, 66 | 3eqtr4rd 2788 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))) |
| 68 | | ofmul12 44344 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑌:𝑆⟶ℂ) ∧ ((𝑆 × {-𝐾}):𝑆⟶ℂ ∧ (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))):𝑆⟶ℂ)) → (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) |
| 69 | 1, 38, 51, 52, 68 | syl22anc 839 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) |
| 70 | 69 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))) |
| 71 | 67, 70 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))) |
| 72 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) → ((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) |
| 73 | 72 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) → (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))) |
| 74 | 71, 73 | sylan9eq 2797 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))) |
| 75 | | mulass 11243 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) |
| 76 | 75 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) |
| 77 | 1, 51, 38, 52, 76 | caofass 7737 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) |
| 78 | 77 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))) |
| 79 | 78 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) ↔ (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))) |
| 80 | 79 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ((𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) ↔ (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))) |
| 81 | 74, 80 | mpbird 257 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) |
| 82 | | mulcl 11239 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
| 83 | 82 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ) |
| 84 | | fconst6g 6797 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℂ → (𝑆 × {𝐾}):𝑆⟶ℂ) |
| 85 | 4, 84 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 × {𝐾}):𝑆⟶ℂ) |
| 86 | | inidm 4227 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∩ 𝑆) = 𝑆 |
| 87 | 83, 85, 38, 1, 1, 86 | off 7715 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑆 × {𝐾}) ∘f · 𝑌):𝑆⟶ℂ) |
| 88 | 83, 51, 38, 1, 1, 86 | off 7715 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑆 × {-𝐾}) ∘f · 𝑌):𝑆⟶ℂ) |
| 89 | | adddir 11252 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) |
| 90 | 89 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) |
| 91 | 1, 52, 87, 88, 90 | caofdir 7740 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) |
| 92 | 91 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ↔ (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))) |
| 93 | 92 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ((𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ↔ (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))) |
| 94 | 81, 93 | mpbird 257 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) |
| 95 | | ofnegsub 12264 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
((𝑆 × {𝐾}) ∘f ·
𝑌):𝑆⟶ℂ ∧ ((𝑆 × {𝐾}) ∘f · 𝑌):𝑆⟶ℂ) → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-1})
∘f · ((𝑆 × {𝐾}) ∘f · 𝑌))) = (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f −
((𝑆 × {𝐾}) ∘f ·
𝑌))) |
| 96 | 1, 87, 87, 95 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-1})
∘f · ((𝑆 × {𝐾}) ∘f · 𝑌))) = (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f −
((𝑆 × {𝐾}) ∘f ·
𝑌))) |
| 97 | | neg1cn 12380 |
. . . . . . . . . . . . . . . . 17
⊢ -1 ∈
ℂ |
| 98 | 97 | fconst6 6798 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 × {-1}):𝑆⟶ℂ |
| 99 | 98 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑆 × {-1}):𝑆⟶ℂ) |
| 100 | 1, 99, 85, 38, 76 | caofass 7737 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑆 × {-1}) ∘f ·
(𝑆 × {𝐾})) ∘f ·
𝑌) = ((𝑆 × {-1}) ∘f ·
((𝑆 × {𝐾}) ∘f ·
𝑌))) |
| 101 | 97 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → -1 ∈
ℂ) |
| 102 | 1, 101, 4 | ofc12 7727 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑆 × {-1}) ∘f ·
(𝑆 × {𝐾})) = (𝑆 × {(-1 · 𝐾)})) |
| 103 | 4 | mulm1d 11715 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (-1 · 𝐾) = -𝐾) |
| 104 | 103 | sneqd 4638 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → {(-1 · 𝐾)} = {-𝐾}) |
| 105 | 104 | xpeq2d 5715 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑆 × {(-1 · 𝐾)}) = (𝑆 × {-𝐾})) |
| 106 | 102, 105 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑆 × {-1}) ∘f ·
(𝑆 × {𝐾})) = (𝑆 × {-𝐾})) |
| 107 | 106 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑆 × {-1}) ∘f ·
(𝑆 × {𝐾})) ∘f ·
𝑌) = ((𝑆 × {-𝐾}) ∘f · 𝑌)) |
| 108 | 100, 107 | eqtr3d 2779 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆 × {-1}) ∘f ·
((𝑆 × {𝐾}) ∘f ·
𝑌)) = ((𝑆 × {-𝐾}) ∘f · 𝑌)) |
| 109 | 108 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-1})
∘f · ((𝑆 × {𝐾}) ∘f · 𝑌))) = (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌))) |
| 110 | | ofsubid 44343 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
((𝑆 × {𝐾}) ∘f ·
𝑌):𝑆⟶ℂ) → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f −
((𝑆 × {𝐾}) ∘f ·
𝑌)) = (𝑆 × {0})) |
| 111 | 1, 87, 110 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f −
((𝑆 × {𝐾}) ∘f ·
𝑌)) = (𝑆 × {0})) |
| 112 | 96, 109, 111 | 3eqtr3d 2785 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) = (𝑆 × {0})) |
| 113 | 112 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑆 × {0}) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) |
| 114 | 113 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ↔ (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 × {0}) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) |
| 115 | 114 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ((𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ↔ (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 × {0}) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) |
| 116 | 94, 115 | mpbid 232 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 × {0}) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) |
| 117 | | 0cnd 11254 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℂ) |
| 118 | | mul02 11439 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → (0
· 𝑥) =
0) |
| 119 | 118 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (0 · 𝑥) = 0) |
| 120 | 1, 52, 117, 117, 119 | caofid2 7733 |
. . . . . . . 8
⊢ (𝜑 → ((𝑆 × {0}) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {0})) |
| 121 | 120 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ((𝑆 × {0}) ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {0})) |
| 122 | 116, 121 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑆 × {0})) |
| 123 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → 𝑆 ∈ {ℝ, ℂ}) |
| 124 | 83, 38, 52, 1, 1, 86 | off 7715 |
. . . . . . . 8
⊢ (𝜑 → (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ) |
| 125 | 124 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ) |
| 126 | 122 | dmeqd 5916 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → dom (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = dom (𝑆 × {0})) |
| 127 | | 0cn 11253 |
. . . . . . . . . 10
⊢ 0 ∈
ℂ |
| 128 | 127 | fconst6 6798 |
. . . . . . . . 9
⊢ (𝑆 × {0}):𝑆⟶ℂ |
| 129 | 128 | fdmi 6747 |
. . . . . . . 8
⊢ dom
(𝑆 × {0}) = 𝑆 |
| 130 | 126, 129 | eqtrdi 2793 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → dom (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = 𝑆) |
| 131 | 123, 125,
130 | dvconstbi 44353 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ((𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑆 × {0}) ↔ ∃𝑥 ∈ ℂ (𝑌 ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}))) |
| 132 | 122, 131 | mpbid 232 |
. . . . 5
⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ∃𝑥 ∈ ℂ (𝑌 ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥})) |
| 133 | | oveq1 7438 |
. . . . . . . . . 10
⊢ ((𝑌 ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → ((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) |
| 134 | | efne0 16133 |
. . . . . . . . . . . . . . 15
⊢ (-(𝐾 · 𝑢) ∈ ℂ → (exp‘-(𝐾 · 𝑢)) ≠ 0) |
| 135 | | eldifsn 4786 |
. . . . . . . . . . . . . . 15
⊢
((exp‘-(𝐾
· 𝑢)) ∈
(ℂ ∖ {0}) ↔ ((exp‘-(𝐾 · 𝑢)) ∈ ℂ ∧ (exp‘-(𝐾 · 𝑢)) ≠ 0)) |
| 136 | 39, 134, 135 | sylanbrc 583 |
. . . . . . . . . . . . . 14
⊢ (-(𝐾 · 𝑢) ∈ ℂ → (exp‘-(𝐾 · 𝑢)) ∈ (ℂ ∖
{0})) |
| 137 | 11, 136 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (exp‘-(𝐾 · 𝑢)) ∈ (ℂ ∖
{0})) |
| 138 | 137 | fmpttd 7135 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))):𝑆⟶(ℂ ∖
{0})) |
| 139 | | ofdivcan4 44346 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝑌:𝑆⟶ℂ ∧ (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))):𝑆⟶(ℂ ∖ {0})) →
((𝑌 ∘f
· (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = 𝑌) |
| 140 | 1, 38, 138, 139 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = 𝑌) |
| 141 | 140 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ↔ 𝑌 = ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) |
| 142 | 133, 141 | imbitrid 244 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → 𝑌 = ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) |
| 143 | 142 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → 𝑌 = ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) |
| 144 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
| 145 | 144 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝑥 ∈ V) |
| 146 | | ovexd 7466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (1 / (exp‘(𝐾 · 𝑢))) ∈ V) |
| 147 | | fconstmpt 5747 |
. . . . . . . . . . . . 13
⊢ (𝑆 × {𝑥}) = (𝑢 ∈ 𝑆 ↦ 𝑥) |
| 148 | 147 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 × {𝑥}) = (𝑢 ∈ 𝑆 ↦ 𝑥)) |
| 149 | | efneg 16134 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 · 𝑢) ∈ ℂ → (exp‘-(𝐾 · 𝑢)) = (1 / (exp‘(𝐾 · 𝑢)))) |
| 150 | 10, 149 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (exp‘-(𝐾 · 𝑢)) = (1 / (exp‘(𝐾 · 𝑢)))) |
| 151 | 150 | mpteq2dva 5242 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ (1 / (exp‘(𝐾 · 𝑢))))) |
| 152 | 1, 145, 146, 148, 151 | offval2 7717 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))))) |
| 153 | 152 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))))) |
| 154 | | efcl 16118 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 · 𝑢) ∈ ℂ → (exp‘(𝐾 · 𝑢)) ∈ ℂ) |
| 155 | | efne0 16133 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 · 𝑢) ∈ ℂ → (exp‘(𝐾 · 𝑢)) ≠ 0) |
| 156 | 154, 155 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 · 𝑢) ∈ ℂ → ((exp‘(𝐾 · 𝑢)) ∈ ℂ ∧ (exp‘(𝐾 · 𝑢)) ≠ 0)) |
| 157 | 10, 156 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((exp‘(𝐾 · 𝑢)) ∈ ℂ ∧ (exp‘(𝐾 · 𝑢)) ≠ 0)) |
| 158 | | ax-1ne0 11224 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ≠
0 |
| 159 | 18, 158 | pm3.2i 470 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℂ ∧ 1 ≠ 0) |
| 160 | | divdiv2 11979 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ (1 ∈
ℂ ∧ 1 ≠ 0) ∧ ((exp‘(𝐾 · 𝑢)) ∈ ℂ ∧ (exp‘(𝐾 · 𝑢)) ≠ 0)) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = ((𝑥 · (exp‘(𝐾 · 𝑢))) / 1)) |
| 161 | 159, 160 | mp3an2 1451 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧
((exp‘(𝐾 ·
𝑢)) ∈ ℂ ∧
(exp‘(𝐾 ·
𝑢)) ≠ 0)) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = ((𝑥 · (exp‘(𝐾 · 𝑢))) / 1)) |
| 162 | 157, 161 | sylan2 593 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧ (𝜑 ∧ 𝑢 ∈ 𝑆)) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = ((𝑥 · (exp‘(𝐾 · 𝑢))) / 1)) |
| 163 | 10, 154 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (exp‘(𝐾 · 𝑢)) ∈ ℂ) |
| 164 | | mulcl 11239 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧
(exp‘(𝐾 ·
𝑢)) ∈ ℂ) →
(𝑥 ·
(exp‘(𝐾 ·
𝑢))) ∈
ℂ) |
| 165 | 163, 164 | sylan2 593 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ (𝜑 ∧ 𝑢 ∈ 𝑆)) → (𝑥 · (exp‘(𝐾 · 𝑢))) ∈ ℂ) |
| 166 | 165 | div1d 12035 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧ (𝜑 ∧ 𝑢 ∈ 𝑆)) → ((𝑥 · (exp‘(𝐾 · 𝑢))) / 1) = (𝑥 · (exp‘(𝐾 · 𝑢)))) |
| 167 | 162, 166 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ (𝜑 ∧ 𝑢 ∈ 𝑆)) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = (𝑥 · (exp‘(𝐾 · 𝑢)))) |
| 168 | 167 | ancoms 458 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑥 ∈ ℂ) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = (𝑥 · (exp‘(𝐾 · 𝑢)))) |
| 169 | 168 | an32s 652 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑢 ∈ 𝑆) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = (𝑥 · (exp‘(𝐾 · 𝑢)))) |
| 170 | 169 | mpteq2dva 5242 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑢 ∈ 𝑆 ↦ (𝑥 / (1 / (exp‘(𝐾 · 𝑢))))) = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) |
| 171 | 153, 170 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) |
| 172 | 171 | eqeq2d 2748 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑌 = ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ↔ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) |
| 173 | 143, 172 | sylibd 239 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) |
| 174 | 173 | reximdva 3168 |
. . . . . 6
⊢ (𝜑 → (∃𝑥 ∈ ℂ (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → ∃𝑥 ∈ ℂ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) |
| 175 | 174 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (∃𝑥 ∈ ℂ (𝑌 ∘f ·
(𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → ∃𝑥 ∈ ℂ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) |
| 176 | 132, 175 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ∃𝑥 ∈ ℂ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) |
| 177 | 176 | ex 412 |
. . 3
⊢ (𝜑 → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) → ∃𝑥 ∈ ℂ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) |
| 178 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) → 𝑆 ∈ {ℝ, ℂ}) |
| 179 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) → 𝐾 ∈ ℂ) |
| 180 | | simprl 771 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) → 𝑥 ∈ ℂ) |
| 181 | | eqid 2737 |
. . . . . . 7
⊢ (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) |
| 182 | 178, 179,
180, 181 | expgrowthi 44352 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) → (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) = ((𝑆 × {𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) |
| 183 | 182 | 3impb 1115 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) → (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) = ((𝑆 × {𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) |
| 184 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) → (𝑆 D 𝑌) = (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) |
| 185 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) → ((𝑆 × {𝐾}) ∘f · 𝑌) = ((𝑆 × {𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) |
| 186 | 184, 185 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) = ((𝑆 × {𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))) |
| 187 | 186 | 3ad2ant3 1136 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) = ((𝑆 × {𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))) |
| 188 | 183, 187 | mpbird 257 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) → (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) |
| 189 | 188 | rexlimdv3a 3159 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ ℂ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) → (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌))) |
| 190 | 177, 189 | impbid 212 |
. 2
⊢ (𝜑 → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ ∃𝑥 ∈ ℂ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) |
| 191 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑢 = 𝑡 → (𝐾 · 𝑢) = (𝐾 · 𝑡)) |
| 192 | 191 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑢 = 𝑡 → (exp‘(𝐾 · 𝑢)) = (exp‘(𝐾 · 𝑡))) |
| 193 | 192 | oveq2d 7447 |
. . . . . 6
⊢ (𝑢 = 𝑡 → (𝑥 · (exp‘(𝐾 · 𝑢))) = (𝑥 · (exp‘(𝐾 · 𝑡)))) |
| 194 | 193 | cbvmptv 5255 |
. . . . 5
⊢ (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) = (𝑡 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑡)))) |
| 195 | | oveq1 7438 |
. . . . . 6
⊢ (𝑥 = 𝑐 → (𝑥 · (exp‘(𝐾 · 𝑡))) = (𝑐 · (exp‘(𝐾 · 𝑡)))) |
| 196 | 195 | mpteq2dv 5244 |
. . . . 5
⊢ (𝑥 = 𝑐 → (𝑡 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑡)))) = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡))))) |
| 197 | 194, 196 | eqtrid 2789 |
. . . 4
⊢ (𝑥 = 𝑐 → (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡))))) |
| 198 | 197 | eqeq2d 2748 |
. . 3
⊢ (𝑥 = 𝑐 → (𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) ↔ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡)))))) |
| 199 | 198 | cbvrexvw 3238 |
. 2
⊢
(∃𝑥 ∈
ℂ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) ↔ ∃𝑐 ∈ ℂ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡))))) |
| 200 | 190, 199 | bitrdi 287 |
1
⊢ (𝜑 → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ ∃𝑐 ∈ ℂ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡)))))) |