Users' Mathboxes Mathbox for Steve Rodriguez < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  expgrowth Structured version   Visualization version   GIF version

Theorem expgrowth 44046
Description: Exponential growth and decay model. The derivative of a function y of variable t equals a constant k times y itself, iff y equals some constant C times the exponential of kt. This theorem and expgrowthi 44044 illustrate one of the simplest and most crucial classes of differential equations, equations that relate functions to their derivatives.

Section 6.3 of [Strang] p. 242 calls y' = ky "the most important differential equation in applied mathematics". In the field of population ecology it is known as the Malthusian growth model or exponential law, and C, k, and t correspond to initial population size, growth rate, and time respectively (https://en.wikipedia.org/wiki/Malthusian_growth_model 44044); and in finance, the model appears in a similar role in continuous compounding with C as the initial amount of money. In exponential decay models, k is often expressed as the negative of a positive constant λ.

Here y' is given as (𝑆 D 𝑌), C as 𝑐, and ky as ((𝑆 × {𝐾}) ∘f · 𝑌). (𝑆 × {𝐾}) is the constant function that maps any real or complex input to k and f · is multiplication as a function operation.

The leftward direction of the biconditional is as given in http://www.saylor.org/site/wp-content/uploads/2011/06/MA221-2.1.1.pdf 44044 pp. 1-2, which also notes the reverse direction ("While we will not prove this here, it turns out that these are the only functions that satisfy this equation."). The rightward direction is Theorem 5.1 of [LarsonHostetlerEdwards] p. 375 (which notes " C is the initial value of y, and k is the proportionality constant. Exponential growth occurs when k > 0, and exponential decay occurs when k < 0."); its proof here closely follows the proof of y' = y in https://proofwiki.org/wiki/Exponential_Growth_Equation/Special_Case 44044.

Statements for this and expgrowthi 44044 formulated by Mario Carneiro. (Contributed by Steve Rodriguez, 24-Nov-2015.)

Hypotheses
Ref Expression
expgrowth.s (𝜑𝑆 ∈ {ℝ, ℂ})
expgrowth.k (𝜑𝐾 ∈ ℂ)
expgrowth.y (𝜑𝑌:𝑆⟶ℂ)
expgrowth.dy (𝜑 → dom (𝑆 D 𝑌) = 𝑆)
Assertion
Ref Expression
expgrowth (𝜑 → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ ∃𝑐 ∈ ℂ 𝑌 = (𝑡𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡))))))
Distinct variable groups:   𝑡,𝑐,𝐾   𝑆,𝑐,𝑡   𝑌,𝑐
Allowed substitution hints:   𝜑(𝑡,𝑐)   𝑌(𝑡)

