Theorem expgrowth 44492

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

Statements for this and expgrowthi 44490 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 11110	. . . . . . . . . . . . . . . . . 18 ⊢ ℂ ∈ {ℝ, ℂ}
3	2	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ℂ ∈ {ℝ, ℂ})
4		expgrowth.k	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 ∈ ℂ)
5		recnprss 25852	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
6	1, 5	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
7	6	sseld 3929	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑢 ∈ 𝑆 → 𝑢 ∈ ℂ))
8		mulcl 11101	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐾 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (𝐾 · 𝑢) ∈ ℂ)
9	4, 7, 8	syl6an 684	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑢 ∈ 𝑆 → (𝐾 · 𝑢) ∈ ℂ))
10	9	imp 406	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (𝐾 · 𝑢) ∈ ℂ)
11	10	negcld 11470	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → -(𝐾 · 𝑢) ∈ ℂ)
12	4	negcld 11470	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → -𝐾 ∈ ℂ)
13	12	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → -𝐾 ∈ ℂ)
14		efcl 15996	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℂ → (exp‘𝑦) ∈ ℂ)
15	14	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (exp‘𝑦) ∈ ℂ)
16	4	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝐾 ∈ ℂ)
17	7	imp 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ ℂ)
18		ax-1cn 11075	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℂ
19	18	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 1 ∈ ℂ)
20	1	dvmptid 25908	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ 𝑢)) = (𝑢 ∈ 𝑆 ↦ 1))
21	1, 17, 19, 20, 4	dvmptcmul 25915	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ (𝐾 · 1)))
22	4	mulridd 11140	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐾 · 1) = 𝐾)
23	22	mpteq2dv 5189	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (𝐾 · 1)) = (𝑢 ∈ 𝑆 ↦ 𝐾))
24	21, 23	eqtrd 2768	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ 𝐾))
25	1, 10, 16, 24	dvmptneg 25917	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ -(𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ -𝐾))
26		dvef 25931	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℂ D exp) = exp
27		eff 15995	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ exp:ℂ⟶ℂ
28		ffn 6659	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (exp:ℂ⟶ℂ → exp Fn ℂ)
29	27, 28	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ exp Fn ℂ
30		dffn5 6889	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (exp Fn ℂ ↔ exp = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
31	29, 30	mpbi 230	. . . . . . . . . . . . . . . . . . . 20 ⊢ exp = (𝑦 ∈ ℂ ↦ (exp‘𝑦))
32	31	oveq2i 7366	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℂ D exp) = (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
33	26, 32, 31	3eqtr3i 2764	. . . . . . . . . . . . . . . . . 18 ⊢ (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦))) = (𝑦 ∈ ℂ ↦ (exp‘𝑦))
34	33	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦))) = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
35		fveq2 6831	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = -(𝐾 · 𝑢) → (exp‘𝑦) = (exp‘-(𝐾 · 𝑢)))
36	1, 3, 11, 13, 15, 15, 25, 34, 35, 35	dvmptco 25923	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))
37	36	oveq2d 7371	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌 ∘f · (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))))
38		expgrowth.y	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌:𝑆⟶ℂ)
39		efcl 15996	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-(𝐾 · 𝑢) ∈ ℂ → (exp‘-(𝐾 · 𝑢)) ∈ ℂ)
40	11, 39	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (exp‘-(𝐾 · 𝑢)) ∈ ℂ)
41	40, 13	mulcld 11143	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((exp‘-(𝐾 · 𝑢)) · -𝐾) ∈ ℂ)
42	41	fmpttd 7057	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)):𝑆⟶ℂ)
43	36	feq1d 6641	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ ↔ (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)):𝑆⟶ℂ))
44	42, 43	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ)
45		mulcom 11103	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
46	45	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
47	1, 38, 44, 46	caofcom 7656	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌 ∘f · (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌))
48	37, 47	eqtr3d 2770	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))) = ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌))
49	48	oveq2d 7371	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌)))
50		fconst6g 6720	. . . . . . . . . . . . . . . . . 18 ⊢ (-𝐾 ∈ ℂ → (𝑆 × {-𝐾}):𝑆⟶ℂ)
51	12, 50	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑆 × {-𝐾}):𝑆⟶ℂ)
52	40	fmpttd 7057	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))):𝑆⟶ℂ)
53	1, 51, 52, 46	caofcom 7656	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))) ∘f · (𝑆 × {-𝐾})))
54		eqidd 2734	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))
55		fconstmpt 5683	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 × {-𝐾}) = (𝑢 ∈ 𝑆 ↦ -𝐾)
56	55	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑆 × {-𝐾}) = (𝑢 ∈ 𝑆 ↦ -𝐾))
57	1, 40, 13, 54, 56	offval2 7639	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))) ∘f · (𝑆 × {-𝐾})) = (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))
58	53, 57	eqtrd 2768	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))
59	58	oveq2d 7371	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))))
60	59	oveq2d 7371	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))))
61		expgrowth.dy	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (𝑆 D 𝑌) = 𝑆)
62	36	dmeqd 5851	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = dom (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)))
63		eqid 2733	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)) = (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾))
64	63, 41	dmmptd 6634	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑢 ∈ 𝑆 ↦ ((exp‘-(𝐾 · 𝑢)) · -𝐾)) = 𝑆)
65	62, 64	eqtrd 2768	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = 𝑆)
66	1, 38, 52, 61, 65	dvmulf 25893	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 D (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f · 𝑌)))
67	49, 60, 66	3eqtr4rd 2779	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
68		ofmul12 44482	. . . . . . . . . . . . . 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 7371	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (𝑌 ∘f · ((𝑆 × {-𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
71	67, 70	eqtrd 2768	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
72		oveq1 7362	. . . . . . . . . . . 12 ⊢ ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) → ((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))
73	72	oveq1d 7370	. . . . . . . . . . 11 ⊢ ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) → (((𝑆 D 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
74	71, 73	sylan9eq 2788	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
75		mulass 11105	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
76	75	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))
77	1, 51, 38, 52, 76	caofass 7659	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
78	77	oveq2d 7371	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + ((𝑆 × {-𝐾}) ∘f · (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))))
79	78	eqeq2d 2744	. . . . . . . . . . 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 11101	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
83	82	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
84		fconst6g 6720	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ ℂ → (𝑆 × {𝐾}):𝑆⟶ℂ)
85	4, 84	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 × {𝐾}):𝑆⟶ℂ)
86		inidm 4176	. . . . . . . . . . . . 13 ⊢ (𝑆 ∩ 𝑆) = 𝑆
87	83, 85, 38, 1, 1, 86	off 7637	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 × {𝐾}) ∘f · 𝑌):𝑆⟶ℂ)
88	83, 51, 38, 1, 1, 86	off 7637	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 × {-𝐾}) ∘f · 𝑌):𝑆⟶ℂ)
89		adddir 11114	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
90	89	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
91	1, 52, 87, 88, 90	caofdir 7662	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f + (((𝑆 × {-𝐾}) ∘f · 𝑌) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))))
92	91	eqeq2d 2744	. . . . . . . . . 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 12134	. . . . . . . . . . . . 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 12121	. . . . . . . . . . . . . . . . 17 ⊢ -1 ∈ ℂ
98	97	fconst6 6721	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 × {-1}):𝑆⟶ℂ
99	98	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆 × {-1}):𝑆⟶ℂ)
100	1, 99, 85, 38, 76	caofass 7659	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑆 × {-1}) ∘f · (𝑆 × {𝐾})) ∘f · 𝑌) = ((𝑆 × {-1}) ∘f · ((𝑆 × {𝐾}) ∘f · 𝑌)))
101	97	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → -1 ∈ ℂ)
102	1, 101, 4	ofc12 7649	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑆 × {-1}) ∘f · (𝑆 × {𝐾})) = (𝑆 × {(-1 · 𝐾)}))
103	4	mulm1d 11580	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (-1 · 𝐾) = -𝐾)
104	103	sneqd 4589	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {(-1 · 𝐾)} = {-𝐾})
105	104	xpeq2d 5651	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑆 × {(-1 · 𝐾)}) = (𝑆 × {-𝐾}))
106	102, 105	eqtrd 2768	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑆 × {-1}) ∘f · (𝑆 × {𝐾})) = (𝑆 × {-𝐾}))
107	106	oveq1d 7370	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑆 × {-1}) ∘f · (𝑆 × {𝐾})) ∘f · 𝑌) = ((𝑆 × {-𝐾}) ∘f · 𝑌))
108	100, 107	eqtr3d 2770	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 × {-1}) ∘f · ((𝑆 × {𝐾}) ∘f · 𝑌)) = ((𝑆 × {-𝐾}) ∘f · 𝑌))
109	108	oveq2d 7371	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-1}) ∘f · ((𝑆 × {𝐾}) ∘f · 𝑌))) = (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)))
110		ofsubid 44481	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ ((𝑆 × {𝐾}) ∘f · 𝑌):𝑆⟶ℂ) → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f − ((𝑆 × {𝐾}) ∘f · 𝑌)) = (𝑆 × {0}))
111	1, 87, 110	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f − ((𝑆 × {𝐾}) ∘f · 𝑌)) = (𝑆 × {0}))
112	96, 109, 111	3eqtr3d 2776	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) = (𝑆 × {0}))
113	112	oveq1d 7370	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝑆 × {𝐾}) ∘f · 𝑌) ∘f + ((𝑆 × {-𝐾}) ∘f · 𝑌)) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑆 × {0}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))
114	113	eqeq2d 2744	. . . . . . . . 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 11116	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℂ)
118		mul02 11302	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℂ → (0 · 𝑥) = 0)
119	118	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (0 · 𝑥) = 0)
120	1, 52, 117, 117, 119	caofid2 7655	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 × {0}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {0}))
121	120	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ((𝑆 × {0}) ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {0}))
122	116, 121	eqtrd 2768	. . . . . 6 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑆 × {0}))
123	1	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → 𝑆 ∈ {ℝ, ℂ})
124	83, 38, 52, 1, 1, 86	off 7637	. . . . . . . 8 ⊢ (𝜑 → (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ)
125	124	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))):𝑆⟶ℂ)
126	122	dmeqd 5851	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → dom (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = dom (𝑆 × {0}))
127		0cn 11115	. . . . . . . . . 10 ⊢ 0 ∈ ℂ
128	127	fconst6 6721	. . . . . . . . 9 ⊢ (𝑆 × {0}):𝑆⟶ℂ
129	128	fdmi 6670	. . . . . . . 8 ⊢ dom (𝑆 × {0}) = 𝑆
130	126, 129	eqtrdi 2784	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → dom (𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = 𝑆)
131	123, 125, 130	dvconstbi 44491	. . . . . 6 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ((𝑆 D (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))))) = (𝑆 × {0}) ↔ ∃𝑥 ∈ ℂ (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥})))
132	122, 131	mpbid 232	. . . . 5 ⊢ ((𝜑 ∧ (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌)) → ∃𝑥 ∈ ℂ (𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}))
133		oveq1 7362	. . . . . . . . . 10 ⊢ ((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑆 × {𝑥}) → ((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))))
134		efne0 16012	. . . . . . . . . . . . . . 15 ⊢ (-(𝐾 · 𝑢) ∈ ℂ → (exp‘-(𝐾 · 𝑢)) ≠ 0)
135		eldifsn 4739	. . . . . . . . . . . . . . 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 7057	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))):𝑆⟶(ℂ ∖ {0}))
139		ofdivcan4 44484	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑌:𝑆⟶ℂ ∧ (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))):𝑆⟶(ℂ ∖ {0})) → ((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = 𝑌)
140	1, 38, 138, 139	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 ∘f · (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = 𝑌)
141	140	eqeq1d 2735	. . . . . . . . . 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 3441	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
145	144	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → 𝑥 ∈ V)
146		ovexd 7390	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (1 / (exp‘(𝐾 · 𝑢))) ∈ V)
147		fconstmpt 5683	. . . . . . . . . . . . 13 ⊢ (𝑆 × {𝑥}) = (𝑢 ∈ 𝑆 ↦ 𝑥)
148	147	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 × {𝑥}) = (𝑢 ∈ 𝑆 ↦ 𝑥))
149		efneg 16014	. . . . . . . . . . . . . 14 ⊢ ((𝐾 · 𝑢) ∈ ℂ → (exp‘-(𝐾 · 𝑢)) = (1 / (exp‘(𝐾 · 𝑢))))
150	10, 149	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → (exp‘-(𝐾 · 𝑢)) = (1 / (exp‘(𝐾 · 𝑢))))
151	150	mpteq2dva 5188	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢))) = (𝑢 ∈ 𝑆 ↦ (1 / (exp‘(𝐾 · 𝑢)))))
152	1, 145, 146, 148, 151	offval2 7639	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ (𝑥 / (1 / (exp‘(𝐾 · 𝑢))))))
153	152	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ (𝑥 / (1 / (exp‘(𝐾 · 𝑢))))))
154		efcl 15996	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 · 𝑢) ∈ ℂ → (exp‘(𝐾 · 𝑢)) ∈ ℂ)
155		efne0 16012	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 · 𝑢) ∈ ℂ → (exp‘(𝐾 · 𝑢)) ≠ 0)
156	154, 155	jca 511	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 · 𝑢) ∈ ℂ → ((exp‘(𝐾 · 𝑢)) ∈ ℂ ∧ (exp‘(𝐾 · 𝑢)) ≠ 0))
157	10, 156	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ((exp‘(𝐾 · 𝑢)) ∈ ℂ ∧ (exp‘(𝐾 · 𝑢)) ≠ 0))
158		ax-1ne0 11086	. . . . . . . . . . . . . . . . 17 ⊢ 1 ≠ 0
159	18, 158	pm3.2i 470	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ ℂ ∧ 1 ≠ 0)
160		divdiv2 11844	. . . . . . . . . . . . . . . 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 11101	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (exp‘(𝐾 · 𝑢)) ∈ ℂ) → (𝑥 · (exp‘(𝐾 · 𝑢))) ∈ ℂ)
165	163, 164	sylan2 593	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ (𝜑 ∧ 𝑢 ∈ 𝑆)) → (𝑥 · (exp‘(𝐾 · 𝑢))) ∈ ℂ)
166	165	div1d 11900	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ (𝜑 ∧ 𝑢 ∈ 𝑆)) → ((𝑥 · (exp‘(𝐾 · 𝑢))) / 1) = (𝑥 · (exp‘(𝐾 · 𝑢))))
167	162, 166	eqtrd 2768	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℂ ∧ (𝜑 ∧ 𝑢 ∈ 𝑆)) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = (𝑥 · (exp‘(𝐾 · 𝑢))))
168	167	ancoms 458	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝑆) ∧ 𝑥 ∈ ℂ) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = (𝑥 · (exp‘(𝐾 · 𝑢))))
169	168	an32s 652	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑢 ∈ 𝑆) → (𝑥 / (1 / (exp‘(𝐾 · 𝑢)))) = (𝑥 · (exp‘(𝐾 · 𝑢))))
170	169	mpteq2dva 5188	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑢 ∈ 𝑆 ↦ (𝑥 / (1 / (exp‘(𝐾 · 𝑢))))) = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))
171	153, 170	eqtrd 2768	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑆 × {𝑥}) ∘f / (𝑢 ∈ 𝑆 ↦ (exp‘-(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))
172	171	eqeq2d 2744	. . . . . . . 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 2733	. . . . . . 7 ⊢ (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))
182	178, 179, 180, 181	expgrowthi 44490	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))))) → (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) = ((𝑆 × {𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
183	182	3impb 1114	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) → (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))) = ((𝑆 × {𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
184		oveq2 7363	. . . . . . 7 ⊢ (𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) → (𝑆 D 𝑌) = (𝑆 D (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
185		oveq2 7363	. . . . . . 7 ⊢ (𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) → ((𝑆 × {𝐾}) ∘f · 𝑌) = ((𝑆 × {𝐾}) ∘f · (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢))))))
186	184, 185	eqeq12d 2749	. . . . . 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 7363	. . . . . . . 8 ⊢ (𝑢 = 𝑡 → (𝐾 · 𝑢) = (𝐾 · 𝑡))
192	191	fveq2d 6835	. . . . . . 7 ⊢ (𝑢 = 𝑡 → (exp‘(𝐾 · 𝑢)) = (exp‘(𝐾 · 𝑡)))
193	192	oveq2d 7371	. . . . . 6 ⊢ (𝑢 = 𝑡 → (𝑥 · (exp‘(𝐾 · 𝑢))) = (𝑥 · (exp‘(𝐾 · 𝑡))))
194	193	cbvmptv 5199	. . . . 5 ⊢ (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) = (𝑡 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑡))))
195		oveq1 7362	. . . . . 6 ⊢ (𝑥 = 𝑐 → (𝑥 · (exp‘(𝐾 · 𝑡))) = (𝑐 · (exp‘(𝐾 · 𝑡))))
196	195	mpteq2dv 5189	. . . . 5 ⊢ (𝑥 = 𝑐 → (𝑡 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑡)))) = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡)))))
197	194, 196	eqtrid 2780	. . . 4 ⊢ (𝑥 = 𝑐 → (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡)))))
198	197	eqeq2d 2744	. . 3 ⊢ (𝑥 = 𝑐 → (𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) ↔ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡))))))
199	198	cbvrexvw 3212	. 2 ⊢ (∃𝑥 ∈ ℂ 𝑌 = (𝑢 ∈ 𝑆 ↦ (𝑥 · (exp‘(𝐾 · 𝑢)))) ↔ ∃𝑐 ∈ ℂ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡)))))
200	190, 199	bitrdi 287	1 ⊢ (𝜑 → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ ∃𝑐 ∈ ℂ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡))))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113   ≠ wne 2929  ∃wrex 3057  Vcvv 3437   ∖ cdif 3895   ⊆ wss 3898  {csn 4577  {cpr 4579   ↦ cmpt 5176   × cxp 5619  dom cdm 5621   Fn wfn 6484  ⟶wf 6485  ‘cfv 6489  (class class class)co 7355   ∘_f cof 7617  ℂcc 11015  ℝcr 11016  0cc0 11017  1c1 11018   + caddc 11020   · cmul 11022   − cmin 11355  -cneg 11356   / cdiv 11785  expce 15975   D cdv 25811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-inf2 9542  ax-cnex 11073  ax-resscn 11074  ax-1cn 11075  ax-icn 11076  ax-addcl 11077  ax-addrcl 11078  ax-mulcl 11079  ax-mulrcl 11080  ax-mulcom 11081  ax-addass 11082  ax-mulass 11083  ax-distr 11084  ax-i2m1 11085  ax-1ne0 11086  ax-1rid 11087  ax-rnegex 11088  ax-rrecex 11089  ax-cnre 11090  ax-pre-lttri 11091  ax-pre-lttrn 11092  ax-pre-ltadd 11093  ax-pre-mulgt0 11094  ax-pre-sup 11095  ax-addf 11096

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rmo 3347  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-tp 4582  df-op 4584  df-uni 4861  df-int 4900  df-iun 4945  df-iin 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-se 5575  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-isom 6498  df-riota 7312  df-ov 7358  df-oprab 7359  df-mpo 7360  df-of 7619  df-om 7806  df-1st 7930  df-2nd 7931  df-supp 8100  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-1o 8394  df-2o 8395  df-er 8631  df-map 8761  df-pm 8762  df-ixp 8832  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-fsupp 9257  df-fi 9306  df-sup 9337  df-inf 9338  df-oi 9407  df-card 9843  df-pnf 11159  df-mnf 11160  df-xr 11161  df-ltxr 11162  df-le 11163  df-sub 11357  df-neg 11358  df-div 11786  df-nn 12137  df-2 12199  df-3 12200  df-4 12201  df-5 12202  df-6 12203  df-7 12204  df-8 12205  df-9 12206  df-n0 12393  df-z 12480  df-dec 12599  df-uz 12743  df-q 12853  df-rp 12897  df-xneg 13017  df-xadd 13018  df-xmul 13019  df-ioo 13256  df-ico 13258  df-icc 13259  df-fz 13415  df-fzo 13562  df-fl 13703  df-seq 13916  df-exp 13976  df-fac 14188  df-bc 14217  df-hash 14245  df-shft 14981  df-cj 15013  df-re 15014  df-im 15015  df-sqrt 15149  df-abs 15150  df-limsup 15385  df-clim 15402  df-rlim 15403  df-sum 15601  df-ef 15981  df-struct 17065  df-sets 17082  df-slot 17100  df-ndx 17112  df-base 17128  df-ress 17149  df-plusg 17181  df-mulr 17182  df-starv 17183  df-sca 17184  df-vsca 17185  df-ip 17186  df-tset 17187  df-ple 17188  df-ds 17190  df-unif 17191  df-hom 17192  df-cco 17193  df-rest 17333  df-topn 17334  df-0g 17352  df-gsum 17353  df-topgen 17354  df-pt 17355  df-prds 17358  df-xrs 17414  df-qtop 17419  df-imas 17420  df-xps 17422  df-mre 17496  df-mrc 17497  df-acs 17499  df-mgm 18556  df-sgrp 18635  df-mnd 18651  df-submnd 18700  df-mulg 18989  df-cntz 19237  df-cmn 19702  df-psmet 21292  df-xmet 21293  df-met 21294  df-bl 21295  df-mopn 21296  df-fbas 21297  df-fg 21298  df-cnfld 21301  df-top 22829  df-topon 22846  df-topsp 22868  df-bases 22881  df-cld 22954  df-ntr 22955  df-cls 22956  df-nei 23033  df-lp 23071  df-perf 23072  df-cn 23162  df-cnp 23163  df-haus 23250  df-cmp 23322  df-tx 23497  df-hmeo 23690  df-fil 23781  df-fm 23873  df-flim 23874  df-flf 23875  df-xms 24255  df-ms 24256  df-tms 24257  df-cncf 24818  df-limc 25814  df-dv 25815

This theorem is referenced by: (None)