smcnlem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > smcnlem		Structured version Visualization version GIF version

Theorem smcnlem 28592

Description: Lemma for smcn 28593. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
smcn.c	⊢ 𝐶 = (IndMet‘𝑈)
smcn.j	⊢ 𝐽 = (MetOpen‘𝐶)
smcn.s	⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
smcn.k	⊢ 𝐾 = (TopOpen‘ℂ_fld)
smcn.x	⊢ 𝑋 = (BaseSet‘𝑈)
smcn.n	⊢ 𝑁 = (norm_CV‘𝑈)
smcn.u	⊢ 𝑈 ∈ NrmCVec
smcn.t	⊢ 𝑇 = (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))

**Assertion**
Ref	Expression
smcnlem	⊢ 𝑆 ∈ ((𝐾 ×_t 𝐽) Cn 𝐽)

Distinct variable groups: 𝑥,𝑟,𝑦,𝐶 𝐽,𝑟,𝑥,𝑦 𝑈,𝑟,𝑥,𝑦 𝐾,𝑟,𝑥,𝑦 𝑆,𝑟,𝑥,𝑦 𝑋,𝑟,𝑥,𝑦 Allowed substitution hints: 𝑇(𝑥,𝑦,𝑟) 𝑁(𝑥,𝑦,𝑟)

