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
|- C = ( IndMet ` U )
smcn.j
|- J = ( MetOpen ` C )
smcn.s
|- S = ( .sOLD ` U )
smcn.k
|- K = ( TopOpen ` CCfld )
smcn.x
|- X = ( BaseSet ` U )
smcn.n
|- N = ( normCV ` U )
smcn.u
|- U e. NrmCVec
smcn.t
|- T = ( 1 / ( 1 + ( ( ( ( N ` y ) + ( abs ` x ) ) + 1 ) / r ) ) )
Assertion smcnlem
|- S e. ( ( K tX J ) Cn J )

Proof

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