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 30772

Description: Lemma for smcn 30773. (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 30694	. . 3 ⊢ (𝑈 ∈ NrmCVec → 𝑆:(ℂ × 𝑋)⟶𝑋)
5	1, 4	ax-mp 5	. 2 ⊢ 𝑆:(ℂ × 𝑋)⟶𝑋
6		smcn.t	. . . . . 6 ⊢ 𝑇 = (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
7		1rp 12909	. . . . . . . 8 ⊢ 1 ∈ ℝ⁺
8		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
9		smcn.n	. . . . . . . . . . . . 13 ⊢ 𝑁 = (norm_CV‘𝑈)
10	2, 9	nvcl 30736	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋) → (𝑁‘𝑦) ∈ ℝ)
11	1, 8, 10	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑁‘𝑦) ∈ ℝ)
12		abscl 15201	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (abs‘𝑥) ∈ ℝ)
13	12	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (abs‘𝑥) ∈ ℝ)
14	11, 13	readdcld 11161	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → ((𝑁‘𝑦) + (abs‘𝑥)) ∈ ℝ)
15	2, 9	nvge0 30748	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝑁‘𝑦))
16	1, 8, 15	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝑁‘𝑦))
17		absge0 15210	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → 0 ≤ (abs‘𝑥))
18	17	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 0 ≤ (abs‘𝑥))
19	11, 13, 16, 18	addge0d 11713	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 0 ≤ ((𝑁‘𝑦) + (abs‘𝑥)))
20	14, 19	ge0p1rpd 12979	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ⁺)
21		rpdivcl 12932	. . . . . . . . 9 ⊢ (((((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ⁺ ∧ 𝑟 ∈ ℝ⁺) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺)
22	20, 21	sylan 580	. . . . . . . 8 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺)
23		rpaddcl 12929	. . . . . . . 8 ⊢ ((1 ∈ ℝ⁺ ∧ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℝ⁺)
24	7, 22, 23	sylancr 587	. . . . . . 7 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℝ⁺)
25	24	rpreccld 12959	. . . . . 6 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) ∈ ℝ⁺)
26	6, 25	eqeltrid 2840	. . . . 5 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → 𝑇 ∈ ℝ⁺)
27		smcn.c	. . . . . . . . . . . 12 ⊢ 𝐶 = (IndMet‘𝑈)
28	2, 27	imsmet 30766	. . . . . . . . . . 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 30701	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑥𝑆𝑦) ∈ 𝑋)
35	31, 32, 33, 34	syl3anc 1373	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥𝑆𝑦) ∈ 𝑋)
36		simprll 778	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑧 ∈ ℂ)
37		simprlr 779	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑤 ∈ 𝑋)
38	2, 3	nvscl 30701	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) → (𝑧𝑆𝑤) ∈ 𝑋)
39	31, 36, 37, 38	syl3anc 1373	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧𝑆𝑤) ∈ 𝑋)
40		metcl 24276	. . . . . . . . 9 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ (𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
41	30, 35, 39, 40	syl3anc 1373	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
42	2, 3	nvscl 30701	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑧𝑆𝑦) ∈ 𝑋)
43	31, 36, 33, 42	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧𝑆𝑦) ∈ 𝑋)
44		metcl 24276	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ (𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑦) ∈ 𝑋) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) ∈ ℝ)
45	30, 35, 43, 44	syl3anc 1373	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) ∈ ℝ)
46		metcl 24276	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ (𝑧𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
47	30, 43, 39, 46	syl3anc 1373	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
48	45, 47	readdcld 11161	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) ∈ ℝ)
49		rpre 12914	. . . . . . . . 9 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ)
50	49	ad2antlr 727	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑟 ∈ ℝ)
51		mettri 24296	. . . . . . . . 9 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ ((𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋 ∧ (𝑧𝑆𝑦) ∈ 𝑋)) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ≤ (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))))
52	30, 35, 39, 43, 51	syl13anc 1374	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ≤ (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))))
53	1, 33, 10	sylancr 587	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘𝑦) ∈ ℝ)
54	32	abscld 15362	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑥) ∈ ℝ)
55	53, 54	readdcld 11161	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑁‘𝑦) + (abs‘𝑥)) ∈ ℝ)
56		peano2re 11306	. . . . . . . . . . 11 ⊢ (((𝑁‘𝑦) + (abs‘𝑥)) ∈ ℝ → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ)
57	55, 56	syl 17	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ)
58	26	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ∈ ℝ⁺)
59	58	rpred 12949	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ∈ ℝ)
60	57, 59	remulcld 11162	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) ∈ ℝ)
61	32, 36	subcld 11492	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 − 𝑧) ∈ ℂ)
62	61	abscld 15362	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 − 𝑧)) ∈ ℝ)
63	62, 53	remulcld 11162	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) ∈ ℝ)
64	36	abscld 15362	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑧) ∈ ℝ)
65		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ ( −_𝑣 ‘𝑈) = ( −_𝑣 ‘𝑈)
66	2, 65	nvmcl 30721	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋)
67	31, 33, 37, 66	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋)
68	2, 9	nvcl 30736	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) ∈ ℝ)
69	1, 67, 68	sylancr 587	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) ∈ ℝ)
70	64, 69	remulcld 11162	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))) ∈ ℝ)
71	53, 59	remulcld 11162	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑁‘𝑦) · 𝑇) ∈ ℝ)
72		peano2re 11306	. . . . . . . . . . . . 13 ⊢ ((abs‘𝑥) ∈ ℝ → ((abs‘𝑥) + 1) ∈ ℝ)
73	54, 72	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + 1) ∈ ℝ)
74	73, 59	remulcld 11162	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((abs‘𝑥) + 1) · 𝑇) ∈ ℝ)
75	1, 33, 15	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 0 ≤ (𝑁‘𝑦))
76	32, 36	abssubd 15379	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 − 𝑧)) = (abs‘(𝑧 − 𝑥)))
77	36, 32	subcld 11492	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧 − 𝑥) ∈ ℂ)
78	77	abscld 15362	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) ∈ ℝ)
79		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs ∘ − ) = (abs ∘ − )
80	79	cnmetdval 24714	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑥(abs ∘ − )𝑧) = (abs‘(𝑥 − 𝑧)))
81	32, 36, 80	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥(abs ∘ − )𝑧) = (abs‘(𝑥 − 𝑧)))
82	81, 76	eqtrd 2771	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥(abs ∘ − )𝑧) = (abs‘(𝑧 − 𝑥)))
83		simprrl 780	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥(abs ∘ − )𝑧) < 𝑇)
84	82, 83	eqbrtrrd 5122	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) < 𝑇)
85	78, 59, 84	ltled 11281	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) ≤ 𝑇)
86	76, 85	eqbrtrd 5120	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 − 𝑧)) ≤ 𝑇)
87	62, 59, 53, 75, 86	lemul1ad 12081	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) ≤ (𝑇 · (𝑁‘𝑦)))
88	58	rpcnd 12951	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ∈ ℂ)
89	53	recnd 11160	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘𝑦) ∈ ℂ)
90	88, 89	mulcomd 11153	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑇 · (𝑁‘𝑦)) = ((𝑁‘𝑦) · 𝑇))
91	87, 90	breqtrd 5124	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) ≤ ((𝑁‘𝑦) · 𝑇))
92	36	absge0d 15370	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 0 ≤ (abs‘𝑧))
93	2, 9	nvge0 30748	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋) → 0 ≤ (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
94	1, 67, 93	sylancr 587	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 0 ≤ (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
95	54, 78	readdcld 11161	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))) ∈ ℝ)
96	32, 36	pncan3d 11495	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + (𝑧 − 𝑥)) = 𝑧)
97	96	fveq2d 6838	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 + (𝑧 − 𝑥))) = (abs‘𝑧))
98	32, 77	abstrid 15382	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 + (𝑧 − 𝑥))) ≤ ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))))
99	97, 98	eqbrtrrd 5122	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑧) ≤ ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))))
100		1red 11133	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 1 ∈ ℝ)
101		1re 11132	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
102	22	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺)
103		ltaddrp 12944	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺) → 1 < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
104	101, 102, 103	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 1 < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
105	24	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℝ⁺)
106	105	recgt1d 12963	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ↔ (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) < 1))
107	104, 106	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) < 1)
108	6, 107	eqbrtrid 5133	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 < 1)
109	59, 100, 108	ltled 11281	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ≤ 1)
110	78, 59, 100, 85, 109	letrd 11290	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) ≤ 1)
111	78, 100, 54, 110	leadd2dd 11752	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))) ≤ ((abs‘𝑥) + 1))
112	64, 95, 73, 99, 111	letrd 11290	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑧) ≤ ((abs‘𝑥) + 1))
113	2, 65, 9, 27	imsdval 30761	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑦𝐶𝑤) = (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
114	31, 33, 37, 113	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑦𝐶𝑤) = (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
115		simprrr 781	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑦𝐶𝑤) < 𝑇)
116	114, 115	eqbrtrrd 5122	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) < 𝑇)
117	69, 59, 116	ltled 11281	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) ≤ 𝑇)
118	64, 73, 69, 59, 92, 94, 112, 117	lemul12ad 12084	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))) ≤ (((abs‘𝑥) + 1) · 𝑇))
119	63, 70, 71, 74, 91, 118	le2addd 11756	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) + ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))) ≤ (((𝑁‘𝑦) · 𝑇) + (((abs‘𝑥) + 1) · 𝑇)))
120		eqid 2736	. . . . . . . . . . . . . 14 ⊢ ( +_𝑣 ‘𝑈) = ( +_𝑣 ‘𝑈)
121	2, 120, 3, 9, 27	imsdval2 30762	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑦) ∈ 𝑋) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) = (𝑁‘((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦)))))
122	31, 35, 43, 121	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) = (𝑁‘((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦)))))
123		neg1cn 12130	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℂ
124		mulcl 11110	. . . . . . . . . . . . . . . 16 ⊢ ((-1 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (-1 · 𝑧) ∈ ℂ)
125	123, 36, 124	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (-1 · 𝑧) ∈ ℂ)
126	2, 120, 3	nvdir 30706	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥 ∈ ℂ ∧ (-1 · 𝑧) ∈ ℂ ∧ 𝑦 ∈ 𝑋)) → ((𝑥 + (-1 · 𝑧))𝑆𝑦) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)((-1 · 𝑧)𝑆𝑦)))
127	31, 32, 125, 33, 126	syl13anc 1374	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥 + (-1 · 𝑧))𝑆𝑦) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)((-1 · 𝑧)𝑆𝑦)))
128	36	mulm1d 11589	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (-1 · 𝑧) = -𝑧)
129	128	oveq2d 7374	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + (-1 · 𝑧)) = (𝑥 + -𝑧))
130	32, 36	negsubd 11498	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + -𝑧) = (𝑥 − 𝑧))
131	129, 130	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + (-1 · 𝑧)) = (𝑥 − 𝑧))
132	131	oveq1d 7373	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥 + (-1 · 𝑧))𝑆𝑦) = ((𝑥 − 𝑧)𝑆𝑦))
133	123	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → -1 ∈ ℂ)
134	2, 3	nvsass 30703	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ NrmCVec ∧ (-1 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋)) → ((-1 · 𝑧)𝑆𝑦) = (-1𝑆(𝑧𝑆𝑦)))
135	31, 133, 36, 33, 134	syl13anc 1374	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((-1 · 𝑧)𝑆𝑦) = (-1𝑆(𝑧𝑆𝑦)))
136	135	oveq2d 7374	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)((-1 · 𝑧)𝑆𝑦)) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦))))
137	127, 132, 136	3eqtr3d 2779	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥 − 𝑧)𝑆𝑦) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦))))
138	137	fveq2d 6838	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘((𝑥 − 𝑧)𝑆𝑦)) = (𝑁‘((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦)))))
139	2, 3, 9	nvs 30738	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥 − 𝑧) ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑁‘((𝑥 − 𝑧)𝑆𝑦)) = ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)))
140	31, 61, 33, 139	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘((𝑥 − 𝑧)𝑆𝑦)) = ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)))
141	122, 138, 140	3eqtr2d 2777	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) = ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)))
142	2, 65, 9, 27	imsdval 30761	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑧𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) = (𝑁‘((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤))))
143	31, 43, 39, 142	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) = (𝑁‘((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤))))
144	2, 65, 3	nvmdi 30723	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤)) = ((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤)))
145	31, 36, 33, 37, 144	syl13anc 1374	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤)) = ((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤)))
146	145	fveq2d 6838	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤))) = (𝑁‘((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤))))
147	2, 3, 9	nvs 30738	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋) → (𝑁‘(𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤))) = ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))))
148	31, 36, 67, 147	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤))) = ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))))
149	143, 146, 148	3eqtr2d 2777	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) = ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))))
150	141, 149	oveq12d 7376	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) = (((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) + ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))))
151	54	recnd 11160	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑥) ∈ ℂ)
152		1cnd 11127	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 1 ∈ ℂ)
153	89, 151, 152	addassd 11154	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) = ((𝑁‘𝑦) + ((abs‘𝑥) + 1)))
154	153	oveq1d 7373	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = (((𝑁‘𝑦) + ((abs‘𝑥) + 1)) · 𝑇))
155	73	recnd 11160	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + 1) ∈ ℂ)
156	89, 155, 88	adddird 11157	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + ((abs‘𝑥) + 1)) · 𝑇) = (((𝑁‘𝑦) · 𝑇) + (((abs‘𝑥) + 1) · 𝑇)))
157	154, 156	eqtrd 2771	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = (((𝑁‘𝑦) · 𝑇) + (((abs‘𝑥) + 1) · 𝑇)))
158	119, 150, 157	3brtr4d 5130	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) ≤ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇))
159	6	oveq2i 7369	. . . . . . . . . . 11 ⊢ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))))
160	57	recnd 11160	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℂ)
161	105	rpcnd 12951	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℂ)
162	105	rpne0d 12954	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ≠ 0)
163	160, 161, 162	divrecd 11920	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) = ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))))
164	159, 163	eqtr4id 2790	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))))
165		simplr 768	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑟 ∈ ℝ⁺)
166	102	rpred 12949	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ)
167	166	ltp1d 12072	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) < (((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) + 1))
168	102	rpcnd 12951	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℂ)
169	168, 152	addcomd 11335	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) + 1) = (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
170	167, 169	breqtrd 5124	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
171	57, 165, 105, 170	ltdiv23d 13016	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) < 𝑟)
172	164, 171	eqbrtrd 5120	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) < 𝑟)
173	48, 60, 50, 158, 172	lelttrd 11291	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) < 𝑟)
174	41, 48, 50, 52, 173	lelttrd 11291	. . . . . . 7 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)
175	174	expr 456	. . . . . 6 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋)) → (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
176	175	ralrimivva 3179	. . . . 5 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
177		breq2 5102	. . . . . . . . 9 ⊢ (𝑠 = 𝑇 → ((𝑥(abs ∘ − )𝑧) < 𝑠 ↔ (𝑥(abs ∘ − )𝑧) < 𝑇))
178		breq2 5102	. . . . . . . . 9 ⊢ (𝑠 = 𝑇 → ((𝑦𝐶𝑤) < 𝑠 ↔ (𝑦𝐶𝑤) < 𝑇))
179	177, 178	anbi12d 632	. . . . . . . 8 ⊢ (𝑠 = 𝑇 → (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) ↔ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇)))
180	179	imbi1d 341	. . . . . . 7 ⊢ (𝑠 = 𝑇 → ((((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟) ↔ (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)))
181	180	2ralbidv 3200	. . . . . 6 ⊢ (𝑠 = 𝑇 → (∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟) ↔ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)))
182	181	rspcev 3576	. . . . 5 ⊢ ((𝑇 ∈ ℝ⁺ ∧ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)) → ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
183	26, 176, 182	syl2anc 584	. . . 4 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
184	183	ralrimiva 3128	. . 3 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
185	184	rgen2 3176	. 2 ⊢ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)
186		cnxmet 24716	. . 3 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
187	2, 27	imsxmet 30767	. . . 4 ⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈ (∞Met‘𝑋))
188	1, 187	ax-mp 5	. . 3 ⊢ 𝐶 ∈ (∞Met‘𝑋)
189		smcn.k	. . . . 5 ⊢ 𝐾 = (TopOpen‘ℂ_fld)
190	189	cnfldtopn 24725	. . . 4 ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))
191		smcn.j	. . . 4 ⊢ 𝐽 = (MetOpen‘𝐶)
192	190, 191, 191	txmetcn 24492	. . 3 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ (∞Met‘𝑋) ∧ 𝐶 ∈ (∞Met‘𝑋)) → (𝑆 ∈ ((𝐾 ×_t 𝐽) Cn 𝐽) ↔ (𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))))
193	186, 188, 188, 192	mp3an 1463	. 2 ⊢ (𝑆 ∈ ((𝐾 ×_t 𝐽) Cn 𝐽) ↔ (𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)))
194	5, 185, 193	mpbir2an 711	1 ⊢ 𝑆 ∈ ((𝐾 ×_t 𝐽) Cn 𝐽)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2113 ∀wral 3051 ∃wrex 3060 class class class wbr 5098 × cxp 5622 ∘ ccom 5628 ⟶wf 6488 ‘cfv 6492 (class class class)co 7358 ℂcc 11024 ℝcr 11025 0cc0 11026 1c1 11027 + caddc 11029 · cmul 11031 < clt 11166 ≤ cle 11167 − cmin 11364 -cneg 11365 / cdiv 11794 ℝ⁺crp 12905 abscabs 15157 TopOpenctopn 17341 ∞Metcxmet 21294 Metcmet 21295 MetOpencmopn 21299 ℂ_fldccnfld 21309 Cn ccn 23168 ×_t ctx 23504 NrmCVeccnv 30659 +_𝑣 cpv 30660 BaseSetcba 30661 ·_𝑠OLD cns 30662 −_𝑣 cnsb 30664 norm_CVcnmcv 30665 IndMetcims 30666

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 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103 ax-pre-sup 11104 ax-addf 11105 ax-mulf 11106

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 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-tp 4585 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-iin 4949 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-se 5578 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-of 7622 df-om 7809 df-1st 7933 df-2nd 7934 df-supp 8103 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-2o 8398 df-er 8635 df-map 8765 df-ixp 8836 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fsupp 9265 df-fi 9314 df-sup 9345 df-inf 9346 df-oi 9415 df-card 9851 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-div 11795 df-nn 12146 df-2 12208 df-3 12209 df-4 12210 df-5 12211 df-6 12212 df-7 12213 df-8 12214 df-9 12215 df-n0 12402 df-z 12489 df-dec 12608 df-uz 12752 df-q 12862 df-rp 12906 df-xneg 13026 df-xadd 13027 df-xmul 13028 df-icc 13268 df-fz 13424 df-fzo 13571 df-seq 13925 df-exp 13985 df-hash 14254 df-cj 15022 df-re 15023 df-im 15024 df-sqrt 15158 df-abs 15159 df-struct 17074 df-sets 17091 df-slot 17109 df-ndx 17121 df-base 17137 df-ress 17158 df-plusg 17190 df-mulr 17191 df-starv 17192 df-sca 17193 df-vsca 17194 df-ip 17195 df-tset 17196 df-ple 17197 df-ds 17199 df-unif 17200 df-hom 17201 df-cco 17202 df-rest 17342 df-topn 17343 df-0g 17361 df-gsum 17362 df-topgen 17363 df-pt 17364 df-prds 17367 df-xrs 17423 df-qtop 17428 df-imas 17429 df-xps 17431 df-mre 17505 df-mrc 17506 df-acs 17508 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-submnd 18709 df-mulg 18998 df-cntz 19246 df-cmn 19711 df-psmet 21301 df-xmet 21302 df-met 21303 df-bl 21304 df-mopn 21305 df-cnfld 21310 df-top 22838 df-topon 22855 df-topsp 22877 df-bases 22890 df-cn 23171 df-cnp 23172 df-tx 23506 df-hmeo 23699 df-xms 24264 df-tms 24266 df-grpo 30568 df-gid 30569 df-ginv 30570 df-gdiv 30571 df-ablo 30620 df-vc 30634 df-nv 30667 df-va 30670 df-ba 30671 df-sm 30672 df-0v 30673 df-vs 30674 df-nmcv 30675 df-ims 30676

This theorem is referenced by: smcn 30773

W3C validator