Proof of Theorem smcnlem Dummy variables 𝑠 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		smcn.u	. . 3 ⊢ 𝑈 ∈ NrmCVec
2		smcn.x	. . . 4 ⊢ 𝑋 = (BaseSet‘𝑈)
3		smcn.s	. . . 4 ⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
4	2, 3	nvsf 28514	. . 3 ⊢ (𝑈 ∈ NrmCVec → 𝑆:(ℂ × 𝑋)⟶𝑋)
5	1, 4	ax-mp 5	. 2 ⊢ 𝑆:(ℂ × 𝑋)⟶𝑋
6		smcn.t	. . . . . 6 ⊢ 𝑇 = (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
7		1rp 12447	. . . . . . . 8 ⊢ 1 ∈ ℝ⁺
8		simpr 488	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
9		smcn.n	. . . . . . . . . . . . 13 ⊢ 𝑁 = (norm_CV‘𝑈)
10	2, 9	nvcl 28556	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋) → (𝑁‘𝑦) ∈ ℝ)
11	1, 8, 10	sylancr 590	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑁‘𝑦) ∈ ℝ)
12		abscl 14699	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (abs‘𝑥) ∈ ℝ)
13	12	adantr 484	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (abs‘𝑥) ∈ ℝ)
14	11, 13	readdcld 10721	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → ((𝑁‘𝑦) + (abs‘𝑥)) ∈ ℝ)
15	2, 9	nvge0 28568	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝑁‘𝑦))
16	1, 8, 15	sylancr 590	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝑁‘𝑦))
17		absge0 14708	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → 0 ≤ (abs‘𝑥))
18	17	adantr 484	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 0 ≤ (abs‘𝑥))
19	11, 13, 16, 18	addge0d 11267	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 0 ≤ ((𝑁‘𝑦) + (abs‘𝑥)))
20	14, 19	ge0p1rpd 12515	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ⁺)
21		rpdivcl 12468	. . . . . . . . 9 ⊢ (((((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ⁺ ∧ 𝑟 ∈ ℝ⁺) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺)
22	20, 21	sylan 583	. . . . . . . 8 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺)
23		rpaddcl 12465	. . . . . . . 8 ⊢ ((1 ∈ ℝ⁺ ∧ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℝ⁺)
24	7, 22, 23	sylancr 590	. . . . . . 7 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℝ⁺)
25	24	rpreccld 12495	. . . . . 6 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) ∈ ℝ⁺)
26	6, 25	eqeltrid 2856	. . . . 5 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → 𝑇 ∈ ℝ⁺)
27		smcn.c	. . . . . . . . . . . 12 ⊢ 𝐶 = (IndMet‘𝑈)
28	2, 27	imsmet 28586	. . . . . . . . . . 11 ⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈ (Met‘𝑋))
29	1, 28	ax-mp 5	. . . . . . . . . 10 ⊢ 𝐶 ∈ (Met‘𝑋)
30	29	a1i 11	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝐶 ∈ (Met‘𝑋))
31	1	a1i 11	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑈 ∈ NrmCVec)
32		simplll 774	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑥 ∈ ℂ)
33		simpllr 775	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑦 ∈ 𝑋)
34	2, 3	nvscl 28521	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑥𝑆𝑦) ∈ 𝑋)
35	31, 32, 33, 34	syl3anc 1368	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥𝑆𝑦) ∈ 𝑋)
36		simprll 778	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑧 ∈ ℂ)
37		simprlr 779	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑤 ∈ 𝑋)
38	2, 3	nvscl 28521	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) → (𝑧𝑆𝑤) ∈ 𝑋)
39	31, 36, 37, 38	syl3anc 1368	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧𝑆𝑤) ∈ 𝑋)
40		metcl 23047	. . . . . . . . 9 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ (𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
41	30, 35, 39, 40	syl3anc 1368	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
42	2, 3	nvscl 28521	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑧𝑆𝑦) ∈ 𝑋)
43	31, 36, 33, 42	syl3anc 1368	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧𝑆𝑦) ∈ 𝑋)
44		metcl 23047	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ (𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑦) ∈ 𝑋) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) ∈ ℝ)
45	30, 35, 43, 44	syl3anc 1368	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) ∈ ℝ)
46		metcl 23047	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ (𝑧𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
47	30, 43, 39, 46	syl3anc 1368	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
48	45, 47	readdcld 10721	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) ∈ ℝ)
49		rpre 12451	. . . . . . . . 9 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ)
50	49	ad2antlr 726	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑟 ∈ ℝ)
51		mettri 23067	. . . . . . . . 9 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ ((𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋 ∧ (𝑧𝑆𝑦) ∈ 𝑋)) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ≤ (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))))
52	30, 35, 39, 43, 51	syl13anc 1369	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ≤ (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))))
53	1, 33, 10	sylancr 590	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘𝑦) ∈ ℝ)
54	32	abscld 14857	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑥) ∈ ℝ)
55	53, 54	readdcld 10721	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑁‘𝑦) + (abs‘𝑥)) ∈ ℝ)
56		peano2re 10864	. . . . . . . . . . 11 ⊢ (((𝑁‘𝑦) + (abs‘𝑥)) ∈ ℝ → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ)
57	55, 56	syl 17	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ)
58	26	adantr 484	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ∈ ℝ⁺)
59	58	rpred 12485	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ∈ ℝ)
60	57, 59	remulcld 10722	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) ∈ ℝ)
61	32, 36	subcld 11048	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 − 𝑧) ∈ ℂ)
62	61	abscld 14857	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 − 𝑧)) ∈ ℝ)
63	62, 53	remulcld 10722	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) ∈ ℝ)
64	36	abscld 14857	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑧) ∈ ℝ)
65		eqid 2758	. . . . . . . . . . . . . . 15 ⊢ ( −_𝑣 ‘𝑈) = ( −_𝑣 ‘𝑈)
66	2, 65	nvmcl 28541	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋)
67	31, 33, 37, 66	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋)
68	2, 9	nvcl 28556	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) ∈ ℝ)
69	1, 67, 68	sylancr 590	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) ∈ ℝ)
70	64, 69	remulcld 10722	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))) ∈ ℝ)
71	53, 59	remulcld 10722	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑁‘𝑦) · 𝑇) ∈ ℝ)
72		peano2re 10864	. . . . . . . . . . . . 13 ⊢ ((abs‘𝑥) ∈ ℝ → ((abs‘𝑥) + 1) ∈ ℝ)
73	54, 72	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + 1) ∈ ℝ)
74	73, 59	remulcld 10722	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((abs‘𝑥) + 1) · 𝑇) ∈ ℝ)
75	1, 33, 15	sylancr 590	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 0 ≤ (𝑁‘𝑦))
76	32, 36	abssubd 14874	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 − 𝑧)) = (abs‘(𝑧 − 𝑥)))
77	36, 32	subcld 11048	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧 − 𝑥) ∈ ℂ)
78	77	abscld 14857	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) ∈ ℝ)
79		eqid 2758	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs ∘ − ) = (abs ∘ − )
80	79	cnmetdval 23485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑥(abs ∘ − )𝑧) = (abs‘(𝑥 − 𝑧)))
81	32, 36, 80	syl2anc 587	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥(abs ∘ − )𝑧) = (abs‘(𝑥 − 𝑧)))
82	81, 76	eqtrd 2793	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥(abs ∘ − )𝑧) = (abs‘(𝑧 − 𝑥)))
83		simprrl 780	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥(abs ∘ − )𝑧) < 𝑇)
84	82, 83	eqbrtrrd 5060	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) < 𝑇)
85	78, 59, 84	ltled 10839	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) ≤ 𝑇)
86	76, 85	eqbrtrd 5058	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 − 𝑧)) ≤ 𝑇)
87	62, 59, 53, 75, 86	lemul1ad 11630	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) ≤ (𝑇 · (𝑁‘𝑦)))
88	58	rpcnd 12487	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ∈ ℂ)
89	53	recnd 10720	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘𝑦) ∈ ℂ)
90	88, 89	mulcomd 10713	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑇 · (𝑁‘𝑦)) = ((𝑁‘𝑦) · 𝑇))
91	87, 90	breqtrd 5062	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) ≤ ((𝑁‘𝑦) · 𝑇))
92	36	absge0d 14865	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 0 ≤ (abs‘𝑧))
93	2, 9	nvge0 28568	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋) → 0 ≤ (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
94	1, 67, 93	sylancr 590	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 0 ≤ (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
95	54, 78	readdcld 10721	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))) ∈ ℝ)
96	32, 36	pncan3d 11051	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + (𝑧 − 𝑥)) = 𝑧)
97	96	fveq2d 6667	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 + (𝑧 − 𝑥))) = (abs‘𝑧))
98	32, 77	abstrid 14877	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 + (𝑧 − 𝑥))) ≤ ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))))
99	97, 98	eqbrtrrd 5060	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑧) ≤ ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))))
100		1red 10693	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 1 ∈ ℝ)
101		1re 10692	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
102	22	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺)
103		ltaddrp 12480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺) → 1 < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
104	101, 102, 103	sylancr 590	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 1 < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
105	24	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℝ⁺)
106	105	recgt1d 12499	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ↔ (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) < 1))
107	104, 106	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) < 1)
108	6, 107	eqbrtrid 5071	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 < 1)
109	59, 100, 108	ltled 10839	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ≤ 1)
110	78, 59, 100, 85, 109	letrd 10848	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) ≤ 1)
111	78, 100, 54, 110	leadd2dd 11306	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))) ≤ ((abs‘𝑥) + 1))
112	64, 95, 73, 99, 111	letrd 10848	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑧) ≤ ((abs‘𝑥) + 1))
113	2, 65, 9, 27	imsdval 28581	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑦𝐶𝑤) = (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
114	31, 33, 37, 113	syl3anc 1368	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑦𝐶𝑤) = (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
115		simprrr 781	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑦𝐶𝑤) < 𝑇)
116	114, 115	eqbrtrrd 5060	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) < 𝑇)
117	69, 59, 116	ltled 10839	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) ≤ 𝑇)
118	64, 73, 69, 59, 92, 94, 112, 117	lemul12ad 11633	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))) ≤ (((abs‘𝑥) + 1) · 𝑇))
119	63, 70, 71, 74, 91, 118	le2addd 11310	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) + ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))) ≤ (((𝑁‘𝑦) · 𝑇) + (((abs‘𝑥) + 1) · 𝑇)))
120		eqid 2758	. . . . . . . . . . . . . 14 ⊢ ( +_𝑣 ‘𝑈) = ( +_𝑣 ‘𝑈)
121	2, 120, 3, 9, 27	imsdval2 28582	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑦) ∈ 𝑋) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) = (𝑁‘((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦)))))
122	31, 35, 43, 121	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) = (𝑁‘((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦)))))
123		neg1cn 11801	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℂ
124		mulcl 10672	. . . . . . . . . . . . . . . 16 ⊢ ((-1 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (-1 · 𝑧) ∈ ℂ)
125	123, 36, 124	sylancr 590	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (-1 · 𝑧) ∈ ℂ)
126	2, 120, 3	nvdir 28526	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥 ∈ ℂ ∧ (-1 · 𝑧) ∈ ℂ ∧ 𝑦 ∈ 𝑋)) → ((𝑥 + (-1 · 𝑧))𝑆𝑦) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)((-1 · 𝑧)𝑆𝑦)))
127	31, 32, 125, 33, 126	syl13anc 1369	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥 + (-1 · 𝑧))𝑆𝑦) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)((-1 · 𝑧)𝑆𝑦)))
128	36	mulm1d 11143	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (-1 · 𝑧) = -𝑧)
129	128	oveq2d 7172	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + (-1 · 𝑧)) = (𝑥 + -𝑧))
130	32, 36	negsubd 11054	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + -𝑧) = (𝑥 − 𝑧))
131	129, 130	eqtrd 2793	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + (-1 · 𝑧)) = (𝑥 − 𝑧))
132	131	oveq1d 7171	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥 + (-1 · 𝑧))𝑆𝑦) = ((𝑥 − 𝑧)𝑆𝑦))
133	123	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → -1 ∈ ℂ)
134	2, 3	nvsass 28523	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ NrmCVec ∧ (-1 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋)) → ((-1 · 𝑧)𝑆𝑦) = (-1𝑆(𝑧𝑆𝑦)))
135	31, 133, 36, 33, 134	syl13anc 1369	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((-1 · 𝑧)𝑆𝑦) = (-1𝑆(𝑧𝑆𝑦)))
136	135	oveq2d 7172	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)((-1 · 𝑧)𝑆𝑦)) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦))))
137	127, 132, 136	3eqtr3d 2801	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥 − 𝑧)𝑆𝑦) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦))))
138	137	fveq2d 6667	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘((𝑥 − 𝑧)𝑆𝑦)) = (𝑁‘((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦)))))
139	2, 3, 9	nvs 28558	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥 − 𝑧) ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑁‘((𝑥 − 𝑧)𝑆𝑦)) = ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)))
140	31, 61, 33, 139	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘((𝑥 − 𝑧)𝑆𝑦)) = ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)))
141	122, 138, 140	3eqtr2d 2799	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) = ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)))
142	2, 65, 9, 27	imsdval 28581	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑧𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) = (𝑁‘((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤))))
143	31, 43, 39, 142	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) = (𝑁‘((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤))))
144	2, 65, 3	nvmdi 28543	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤)) = ((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤)))
145	31, 36, 33, 37, 144	syl13anc 1369	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤)) = ((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤)))
146	145	fveq2d 6667	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤))) = (𝑁‘((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤))))
147	2, 3, 9	nvs 28558	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋) → (𝑁‘(𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤))) = ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))))
148	31, 36, 67, 147	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤))) = ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))))
149	143, 146, 148	3eqtr2d 2799	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) = ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))))
150	141, 149	oveq12d 7174	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) = (((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) + ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))))
151	54	recnd 10720	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑥) ∈ ℂ)
152		1cnd 10687	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 1 ∈ ℂ)
153	89, 151, 152	addassd 10714	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) = ((𝑁‘𝑦) + ((abs‘𝑥) + 1)))
154	153	oveq1d 7171	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = (((𝑁‘𝑦) + ((abs‘𝑥) + 1)) · 𝑇))
155	73	recnd 10720	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + 1) ∈ ℂ)
156	89, 155, 88	adddird 10717	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + ((abs‘𝑥) + 1)) · 𝑇) = (((𝑁‘𝑦) · 𝑇) + (((abs‘𝑥) + 1) · 𝑇)))
157	154, 156	eqtrd 2793	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = (((𝑁‘𝑦) · 𝑇) + (((abs‘𝑥) + 1) · 𝑇)))
158	119, 150, 157	3brtr4d 5068	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) ≤ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇))
159	6	oveq2i 7167	. . . . . . . . . . 11 ⊢ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))))
160	57	recnd 10720	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℂ)
161	105	rpcnd 12487	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℂ)
162	105	rpne0d 12490	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ≠ 0)
163	160, 161, 162	divrecd 11470	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) = ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))))
164	159, 163	eqtr4id 2812	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))))
165		simplr 768	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑟 ∈ ℝ⁺)
166	102	rpred 12485	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ)
167	166	ltp1d 11621	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) < (((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) + 1))
168	102	rpcnd 12487	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℂ)
169	168, 152	addcomd 10893	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) + 1) = (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
170	167, 169	breqtrd 5062	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
171	57, 165, 105, 170	ltdiv23d 12552	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) < 𝑟)
172	164, 171	eqbrtrd 5058	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) < 𝑟)
173	48, 60, 50, 158, 172	lelttrd 10849	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) < 𝑟)
174	41, 48, 50, 52, 173	lelttrd 10849	. . . . . . 7 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)
175	174	expr 460	. . . . . 6 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋)) → (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
176	175	ralrimivva 3120	. . . . 5 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
177		breq2 5040	. . . . . . . . 9 ⊢ (𝑠 = 𝑇 → ((𝑥(abs ∘ − )𝑧) < 𝑠 ↔ (𝑥(abs ∘ − )𝑧) < 𝑇))
178		breq2 5040	. . . . . . . . 9 ⊢ (𝑠 = 𝑇 → ((𝑦𝐶𝑤) < 𝑠 ↔ (𝑦𝐶𝑤) < 𝑇))
179	177, 178	anbi12d 633	. . . . . . . 8 ⊢ (𝑠 = 𝑇 → (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) ↔ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇)))
180	179	imbi1d 345	. . . . . . 7 ⊢ (𝑠 = 𝑇 → ((((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟) ↔ (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)))
181	180	2ralbidv 3128	. . . . . 6 ⊢ (𝑠 = 𝑇 → (∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟) ↔ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)))
182	181	rspcev 3543	. . . . 5 ⊢ ((𝑇 ∈ ℝ⁺ ∧ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)) → ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
183	26, 176, 182	syl2anc 587	. . . 4 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
184	183	ralrimiva 3113	. . 3 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
185	184	rgen2 3132	. 2 ⊢ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)
186		cnxmet 23487	. . 3 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
187	2, 27	imsxmet 28587	. . . 4 ⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈ (∞Met‘𝑋))
188	1, 187	ax-mp 5	. . 3 ⊢ 𝐶 ∈ (∞Met‘𝑋)
189		smcn.k	. . . . 5 ⊢ 𝐾 = (TopOpen‘ℂ_fld)
190	189	cnfldtopn 23496	. . . 4 ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))
191		smcn.j	. . . 4 ⊢ 𝐽 = (MetOpen‘𝐶)
192	190, 191, 191	txmetcn 23263	. . 3 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ (∞Met‘𝑋) ∧ 𝐶 ∈ (∞Met‘𝑋)) → (𝑆 ∈ ((𝐾 ×_t 𝐽) Cn 𝐽) ↔ (𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))))
193	186, 188, 188, 192	mp3an 1458	. 2 ⊢ (𝑆 ∈ ((𝐾 ×_t 𝐽) Cn 𝐽) ↔ (𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)))
194	5, 185, 193	mpbir2an 710	1 ⊢ 𝑆 ∈ ((𝐾 ×_t 𝐽) Cn 𝐽)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1538 ∈ wcel 2111 ∀wral 3070 ∃wrex 3071 class class class wbr 5036 × cxp 5526 ∘ ccom 5532 ⟶wf 6336 ‘cfv 6340 (class class class)co 7156 ℂcc 10586 ℝcr 10587 0cc0 10588 1c1 10589 + caddc 10591 · cmul 10593 < clt 10726 ≤ cle 10727 − cmin 10921 -cneg 10922 / cdiv 11348 ℝ⁺crp 12443 abscabs 14654 TopOpenctopn 16766 ∞Metcxmet 20164 Metcmet 20165 MetOpencmopn 20169 ℂ_fldccnfld 20179 Cn ccn 21937 ×_t ctx 22273 NrmCVeccnv 28479 +_𝑣 cpv 28480 BaseSetcba 28481 ·_𝑠OLD cns 28482 −_𝑣 cnsb 28484 norm_CVcnmcv 28485 IndMetcims 28486

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5160 ax-sep 5173 ax-nul 5180 ax-pow 5238 ax-pr 5302 ax-un 7465 ax-cnex 10644 ax-resscn 10645 ax-1cn 10646 ax-icn 10647 ax-addcl 10648 ax-addrcl 10649 ax-mulcl 10650 ax-mulrcl 10651 ax-mulcom 10652 ax-addass 10653 ax-mulass 10654 ax-distr 10655 ax-i2m1 10656 ax-1ne0 10657 ax-1rid 10658 ax-rnegex 10659 ax-rrecex 10660 ax-cnre 10661 ax-pre-lttri 10662 ax-pre-lttrn 10663 ax-pre-ltadd 10664 ax-pre-mulgt0 10665 ax-pre-sup 10666 ax-addf 10667 ax-mulf 10668

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3699 df-csb 3808 df-dif 3863 df-un 3865 df-in 3867 df-ss 3877 df-pss 3879 df-nul 4228 df-if 4424 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4802 df-int 4842 df-iun 4888 df-iin 4889 df-br 5037 df-opab 5099 df-mpt 5117 df-tr 5143 df-id 5434 df-eprel 5439 df-po 5447 df-so 5448 df-fr 5487 df-se 5488 df-we 5489 df-xp 5534 df-rel 5535 df-cnv 5536 df-co 5537 df-dm 5538 df-rn 5539 df-res 5540 df-ima 5541 df-pred 6131 df-ord 6177 df-on 6178 df-lim 6179 df-suc 6180 df-iota 6299 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-isom 6349 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-of 7411 df-om 7586 df-1st 7699 df-2nd 7700 df-supp 7842 df-wrecs 7963 df-recs 8024 df-rdg 8062 df-1o 8118 df-2o 8119 df-er 8305 df-map 8424 df-ixp 8493 df-en 8541 df-dom 8542 df-sdom 8543 df-fin 8544 df-fsupp 8880 df-fi 8921 df-sup 8952 df-inf 8953 df-oi 9020 df-card 9414 df-pnf 10728 df-mnf 10729 df-xr 10730 df-ltxr 10731 df-le 10732 df-sub 10923 df-neg 10924 df-div 11349 df-nn 11688 df-2 11750 df-3 11751 df-4 11752 df-5 11753 df-6 11754 df-7 11755 df-8 11756 df-9 11757 df-n0 11948 df-z 12034 df-dec 12151 df-uz 12296 df-q 12402 df-rp 12444 df-xneg 12561 df-xadd 12562 df-xmul 12563 df-icc 12799 df-fz 12953 df-fzo 13096 df-seq 13432 df-exp 13493 df-hash 13754 df-cj 14519 df-re 14520 df-im 14521 df-sqrt 14655 df-abs 14656 df-struct 16556 df-ndx 16557 df-slot 16558 df-base 16560 df-sets 16561 df-ress 16562 df-plusg 16649 df-mulr 16650 df-starv 16651 df-sca 16652 df-vsca 16653 df-ip 16654 df-tset 16655 df-ple 16656 df-ds 16658 df-unif 16659 df-hom 16660 df-cco 16661 df-rest 16767 df-topn 16768 df-0g 16786 df-gsum 16787 df-topgen 16788 df-pt 16789 df-prds 16792 df-xrs 16846 df-qtop 16851 df-imas 16852 df-xps 16854 df-mre 16928 df-mrc 16929 df-acs 16931 df-mgm 17931 df-sgrp 17980 df-mnd 17991 df-submnd 18036 df-mulg 18305 df-cntz 18527 df-cmn 18988 df-psmet 20171 df-xmet 20172 df-met 20173 df-bl 20174 df-mopn 20175 df-cnfld 20180 df-top 21607 df-topon 21624 df-topsp 21646 df-bases 21659 df-cn 21940 df-cnp 21941 df-tx 22275 df-hmeo 22468 df-xms 23035 df-tms 23037 df-grpo 28388 df-gid 28389 df-ginv 28390 df-gdiv 28391 df-ablo 28440 df-vc 28454 df-nv 28487 df-va 28490 df-ba 28491 df-sm 28492 df-0v 28493 df-vs 28494 df-nmcv 28495 df-ims 28496

This theorem is referenced by: smcn 28593

W3C validator