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 30454

Description: Lemma for smcn 30455. (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 30376	. . 3 ⊢ (𝑈 ∈ NrmCVec → 𝑆:(ℂ × 𝑋)⟶𝑋)
5	1, 4	ax-mp 5	. 2 ⊢ 𝑆:(ℂ × 𝑋)⟶𝑋
6		smcn.t	. . . . . 6 ⊢ 𝑇 = (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
7		1rp 12981	. . . . . . . 8 ⊢ 1 ∈ ℝ⁺
8		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
9		smcn.n	. . . . . . . . . . . . 13 ⊢ 𝑁 = (norm_CV‘𝑈)
10	2, 9	nvcl 30418	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋) → (𝑁‘𝑦) ∈ ℝ)
11	1, 8, 10	sylancr 586	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑁‘𝑦) ∈ ℝ)
12		abscl 15228	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (abs‘𝑥) ∈ ℝ)
13	12	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (abs‘𝑥) ∈ ℝ)
14	11, 13	readdcld 11244	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → ((𝑁‘𝑦) + (abs‘𝑥)) ∈ ℝ)
15	2, 9	nvge0 30430	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝑁‘𝑦))
16	1, 8, 15	sylancr 586	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝑁‘𝑦))
17		absge0 15237	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → 0 ≤ (abs‘𝑥))
18	17	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 0 ≤ (abs‘𝑥))
19	11, 13, 16, 18	addge0d 11791	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 0 ≤ ((𝑁‘𝑦) + (abs‘𝑥)))
20	14, 19	ge0p1rpd 13049	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ⁺)
21		rpdivcl 13002	. . . . . . . . 9 ⊢ (((((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ⁺ ∧ 𝑟 ∈ ℝ⁺) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺)
22	20, 21	sylan 579	. . . . . . . 8 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺)
23		rpaddcl 12999	. . . . . . . 8 ⊢ ((1 ∈ ℝ⁺ ∧ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℝ⁺)
24	7, 22, 23	sylancr 586	. . . . . . 7 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℝ⁺)
25	24	rpreccld 13029	. . . . . 6 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) ∈ ℝ⁺)
26	6, 25	eqeltrid 2831	. . . . 5 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → 𝑇 ∈ ℝ⁺)
27		smcn.c	. . . . . . . . . . . 12 ⊢ 𝐶 = (IndMet‘𝑈)
28	2, 27	imsmet 30448	. . . . . . . . . . 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 772	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑥 ∈ ℂ)
33		simpllr 773	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑦 ∈ 𝑋)
34	2, 3	nvscl 30383	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑥𝑆𝑦) ∈ 𝑋)
35	31, 32, 33, 34	syl3anc 1368	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥𝑆𝑦) ∈ 𝑋)
36		simprll 776	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑧 ∈ ℂ)
37		simprlr 777	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑤 ∈ 𝑋)
38	2, 3	nvscl 30383	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) → (𝑧𝑆𝑤) ∈ 𝑋)
39	31, 36, 37, 38	syl3anc 1368	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧𝑆𝑤) ∈ 𝑋)
40		metcl 24188	. . . . . . . . 9 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ (𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
41	30, 35, 39, 40	syl3anc 1368	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
42	2, 3	nvscl 30383	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑧𝑆𝑦) ∈ 𝑋)
43	31, 36, 33, 42	syl3anc 1368	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧𝑆𝑦) ∈ 𝑋)
44		metcl 24188	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ (𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑦) ∈ 𝑋) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) ∈ ℝ)
45	30, 35, 43, 44	syl3anc 1368	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) ∈ ℝ)
46		metcl 24188	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ (𝑧𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
47	30, 43, 39, 46	syl3anc 1368	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
48	45, 47	readdcld 11244	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) ∈ ℝ)
49		rpre 12985	. . . . . . . . 9 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ)
50	49	ad2antlr 724	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑟 ∈ ℝ)
51		mettri 24208	. . . . . . . . 9 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ ((𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋 ∧ (𝑧𝑆𝑦) ∈ 𝑋)) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ≤ (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))))
52	30, 35, 39, 43, 51	syl13anc 1369	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ≤ (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))))
53	1, 33, 10	sylancr 586	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘𝑦) ∈ ℝ)
54	32	abscld 15386	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑥) ∈ ℝ)
55	53, 54	readdcld 11244	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑁‘𝑦) + (abs‘𝑥)) ∈ ℝ)
56		peano2re 11388	. . . . . . . . . . 11 ⊢ (((𝑁‘𝑦) + (abs‘𝑥)) ∈ ℝ → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ)
57	55, 56	syl 17	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ)
58	26	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ∈ ℝ⁺)
59	58	rpred 13019	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ∈ ℝ)
60	57, 59	remulcld 11245	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) ∈ ℝ)
61	32, 36	subcld 11572	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 − 𝑧) ∈ ℂ)
62	61	abscld 15386	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 − 𝑧)) ∈ ℝ)
63	62, 53	remulcld 11245	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) ∈ ℝ)
64	36	abscld 15386	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑧) ∈ ℝ)
65		eqid 2726	. . . . . . . . . . . . . . 15 ⊢ ( −_𝑣 ‘𝑈) = ( −_𝑣 ‘𝑈)
66	2, 65	nvmcl 30403	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋)
67	31, 33, 37, 66	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋)
68	2, 9	nvcl 30418	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) ∈ ℝ)
69	1, 67, 68	sylancr 586	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) ∈ ℝ)
70	64, 69	remulcld 11245	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))) ∈ ℝ)
71	53, 59	remulcld 11245	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑁‘𝑦) · 𝑇) ∈ ℝ)
72		peano2re 11388	. . . . . . . . . . . . 13 ⊢ ((abs‘𝑥) ∈ ℝ → ((abs‘𝑥) + 1) ∈ ℝ)
73	54, 72	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + 1) ∈ ℝ)
74	73, 59	remulcld 11245	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((abs‘𝑥) + 1) · 𝑇) ∈ ℝ)
75	1, 33, 15	sylancr 586	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 0 ≤ (𝑁‘𝑦))
76	32, 36	abssubd 15403	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 − 𝑧)) = (abs‘(𝑧 − 𝑥)))
77	36, 32	subcld 11572	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧 − 𝑥) ∈ ℂ)
78	77	abscld 15386	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) ∈ ℝ)
79		eqid 2726	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs ∘ − ) = (abs ∘ − )
80	79	cnmetdval 24637	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑥(abs ∘ − )𝑧) = (abs‘(𝑥 − 𝑧)))
81	32, 36, 80	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥(abs ∘ − )𝑧) = (abs‘(𝑥 − 𝑧)))
82	81, 76	eqtrd 2766	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥(abs ∘ − )𝑧) = (abs‘(𝑧 − 𝑥)))
83		simprrl 778	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥(abs ∘ − )𝑧) < 𝑇)
84	82, 83	eqbrtrrd 5165	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) < 𝑇)
85	78, 59, 84	ltled 11363	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) ≤ 𝑇)
86	76, 85	eqbrtrd 5163	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 − 𝑧)) ≤ 𝑇)
87	62, 59, 53, 75, 86	lemul1ad 12154	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) ≤ (𝑇 · (𝑁‘𝑦)))
88	58	rpcnd 13021	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ∈ ℂ)
89	53	recnd 11243	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘𝑦) ∈ ℂ)
90	88, 89	mulcomd 11236	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑇 · (𝑁‘𝑦)) = ((𝑁‘𝑦) · 𝑇))
91	87, 90	breqtrd 5167	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) ≤ ((𝑁‘𝑦) · 𝑇))
92	36	absge0d 15394	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 0 ≤ (abs‘𝑧))
93	2, 9	nvge0 30430	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋) → 0 ≤ (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
94	1, 67, 93	sylancr 586	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 0 ≤ (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
95	54, 78	readdcld 11244	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))) ∈ ℝ)
96	32, 36	pncan3d 11575	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + (𝑧 − 𝑥)) = 𝑧)
97	96	fveq2d 6888	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 + (𝑧 − 𝑥))) = (abs‘𝑧))
98	32, 77	abstrid 15406	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 + (𝑧 − 𝑥))) ≤ ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))))
99	97, 98	eqbrtrrd 5165	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑧) ≤ ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))))
100		1red 11216	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 1 ∈ ℝ)
101		1re 11215	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
102	22	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺)
103		ltaddrp 13014	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺) → 1 < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
104	101, 102, 103	sylancr 586	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 1 < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
105	24	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℝ⁺)
106	105	recgt1d 13033	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ↔ (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) < 1))
107	104, 106	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) < 1)
108	6, 107	eqbrtrid 5176	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 < 1)
109	59, 100, 108	ltled 11363	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ≤ 1)
110	78, 59, 100, 85, 109	letrd 11372	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) ≤ 1)
111	78, 100, 54, 110	leadd2dd 11830	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))) ≤ ((abs‘𝑥) + 1))
112	64, 95, 73, 99, 111	letrd 11372	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑧) ≤ ((abs‘𝑥) + 1))
113	2, 65, 9, 27	imsdval 30443	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑦𝐶𝑤) = (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
114	31, 33, 37, 113	syl3anc 1368	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑦𝐶𝑤) = (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
115		simprrr 779	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑦𝐶𝑤) < 𝑇)
116	114, 115	eqbrtrrd 5165	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) < 𝑇)
117	69, 59, 116	ltled 11363	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) ≤ 𝑇)
118	64, 73, 69, 59, 92, 94, 112, 117	lemul12ad 12157	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))) ≤ (((abs‘𝑥) + 1) · 𝑇))
119	63, 70, 71, 74, 91, 118	le2addd 11834	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) + ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))) ≤ (((𝑁‘𝑦) · 𝑇) + (((abs‘𝑥) + 1) · 𝑇)))
120		eqid 2726	. . . . . . . . . . . . . 14 ⊢ ( +_𝑣 ‘𝑈) = ( +_𝑣 ‘𝑈)
121	2, 120, 3, 9, 27	imsdval2 30444	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑦) ∈ 𝑋) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) = (𝑁‘((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦)))))
122	31, 35, 43, 121	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) = (𝑁‘((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦)))))
123		neg1cn 12327	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℂ
124		mulcl 11193	. . . . . . . . . . . . . . . 16 ⊢ ((-1 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (-1 · 𝑧) ∈ ℂ)
125	123, 36, 124	sylancr 586	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (-1 · 𝑧) ∈ ℂ)
126	2, 120, 3	nvdir 30388	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥 ∈ ℂ ∧ (-1 · 𝑧) ∈ ℂ ∧ 𝑦 ∈ 𝑋)) → ((𝑥 + (-1 · 𝑧))𝑆𝑦) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)((-1 · 𝑧)𝑆𝑦)))
127	31, 32, 125, 33, 126	syl13anc 1369	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥 + (-1 · 𝑧))𝑆𝑦) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)((-1 · 𝑧)𝑆𝑦)))
128	36	mulm1d 11667	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (-1 · 𝑧) = -𝑧)
129	128	oveq2d 7420	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + (-1 · 𝑧)) = (𝑥 + -𝑧))
130	32, 36	negsubd 11578	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + -𝑧) = (𝑥 − 𝑧))
131	129, 130	eqtrd 2766	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + (-1 · 𝑧)) = (𝑥 − 𝑧))
132	131	oveq1d 7419	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥 + (-1 · 𝑧))𝑆𝑦) = ((𝑥 − 𝑧)𝑆𝑦))
133	123	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → -1 ∈ ℂ)
134	2, 3	nvsass 30385	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ NrmCVec ∧ (-1 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋)) → ((-1 · 𝑧)𝑆𝑦) = (-1𝑆(𝑧𝑆𝑦)))
135	31, 133, 36, 33, 134	syl13anc 1369	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((-1 · 𝑧)𝑆𝑦) = (-1𝑆(𝑧𝑆𝑦)))
136	135	oveq2d 7420	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)((-1 · 𝑧)𝑆𝑦)) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦))))
137	127, 132, 136	3eqtr3d 2774	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥 − 𝑧)𝑆𝑦) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦))))
138	137	fveq2d 6888	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘((𝑥 − 𝑧)𝑆𝑦)) = (𝑁‘((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦)))))
139	2, 3, 9	nvs 30420	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥 − 𝑧) ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑁‘((𝑥 − 𝑧)𝑆𝑦)) = ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)))
140	31, 61, 33, 139	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘((𝑥 − 𝑧)𝑆𝑦)) = ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)))
141	122, 138, 140	3eqtr2d 2772	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) = ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)))
142	2, 65, 9, 27	imsdval 30443	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑧𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) = (𝑁‘((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤))))
143	31, 43, 39, 142	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) = (𝑁‘((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤))))
144	2, 65, 3	nvmdi 30405	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤)) = ((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤)))
145	31, 36, 33, 37, 144	syl13anc 1369	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤)) = ((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤)))
146	145	fveq2d 6888	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤))) = (𝑁‘((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤))))
147	2, 3, 9	nvs 30420	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋) → (𝑁‘(𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤))) = ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))))
148	31, 36, 67, 147	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤))) = ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))))
149	143, 146, 148	3eqtr2d 2772	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) = ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))))
150	141, 149	oveq12d 7422	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) = (((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) + ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))))
151	54	recnd 11243	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑥) ∈ ℂ)
152		1cnd 11210	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 1 ∈ ℂ)
153	89, 151, 152	addassd 11237	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) = ((𝑁‘𝑦) + ((abs‘𝑥) + 1)))
154	153	oveq1d 7419	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = (((𝑁‘𝑦) + ((abs‘𝑥) + 1)) · 𝑇))
155	73	recnd 11243	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + 1) ∈ ℂ)
156	89, 155, 88	adddird 11240	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + ((abs‘𝑥) + 1)) · 𝑇) = (((𝑁‘𝑦) · 𝑇) + (((abs‘𝑥) + 1) · 𝑇)))
157	154, 156	eqtrd 2766	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = (((𝑁‘𝑦) · 𝑇) + (((abs‘𝑥) + 1) · 𝑇)))
158	119, 150, 157	3brtr4d 5173	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) ≤ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇))
159	6	oveq2i 7415	. . . . . . . . . . 11 ⊢ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))))
160	57	recnd 11243	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℂ)
161	105	rpcnd 13021	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℂ)
162	105	rpne0d 13024	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ≠ 0)
163	160, 161, 162	divrecd 11994	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) = ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))))
164	159, 163	eqtr4id 2785	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))))
165		simplr 766	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑟 ∈ ℝ⁺)
166	102	rpred 13019	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ)
167	166	ltp1d 12145	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) < (((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) + 1))
168	102	rpcnd 13021	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℂ)
169	168, 152	addcomd 11417	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) + 1) = (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
170	167, 169	breqtrd 5167	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
171	57, 165, 105, 170	ltdiv23d 13086	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) < 𝑟)
172	164, 171	eqbrtrd 5163	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) < 𝑟)
173	48, 60, 50, 158, 172	lelttrd 11373	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) < 𝑟)
174	41, 48, 50, 52, 173	lelttrd 11373	. . . . . . 7 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)
175	174	expr 456	. . . . . 6 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋)) → (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
176	175	ralrimivva 3194	. . . . 5 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
177		breq2 5145	. . . . . . . . 9 ⊢ (𝑠 = 𝑇 → ((𝑥(abs ∘ − )𝑧) < 𝑠 ↔ (𝑥(abs ∘ − )𝑧) < 𝑇))
178		breq2 5145	. . . . . . . . 9 ⊢ (𝑠 = 𝑇 → ((𝑦𝐶𝑤) < 𝑠 ↔ (𝑦𝐶𝑤) < 𝑇))
179	177, 178	anbi12d 630	. . . . . . . 8 ⊢ (𝑠 = 𝑇 → (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) ↔ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇)))
180	179	imbi1d 341	. . . . . . 7 ⊢ (𝑠 = 𝑇 → ((((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟) ↔ (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)))
181	180	2ralbidv 3212	. . . . . 6 ⊢ (𝑠 = 𝑇 → (∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟) ↔ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)))
182	181	rspcev 3606	. . . . 5 ⊢ ((𝑇 ∈ ℝ⁺ ∧ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)) → ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
183	26, 176, 182	syl2anc 583	. . . 4 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
184	183	ralrimiva 3140	. . 3 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
185	184	rgen2 3191	. 2 ⊢ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)
186		cnxmet 24639	. . 3 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
187	2, 27	imsxmet 30449	. . . 4 ⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈ (∞Met‘𝑋))
188	1, 187	ax-mp 5	. . 3 ⊢ 𝐶 ∈ (∞Met‘𝑋)
189		smcn.k	. . . . 5 ⊢ 𝐾 = (TopOpen‘ℂ_fld)
190	189	cnfldtopn 24648	. . . 4 ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))
191		smcn.j	. . . 4 ⊢ 𝐽 = (MetOpen‘𝐶)
192	190, 191, 191	txmetcn 24407	. . 3 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ (∞Met‘𝑋) ∧ 𝐶 ∈ (∞Met‘𝑋)) → (𝑆 ∈ ((𝐾 ×_t 𝐽) Cn 𝐽) ↔ (𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))))
193	186, 188, 188, 192	mp3an 1457	. 2 ⊢ (𝑆 ∈ ((𝐾 ×_t 𝐽) Cn 𝐽) ↔ (𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)))
194	5, 185, 193	mpbir2an 708	1 ⊢ 𝑆 ∈ ((𝐾 ×_t 𝐽) Cn 𝐽)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1533 ∈ wcel 2098 ∀wral 3055 ∃wrex 3064 class class class wbr 5141 × cxp 5667 ∘ ccom 5673 ⟶wf 6532 ‘cfv 6536 (class class class)co 7404 ℂcc 11107 ℝcr 11108 0cc0 11109 1c1 11110 + caddc 11112 · cmul 11114 < clt 11249 ≤ cle 11250 − cmin 11445 -cneg 11446 / cdiv 11872 ℝ⁺crp 12977 abscabs 15184 TopOpenctopn 17373 ∞Metcxmet 21220 Metcmet 21221 MetOpencmopn 21225 ℂ_fldccnfld 21235 Cn ccn 23078 ×_t ctx 23414 NrmCVeccnv 30341 +_𝑣 cpv 30342 BaseSetcba 30343 ·_𝑠OLD cns 30344 −_𝑣 cnsb 30346 norm_CVcnmcv 30347 IndMetcims 30348

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2697 ax-rep 5278 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7721 ax-cnex 11165 ax-resscn 11166 ax-1cn 11167 ax-icn 11168 ax-addcl 11169 ax-addrcl 11170 ax-mulcl 11171 ax-mulrcl 11172 ax-mulcom 11173 ax-addass 11174 ax-mulass 11175 ax-distr 11176 ax-i2m1 11177 ax-1ne0 11178 ax-1rid 11179 ax-rnegex 11180 ax-rrecex 11181 ax-cnre 11182 ax-pre-lttri 11183 ax-pre-lttrn 11184 ax-pre-ltadd 11185 ax-pre-mulgt0 11186 ax-pre-sup 11187 ax-addf 11188 ax-mulf 11189

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-nfc 2879 df-ne 2935 df-nel 3041 df-ral 3056 df-rex 3065 df-rmo 3370 df-reu 3371 df-rab 3427 df-v 3470 df-sbc 3773 df-csb 3889 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-pss 3962 df-nul 4318 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-tp 4628 df-op 4630 df-uni 4903 df-int 4944 df-iun 4992 df-iin 4993 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5567 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-se 5625 df-we 5626 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-pred 6293 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6488 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7360 df-ov 7407 df-oprab 7408 df-mpo 7409 df-of 7666 df-om 7852 df-1st 7971 df-2nd 7972 df-supp 8144 df-frecs 8264 df-wrecs 8295 df-recs 8369 df-rdg 8408 df-1o 8464 df-2o 8465 df-er 8702 df-map 8821 df-ixp 8891 df-en 8939 df-dom 8940 df-sdom 8941 df-fin 8942 df-fsupp 9361 df-fi 9405 df-sup 9436 df-inf 9437 df-oi 9504 df-card 9933 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11447 df-neg 11448 df-div 11873 df-nn 12214 df-2 12276 df-3 12277 df-4 12278 df-5 12279 df-6 12280 df-7 12281 df-8 12282 df-9 12283 df-n0 12474 df-z 12560 df-dec 12679 df-uz 12824 df-q 12934 df-rp 12978 df-xneg 13095 df-xadd 13096 df-xmul 13097 df-icc 13334 df-fz 13488 df-fzo 13631 df-seq 13970 df-exp 14030 df-hash 14293 df-cj 15049 df-re 15050 df-im 15051 df-sqrt 15185 df-abs 15186 df-struct 17086 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17151 df-ress 17180 df-plusg 17216 df-mulr 17217 df-starv 17218 df-sca 17219 df-vsca 17220 df-ip 17221 df-tset 17222 df-ple 17223 df-ds 17225 df-unif 17226 df-hom 17227 df-cco 17228 df-rest 17374 df-topn 17375 df-0g 17393 df-gsum 17394 df-topgen 17395 df-pt 17396 df-prds 17399 df-xrs 17454 df-qtop 17459 df-imas 17460 df-xps 17462 df-mre 17536 df-mrc 17537 df-acs 17539 df-mgm 18570 df-sgrp 18649 df-mnd 18665 df-submnd 18711 df-mulg 18993 df-cntz 19230 df-cmn 19699 df-psmet 21227 df-xmet 21228 df-met 21229 df-bl 21230 df-mopn 21231 df-cnfld 21236 df-top 22746 df-topon 22763 df-topsp 22785 df-bases 22799 df-cn 23081 df-cnp 23082 df-tx 23416 df-hmeo 23609 df-xms 24176 df-tms 24178 df-grpo 30250 df-gid 30251 df-ginv 30252 df-gdiv 30253 df-ablo 30302 df-vc 30316 df-nv 30349 df-va 30352 df-ba 30353 df-sm 30354 df-0v 30355 df-vs 30356 df-nmcv 30357 df-ims 30358

This theorem is referenced by: smcn 30455

W3C validator