Metamath Proof Explorer

Theorem smcnlem

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

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

Proof

Step Hyp Ref Expression
1 smcn.c ⊢ 𝐶 = ( IndMet ‘ 𝑈 )
2 smcn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
3 smcn.s ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
4 smcn.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
5 smcn.x ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
6 smcn.n ⊢ 𝑁 = ( normCV ‘ 𝑈 )
7 smcn.u ⊢ 𝑈 ∈ NrmCVec
8 smcn.t ⊢ 𝑇 = ( 1 / ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) )
9 5 3 nvsf ⊢ ( 𝑈 ∈ NrmCVec → 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 )
10 7 9 ax-mp ⊢ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋
11 1rp ⊢ 1 ∈ ℝ+
12 simpr ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ 𝑋 )
13 5 6 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑦 ) ∈ ℝ )
14 7 12 13 sylancr ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑦 ) ∈ ℝ )
15 abscl ⊢ ( 𝑥 ∈ ℂ → ( abs ‘ 𝑥 ) ∈ ℝ )
16 15 adantr ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → ( abs ‘ 𝑥 ) ∈ ℝ )
17 14 16 readdcld ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) ∈ ℝ )
18 5 6 nvge0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ 𝑦 ) )
19 7 12 18 sylancr ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ 𝑦 ) )
20 absge0 ⊢ ( 𝑥 ∈ ℂ → 0 ≤ ( abs ‘ 𝑥 ) )
21 20 adantr ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → 0 ≤ ( abs ‘ 𝑥 ) )
22 14 16 19 21 addge0d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → 0 ≤ ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) )
23 17 22 ge0p1rpd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) ∈ ℝ+ )
24 rpdivcl ⊢ ( ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) ∈ ℝ+ ∧ 𝑟 ∈ ℝ+ ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ∈ ℝ+ )
25 23 24 sylan ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ∈ ℝ+ )
26 rpaddcl ⊢ ( ( 1 ∈ ℝ+ ∧ ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ∈ ℝ+ ) → ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ∈ ℝ+ )
27 11 25 26 sylancr ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ∈ ℝ+ )
28 27 rpreccld ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( 1 / ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) ∈ ℝ+ )
29 8 28 eqeltrid ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → 𝑇 ∈ ℝ+ )
30 5 1 imsmet ⊢ ( 𝑈 ∈ NrmCVec → 𝐶 ∈ ( Met ‘ 𝑋 ) )
31 7 30 ax-mp ⊢ 𝐶 ∈ ( Met ‘ 𝑋 )
32 31 a1i ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝐶 ∈ ( Met ‘ 𝑋 ) )
33 7 a1i ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑈 ∈ NrmCVec )
34 simplll ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑥 ∈ ℂ )
35 simpllr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑦 ∈ 𝑋 )
36 5 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑆 𝑦 ) ∈ 𝑋 )
37 33 34 35 36 syl3anc ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑥 𝑆 𝑦 ) ∈ 𝑋 )
38 simprll ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑧 ∈ ℂ )
39 simprlr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑤 ∈ 𝑋 )
40 5 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) → ( 𝑧 𝑆 𝑤 ) ∈ 𝑋 )
41 33 38 39 40 syl3anc ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑧 𝑆 𝑤 ) ∈ 𝑋 )
42 metcl ⊢ ( ( 𝐶 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 𝑆 𝑦 ) ∈ 𝑋 ∧ ( 𝑧 𝑆 𝑤 ) ∈ 𝑋 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ∈ ℝ )
43 32 37 41 42 syl3anc ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ∈ ℝ )
44 5 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → ( 𝑧 𝑆 𝑦 ) ∈ 𝑋 )
45 33 38 35 44 syl3anc ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑧 𝑆 𝑦 ) ∈ 𝑋 )
46 metcl ⊢ ( ( 𝐶 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 𝑆 𝑦 ) ∈ 𝑋 ∧ ( 𝑧 𝑆 𝑦 ) ∈ 𝑋 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) ∈ ℝ )
47 32 37 45 46 syl3anc ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) ∈ ℝ )
48 metcl ⊢ ( ( 𝐶 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑧 𝑆 𝑦 ) ∈ 𝑋 ∧ ( 𝑧 𝑆 𝑤 ) ∈ 𝑋 ) → ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ∈ ℝ )
49 32 45 41 48 syl3anc ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ∈ ℝ )
50 47 49 readdcld ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) + ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ) ∈ ℝ )
51 rpre ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ )
52 51 ad2antlr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑟 ∈ ℝ )
53 mettri ⊢ ( ( 𝐶 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑥 𝑆 𝑦 ) ∈ 𝑋 ∧ ( 𝑧 𝑆 𝑤 ) ∈ 𝑋 ∧ ( 𝑧 𝑆 𝑦 ) ∈ 𝑋 ) ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ≤ ( ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) + ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ) )
54 32 37 41 45 53 syl13anc ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ≤ ( ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) + ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ) )
55 7 35 13 sylancr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑁 ‘ 𝑦 ) ∈ ℝ )
56 34 abscld ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ 𝑥 ) ∈ ℝ )
57 55 56 readdcld ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) ∈ ℝ )
58 peano2re ⊢ ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) ∈ ℝ → ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) ∈ ℝ )
59 57 58 syl ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) ∈ ℝ )
60 29 adantr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑇 ∈ ℝ+ )
61 60 rpred ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑇 ∈ ℝ )
62 59 61 remulcld ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) · 𝑇 ) ∈ ℝ )
63 34 38 subcld ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑥 − 𝑧 ) ∈ ℂ )
64 63 abscld ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ ( 𝑥 − 𝑧 ) ) ∈ ℝ )
65 64 55 remulcld ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( abs ‘ ( 𝑥 − 𝑧 ) ) · ( 𝑁 ‘ 𝑦 ) ) ∈ ℝ )
66 38 abscld ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ 𝑧 ) ∈ ℝ )
67 eqid ⊢ ( −𝑣 ‘ 𝑈 ) = ( −𝑣 ‘ 𝑈 )
68 5 67 nvmcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 )
69 33 35 39 68 syl3anc ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 )
70 5 6 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ∈ ℝ )
71 7 69 70 sylancr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ∈ ℝ )
72 66 71 remulcld ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( abs ‘ 𝑧 ) · ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) ∈ ℝ )
73 55 61 remulcld ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑁 ‘ 𝑦 ) · 𝑇 ) ∈ ℝ )
74 peano2re ⊢ ( ( abs ‘ 𝑥 ) ∈ ℝ → ( ( abs ‘ 𝑥 ) + 1 ) ∈ ℝ )
75 56 74 syl ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( abs ‘ 𝑥 ) + 1 ) ∈ ℝ )
76 75 61 remulcld ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( abs ‘ 𝑥 ) + 1 ) · 𝑇 ) ∈ ℝ )
77 7 35 18 sylancr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 0 ≤ ( 𝑁 ‘ 𝑦 ) )
78 34 38 abssubd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ ( 𝑥 − 𝑧 ) ) = ( abs ‘ ( 𝑧 − 𝑥 ) ) )
79 38 34 subcld ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑧 − 𝑥 ) ∈ ℂ )
80 79 abscld ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ ( 𝑧 − 𝑥 ) ) ∈ ℝ )
81 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
82 81 cnmetdval ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 ( abs ∘ − ) 𝑧 ) = ( abs ‘ ( 𝑥 − 𝑧 ) ) )
83 34 38 82 syl2anc ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑥 ( abs ∘ − ) 𝑧 ) = ( abs ‘ ( 𝑥 − 𝑧 ) ) )
84 83 78 eqtrd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑥 ( abs ∘ − ) 𝑧 ) = ( abs ‘ ( 𝑧 − 𝑥 ) ) )
85 simprrl ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 )
86 84 85 eqbrtrrd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ ( 𝑧 − 𝑥 ) ) < 𝑇 )
87 80 61 86 ltled ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ ( 𝑧 − 𝑥 ) ) ≤ 𝑇 )
88 78 87 eqbrtrd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ ( 𝑥 − 𝑧 ) ) ≤ 𝑇 )
89 64 61 55 77 88 lemul1ad ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( abs ‘ ( 𝑥 − 𝑧 ) ) · ( 𝑁 ‘ 𝑦 ) ) ≤ ( 𝑇 · ( 𝑁 ‘ 𝑦 ) ) )
90 60 rpcnd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑇 ∈ ℂ )
91 55 recnd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑁 ‘ 𝑦 ) ∈ ℂ )
92 90 91 mulcomd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑇 · ( 𝑁 ‘ 𝑦 ) ) = ( ( 𝑁 ‘ 𝑦 ) · 𝑇 ) )
93 89 92 breqtrd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( abs ‘ ( 𝑥 − 𝑧 ) ) · ( 𝑁 ‘ 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑦 ) · 𝑇 ) )
94 38 absge0d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 0 ≤ ( abs ‘ 𝑧 ) )
95 5 6 nvge0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) )
96 7 69 95 sylancr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 0 ≤ ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) )
97 56 80 readdcld ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( abs ‘ 𝑥 ) + ( abs ‘ ( 𝑧 − 𝑥 ) ) ) ∈ ℝ )
98 34 38 pncan3d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑥 + ( 𝑧 − 𝑥 ) ) = 𝑧 )
99 98 fveq2d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ ( 𝑥 + ( 𝑧 − 𝑥 ) ) ) = ( abs ‘ 𝑧 ) )
100 34 79 abstrid ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ ( 𝑥 + ( 𝑧 − 𝑥 ) ) ) ≤ ( ( abs ‘ 𝑥 ) + ( abs ‘ ( 𝑧 − 𝑥 ) ) ) )
101 99 100 eqbrtrrd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ 𝑧 ) ≤ ( ( abs ‘ 𝑥 ) + ( abs ‘ ( 𝑧 − 𝑥 ) ) ) )
102 1red ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 1 ∈ ℝ )
103 1re ⊢ 1 ∈ ℝ
104 25 adantr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ∈ ℝ+ )
105 ltaddrp ⊢ ( ( 1 ∈ ℝ ∧ ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ∈ ℝ+ ) → 1 < ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) )
106 103 104 105 sylancr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 1 < ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) )
107 27 adantr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ∈ ℝ+ )
108 107 recgt1d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 1 < ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ↔ ( 1 / ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) < 1 ) )
109 106 108 mpbid ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 1 / ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) < 1 )
110 8 109 eqbrtrid ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑇 < 1 )
111 61 102 110 ltled ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑇 ≤ 1 )
112 80 61 102 87 111 letrd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ ( 𝑧 − 𝑥 ) ) ≤ 1 )
113 80 102 56 112 leadd2dd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( abs ‘ 𝑥 ) + ( abs ‘ ( 𝑧 − 𝑥 ) ) ) ≤ ( ( abs ‘ 𝑥 ) + 1 ) )
114 66 97 75 101 113 letrd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ 𝑧 ) ≤ ( ( abs ‘ 𝑥 ) + 1 ) )
115 5 67 6 1 imsdval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑦 𝐶 𝑤 ) = ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) )
116 33 35 39 115 syl3anc ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑦 𝐶 𝑤 ) = ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) )
117 simprrr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑦 𝐶 𝑤 ) < 𝑇 )
118 116 117 eqbrtrrd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) < 𝑇 )
119 71 61 118 ltled ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ≤ 𝑇 )
120 66 75 71 61 94 96 114 119 lemul12ad ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( abs ‘ 𝑧 ) · ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) ≤ ( ( ( abs ‘ 𝑥 ) + 1 ) · 𝑇 ) )
121 65 72 73 76 93 120 le2addd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( abs ‘ ( 𝑥 − 𝑧 ) ) · ( 𝑁 ‘ 𝑦 ) ) + ( ( abs ‘ 𝑧 ) · ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) ) ≤ ( ( ( 𝑁 ‘ 𝑦 ) · 𝑇 ) + ( ( ( abs ‘ 𝑥 ) + 1 ) · 𝑇 ) ) )
122 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
123 5 122 3 6 1 imsdval2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 𝑆 𝑦 ) ∈ 𝑋 ∧ ( 𝑧 𝑆 𝑦 ) ∈ 𝑋 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) = ( 𝑁 ‘ ( ( 𝑥 𝑆 𝑦 ) ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 ( 𝑧 𝑆 𝑦 ) ) ) ) )
124 33 37 45 123 syl3anc ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) = ( 𝑁 ‘ ( ( 𝑥 𝑆 𝑦 ) ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 ( 𝑧 𝑆 𝑦 ) ) ) ) )
125 neg1cn ⊢ - 1 ∈ ℂ
126 mulcl ⊢ ( ( - 1 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( - 1 · 𝑧 ) ∈ ℂ )
127 125 38 126 sylancr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( - 1 · 𝑧 ) ∈ ℂ )
128 5 122 3 nvdir ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ℂ ∧ ( - 1 · 𝑧 ) ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 + ( - 1 · 𝑧 ) ) 𝑆 𝑦 ) = ( ( 𝑥 𝑆 𝑦 ) ( +𝑣 ‘ 𝑈 ) ( ( - 1 · 𝑧 ) 𝑆 𝑦 ) ) )
129 33 34 127 35 128 syl13anc ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 + ( - 1 · 𝑧 ) ) 𝑆 𝑦 ) = ( ( 𝑥 𝑆 𝑦 ) ( +𝑣 ‘ 𝑈 ) ( ( - 1 · 𝑧 ) 𝑆 𝑦 ) ) )
130 38 mulm1d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( - 1 · 𝑧 ) = - 𝑧 )
131 130 oveq2d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑥 + ( - 1 · 𝑧 ) ) = ( 𝑥 + - 𝑧 ) )
132 34 38 negsubd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑥 + - 𝑧 ) = ( 𝑥 − 𝑧 ) )
133 131 132 eqtrd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑥 + ( - 1 · 𝑧 ) ) = ( 𝑥 − 𝑧 ) )
134 133 oveq1d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 + ( - 1 · 𝑧 ) ) 𝑆 𝑦 ) = ( ( 𝑥 − 𝑧 ) 𝑆 𝑦 ) )
135 125 a1i ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → - 1 ∈ ℂ )
136 5 3 nvsass ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( - 1 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ) → ( ( - 1 · 𝑧 ) 𝑆 𝑦 ) = ( - 1 𝑆 ( 𝑧 𝑆 𝑦 ) ) )
137 33 135 38 35 136 syl13anc ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( - 1 · 𝑧 ) 𝑆 𝑦 ) = ( - 1 𝑆 ( 𝑧 𝑆 𝑦 ) ) )
138 137 oveq2d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 𝑆 𝑦 ) ( +𝑣 ‘ 𝑈 ) ( ( - 1 · 𝑧 ) 𝑆 𝑦 ) ) = ( ( 𝑥 𝑆 𝑦 ) ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 ( 𝑧 𝑆 𝑦 ) ) ) )
139 129 134 138 3eqtr3d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 − 𝑧 ) 𝑆 𝑦 ) = ( ( 𝑥 𝑆 𝑦 ) ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 ( 𝑧 𝑆 𝑦 ) ) ) )
140 139 fveq2d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑁 ‘ ( ( 𝑥 − 𝑧 ) 𝑆 𝑦 ) ) = ( 𝑁 ‘ ( ( 𝑥 𝑆 𝑦 ) ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 ( 𝑧 𝑆 𝑦 ) ) ) ) )
141 5 3 6 nvs ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 − 𝑧 ) ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → ( 𝑁 ‘ ( ( 𝑥 − 𝑧 ) 𝑆 𝑦 ) ) = ( ( abs ‘ ( 𝑥 − 𝑧 ) ) · ( 𝑁 ‘ 𝑦 ) ) )
142 33 63 35 141 syl3anc ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑁 ‘ ( ( 𝑥 − 𝑧 ) 𝑆 𝑦 ) ) = ( ( abs ‘ ( 𝑥 − 𝑧 ) ) · ( 𝑁 ‘ 𝑦 ) ) )
143 124 140 142 3eqtr2d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) = ( ( abs ‘ ( 𝑥 − 𝑧 ) ) · ( 𝑁 ‘ 𝑦 ) ) )
144 5 67 6 1 imsdval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑧 𝑆 𝑦 ) ∈ 𝑋 ∧ ( 𝑧 𝑆 𝑤 ) ∈ 𝑋 ) → ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) = ( 𝑁 ‘ ( ( 𝑧 𝑆 𝑦 ) ( −𝑣 ‘ 𝑈 ) ( 𝑧 𝑆 𝑤 ) ) ) )
145 33 45 41 144 syl3anc ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) = ( 𝑁 ‘ ( ( 𝑧 𝑆 𝑦 ) ( −𝑣 ‘ 𝑈 ) ( 𝑧 𝑆 𝑤 ) ) ) )
146 5 67 3 nvmdi ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑧 𝑆 ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑧 𝑆 𝑦 ) ( −𝑣 ‘ 𝑈 ) ( 𝑧 𝑆 𝑤 ) ) )
147 33 38 35 39 146 syl13anc ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑧 𝑆 ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑧 𝑆 𝑦 ) ( −𝑣 ‘ 𝑈 ) ( 𝑧 𝑆 𝑤 ) ) )
148 147 fveq2d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑁 ‘ ( 𝑧 𝑆 ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) = ( 𝑁 ‘ ( ( 𝑧 𝑆 𝑦 ) ( −𝑣 ‘ 𝑈 ) ( 𝑧 𝑆 𝑤 ) ) ) )
149 5 3 6 nvs ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑧 𝑆 ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) = ( ( abs ‘ 𝑧 ) · ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) )
150 33 38 69 149 syl3anc ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑁 ‘ ( 𝑧 𝑆 ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) = ( ( abs ‘ 𝑧 ) · ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) )
151 145 148 150 3eqtr2d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) = ( ( abs ‘ 𝑧 ) · ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) )
152 143 151 oveq12d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) + ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ) = ( ( ( abs ‘ ( 𝑥 − 𝑧 ) ) · ( 𝑁 ‘ 𝑦 ) ) + ( ( abs ‘ 𝑧 ) · ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) ) )
153 56 recnd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ 𝑥 ) ∈ ℂ )
154 1cnd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 1 ∈ ℂ )
155 91 153 154 addassd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) = ( ( 𝑁 ‘ 𝑦 ) + ( ( abs ‘ 𝑥 ) + 1 ) ) )
156 155 oveq1d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) · 𝑇 ) = ( ( ( 𝑁 ‘ 𝑦 ) + ( ( abs ‘ 𝑥 ) + 1 ) ) · 𝑇 ) )
157 75 recnd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( abs ‘ 𝑥 ) + 1 ) ∈ ℂ )
158 91 157 90 adddird ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( 𝑁 ‘ 𝑦 ) + ( ( abs ‘ 𝑥 ) + 1 ) ) · 𝑇 ) = ( ( ( 𝑁 ‘ 𝑦 ) · 𝑇 ) + ( ( ( abs ‘ 𝑥 ) + 1 ) · 𝑇 ) ) )
159 156 158 eqtrd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) · 𝑇 ) = ( ( ( 𝑁 ‘ 𝑦 ) · 𝑇 ) + ( ( ( abs ‘ 𝑥 ) + 1 ) · 𝑇 ) ) )
160 121 152 159 3brtr4d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) + ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ) ≤ ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) · 𝑇 ) )
161 8 oveq2i ⊢ ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) · 𝑇 ) = ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) · ( 1 / ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) )
162 59 recnd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) ∈ ℂ )
163 107 rpcnd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ∈ ℂ )
164 107 rpne0d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ≠ 0 )
165 162 163 164 divrecd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) = ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) · ( 1 / ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) ) )
166 161 165 eqtr4id ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) · 𝑇 ) = ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) )
167 simplr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑟 ∈ ℝ+ )
168 104 rpred ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ∈ ℝ )
169 168 ltp1d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) < ( ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) + 1 ) )
170 104 rpcnd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ∈ ℂ )
171 170 154 addcomd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) + 1 ) = ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) )
172 169 171 breqtrd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) < ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) )
173 59 167 107 172 ltdiv23d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) < 𝑟 )
174 166 173 eqbrtrd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) · 𝑇 ) < 𝑟 )
175 50 62 52 160 174 lelttrd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) + ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ) < 𝑟 )
176 43 50 52 54 175 lelttrd ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 )
177 176 expr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ) → ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) )
178 177 ralrimivva ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) )
179 breq2 ⊢ ( 𝑠 = 𝑇 → ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ↔ ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ) )
180 breq2 ⊢ ( 𝑠 = 𝑇 → ( ( 𝑦 𝐶 𝑤 ) < 𝑠 ↔ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) )
181 179 180 anbi12d ⊢ ( 𝑠 = 𝑇 → ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) ↔ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) )
182 181 imbi1d ⊢ ( 𝑠 = 𝑇 → ( ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) ↔ ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) ) )
183 182 2ralbidv ⊢ ( 𝑠 = 𝑇 → ( ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) ↔ ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) ) )
184 183 rspcev ⊢ ( ( 𝑇 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) ) → ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) )
185 29 178 184 syl2anc ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) )
186 185 ralrimiva ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) )
187 186 rgen2 ⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 )
188 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
189 5 1 imsxmet ⊢ ( 𝑈 ∈ NrmCVec → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
190 7 189 ax-mp ⊢ 𝐶 ∈ ( ∞Met ‘ 𝑋 )
191 4 cnfldtopn ⊢ 𝐾 = ( MetOpen ‘ ( abs ∘ − ) )
192 191 2 2 txmetcn ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ) → ( 𝑆 ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) ↔ ( 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) ) ) )
193 188 190 190 192 mp3an ⊢ ( 𝑆 ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) ↔ ( 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) ) )
194 10 187 193 mpbir2an ⊢ 𝑆 ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 )