Proof of Theorem expgrowth
Dummy variables 𝑢 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 expgrowth.s . . . . . . . . . . . . . . . . 17 (𝜑𝑆 ∈ {ℝ, ℂ})
2 cnelprrecn 11242 . . . . . . . . . . . . . . . . . 18 ℂ ∈ {ℝ, ℂ}
32a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ℂ ∈ {ℝ, ℂ})
4 expgrowth.k . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾 ∈ ℂ)
5 recnprss 25921 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
61, 5syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑆 ⊆ ℂ)
76sseld 3977 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑢𝑆𝑢 ∈ ℂ))
8 mulcl 11233 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (𝐾 · 𝑢) ∈ ℂ)
94, 7, 8syl6an 682 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑢𝑆 → (𝐾 · 𝑢) ∈ ℂ))
109imp 405 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑆) → (𝐾 · 𝑢) ∈ ℂ)
1110negcld 11599 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑆) → -(𝐾 · 𝑢) ∈ ℂ)
124negcld 11599 . . . . . . . . . . . . . . . . . 18 (𝜑 → -𝐾 ∈ ℂ)
1312adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢𝑆) → -𝐾 ∈ ℂ)
14 efcl 16079 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℂ → (exp‘𝑦) ∈ ℂ)
1514adantl 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ℂ) → (exp‘𝑦) ∈ ℂ)
164adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑆) → 𝐾 ∈ ℂ)
177imp 405 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑆) → 𝑢 ∈ ℂ)
18 ax-1cn 11207 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℂ
1918a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢𝑆) → 1 ∈ ℂ)
201dvmptid 25977 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑆 D (𝑢𝑆𝑢)) = (𝑢𝑆 ↦ 1))
211, 17, 19, 20, 4dvmptcmul 25984 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆 D (𝑢𝑆 ↦ (𝐾 · 𝑢))) = (𝑢𝑆 ↦ (𝐾 · 1)))
224mulridd 11272 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐾 · 1) = 𝐾)
2322mpteq2dv 5247 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑢𝑆 ↦ (𝐾 · 1)) = (𝑢𝑆𝐾))
2421, 23eqtrd 2766 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑆 D (𝑢𝑆 ↦ (𝐾 · 𝑢))) = (𝑢𝑆𝐾))
251, 10, 16, 24dvmptneg 25986 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑆 D (𝑢𝑆 ↦ -(𝐾 · 𝑢))) = (𝑢𝑆 ↦ -𝐾))
26 dvef 26000 . . . . . . . . . . . . . . . . . . 19 (ℂ D exp) = exp
27 eff 16078 . . . . . . . . . . . . . . . . . . . . . 22 exp:ℂ⟶ℂ
28 ffn 6720 . . . . . . . . . . . . . . . . . . . . . 22 (exp:ℂ⟶ℂ → exp Fn ℂ)
2927, 28ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 exp Fn ℂ
30 dffn5 6953 . . . . . . . . . . . . . . . . . . . . 21 (exp Fn ℂ ↔ exp = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
3129, 30mpbi 229 . . . . . . . . . . . . . . . . . . . 20 exp = (𝑦 ∈ ℂ ↦ (exp‘𝑦))
3231oveq2i 7427 . . . . . . . . . . . . . . . . . . 19 (ℂ D exp) = (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
3326, 32, 313eqtr3i 2762 . . . . . . . . . . . . . . . . . 18 (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦))) = (𝑦 ∈ ℂ ↦ (exp‘𝑦))
3433a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦))) = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
35 fveq2 6893 . . . . . . . . . . . . . . . . 17 (𝑦 = -(𝐾 · 𝑢) → (exp‘𝑦) = (exp‘-(𝐾 · 𝑢)))
361, 3, 11, 13, 15, 15, 25, 34, 35, 35dvmptco 25992 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑆 D (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))
3736oveq2d 7432 . . . . . . . . . . . . . . 15 (𝜑 → (𝑌f · (𝑆 D (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑌f · (𝑢𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))))
38 expgrowth.y . . . . . . . . . . . . . . . 16 (𝜑𝑌:𝑆⟶ℂ)
39 efcl 16079 . . . . . . . . . . . . . . . . . . . 20 (-(𝐾 · 𝑢) ∈ ℂ → (exp‘-(𝐾 · 𝑢)) ∈ ℂ)
4011, 39syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢𝑆) → (exp‘-(𝐾 · 𝑢)) ∈ ℂ)
4140, 13mulcld 11275 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢𝑆) → ((exp‘-(𝐾 · 𝑢)) · -𝐾) ∈ ℂ)
4241fmpttd 7121 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑢𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)):𝑆⟶ℂ)
4336feq1d 6705 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑆 D (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ ↔ (𝑢𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)):𝑆⟶ℂ))
4442, 43mpbird 256 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑆 D (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ)
45 mulcom 11235 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
4645adantl 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
471, 38, 44, 46caofcom 7718 . . . . . . . . . . . . . . 15 (𝜑 → (𝑌f · (𝑆 D (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 D (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌))
4837, 47eqtr3d 2768 . . . . . . . . . . . . . 14 (𝜑 → (𝑌f · (𝑢𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))) = ((𝑆 D (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌))
4948oveq2d 7432 . . . . . . . . . . . . 13 (𝜑 → (((𝑆 D 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌f · (𝑢𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))) = (((𝑆 D 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 D (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌)))
50 fconst6g 6783 . . . . . . . . . . . . . . . . . 18 (-𝐾 ∈ ℂ → (𝑆 × {-𝐾}):𝑆⟶ℂ)
5112, 50syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑆 × {-𝐾}):𝑆⟶ℂ)
5240fmpttd 7121 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))):𝑆⟶ℂ)
531, 51, 52, 46caofcom 7718 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑆 × {-𝐾}) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))) ∘f · (𝑆 × {-𝐾})))
54 eqidd 2727 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))) = (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))
55 fconstmpt 5736 . . . . . . . . . . . . . . . . . 18 (𝑆 × {-𝐾}) = (𝑢𝑆 ↦ -𝐾)
5655a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑆 × {-𝐾}) = (𝑢𝑆 ↦ -𝐾))
571, 40, 13, 54, 56offval2 7702 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))) ∘f · (𝑆 × {-𝐾})) = (𝑢𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))
5853, 57eqtrd 2766 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑆 × {-𝐾}) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))
5958oveq2d 7432 . . . . . . . . . . . . . 14 (𝜑 → (𝑌f · ((𝑆 × {-𝐾}) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑌f · (𝑢𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))))
6059oveq2d 7432 . . . . . . . . . . . . 13 (𝜑 → (((𝑆 D 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌f · ((𝑆 × {-𝐾}) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) = (((𝑆 D 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌f · (𝑢𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))))
61 expgrowth.dy . . . . . . . . . . . . . 14 (𝜑 → dom (𝑆 D 𝑌) = 𝑆)
6236dmeqd 5904 . . . . . . . . . . . . . . 15 (𝜑 → dom (𝑆 D (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = dom (𝑢𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))
63 eqid 2726 . . . . . . . . . . . . . . . 16 (𝑢𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)) = (𝑢𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))
6463, 41dmmptd 6698 . . . . . . . . . . . . . . 15 (𝜑 → dom (𝑢𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)) = 𝑆)
6562, 64eqtrd 2766 . . . . . . . . . . . . . 14 (𝜑 → dom (𝑆 D (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = 𝑆)
661, 38, 52, 61, 65dvmulf 25962 . . . . . . . . . . . . 13 (𝜑 → (𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (((𝑆 D 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 D (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌)))
6749, 60, 663eqtr4rd 2777 . . . . . . . . . . . 12 (𝜑 → (𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (((𝑆 D 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌f · ((𝑆 × {-𝐾}) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
68 ofmul12 44036 . . . . . . . . . . . . . 14 (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑌:𝑆⟶ℂ) ∧ ((𝑆 × {-𝐾}):𝑆⟶ℂ ∧ (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))):𝑆⟶ℂ)) → (𝑌f · ((𝑆 × {-𝐾}) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 × {-𝐾}) ∘f · (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
691, 38, 51, 52, 68syl22anc 837 . . . . . . . . . . . . 13 (𝜑 → (𝑌f · ((𝑆 × {-𝐾}) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 × {-𝐾}) ∘f · (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
7069oveq2d 7432 . . . . . . . . . . . 12 (𝜑 → (((𝑆 D 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌f · ((𝑆 × {-𝐾}) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) = (((𝑆 D 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
7167, 70eqtrd 2766 . . . . . . . . . . 11 (𝜑 → (𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (((𝑆 D 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
72 oveq1 7423 . . . . . . . . . . . 12 ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) → ((𝑆 D 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))
7372oveq1d 7431 . . . . . . . . . . 11 ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) → (((𝑆 D 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
7471, 73sylan9eq 2786 . . . . . . . . . 10 ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
75 mulass 11237 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
7675adantl 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
771, 51, 38, 52, 76caofass 7720 . . . . . . . . . . . . 13 (𝜑 → (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑆 × {-𝐾}) ∘f · (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
7877oveq2d 7432 . . . . . . . . . . . 12 (𝜑 → ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
7978eqeq2d 2737 . . . . . . . . . . 11 (𝜑 → ((𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) ↔ (𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))))
8079adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ((𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) ↔ (𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))))
8174, 80mpbird 256 . . . . . . . . 9 ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
82 mulcl 11233 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
8382adantl 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
84 fconst6g 6783 . . . . . . . . . . . . . 14 (𝐾 ∈ ℂ → (𝑆 × {𝐾}):𝑆⟶ℂ)
854, 84syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑆 × {𝐾}):𝑆⟶ℂ)
86 inidm 4217 . . . . . . . . . . . . 13 (𝑆𝑆) = 𝑆
8783, 85, 38, 1, 1, 86off 7700 . . . . . . . . . . . 12 (𝜑 → ((𝑆 × {𝐾}) ∘f · 𝑌):𝑆⟶ℂ)
8883, 51, 38, 1, 1, 86off 7700 . . . . . . . . . . . 12 (𝜑 → ((𝑆 × {-𝐾}) ∘f · 𝑌):𝑆⟶ℂ)
89 adddir 11246 . . . . . . . . . . . . 13 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
9089adantl 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
911, 52, 87, 88, 90caofdir 7723 . . . . . . . . . . 11 (𝜑 → ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
9291eqeq2d 2737 . . . . . . . . . 10 (𝜑 → ((𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ↔ (𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
9392adantr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ((𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ↔ (𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
9481, 93mpbird 256 . . . . . . . 8 ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))
95 ofnegsub 12256 . . . . . . . . . . . . 13 ((𝑆 ∈ {ℝ, ℂ} ∧ ((𝑆 × {𝐾}) ∘f · 𝑌):𝑆⟶ℂ ∧ ((𝑆 × {𝐾}) ∘f · 𝑌):𝑆⟶ℂ) → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-1}) ∘f · ((𝑆 × {𝐾}) ∘f · 𝑌))) = (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f − ((𝑆 × {𝐾}) ∘f · 𝑌)))
961, 87, 87, 95syl3anc 1368 . . . . . . . . . . . 12 (𝜑 → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-1}) ∘f · ((𝑆 × {𝐾}) ∘f · 𝑌))) = (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f − ((𝑆 × {𝐾}) ∘f · 𝑌)))
97 neg1cn 12372 . . . . . . . . . . . . . . . . 17 -1 ∈ ℂ
9897fconst6 6784 . . . . . . . . . . . . . . . 16 (𝑆 × {-1}):𝑆⟶ℂ
9998a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (𝑆 × {-1}):𝑆⟶ℂ)
1001, 99, 85, 38, 76caofass 7720 . . . . . . . . . . . . . 14 (𝜑 → (((𝑆 × {-1}) ∘f · (𝑆 × {𝐾})) ∘f · 𝑌) = ((𝑆 × {-1}) ∘f · ((𝑆 × {𝐾}) ∘f · 𝑌)))
10197a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → -1 ∈ ℂ)
1021, 101, 4ofc12 7711 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑆 × {-1}) ∘f · (𝑆 × {𝐾})) = (𝑆 × {(-1 · 𝐾)}))
1034mulm1d 11707 . . . . . . . . . . . . . . . . . 18 (𝜑 → (-1 · 𝐾) = -𝐾)
104103sneqd 4635 . . . . . . . . . . . . . . . . 17 (𝜑 → {(-1 · 𝐾)} = {-𝐾})
105104xpeq2d 5704 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑆 × {(-1 · 𝐾)}) = (𝑆 × {-𝐾}))
106102, 105eqtrd 2766 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑆 × {-1}) ∘f · (𝑆 × {𝐾})) = (𝑆 × {-𝐾}))
107106oveq1d 7431 . . . . . . . . . . . . . 14 (𝜑 → (((𝑆 × {-1}) ∘f · (𝑆 × {𝐾})) ∘f · 𝑌) = ((𝑆 × {-𝐾}) ∘f · 𝑌))
108100, 107eqtr3d 2768 . . . . . . . . . . . . 13 (𝜑 → ((𝑆 × {-1}) ∘f · ((𝑆 × {𝐾}) ∘f · 𝑌)) = ((𝑆 × {-𝐾}) ∘f · 𝑌))
109108oveq2d 7432 . . . . . . . . . . . 12 (𝜑 → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-1}) ∘f · ((𝑆 × {𝐾}) ∘f · 𝑌))) = (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)))
110 ofsubid 44035 . . . . . . . . . . . . 13 ((𝑆 ∈ {ℝ, ℂ} ∧ ((𝑆 × {𝐾}) ∘f · 𝑌):𝑆⟶ℂ) → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f − ((𝑆 × {𝐾}) ∘f · 𝑌)) = (𝑆 × {0}))
1111, 87, 110syl2anc 582 . . . . . . . . . . . 12 (𝜑 → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f − ((𝑆 × {𝐾}) ∘f · 𝑌)) = (𝑆 × {0}))
11296, 109, 1113eqtr3d 2774 . . . . . . . . . . 11 (𝜑 → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) = (𝑆 × {0}))
113112oveq1d 7431 . . . . . . . . . 10 (𝜑 → ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑆 × {0}) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))
114113eqeq2d 2737 . . . . . . . . 9 (𝜑 → ((𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ↔ (𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 × {0}) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
115114adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ((𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ↔ (𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 × {0}) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
11694, 115mpbid 231 . . . . . . 7 ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 × {0}) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))
117 0cnd 11248 . . . . . . . . 9 (𝜑 → 0 ∈ ℂ)
118 mul02 11433 . . . . . . . . . 10 (𝑥 ∈ ℂ → (0 · 𝑥) = 0)
119118adantl 480 . . . . . . . . 9 ((𝜑𝑥 ∈ ℂ) → (0 · 𝑥) = 0)
1201, 52, 117, 117, 119caofid2 7717 . . . . . . . 8 (𝜑 → ((𝑆 × {0}) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {0}))
121120adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ((𝑆 × {0}) ∘f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {0}))
122116, 121eqtrd 2766 . . . . . 6 ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑆 × {0}))
1231adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → 𝑆 ∈ {ℝ, ℂ})
12483, 38, 52, 1, 1, 86off 7700 . . . . . . . 8 (𝜑 → (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ)
125124adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ)
126122dmeqd 5904 . . . . . . . 8 ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → dom (𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = dom (𝑆 × {0}))
127 0cn 11247 . . . . . . . . . 10 0 ∈ ℂ
128127fconst6 6784 . . . . . . . . 9 (𝑆 × {0}):𝑆⟶ℂ
129128fdmi 6731 . . . . . . . 8 dom (𝑆 × {0}) = 𝑆
130126, 129eqtrdi 2782 . . . . . . 7 ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → dom (𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = 𝑆)
131123, 125, 130dvconstbi 44045 . . . . . 6 ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ((𝑆 D (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑆 × {0}) ↔ ∃𝑥 ∈ ℂ (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥})))
132122, 131mpbid 231 . . . . 5 ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ∃𝑥 ∈ ℂ (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}))
133 oveq1 7423 . . . . . . . . . 10 ((𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → ((𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f / (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑆 × {𝑥}) ∘f / (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))
134 efne0 16094 . . . . . . . . . . . . . . 15 (-(𝐾 · 𝑢) ∈ ℂ → (exp‘-(𝐾 · 𝑢)) ≠ 0)
135 eldifsn 4785 . . . . . . . . . . . . . . 15 ((exp‘-(𝐾 · 𝑢)) ∈ (ℂ ∖ {0}) ↔ ((exp‘-(𝐾 · 𝑢)) ∈ ℂ ∧ (exp‘-(𝐾 · 𝑢)) ≠ 0))
13639, 134, 135sylanbrc 581 . . . . . . . . . . . . . 14 (-(𝐾 · 𝑢) ∈ ℂ → (exp‘-(𝐾 · 𝑢)) ∈ (ℂ ∖ {0}))
13711, 136syl 17 . . . . . . . . . . . . 13 ((𝜑𝑢𝑆) → (exp‘-(𝐾 · 𝑢)) ∈ (ℂ ∖ {0}))
138137fmpttd 7121 . . . . . . . . . . . 12 (𝜑 → (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))):𝑆⟶(ℂ ∖ {0}))
139 ofdivcan4 44038 . . . . . . . . . . . 12 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑌:𝑆⟶ℂ ∧ (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))):𝑆⟶(ℂ ∖ {0})) → ((𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f / (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = 𝑌)
1401, 38, 138, 139syl3anc 1368 . . . . . . . . . . 11 (𝜑 → ((𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f / (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = 𝑌)
141140eqeq1d 2728 . . . . . . . . . 10 (𝜑 → (((𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f / (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑆 × {𝑥}) ∘f / (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ↔ 𝑌 = ((𝑆 × {𝑥}) ∘f / (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
142133, 141imbitrid 243 . . . . . . . . 9 (𝜑 → ((𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → 𝑌 = ((𝑆 × {𝑥}) ∘f / (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
143142adantr 479 . . . . . . . 8 ((𝜑𝑥 ∈ ℂ) → ((𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → 𝑌 = ((𝑆 × {𝑥}) ∘f / (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
144 vex 3466 . . . . . . . . . . . . 13 𝑥 ∈ V
145144a1i 11 . . . . . . . . . . . 12 ((𝜑𝑢𝑆) → 𝑥 ∈ V)
146 ovexd 7451 . . . . . . . . . . . 12 ((𝜑𝑢𝑆) → (1 / (exp‘(𝐾 · 𝑢))) ∈ V)
147 fconstmpt 5736 . . . . . . . . . . . . 13 (𝑆 × {𝑥}) = (𝑢𝑆𝑥)
148147a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝑆 × {𝑥}) = (𝑢𝑆𝑥))
149 efneg 16095 . . . . . . . . . . . . . 14 ((𝐾 · 𝑢) ∈ ℂ → (exp‘-(𝐾 · 𝑢)) = (1 / (exp‘(𝐾 · 𝑢))))
15010, 149syl 17 . . . . . . . . . . . . 13 ((𝜑𝑢𝑆) → (exp‘-(𝐾 · 𝑢)) = (1 / (exp‘(𝐾 · 𝑢))))
151150mpteq2dva 5245 . . . . . . . . . . . 12 (𝜑 → (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢))) = (𝑢𝑆 ↦ (1 / (exp‘(𝐾 · 𝑢)))))
1521, 145, 146, 148, 151offval2 7702 . . . . . . . . . . 11 (𝜑 → ((𝑆 × {𝑥}) ∘f / (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢𝑆 ↦ (𝑥 / (1 / (exp‘(𝐾 · 𝑢))))))
153152adantr 479 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℂ) → ((𝑆 × {𝑥}) ∘f / (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢𝑆 ↦ (𝑥 / (1 / (exp‘(𝐾 · 𝑢))))))
154 efcl 16079 . . . . . . . . . . . . . . . . 17 ((𝐾 · 𝑢) ∈ ℂ → (exp‘(𝐾 · 𝑢)) ∈ ℂ)
155 efne0 16094 . . . . . . . . . . . . . . . . 17 ((𝐾 · 𝑢) ∈ ℂ → (exp‘(𝐾 · 𝑢)) ≠ 0)
156154, 155jca 510 . . . . . . . . . . . . . . . 16 ((𝐾 · 𝑢) ∈ ℂ → ((exp‘(𝐾 · 𝑢)) ∈ ℂ ∧ (exp‘(𝐾 · 𝑢)) ≠ 0))
15710, 156syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑢𝑆) → ((exp‘(𝐾 · 𝑢)) ∈ ℂ ∧ (exp‘(𝐾 · 𝑢)) ≠ 0))
158 ax-1ne0 11218 . . . . . . . . . . . . . . . . 17 1 ≠ 0
15918, 158pm3.2i 469 . . . . . . . . . . . . . . . 16 (1 ∈ ℂ ∧ 1 ≠ 0)
160 divdiv2 11971 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (1 ∈ ℂ ∧ 1 ≠ 0) ∧ ((exp‘(𝐾 · 𝑢)) ∈ ℂ ∧ (exp‘(𝐾 · 𝑢)) ≠ 0)) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = ((𝑥 · (exp‘(𝐾 · 𝑢))) / 1))
161159, 160mp3an2 1446 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℂ ∧ ((exp‘(𝐾 · 𝑢)) ∈ ℂ ∧ (exp‘(𝐾 · 𝑢)) ≠ 0)) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = ((𝑥 · (exp‘(𝐾 · 𝑢))) / 1))
162157, 161sylan2 591 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ (𝜑𝑢𝑆)) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = ((𝑥 · (exp‘(𝐾 · 𝑢))) / 1))
16310, 154syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑢𝑆) → (exp‘(𝐾 · 𝑢)) ∈ ℂ)
164 mulcl 11233 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ (exp‘(𝐾 · 𝑢)) ∈ ℂ) → (𝑥 · (exp‘(𝐾 · 𝑢))) ∈ ℂ)
165163, 164sylan2 591 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℂ ∧ (𝜑𝑢𝑆)) → (𝑥 · (exp‘(𝐾 · 𝑢))) ∈ ℂ)
166165div1d 12027 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ (𝜑𝑢𝑆)) → ((𝑥 · (exp‘(𝐾 · 𝑢))) / 1) = (𝑥 · (exp‘(𝐾 · 𝑢))))
167162, 166eqtrd 2766 . . . . . . . . . . . . 13 ((𝑥 ∈ ℂ ∧ (𝜑𝑢𝑆)) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = (𝑥 · (exp‘(𝐾 · 𝑢))))
168167ancoms 457 . . . . . . . . . . . 12 (((𝜑𝑢𝑆) ∧ 𝑥 ∈ ℂ) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = (𝑥 · (exp‘(𝐾 · 𝑢))))
169168an32s 650 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ 𝑢𝑆) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = (𝑥 · (exp‘(𝐾 · 𝑢))))
170169mpteq2dva 5245 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℂ) → (𝑢𝑆 ↦ (𝑥 / (1 / (exp‘(𝐾 · 𝑢))))) = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))
171153, 170eqtrd 2766 . . . . . . . . 9 ((𝜑𝑥 ∈ ℂ) → ((𝑆 × {𝑥}) ∘f / (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))
172171eqeq2d 2737 . . . . . . . 8 ((𝜑𝑥 ∈ ℂ) → (𝑌 = ((𝑆 × {𝑥}) ∘f / (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ↔ 𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
173143, 172sylibd 238 . . . . . . 7 ((𝜑𝑥 ∈ ℂ) → ((𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → 𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
174173reximdva 3158 . . . . . 6 (𝜑 → (∃𝑥 ∈ ℂ (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → ∃𝑥 ∈ ℂ 𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
175174adantr 479 . . . . 5 ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (∃𝑥 ∈ ℂ (𝑌f · (𝑢𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → ∃𝑥 ∈ ℂ 𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
176132, 175mpd 15 . . . 4 ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ∃𝑥 ∈ ℂ 𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))
177176ex 411 . . 3 (𝜑 → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) → ∃𝑥 ∈ ℂ 𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
1781adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) → 𝑆 ∈ {ℝ, ℂ})
1794adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) → 𝐾 ∈ ℂ)
180 simprl 769 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) → 𝑥 ∈ ℂ)
181 eqid 2726 . . . . . . 7 (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))
182178, 179, 180, 181expgrowthi 44044 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) → (𝑆 D (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) = ((𝑆 × {𝐾}) ∘f · (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
1831823impb 1112 . . . . 5 ((𝜑𝑥 ∈ ℂ ∧ 𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) → (𝑆 D (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) = ((𝑆 × {𝐾}) ∘f · (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
184 oveq2 7424 . . . . . . 7 (𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) → (𝑆 D 𝑌) = (𝑆 D (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
185 oveq2 7424 . . . . . . 7 (𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) → ((𝑆 × {𝐾}) ∘f · 𝑌) = ((𝑆 × {𝐾}) ∘f · (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
186184, 185eqeq12d 2742 . . . . . 6 (𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ (𝑆 D (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) = ((𝑆 × {𝐾}) ∘f · (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))))
1871863ad2ant3 1132 . . . . 5 ((𝜑𝑥 ∈ ℂ ∧ 𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ (𝑆 D (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) = ((𝑆 × {𝐾}) ∘f · (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))))
188183, 187mpbird 256 . . . 4 ((𝜑𝑥 ∈ ℂ ∧ 𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) → (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌))
189188rexlimdv3a 3149 . . 3 (𝜑 → (∃𝑥 ∈ ℂ 𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) → (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)))
190177, 189impbid 211 . 2 (𝜑 → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ ∃𝑥 ∈ ℂ 𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
191 oveq2 7424 . . . . . . . 8 (𝑢 = 𝑡 → (𝐾 · 𝑢) = (𝐾 · 𝑡))
192191fveq2d 6897 . . . . . . 7 (𝑢 = 𝑡 → (exp‘(𝐾 · 𝑢)) = (exp‘(𝐾 · 𝑡)))
193192oveq2d 7432 . . . . . 6 (𝑢 = 𝑡 → (𝑥 · (exp‘(𝐾 · 𝑢))) = (𝑥 · (exp‘(𝐾 · 𝑡))))
194193cbvmptv 5258 . . . . 5 (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) = (𝑡𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑡))))
195 oveq1 7423 . . . . . 6 (𝑥 = 𝑐 → (𝑥 · (exp‘(𝐾 · 𝑡))) = (𝑐 · (exp‘(𝐾 · 𝑡))))
196195mpteq2dv 5247 . . . . 5 (𝑥 = 𝑐 → (𝑡𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑡)))) = (𝑡𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡)))))
197194, 196eqtrid 2778 . . . 4 (𝑥 = 𝑐 → (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) = (𝑡𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡)))))
198197eqeq2d 2737 . . 3 (𝑥 = 𝑐 → (𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) ↔ 𝑌 = (𝑡𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡))))))
199198cbvrexvw 3226 . 2 (∃𝑥 ∈ ℂ 𝑌 = (𝑢𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) ↔ ∃𝑐 ∈ ℂ 𝑌 = (𝑡𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡)))))
200190, 199bitrdi 286 1 (𝜑 → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ ∃𝑐 ∈ ℂ 𝑌 = (𝑡𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1534  wcel 2099  wne 2930  wrex 3060  Vcvv 3462  cdif 3943  wss 3946  {csn 4623  {cpr 4625  cmpt 5228   × cxp 5672  dom cdm 5674   Fn wfn 6541  wf 6542  cfv 6546  (class class class)co 7416  f cof 7680  cc 11147  cr 11148  0cc0 11149  1c1 11150   + caddc 11152   · cmul 11154  cmin 11485  -cneg 11486   / cdiv 11912  expce 16058   D cdv 25880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7738  ax-inf2 9677  ax-cnex 11205  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225  ax-pre-mulgt0 11226  ax-pre-sup 11227  ax-addf 11228
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4906  df-int 4947  df-iun 4995  df-iin 4996  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-se 5630  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-pred 6304  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-isom 6555  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7682  df-om 7869  df-1st 7995  df-2nd 7996  df-supp 8167  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-1o 8488  df-2o 8489  df-er 8726  df-map 8849  df-pm 8850  df-ixp 8919  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-fsupp 9399  df-fi 9447  df-sup 9478  df-inf 9479  df-oi 9546  df-card 9975  df-pnf 11291  df-mnf 11292  df-xr 11293  df-ltxr 11294  df-le 11295  df-sub 11487  df-neg 11488  df-div 11913  df-nn 12259  df-2 12321  df-3 12322  df-4 12323  df-5 12324  df-6 12325  df-7 12326  df-8 12327  df-9 12328  df-n0 12519  df-z 12605  df-dec 12724  df-uz 12869  df-q 12979  df-rp 13023  df-xneg 13140  df-xadd 13141  df-xmul 13142  df-ioo 13376  df-ico 13378  df-icc 13379  df-fz 13533  df-fzo 13676  df-fl 13806  df-seq 14016  df-exp 14076  df-fac 14286  df-bc 14315  df-hash 14343  df-shft 15067  df-cj 15099  df-re 15100  df-im 15101  df-sqrt 15235  df-abs 15236  df-limsup 15468  df-clim 15485  df-rlim 15486  df-sum 15686  df-ef 16064  df-struct 17144  df-sets 17161  df-slot 17179  df-ndx 17191  df-base 17209  df-ress 17238  df-plusg 17274  df-mulr 17275  df-starv 17276  df-sca 17277  df-vsca 17278  df-ip 17279  df-tset 17280  df-ple 17281  df-ds 17283  df-unif 17284  df-hom 17285  df-cco 17286  df-rest 17432  df-topn 17433  df-0g 17451  df-gsum 17452  df-topgen 17453  df-pt 17454  df-prds 17457  df-xrs 17512  df-qtop 17517  df-imas 17518  df-xps 17520  df-mre 17594  df-mrc 17595  df-acs 17597  df-mgm 18628  df-sgrp 18707  df-mnd 18723  df-submnd 18769  df-mulg 19058  df-cntz 19307  df-cmn 19776  df-psmet 21331  df-xmet 21332  df-met 21333  df-bl 21334  df-mopn 21335  df-fbas 21336  df-fg 21337  df-cnfld 21340  df-top 22884  df-topon 22901  df-topsp 22923  df-bases 22937  df-cld 23011  df-ntr 23012  df-cls 23013  df-nei 23090  df-lp 23128  df-perf 23129  df-cn 23219  df-cnp 23220  df-haus 23307  df-cmp 23379  df-tx 23554  df-hmeo 23747  df-fil 23838  df-fm 23930  df-flim 23931  df-flf 23932  df-xms 24314  df-ms 24315  df-tms 24316  df-cncf 24886  df-limc 25883  df-dv 25884
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator