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 ) |