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.

Step	Hyp	Ref	Expression
1		expgrowth.s	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
2		cnelprrecn 11242	. . . . . . . . . . . . . . . . . 18 ⊢ ℂ ∈ {ℝ, ℂ}
3	2	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ℂ ∈ {ℝ, ℂ})
4		expgrowth.k	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 ∈ ℂ)
5		recnprss 25921	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
6	1, 5	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
7	6	sseld 3977	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑢 ∈ 𝑆 → 𝑢 ∈ ℂ))
8		mulcl 11233	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐾 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (𝐾 · 𝑢) ∈ ℂ)
9	4, 7, 8	syl6an 682	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑢 ∈ 𝑆 → (𝐾 · 𝑢) ∈ ℂ))
10	9	imp 405	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (𝐾 · 𝑢) ∈ ℂ)
11	10	negcld 11599	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → -(𝐾 · 𝑢) ∈ ℂ)
12	4	negcld 11599	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → -𝐾 ∈ ℂ)
13	12	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → -𝐾 ∈ ℂ)
14		efcl 16079	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℂ → (exp‘𝑦) ∈ ℂ)
15	14	adantl 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (exp‘𝑦) ∈ ℂ)
16	4	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝐾 ∈ ℂ)
17	7	imp 405	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ ℂ)
18		ax-1cn 11207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℂ
19	18	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 1 ∈ ℂ)
20	1	dvmptid 25977	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ 𝑢)) = (𝑢 ∈ 𝑆 ↦ 1))
21	1, 17, 19, 20, 4	dvmptcmul 25984	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ (𝐾 · 1)))
22	4	mulridd 11272	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐾 · 1) = 𝐾)
23	22	mpteq2dv 5247	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (𝐾 · 1)) = (𝑢 ∈ 𝑆 ↦ 𝐾))
24	21, 23	eqtrd 2766	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ 𝐾))
25	1, 10, 16, 24	dvmptneg 25986	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ -(𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ -𝐾))
26		dvef 26000	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℂ D exp) = exp
27		eff 16078	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ exp:ℂ⟶ℂ
28		ffn 6720	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (exp:ℂ⟶ℂ → exp Fn ℂ)
29	27, 28	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ exp Fn ℂ
30		dffn5 6953	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (exp Fn ℂ ↔ exp = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
31	29, 30	mpbi 229	. . . . . . . . . . . . . . . . . . . 20 ⊢ exp = (𝑦 ∈ ℂ ↦ (exp‘𝑦))
32	31	oveq2i 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℂ D exp) = (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
33	26, 32, 31	3eqtr3i 2762	. . . . . . . . . . . . . . . . . 18 ⊢ (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦))) = (𝑦 ∈ ℂ ↦ (exp‘𝑦))
34	33	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦))) = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
35		fveq2 6893	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = -(𝐾 · 𝑢) → (exp‘𝑦) = (exp‘-(𝐾 · 𝑢)))
36	1, 3, 11, 13, 15, 15, 25, 34, 35, 35	dvmptco 25992	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))
37	36	oveq2d 7432	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌 ∘f · (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))))
38		expgrowth.y	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌:𝑆⟶ℂ)
39		efcl 16079	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-(𝐾 · 𝑢) ∈ ℂ → (exp‘-(𝐾 · 𝑢)) ∈ ℂ)
40	11, 39	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (exp‘-(𝐾 · 𝑢)) ∈ ℂ)
41	40, 13	mulcld 11275	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((exp‘-(𝐾 · 𝑢)) · -𝐾) ∈ ℂ)
42	41	fmpttd 7121	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)):𝑆⟶ℂ)
43	36	feq1d 6705	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ ↔ (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)):𝑆⟶ℂ))
44	42, 43	mpbird 256	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ)
45		mulcom 11235	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
46	45	adantl 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
47	1, 38, 44, 46	caofcom 7718	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌 ∘f · (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌))
48	37, 47	eqtr3d 2768	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))) = ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌))
49	48	oveq2d 7432	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌)))
50		fconst6g 6783	. . . . . . . . . . . . . . . . . 18 ⊢ (-𝐾 ∈ ℂ → (𝑆 × {-𝐾}):𝑆⟶ℂ)
51	12, 50	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑆 × {-𝐾}):𝑆⟶ℂ)
52	40	fmpttd 7121	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))):𝑆⟶ℂ)
53	1, 51, 52, 46	caofcom 7718	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))) ∘f · (𝑆 × {-𝐾})))
54		eqidd 2727	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))
55		fconstmpt 5736	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 × {-𝐾}) = (𝑢 ∈ 𝑆 ↦ -𝐾)
56	55	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑆 × {-𝐾}) = (𝑢 ∈ 𝑆 ↦ -𝐾))
57	1, 40, 13, 54, 56	offval2 7702	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))) ∘f · (𝑆 × {-𝐾})) = (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))
58	53, 57	eqtrd 2766	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))
59	58	oveq2d 7432	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))))
60	59	oveq2d 7432	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))))
61		expgrowth.dy	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (𝑆 D 𝑌) = 𝑆)
62	36	dmeqd 5904	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = dom (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))
63		eqid 2726	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)) = (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))
64	63, 41	dmmptd 6698	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)) = 𝑆)
65	62, 64	eqtrd 2766	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = 𝑆)
66	1, 38, 52, 61, 65	dvmulf 25962	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌)))
67	49, 60, 66	3eqtr4rd 2777	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
68		ofmul12 44036	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑌:𝑆⟶ℂ) ∧ ((𝑆 × {-𝐾}):𝑆⟶ℂ ∧ (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))):𝑆⟶ℂ)) → (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
69	1, 38, 51, 52, 68	syl22anc 837	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
70	69	oveq2d 7432	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
71	67, 70	eqtrd 2766	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
72		oveq1 7423	. . . . . . . . . . . 12 ⊢ ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) → ((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))
73	72	oveq1d 7431	. . . . . . . . . . 11 ⊢ ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) → (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
74	71, 73	sylan9eq 2786	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
75		mulass 11237	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
76	75	adantl 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
77	1, 51, 38, 52, 76	caofass 7720	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
78	77	oveq2d 7432	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
79	78	eqeq2d 2737	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) ↔ (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))))
80	79	adantr 479	. . . . . . . . . 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 256	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
82		mulcl 11233	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
83	82	adantl 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
84		fconst6g 6783	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ ℂ → (𝑆 × {𝐾}):𝑆⟶ℂ)
85	4, 84	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 × {𝐾}):𝑆⟶ℂ)
86		inidm 4217	. . . . . . . . . . . . 13 ⊢ (𝑆 ∩ 𝑆) = 𝑆
87	83, 85, 38, 1, 1, 86	off 7700	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 × {𝐾}) ∘f · 𝑌):𝑆⟶ℂ)
88	83, 51, 38, 1, 1, 86	off 7700	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 × {-𝐾}) ∘f · 𝑌):𝑆⟶ℂ)
89		adddir 11246	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
90	89	adantl 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
91	1, 52, 87, 88, 90	caofdir 7723	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
92	91	eqeq2d 2737	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ↔ (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
93	92	adantr 479	. . . . . . . . 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 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 · 𝑌)))
96	1, 87, 87, 95	syl3anc 1368	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-1}) ∘f · ((𝑆 × {𝐾}) ∘f · 𝑌))) = (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f − ((𝑆 × {𝐾}) ∘f · 𝑌)))
97		neg1cn 12372	. . . . . . . . . . . . . . . . 17 ⊢ -1 ∈ ℂ
98	97	fconst6 6784	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 × {-1}):𝑆⟶ℂ
99	98	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆 × {-1}):𝑆⟶ℂ)
100	1, 99, 85, 38, 76	caofass 7720	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑆 × {-1}) ∘f · (𝑆 × {𝐾})) ∘f · 𝑌) = ((𝑆 × {-1}) ∘f · ((𝑆 × {𝐾}) ∘f · 𝑌)))
101	97	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → -1 ∈ ℂ)
102	1, 101, 4	ofc12 7711	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑆 × {-1}) ∘f · (𝑆 × {𝐾})) = (𝑆 × {(-1 · 𝐾)}))
103	4	mulm1d 11707	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (-1 · 𝐾) = -𝐾)
104	103	sneqd 4635	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {(-1 · 𝐾)} = {-𝐾})
105	104	xpeq2d 5704	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑆 × {(-1 · 𝐾)}) = (𝑆 × {-𝐾}))
106	102, 105	eqtrd 2766	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑆 × {-1}) ∘f · (𝑆 × {𝐾})) = (𝑆 × {-𝐾}))
107	106	oveq1d 7431	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑆 × {-1}) ∘f · (𝑆 × {𝐾})) ∘f · 𝑌) = ((𝑆 × {-𝐾}) ∘f · 𝑌))
108	100, 107	eqtr3d 2768	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 × {-1}) ∘f · ((𝑆 × {𝐾}) ∘f · 𝑌)) = ((𝑆 × {-𝐾}) ∘f · 𝑌))
109	108	oveq2d 7432	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-1}) ∘f · ((𝑆 × {𝐾}) ∘f · 𝑌))) = (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)))
110		ofsubid 44035	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ ((𝑆 × {𝐾}) ∘f · 𝑌):𝑆⟶ℂ) → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f − ((𝑆 × {𝐾}) ∘f · 𝑌)) = (𝑆 × {0}))
111	1, 87, 110	syl2anc 582	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f − ((𝑆 × {𝐾}) ∘f · 𝑌)) = (𝑆 × {0}))
112	96, 109, 111	3eqtr3d 2774	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) = (𝑆 × {0}))
113	112	oveq1d 7431	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑆 × {0}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))
114	113	eqeq2d 2737	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ↔ (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 × {0}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
115	114	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ((𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ↔ (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 × {0}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
116	94, 115	mpbid 231	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 × {0}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))
117		0cnd 11248	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℂ)
118		mul02 11433	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℂ → (0 · 𝑥) = 0)
119	118	adantl 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (0 · 𝑥) = 0)
120	1, 52, 117, 117, 119	caofid2 7717	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 × {0}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {0}))
121	120	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ((𝑆 × {0}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {0}))
122	116, 121	eqtrd 2766	. . . . . 6 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑆 × {0}))
123	1	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → 𝑆 ∈ {ℝ, ℂ})
124	83, 38, 52, 1, 1, 86	off 7700	. . . . . . . 8 ⊢ (𝜑 → (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ)
125	124	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ)
126	122	dmeqd 5904	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → dom (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = dom (𝑆 × {0}))
127		0cn 11247	. . . . . . . . . 10 ⊢ 0 ∈ ℂ
128	127	fconst6 6784	. . . . . . . . 9 ⊢ (𝑆 × {0}):𝑆⟶ℂ
129	128	fdmi 6731	. . . . . . . 8 ⊢ dom (𝑆 × {0}) = 𝑆
130	126, 129	eqtrdi 2782	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → dom (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = 𝑆)
131	123, 125, 130	dvconstbi 44045	. . . . . 6 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ((𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑆 × {0}) ↔ ∃𝑥 ∈ ℂ (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥})))
132	122, 131	mpbid 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))
136	39, 134, 135	sylanbrc 581	. . . . . . . . . . . . . 14 ⊢ (-(𝐾 · 𝑢) ∈ ℂ → (exp‘-(𝐾 · 𝑢)) ∈ (ℂ ∖ {0}))
137	11, 136	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (exp‘-(𝐾 · 𝑢)) ∈ (ℂ ∖ {0}))
138	137	fmpttd 7121	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))):𝑆⟶(ℂ ∖ {0}))
139		ofdivcan4 44038	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑌:𝑆⟶ℂ ∧ (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))):𝑆⟶(ℂ ∖ {0})) → ((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = 𝑌)
140	1, 38, 138, 139	syl3anc 1368	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = 𝑌)
141	140	eqeq1d 2728	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ↔ 𝑌 = ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
142	133, 141	imbitrid 243	. . . . . . . . 9 ⊢ (𝜑 → ((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → 𝑌 = ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
143	142	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → 𝑌 = ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
144		vex 3466	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
145	144	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝑥 ∈ V)
146		ovexd 7451	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (1 / (exp‘(𝐾 · 𝑢))) ∈ V)
147		fconstmpt 5736	. . . . . . . . . . . . 13 ⊢ (𝑆 × {𝑥}) = (𝑢 ∈ 𝑆 ↦ 𝑥)
148	147	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 × {𝑥}) = (𝑢 ∈ 𝑆 ↦ 𝑥))
149		efneg 16095	. . . . . . . . . . . . . 14 ⊢ ((𝐾 · 𝑢) ∈ ℂ → (exp‘-(𝐾 · 𝑢)) = (1 / (exp‘(𝐾 · 𝑢))))
150	10, 149	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (exp‘-(𝐾 · 𝑢)) = (1 / (exp‘(𝐾 · 𝑢))))
151	150	mpteq2dva 5245	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ (1 / (exp‘(𝐾 · 𝑢)))))
152	1, 145, 146, 148, 151	offval2 7702	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ (𝑥 / (1 / (exp‘(𝐾 · 𝑢))))))
153	152	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ (𝑥 / (1 / (exp‘(𝐾 · 𝑢))))))
154		efcl 16079	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 · 𝑢) ∈ ℂ → (exp‘(𝐾 · 𝑢)) ∈ ℂ)
155		efne0 16094	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 · 𝑢) ∈ ℂ → (exp‘(𝐾 · 𝑢)) ≠ 0)
156	154, 155	jca 510	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 · 𝑢) ∈ ℂ → ((exp‘(𝐾 · 𝑢)) ∈ ℂ ∧ (exp‘(𝐾 · 𝑢)) ≠ 0))
157	10, 156	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((exp‘(𝐾 · 𝑢)) ∈ ℂ ∧ (exp‘(𝐾 · 𝑢)) ≠ 0))
158		ax-1ne0 11218	. . . . . . . . . . . . . . . . 17 ⊢ 1 ≠ 0
159	18, 158	pm3.2i 469	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ ℂ ∧ 1 ≠ 0)
160		divdiv2 11971	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (1 ∈ ℂ ∧ 1 ≠ 0) ∧ ((exp‘(𝐾 · 𝑢)) ∈ ℂ ∧ (exp‘(𝐾 · 𝑢)) ≠ 0)) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = ((𝑥 · (exp‘(𝐾 · 𝑢))) / 1))
161	159, 160	mp3an2 1446	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ ((exp‘(𝐾 · 𝑢)) ∈ ℂ ∧ (exp‘(𝐾 · 𝑢)) ≠ 0)) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = ((𝑥 · (exp‘(𝐾 · 𝑢))) / 1))
162	157, 161	sylan2 591	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ (𝜑 ∧ 𝑢 ∈ 𝑆)) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = ((𝑥 · (exp‘(𝐾 · 𝑢))) / 1))
163	10, 154	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (exp‘(𝐾 · 𝑢)) ∈ ℂ)
164		mulcl 11233	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (exp‘(𝐾 · 𝑢)) ∈ ℂ) → (𝑥 · (exp‘(𝐾 · 𝑢))) ∈ ℂ)
165	163, 164	sylan2 591	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ (𝜑 ∧ 𝑢 ∈ 𝑆)) → (𝑥 · (exp‘(𝐾 · 𝑢))) ∈ ℂ)
166	165	div1d 12027	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ (𝜑 ∧ 𝑢 ∈ 𝑆)) → ((𝑥 · (exp‘(𝐾 · 𝑢))) / 1) = (𝑥 · (exp‘(𝐾 · 𝑢))))
167	162, 166	eqtrd 2766	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℂ ∧ (𝜑 ∧ 𝑢 ∈ 𝑆)) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = (𝑥 · (exp‘(𝐾 · 𝑢))))
168	167	ancoms 457	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑥 ∈ ℂ) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = (𝑥 · (exp‘(𝐾 · 𝑢))))
169	168	an32s 650	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑢 ∈ 𝑆) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = (𝑥 · (exp‘(𝐾 · 𝑢))))
170	169	mpteq2dva 5245	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑢 ∈ 𝑆 ↦ (𝑥 / (1 / (exp‘(𝐾 · 𝑢))))) = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))
171	153, 170	eqtrd 2766	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))
172	171	eqeq2d 2737	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑌 = ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ↔ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
173	143, 172	sylibd 238	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
174	173	reximdva 3158	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ ℂ (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → ∃𝑥 ∈ ℂ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
175	174	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (∃𝑥 ∈ ℂ (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → ∃𝑥 ∈ ℂ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
176	132, 175	mpd 15	. . . 4 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ∃𝑥 ∈ ℂ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))
177	176	ex 411	. . 3 ⊢ (𝜑 → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) → ∃𝑥 ∈ ℂ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
178	1	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) → 𝑆 ∈ {ℝ, ℂ})
179	4	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) → 𝐾 ∈ ℂ)
180		simprl 769	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) → 𝑥 ∈ ℂ)
181		eqid 2726	. . . . . . 7 ⊢ (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))
182	178, 179, 180, 181	expgrowthi 44044	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) → (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) = ((𝑆 × {𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
183	182	3impb 1112	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) → (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) = ((𝑆 × {𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
184		oveq2 7424	. . . . . . 7 ⊢ (𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) → (𝑆 D 𝑌) = (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
185		oveq2 7424	. . . . . . 7 ⊢ (𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) → ((𝑆 × {𝐾}) ∘f · 𝑌) = ((𝑆 × {𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
186	184, 185	eqeq12d 2742	. . . . . 6 ⊢ (𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) = ((𝑆 × {𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))))
187	186	3ad2ant3 1132	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) = ((𝑆 × {𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))))
188	183, 187	mpbird 256	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) → (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌))
189	188	rexlimdv3a 3149	. . 3 ⊢ (𝜑 → (∃𝑥 ∈ ℂ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) → (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)))
190	177, 189	impbid 211	. 2 ⊢ (𝜑 → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ ∃𝑥 ∈ ℂ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
191		oveq2 7424	. . . . . . . 8 ⊢ (𝑢 = 𝑡 → (𝐾 · 𝑢) = (𝐾 · 𝑡))
192	191	fveq2d 6897	. . . . . . 7 ⊢ (𝑢 = 𝑡 → (exp‘(𝐾 · 𝑢)) = (exp‘(𝐾 · 𝑡)))
193	192	oveq2d 7432	. . . . . 6 ⊢ (𝑢 = 𝑡 → (𝑥 · (exp‘(𝐾 · 𝑢))) = (𝑥 · (exp‘(𝐾 · 𝑡))))
194	193	cbvmptv 5258	. . . . 5 ⊢ (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) = (𝑡 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑡))))
195		oveq1 7423	. . . . . 6 ⊢ (𝑥 = 𝑐 → (𝑥 · (exp‘(𝐾 · 𝑡))) = (𝑐 · (exp‘(𝐾 · 𝑡))))
196	195	mpteq2dv 5247	. . . . 5 ⊢ (𝑥 = 𝑐 → (𝑡 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑡)))) = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡)))))
197	194, 196	eqtrid 2778	. . . 4 ⊢ (𝑥 = 𝑐 → (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡)))))
198	197	eqeq2d 2737	. . 3 ⊢ (𝑥 = 𝑐 → (𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) ↔ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡))))))
199	198	cbvrexvw 3226	. 2 ⊢ (∃𝑥 ∈ ℂ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) ↔ ∃𝑐 ∈ ℂ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡)))))
200	190, 199	bitrdi 286	1 ⊢ (𝜑 → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ ∃𝑐 ∈ ℂ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡))))))

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)