Theorem expgrowth 44297

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 44295 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 44295); 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 44295 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 44295.

Statements for this and expgrowthi 44295 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 11137	. . . . . . . . . . . . . . . . . 18 ⊢ ℂ ∈ {ℝ, ℂ}
3	2	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ℂ ∈ {ℝ, ℂ})
4		expgrowth.k	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 ∈ ℂ)
5		recnprss 25781	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
6	1, 5	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
7	6	sseld 3942	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑢 ∈ 𝑆 → 𝑢 ∈ ℂ))
8		mulcl 11128	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐾 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (𝐾 · 𝑢) ∈ ℂ)
9	4, 7, 8	syl6an 684	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑢 ∈ 𝑆 → (𝐾 · 𝑢) ∈ ℂ))
10	9	imp 406	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (𝐾 · 𝑢) ∈ ℂ)
11	10	negcld 11496	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → -(𝐾 · 𝑢) ∈ ℂ)
12	4	negcld 11496	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → -𝐾 ∈ ℂ)
13	12	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → -𝐾 ∈ ℂ)
14		efcl 16024	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℂ → (exp‘𝑦) ∈ ℂ)
15	14	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (exp‘𝑦) ∈ ℂ)
16	4	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝐾 ∈ ℂ)
17	7	imp 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ ℂ)
18		ax-1cn 11102	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℂ
19	18	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 1 ∈ ℂ)
20	1	dvmptid 25837	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ 𝑢)) = (𝑢 ∈ 𝑆 ↦ 1))
21	1, 17, 19, 20, 4	dvmptcmul 25844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ (𝐾 · 1)))
22	4	mulridd 11167	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐾 · 1) = 𝐾)
23	22	mpteq2dv 5196	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (𝐾 · 1)) = (𝑢 ∈ 𝑆 ↦ 𝐾))
24	21, 23	eqtrd 2764	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ 𝐾))
25	1, 10, 16, 24	dvmptneg 25846	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ -(𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ -𝐾))
26		dvef 25860	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℂ D exp) = exp
27		eff 16023	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ exp:ℂ⟶ℂ
28		ffn 6670	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (exp:ℂ⟶ℂ → exp Fn ℂ)
29	27, 28	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ exp Fn ℂ
30		dffn5 6901	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (exp Fn ℂ ↔ exp = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
31	29, 30	mpbi 230	. . . . . . . . . . . . . . . . . . . 20 ⊢ exp = (𝑦 ∈ ℂ ↦ (exp‘𝑦))
32	31	oveq2i 7380	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℂ D exp) = (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
33	26, 32, 31	3eqtr3i 2760	. . . . . . . . . . . . . . . . . 18 ⊢ (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦))) = (𝑦 ∈ ℂ ↦ (exp‘𝑦))
34	33	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦))) = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
35		fveq2 6840	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = -(𝐾 · 𝑢) → (exp‘𝑦) = (exp‘-(𝐾 · 𝑢)))
36	1, 3, 11, 13, 15, 15, 25, 34, 35, 35	dvmptco 25852	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))
37	36	oveq2d 7385	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌 ∘f · (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))))
38		expgrowth.y	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌:𝑆⟶ℂ)
39		efcl 16024	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-(𝐾 · 𝑢) ∈ ℂ → (exp‘-(𝐾 · 𝑢)) ∈ ℂ)
40	11, 39	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (exp‘-(𝐾 · 𝑢)) ∈ ℂ)
41	40, 13	mulcld 11170	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((exp‘-(𝐾 · 𝑢)) · -𝐾) ∈ ℂ)
42	41	fmpttd 7069	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)):𝑆⟶ℂ)
43	36	feq1d 6652	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ ↔ (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)):𝑆⟶ℂ))
44	42, 43	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ)
45		mulcom 11130	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
46	45	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
47	1, 38, 44, 46	caofcom 7670	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌 ∘f · (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌))
48	37, 47	eqtr3d 2766	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))) = ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌))
49	48	oveq2d 7385	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌)))
50		fconst6g 6731	. . . . . . . . . . . . . . . . . 18 ⊢ (-𝐾 ∈ ℂ → (𝑆 × {-𝐾}):𝑆⟶ℂ)
51	12, 50	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑆 × {-𝐾}):𝑆⟶ℂ)
52	40	fmpttd 7069	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))):𝑆⟶ℂ)
53	1, 51, 52, 46	caofcom 7670	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))) ∘f · (𝑆 × {-𝐾})))
54		eqidd 2730	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))
55		fconstmpt 5693	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 × {-𝐾}) = (𝑢 ∈ 𝑆 ↦ -𝐾)
56	55	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑆 × {-𝐾}) = (𝑢 ∈ 𝑆 ↦ -𝐾))
57	1, 40, 13, 54, 56	offval2 7653	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))) ∘f · (𝑆 × {-𝐾})) = (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))
58	53, 57	eqtrd 2764	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))
59	58	oveq2d 7385	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))))
60	59	oveq2d 7385	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))))
61		expgrowth.dy	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (𝑆 D 𝑌) = 𝑆)
62	36	dmeqd 5859	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = dom (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))
63		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)) = (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))
64	63, 41	dmmptd 6645	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)) = 𝑆)
65	62, 64	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = 𝑆)
66	1, 38, 52, 61, 65	dvmulf 25822	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌)))
67	49, 60, 66	3eqtr4rd 2775	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
68		ofmul12 44287	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑌:𝑆⟶ℂ) ∧ ((𝑆 × {-𝐾}):𝑆⟶ℂ ∧ (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))):𝑆⟶ℂ)) → (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
69	1, 38, 51, 52, 68	syl22anc 838	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
70	69	oveq2d 7385	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
71	67, 70	eqtrd 2764	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
72		oveq1 7376	. . . . . . . . . . . 12 ⊢ ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) → ((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))
73	72	oveq1d 7384	. . . . . . . . . . 11 ⊢ ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) → (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
74	71, 73	sylan9eq 2784	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
75		mulass 11132	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
76	75	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
77	1, 51, 38, 52, 76	caofass 7673	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
78	77	oveq2d 7385	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
79	78	eqeq2d 2740	. . . . . . . . . . 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 11128	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
83	82	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
84		fconst6g 6731	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ ℂ → (𝑆 × {𝐾}):𝑆⟶ℂ)
85	4, 84	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 × {𝐾}):𝑆⟶ℂ)
86		inidm 4186	. . . . . . . . . . . . 13 ⊢ (𝑆 ∩ 𝑆) = 𝑆
87	83, 85, 38, 1, 1, 86	off 7651	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 × {𝐾}) ∘f · 𝑌):𝑆⟶ℂ)
88	83, 51, 38, 1, 1, 86	off 7651	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 × {-𝐾}) ∘f · 𝑌):𝑆⟶ℂ)
89		adddir 11141	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
90	89	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
91	1, 52, 87, 88, 90	caofdir 7676	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
92	91	eqeq2d 2740	. . . . . . . . . 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 12160	. . . . . . . . . . . . 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 12147	. . . . . . . . . . . . . . . . 17 ⊢ -1 ∈ ℂ
98	97	fconst6 6732	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 × {-1}):𝑆⟶ℂ
99	98	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆 × {-1}):𝑆⟶ℂ)
100	1, 99, 85, 38, 76	caofass 7673	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑆 × {-1}) ∘f · (𝑆 × {𝐾})) ∘f · 𝑌) = ((𝑆 × {-1}) ∘f · ((𝑆 × {𝐾}) ∘f · 𝑌)))
101	97	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → -1 ∈ ℂ)
102	1, 101, 4	ofc12 7663	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑆 × {-1}) ∘f · (𝑆 × {𝐾})) = (𝑆 × {(-1 · 𝐾)}))
103	4	mulm1d 11606	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (-1 · 𝐾) = -𝐾)
104	103	sneqd 4597	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {(-1 · 𝐾)} = {-𝐾})
105	104	xpeq2d 5661	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑆 × {(-1 · 𝐾)}) = (𝑆 × {-𝐾}))
106	102, 105	eqtrd 2764	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑆 × {-1}) ∘f · (𝑆 × {𝐾})) = (𝑆 × {-𝐾}))
107	106	oveq1d 7384	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑆 × {-1}) ∘f · (𝑆 × {𝐾})) ∘f · 𝑌) = ((𝑆 × {-𝐾}) ∘f · 𝑌))
108	100, 107	eqtr3d 2766	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 × {-1}) ∘f · ((𝑆 × {𝐾}) ∘f · 𝑌)) = ((𝑆 × {-𝐾}) ∘f · 𝑌))
109	108	oveq2d 7385	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-1}) ∘f · ((𝑆 × {𝐾}) ∘f · 𝑌))) = (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)))
110		ofsubid 44286	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ ((𝑆 × {𝐾}) ∘f · 𝑌):𝑆⟶ℂ) → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f − ((𝑆 × {𝐾}) ∘f · 𝑌)) = (𝑆 × {0}))
111	1, 87, 110	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f − ((𝑆 × {𝐾}) ∘f · 𝑌)) = (𝑆 × {0}))
112	96, 109, 111	3eqtr3d 2772	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) = (𝑆 × {0}))
113	112	oveq1d 7384	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑆 × {0}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))
114	113	eqeq2d 2740	. . . . . . . . 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 11143	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℂ)
118		mul02 11328	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℂ → (0 · 𝑥) = 0)
119	118	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (0 · 𝑥) = 0)
120	1, 52, 117, 117, 119	caofid2 7669	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 × {0}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {0}))
121	120	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ((𝑆 × {0}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {0}))
122	116, 121	eqtrd 2764	. . . . . 6 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑆 × {0}))
123	1	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → 𝑆 ∈ {ℝ, ℂ})
124	83, 38, 52, 1, 1, 86	off 7651	. . . . . . . 8 ⊢ (𝜑 → (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ)
125	124	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ)
126	122	dmeqd 5859	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → dom (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = dom (𝑆 × {0}))
127		0cn 11142	. . . . . . . . . 10 ⊢ 0 ∈ ℂ
128	127	fconst6 6732	. . . . . . . . 9 ⊢ (𝑆 × {0}):𝑆⟶ℂ
129	128	fdmi 6681	. . . . . . . 8 ⊢ dom (𝑆 × {0}) = 𝑆
130	126, 129	eqtrdi 2780	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → dom (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = 𝑆)
131	123, 125, 130	dvconstbi 44296	. . . . . 6 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ((𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑆 × {0}) ↔ ∃𝑥 ∈ ℂ (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥})))
132	122, 131	mpbid 232	. . . . 5 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ∃𝑥 ∈ ℂ (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}))
133		oveq1 7376	. . . . . . . . . 10 ⊢ ((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → ((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))
134		efne0 16040	. . . . . . . . . . . . . . 15 ⊢ (-(𝐾 · 𝑢) ∈ ℂ → (exp‘-(𝐾 · 𝑢)) ≠ 0)
135		eldifsn 4746	. . . . . . . . . . . . . . 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 7069	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))):𝑆⟶(ℂ ∖ {0}))
139		ofdivcan4 44289	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑌:𝑆⟶ℂ ∧ (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))):𝑆⟶(ℂ ∖ {0})) → ((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = 𝑌)
140	1, 38, 138, 139	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = 𝑌)
141	140	eqeq1d 2731	. . . . . . . . . 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 3448	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
145	144	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝑥 ∈ V)
146		ovexd 7404	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (1 / (exp‘(𝐾 · 𝑢))) ∈ V)
147		fconstmpt 5693	. . . . . . . . . . . . 13 ⊢ (𝑆 × {𝑥}) = (𝑢 ∈ 𝑆 ↦ 𝑥)
148	147	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 × {𝑥}) = (𝑢 ∈ 𝑆 ↦ 𝑥))
149		efneg 16042	. . . . . . . . . . . . . 14 ⊢ ((𝐾 · 𝑢) ∈ ℂ → (exp‘-(𝐾 · 𝑢)) = (1 / (exp‘(𝐾 · 𝑢))))
150	10, 149	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (exp‘-(𝐾 · 𝑢)) = (1 / (exp‘(𝐾 · 𝑢))))
151	150	mpteq2dva 5195	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ (1 / (exp‘(𝐾 · 𝑢)))))
152	1, 145, 146, 148, 151	offval2 7653	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ (𝑥 / (1 / (exp‘(𝐾 · 𝑢))))))
153	152	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ (𝑥 / (1 / (exp‘(𝐾 · 𝑢))))))
154		efcl 16024	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 · 𝑢) ∈ ℂ → (exp‘(𝐾 · 𝑢)) ∈ ℂ)
155		efne0 16040	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 · 𝑢) ∈ ℂ → (exp‘(𝐾 · 𝑢)) ≠ 0)
156	154, 155	jca 511	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 · 𝑢) ∈ ℂ → ((exp‘(𝐾 · 𝑢)) ∈ ℂ ∧ (exp‘(𝐾 · 𝑢)) ≠ 0))
157	10, 156	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((exp‘(𝐾 · 𝑢)) ∈ ℂ ∧ (exp‘(𝐾 · 𝑢)) ≠ 0))
158		ax-1ne0 11113	. . . . . . . . . . . . . . . . 17 ⊢ 1 ≠ 0
159	18, 158	pm3.2i 470	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ ℂ ∧ 1 ≠ 0)
160		divdiv2 11870	. . . . . . . . . . . . . . . 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 11128	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (exp‘(𝐾 · 𝑢)) ∈ ℂ) → (𝑥 · (exp‘(𝐾 · 𝑢))) ∈ ℂ)
165	163, 164	sylan2 593	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ (𝜑 ∧ 𝑢 ∈ 𝑆)) → (𝑥 · (exp‘(𝐾 · 𝑢))) ∈ ℂ)
166	165	div1d 11926	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ (𝜑 ∧ 𝑢 ∈ 𝑆)) → ((𝑥 · (exp‘(𝐾 · 𝑢))) / 1) = (𝑥 · (exp‘(𝐾 · 𝑢))))
167	162, 166	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℂ ∧ (𝜑 ∧ 𝑢 ∈ 𝑆)) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = (𝑥 · (exp‘(𝐾 · 𝑢))))
168	167	ancoms 458	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑥 ∈ ℂ) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = (𝑥 · (exp‘(𝐾 · 𝑢))))
169	168	an32s 652	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑢 ∈ 𝑆) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = (𝑥 · (exp‘(𝐾 · 𝑢))))
170	169	mpteq2dva 5195	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑢 ∈ 𝑆 ↦ (𝑥 / (1 / (exp‘(𝐾 · 𝑢))))) = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))
171	153, 170	eqtrd 2764	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))
172	171	eqeq2d 2740	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑌 = ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ↔ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
173	143, 172	sylibd 239	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
174	173	reximdva 3146	. . . . . 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 770	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) → 𝑥 ∈ ℂ)
181		eqid 2729	. . . . . . 7 ⊢ (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))
182	178, 179, 180, 181	expgrowthi 44295	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) → (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) = ((𝑆 × {𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
183	182	3impb 1114	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) → (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) = ((𝑆 × {𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
184		oveq2 7377	. . . . . . 7 ⊢ (𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) → (𝑆 D 𝑌) = (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
185		oveq2 7377	. . . . . . 7 ⊢ (𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) → ((𝑆 × {𝐾}) ∘f · 𝑌) = ((𝑆 × {𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
186	184, 185	eqeq12d 2745	. . . . . 6 ⊢ (𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) = ((𝑆 × {𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))))
187	186	3ad2ant3 1135	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) = ((𝑆 × {𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))))
188	183, 187	mpbird 257	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) → (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌))
189	188	rexlimdv3a 3138	. . 3 ⊢ (𝜑 → (∃𝑥 ∈ ℂ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) → (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)))
190	177, 189	impbid 212	. 2 ⊢ (𝜑 → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ ∃𝑥 ∈ ℂ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
191		oveq2 7377	. . . . . . . 8 ⊢ (𝑢 = 𝑡 → (𝐾 · 𝑢) = (𝐾 · 𝑡))
192	191	fveq2d 6844	. . . . . . 7 ⊢ (𝑢 = 𝑡 → (exp‘(𝐾 · 𝑢)) = (exp‘(𝐾 · 𝑡)))
193	192	oveq2d 7385	. . . . . 6 ⊢ (𝑢 = 𝑡 → (𝑥 · (exp‘(𝐾 · 𝑢))) = (𝑥 · (exp‘(𝐾 · 𝑡))))
194	193	cbvmptv 5206	. . . . 5 ⊢ (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) = (𝑡 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑡))))
195		oveq1 7376	. . . . . 6 ⊢ (𝑥 = 𝑐 → (𝑥 · (exp‘(𝐾 · 𝑡))) = (𝑐 · (exp‘(𝐾 · 𝑡))))
196	195	mpteq2dv 5196	. . . . 5 ⊢ (𝑥 = 𝑐 → (𝑡 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑡)))) = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡)))))
197	194, 196	eqtrid 2776	. . . 4 ⊢ (𝑥 = 𝑐 → (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡)))))
198	197	eqeq2d 2740	. . 3 ⊢ (𝑥 = 𝑐 → (𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) ↔ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡))))))
199	198	cbvrexvw 3214	. 2 ⊢ (∃𝑥 ∈ ℂ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) ↔ ∃𝑐 ∈ ℂ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡)))))
200	190, 199	bitrdi 287	1 ⊢ (𝜑 → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ ∃𝑐 ∈ ℂ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡))))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∃wrex 3053  Vcvv 3444   ∖ cdif 3908   ⊆ wss 3911  {csn 4585  {cpr 4587   ↦ cmpt 5183   × cxp 5629  dom cdm 5631   Fn wfn 6494  ⟶wf 6495  ‘cfv 6499  (class class class)co 7369   ∘_f cof 7631  ℂcc 11042  ℝcr 11043  0cc0 11044  1c1 11045   + caddc 11047   · cmul 11049   − cmin 11381  -cneg 11382   / cdiv 11811  expce 16003   D cdv 25740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-inf2 9570  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121  ax-pre-sup 11122  ax-addf 11123

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4868  df-int 4907  df-iun 4953  df-iin 4954  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-isom 6508  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-of 7633  df-om 7823  df-1st 7947  df-2nd 7948  df-supp 8117  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-1o 8411  df-2o 8412  df-er 8648  df-map 8778  df-pm 8779  df-ixp 8848  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fsupp 9289  df-fi 9338  df-sup 9369  df-inf 9370  df-oi 9439  df-card 9868  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-div 11812  df-nn 12163  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230  df-8 12231  df-9 12232  df-n0 12419  df-z 12506  df-dec 12626  df-uz 12770  df-q 12884  df-rp 12928  df-xneg 13048  df-xadd 13049  df-xmul 13050  df-ioo 13286  df-ico 13288  df-icc 13289  df-fz 13445  df-fzo 13592  df-fl 13730  df-seq 13943  df-exp 14003  df-fac 14215  df-bc 14244  df-hash 14272  df-shft 15009  df-cj 15041  df-re 15042  df-im 15043  df-sqrt 15177  df-abs 15178  df-limsup 15413  df-clim 15430  df-rlim 15431  df-sum 15629  df-ef 16009  df-struct 17093  df-sets 17110  df-slot 17128  df-ndx 17140  df-base 17156  df-ress 17177  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-rest 17361  df-topn 17362  df-0g 17380  df-gsum 17381  df-topgen 17382  df-pt 17383  df-prds 17386  df-xrs 17441  df-qtop 17446  df-imas 17447  df-xps 17449  df-mre 17523  df-mrc 17524  df-acs 17526  df-mgm 18543  df-sgrp 18622  df-mnd 18638  df-submnd 18687  df-mulg 18976  df-cntz 19225  df-cmn 19688  df-psmet 21232  df-xmet 21233  df-met 21234  df-bl 21235  df-mopn 21236  df-fbas 21237  df-fg 21238  df-cnfld 21241  df-top 22757  df-topon 22774  df-topsp 22796  df-bases 22809  df-cld 22882  df-ntr 22883  df-cls 22884  df-nei 22961  df-lp 22999  df-perf 23000  df-cn 23090  df-cnp 23091  df-haus 23178  df-cmp 23250  df-tx 23425  df-hmeo 23618  df-fil 23709  df-fm 23801  df-flim 23802  df-flf 23803  df-xms 24184  df-ms 24185  df-tms 24186  df-cncf 24747  df-limc 25743  df-dv 25744

This theorem is referenced by: (None)