Theorem rlimcnp

Description: Relate a limit of a real-valued sequence at infinity to the continuity of the function S ( y ) = R ( 1 / y ) at zero. (Contributed by Mario Carneiro, 1-Mar-2015)

	Ref	Expression
Hypotheses	rlimcnp.a	|- ( ph -> A C_ ( 0 [,) +oo ) )
	rlimcnp.0	|- ( ph -> 0 e. A )
	rlimcnp.b	|- ( ph -> B C_ RR+ )
	rlimcnp.r	|- ( ( ph /\ x e. A ) -> R e. CC )
	rlimcnp.d	|- ( ( ph /\ x e. RR+ ) -> ( x e. A <-> ( 1 / x ) e. B ) )
	rlimcnp.c	|- ( x = 0 -> R = C )
	rlimcnp.s	|- ( x = ( 1 / y ) -> R = S )
	rlimcnp.j	|- J = ( TopOpen ` CCfld )
	rlimcnp.k	|- K = ( J |`t A )
Assertion	rlimcnp	|- ( ph -> ( ( y e. B |-> S ) ~~>r C <-> ( x e. A |-> R ) e. ( ( K CnP J ) ` 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rlimcnp.a	|- ( ph -> A C_ ( 0 [,) +oo ) )
2		rlimcnp.0	|- ( ph -> 0 e. A )
3		rlimcnp.b	|- ( ph -> B C_ RR+ )
4		rlimcnp.r	|- ( ( ph /\ x e. A ) -> R e. CC )
5		rlimcnp.d	|- ( ( ph /\ x e. RR+ ) -> ( x e. A <-> ( 1 / x ) e. B ) )
6		rlimcnp.c	|- ( x = 0 -> R = C )
7		rlimcnp.s	|- ( x = ( 1 / y ) -> R = S )
8		rlimcnp.j	|- J = ( TopOpen ` CCfld )
9		rlimcnp.k	|- K = ( J |`t A )
10		rpreccl	|- ( r e. RR+ -> ( 1 / r ) e. RR+ )
11	10	adantl	|- ( ( ph /\ r e. RR+ ) -> ( 1 / r ) e. RR+ )
12		rpreccl	|- ( t e. RR+ -> ( 1 / t ) e. RR+ )
13		rpcnne0	|- ( t e. RR+ -> ( t e. CC /\ t =/= 0 ) )
14	13	adantl	|- ( ( ph /\ t e. RR+ ) -> ( t e. CC /\ t =/= 0 ) )
15		recrec	|- ( ( t e. CC /\ t =/= 0 ) -> ( 1 / ( 1 / t ) ) = t )
16	14 15	syl	|- ( ( ph /\ t e. RR+ ) -> ( 1 / ( 1 / t ) ) = t )
17	16	eqcomd	|- ( ( ph /\ t e. RR+ ) -> t = ( 1 / ( 1 / t ) ) )
18		oveq2	|- ( r = ( 1 / t ) -> ( 1 / r ) = ( 1 / ( 1 / t ) ) )
19	18	rspceeqv	|- ( ( ( 1 / t ) e. RR+ /\ t = ( 1 / ( 1 / t ) ) ) -> E. r e. RR+ t = ( 1 / r ) )
20	12 17 19	syl2an2	|- ( ( ph /\ t e. RR+ ) -> E. r e. RR+ t = ( 1 / r ) )
21		simpr	|- ( ( ph /\ t = ( 1 / r ) ) -> t = ( 1 / r ) )
22	21	breq1d	|- ( ( ph /\ t = ( 1 / r ) ) -> ( t < y <-> ( 1 / r ) < y ) )
23	22	imbi1d	|- ( ( ph /\ t = ( 1 / r ) ) -> ( ( t < y -> ( abs ` ( S - C ) ) < z ) <-> ( ( 1 / r ) < y -> ( abs ` ( S - C ) ) < z ) ) )
24	23	ralbidv	|- ( ( ph /\ t = ( 1 / r ) ) -> ( A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) <-> A. y e. B ( ( 1 / r ) < y -> ( abs ` ( S - C ) ) < z ) ) )
25	11 20 24	rexxfrd	|- ( ph -> ( E. t e. RR+ A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) <-> E. r e. RR+ A. y e. B ( ( 1 / r ) < y -> ( abs ` ( S - C ) ) < z ) ) )
26	25	adantr	|- ( ( ph /\ z e. RR+ ) -> ( E. t e. RR+ A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) <-> E. r e. RR+ A. y e. B ( ( 1 / r ) < y -> ( abs ` ( S - C ) ) < z ) ) )
27		simplr	|- ( ( ( ph /\ r e. RR+ ) /\ y e. B ) -> r e. RR+ )
28	3	sselda	|- ( ( ph /\ y e. B ) -> y e. RR+ )
29	28	adantlr	|- ( ( ( ph /\ r e. RR+ ) /\ y e. B ) -> y e. RR+ )
30		elrp	|- ( r e. RR+ <-> ( r e. RR /\ 0 < r ) )
31		elrp	|- ( y e. RR+ <-> ( y e. RR /\ 0 < y ) )
32		ltrec1	|- ( ( ( r e. RR /\ 0 < r ) /\ ( y e. RR /\ 0 < y ) ) -> ( ( 1 / r ) < y <-> ( 1 / y ) < r ) )
33	30 31 32	syl2anb	|- ( ( r e. RR+ /\ y e. RR+ ) -> ( ( 1 / r ) < y <-> ( 1 / y ) < r ) )
34	27 29 33	syl2anc	|- ( ( ( ph /\ r e. RR+ ) /\ y e. B ) -> ( ( 1 / r ) < y <-> ( 1 / y ) < r ) )
35	34	imbi1d	|- ( ( ( ph /\ r e. RR+ ) /\ y e. B ) -> ( ( ( 1 / r ) < y -> ( abs ` ( S - C ) ) < z ) <-> ( ( 1 / y ) < r -> ( abs ` ( S - C ) ) < z ) ) )
36	35	ralbidva	|- ( ( ph /\ r e. RR+ ) -> ( A. y e. B ( ( 1 / r ) < y -> ( abs ` ( S - C ) ) < z ) <-> A. y e. B ( ( 1 / y ) < r -> ( abs ` ( S - C ) ) < z ) ) )
37	36	adantlr	|- ( ( ( ph /\ z e. RR+ ) /\ r e. RR+ ) -> ( A. y e. B ( ( 1 / r ) < y -> ( abs ` ( S - C ) ) < z ) <-> A. y e. B ( ( 1 / y ) < r -> ( abs ` ( S - C ) ) < z ) ) )
38		rpcn	|- ( y e. RR+ -> y e. CC )
39		rpne0	|- ( y e. RR+ -> y =/= 0 )
40	38 39	recrecd	|- ( y e. RR+ -> ( 1 / ( 1 / y ) ) = y )
41	28 40	syl	|- ( ( ph /\ y e. B ) -> ( 1 / ( 1 / y ) ) = y )
42		simpr	|- ( ( ph /\ y e. B ) -> y e. B )
43	41 42	eqeltrd	|- ( ( ph /\ y e. B ) -> ( 1 / ( 1 / y ) ) e. B )
44		eleq1	|- ( x = ( 1 / y ) -> ( x e. A <-> ( 1 / y ) e. A ) )
45		oveq2	|- ( x = ( 1 / y ) -> ( 1 / x ) = ( 1 / ( 1 / y ) ) )
46	45	eleq1d	|- ( x = ( 1 / y ) -> ( ( 1 / x ) e. B <-> ( 1 / ( 1 / y ) ) e. B ) )
47	44 46	bibi12d	|- ( x = ( 1 / y ) -> ( ( x e. A <-> ( 1 / x ) e. B ) <-> ( ( 1 / y ) e. A <-> ( 1 / ( 1 / y ) ) e. B ) ) )
48	5	ralrimiva	|- ( ph -> A. x e. RR+ ( x e. A <-> ( 1 / x ) e. B ) )
49	48	adantr	|- ( ( ph /\ y e. B ) -> A. x e. RR+ ( x e. A <-> ( 1 / x ) e. B ) )
50	28	rpreccld	|- ( ( ph /\ y e. B ) -> ( 1 / y ) e. RR+ )
51	47 49 50	rspcdva	|- ( ( ph /\ y e. B ) -> ( ( 1 / y ) e. A <-> ( 1 / ( 1 / y ) ) e. B ) )
52	43 51	mpbird	|- ( ( ph /\ y e. B ) -> ( 1 / y ) e. A )
53	50	rpne0d	|- ( ( ph /\ y e. B ) -> ( 1 / y ) =/= 0 )
54		eldifsn	|- ( ( 1 / y ) e. ( A \ { 0 } ) <-> ( ( 1 / y ) e. A /\ ( 1 / y ) =/= 0 ) )
55	52 53 54	sylanbrc	|- ( ( ph /\ y e. B ) -> ( 1 / y ) e. ( A \ { 0 } ) )
56		eldifi	|- ( x e. ( A \ { 0 } ) -> x e. A )
57	56	adantl	|- ( ( ph /\ x e. ( A \ { 0 } ) ) -> x e. A )
58		rge0ssre	|- ( 0 [,) +oo ) C_ RR
59	1	ssdifssd	|- ( ph -> ( A \ { 0 } ) C_ ( 0 [,) +oo ) )
60	59	sselda	|- ( ( ph /\ x e. ( A \ { 0 } ) ) -> x e. ( 0 [,) +oo ) )
61	58 60	sselid	|- ( ( ph /\ x e. ( A \ { 0 } ) ) -> x e. RR )
62		0re	|- 0 e. RR
63		pnfxr	|- +oo e. RR*
64		elico2	|- ( ( 0 e. RR /\ +oo e. RR* ) -> ( x e. ( 0 [,) +oo ) <-> ( x e. RR /\ 0 <_ x /\ x < +oo ) ) )
65	62 63 64	mp2an	|- ( x e. ( 0 [,) +oo ) <-> ( x e. RR /\ 0 <_ x /\ x < +oo ) )
66	65	simp2bi	|- ( x e. ( 0 [,) +oo ) -> 0 <_ x )
67	60 66	syl	|- ( ( ph /\ x e. ( A \ { 0 } ) ) -> 0 <_ x )
68		eldifsni	|- ( x e. ( A \ { 0 } ) -> x =/= 0 )
69	68	adantl	|- ( ( ph /\ x e. ( A \ { 0 } ) ) -> x =/= 0 )
70	61 67 69	ne0gt0d	|- ( ( ph /\ x e. ( A \ { 0 } ) ) -> 0 < x )
71	61 70	elrpd	|- ( ( ph /\ x e. ( A \ { 0 } ) ) -> x e. RR+ )
72	71 5	syldan	|- ( ( ph /\ x e. ( A \ { 0 } ) ) -> ( x e. A <-> ( 1 / x ) e. B ) )
73	57 72	mpbid	|- ( ( ph /\ x e. ( A \ { 0 } ) ) -> ( 1 / x ) e. B )
74		rpcn	|- ( x e. RR+ -> x e. CC )
75		rpne0	|- ( x e. RR+ -> x =/= 0 )
76	74 75	recrecd	|- ( x e. RR+ -> ( 1 / ( 1 / x ) ) = x )
77	71 76	syl	|- ( ( ph /\ x e. ( A \ { 0 } ) ) -> ( 1 / ( 1 / x ) ) = x )
78	77	eqcomd	|- ( ( ph /\ x e. ( A \ { 0 } ) ) -> x = ( 1 / ( 1 / x ) ) )
79		oveq2	|- ( y = ( 1 / x ) -> ( 1 / y ) = ( 1 / ( 1 / x ) ) )
80	79	rspceeqv	|- ( ( ( 1 / x ) e. B /\ x = ( 1 / ( 1 / x ) ) ) -> E. y e. B x = ( 1 / y ) )
81	73 78 80	syl2anc	|- ( ( ph /\ x e. ( A \ { 0 } ) ) -> E. y e. B x = ( 1 / y ) )
82		breq1	|- ( x = ( 1 / y ) -> ( x < r <-> ( 1 / y ) < r ) )
83	7	fvoveq1d	|- ( x = ( 1 / y ) -> ( abs ` ( R - C ) ) = ( abs ` ( S - C ) ) )
84	83	breq1d	|- ( x = ( 1 / y ) -> ( ( abs ` ( R - C ) ) < z <-> ( abs ` ( S - C ) ) < z ) )
85	82 84	imbi12d	|- ( x = ( 1 / y ) -> ( ( x < r -> ( abs ` ( R - C ) ) < z ) <-> ( ( 1 / y ) < r -> ( abs ` ( S - C ) ) < z ) ) )
86	85	adantl	|- ( ( ph /\ x = ( 1 / y ) ) -> ( ( x < r -> ( abs ` ( R - C ) ) < z ) <-> ( ( 1 / y ) < r -> ( abs ` ( S - C ) ) < z ) ) )
87	55 81 86	ralxfrd	|- ( ph -> ( A. x e. ( A \ { 0 } ) ( x < r -> ( abs ` ( R - C ) ) < z ) <-> A. y e. B ( ( 1 / y ) < r -> ( abs ` ( S - C ) ) < z ) ) )
88	87	ad2antrr	|- ( ( ( ph /\ z e. RR+ ) /\ r e. RR+ ) -> ( A. x e. ( A \ { 0 } ) ( x < r -> ( abs ` ( R - C ) ) < z ) <-> A. y e. B ( ( 1 / y ) < r -> ( abs ` ( S - C ) ) < z ) ) )
89	37 88	bitr4d	|- ( ( ( ph /\ z e. RR+ ) /\ r e. RR+ ) -> ( A. y e. B ( ( 1 / r ) < y -> ( abs ` ( S - C ) ) < z ) <-> A. x e. ( A \ { 0 } ) ( x < r -> ( abs ` ( R - C ) ) < z ) ) )
90		elsni	|- ( x e. { 0 } -> x = 0 )
91	90	adantl	|- ( ( ( ph /\ z e. RR+ ) /\ x e. { 0 } ) -> x = 0 )
92	91 6	syl	|- ( ( ( ph /\ z e. RR+ ) /\ x e. { 0 } ) -> R = C )
93	92	oveq1d	|- ( ( ( ph /\ z e. RR+ ) /\ x e. { 0 } ) -> ( R - C ) = ( C - C ) )
94	6	eleq1d	|- ( x = 0 -> ( R e. CC <-> C e. CC ) )
95	4	ralrimiva	|- ( ph -> A. x e. A R e. CC )
96	94 95 2	rspcdva	|- ( ph -> C e. CC )
97	96	subidd	|- ( ph -> ( C - C ) = 0 )
98	97	ad2antrr	|- ( ( ( ph /\ z e. RR+ ) /\ x e. { 0 } ) -> ( C - C ) = 0 )
99	93 98	eqtrd	|- ( ( ( ph /\ z e. RR+ ) /\ x e. { 0 } ) -> ( R - C ) = 0 )
100	99	abs00bd	|- ( ( ( ph /\ z e. RR+ ) /\ x e. { 0 } ) -> ( abs ` ( R - C ) ) = 0 )
101		rpgt0	|- ( z e. RR+ -> 0 < z )
102	101	ad2antlr	|- ( ( ( ph /\ z e. RR+ ) /\ x e. { 0 } ) -> 0 < z )
103	100 102	eqbrtrd	|- ( ( ( ph /\ z e. RR+ ) /\ x e. { 0 } ) -> ( abs ` ( R - C ) ) < z )
104	103	a1d	|- ( ( ( ph /\ z e. RR+ ) /\ x e. { 0 } ) -> ( x < r -> ( abs ` ( R - C ) ) < z ) )
105	104	ralrimiva	|- ( ( ph /\ z e. RR+ ) -> A. x e. { 0 } ( x < r -> ( abs ` ( R - C ) ) < z ) )
106	105	adantr	|- ( ( ( ph /\ z e. RR+ ) /\ r e. RR+ ) -> A. x e. { 0 } ( x < r -> ( abs ` ( R - C ) ) < z ) )
107	106	biantrud	|- ( ( ( ph /\ z e. RR+ ) /\ r e. RR+ ) -> ( A. x e. ( A \ { 0 } ) ( x < r -> ( abs ` ( R - C ) ) < z ) <-> ( A. x e. ( A \ { 0 } ) ( x < r -> ( abs ` ( R - C ) ) < z ) /\ A. x e. { 0 } ( x < r -> ( abs ` ( R - C ) ) < z ) ) ) )
108		ralunb	|- ( A. x e. ( ( A \ { 0 } ) u. { 0 } ) ( x < r -> ( abs ` ( R - C ) ) < z ) <-> ( A. x e. ( A \ { 0 } ) ( x < r -> ( abs ` ( R - C ) ) < z ) /\ A. x e. { 0 } ( x < r -> ( abs ` ( R - C ) ) < z ) ) )
109	107 108	bitr4di	|- ( ( ( ph /\ z e. RR+ ) /\ r e. RR+ ) -> ( A. x e. ( A \ { 0 } ) ( x < r -> ( abs ` ( R - C ) ) < z ) <-> A. x e. ( ( A \ { 0 } ) u. { 0 } ) ( x < r -> ( abs ` ( R - C ) ) < z ) ) )
110		undif1	|- ( ( A \ { 0 } ) u. { 0 } ) = ( A u. { 0 } )
111	2	ad2antrr	|- ( ( ( ph /\ z e. RR+ ) /\ r e. RR+ ) -> 0 e. A )
112	111	snssd	|- ( ( ( ph /\ z e. RR+ ) /\ r e. RR+ ) -> { 0 } C_ A )
113		ssequn2	|- ( { 0 } C_ A <-> ( A u. { 0 } ) = A )
114	112 113	sylib	|- ( ( ( ph /\ z e. RR+ ) /\ r e. RR+ ) -> ( A u. { 0 } ) = A )
115	110 114	syl5eq	|- ( ( ( ph /\ z e. RR+ ) /\ r e. RR+ ) -> ( ( A \ { 0 } ) u. { 0 } ) = A )
116	115	raleqdv	|- ( ( ( ph /\ z e. RR+ ) /\ r e. RR+ ) -> ( A. x e. ( ( A \ { 0 } ) u. { 0 } ) ( x < r -> ( abs ` ( R - C ) ) < z ) <-> A. x e. A ( x < r -> ( abs ` ( R - C ) ) < z ) ) )
117	89 109 116	3bitrd	|- ( ( ( ph /\ z e. RR+ ) /\ r e. RR+ ) -> ( A. y e. B ( ( 1 / r ) < y -> ( abs ` ( S - C ) ) < z ) <-> A. x e. A ( x < r -> ( abs ` ( R - C ) ) < z ) ) )
118	117	rexbidva	|- ( ( ph /\ z e. RR+ ) -> ( E. r e. RR+ A. y e. B ( ( 1 / r ) < y -> ( abs ` ( S - C ) ) < z ) <-> E. r e. RR+ A. x e. A ( x < r -> ( abs ` ( R - C ) ) < z ) ) )
119	26 118	bitrd	|- ( ( ph /\ z e. RR+ ) -> ( E. t e. RR+ A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) <-> E. r e. RR+ A. x e. A ( x < r -> ( abs ` ( R - C ) ) < z ) ) )
120	119	ralbidva	|- ( ph -> ( A. z e. RR+ E. t e. RR+ A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) <-> A. z e. RR+ E. r e. RR+ A. x e. A ( x < r -> ( abs ` ( R - C ) ) < z ) ) )
121		nfv	|- F/ x ( w ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r
122		nffvmpt1	|- F/_ x ( ( x e. A |-> R ) ` w )
123		nfcv	|- F/_ x ( abs o. - )
124		nffvmpt1	|- F/_ x ( ( x e. A |-> R ) ` 0 )
125	122 123 124	nfov	|- F/_ x ( ( ( x e. A |-> R ) ` w ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) )
126		nfcv	|- F/_ x <
127		nfcv	|- F/_ x z
128	125 126 127	nfbr	|- F/ x ( ( ( x e. A |-> R ) ` w ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z
129	121 128	nfim	|- F/ x ( ( w ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r -> ( ( ( x e. A |-> R ) ` w ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z )
130		nfv	|- F/ w ( ( x ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r -> ( ( ( x e. A |-> R ) ` x ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z )
131		oveq1	|- ( w = x -> ( w ( ( abs o. - ) |` ( A X. A ) ) 0 ) = ( x ( ( abs o. - ) |` ( A X. A ) ) 0 ) )
132	131	breq1d	|- ( w = x -> ( ( w ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r <-> ( x ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r ) )
133		fveq2	|- ( w = x -> ( ( x e. A |-> R ) ` w ) = ( ( x e. A |-> R ) ` x ) )
134	133	oveq1d	|- ( w = x -> ( ( ( x e. A |-> R ) ` w ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) = ( ( ( x e. A |-> R ) ` x ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) )
135	134	breq1d	|- ( w = x -> ( ( ( ( x e. A |-> R ) ` w ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z <-> ( ( ( x e. A |-> R ) ` x ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z ) )
136	132 135	imbi12d	|- ( w = x -> ( ( ( w ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r -> ( ( ( x e. A |-> R ) ` w ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z ) <-> ( ( x ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r -> ( ( ( x e. A |-> R ) ` x ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z ) ) )
137	129 130 136	cbvralw	|- ( A. w e. A ( ( w ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r -> ( ( ( x e. A |-> R ) ` w ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z ) <-> A. x e. A ( ( x ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r -> ( ( ( x e. A |-> R ) ` x ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z ) )
138		simpr	|- ( ( ph /\ x e. A ) -> x e. A )
139	2	adantr	|- ( ( ph /\ x e. A ) -> 0 e. A )
140	138 139	ovresd	|- ( ( ph /\ x e. A ) -> ( x ( ( abs o. - ) |` ( A X. A ) ) 0 ) = ( x ( abs o. - ) 0 ) )
141	1 58	sstrdi	|- ( ph -> A C_ RR )
142		ax-resscn	|- RR C_ CC
143	141 142	sstrdi	|- ( ph -> A C_ CC )
144	143	sselda	|- ( ( ph /\ x e. A ) -> x e. CC )
145		0cnd	|- ( ( ph /\ x e. A ) -> 0 e. CC )
146		eqid	|- ( abs o. - ) = ( abs o. - )
147	146	cnmetdval	|- ( ( x e. CC /\ 0 e. CC ) -> ( x ( abs o. - ) 0 ) = ( abs ` ( x - 0 ) ) )
148	144 145 147	syl2anc	|- ( ( ph /\ x e. A ) -> ( x ( abs o. - ) 0 ) = ( abs ` ( x - 0 ) ) )
149	144	subid1d	|- ( ( ph /\ x e. A ) -> ( x - 0 ) = x )
150	149	fveq2d	|- ( ( ph /\ x e. A ) -> ( abs ` ( x - 0 ) ) = ( abs ` x ) )
151	140 148 150	3eqtrd	|- ( ( ph /\ x e. A ) -> ( x ( ( abs o. - ) |` ( A X. A ) ) 0 ) = ( abs ` x ) )
152	141	sselda	|- ( ( ph /\ x e. A ) -> x e. RR )
153	1	sselda	|- ( ( ph /\ x e. A ) -> x e. ( 0 [,) +oo ) )
154	153 66	syl	|- ( ( ph /\ x e. A ) -> 0 <_ x )
155	152 154	absidd	|- ( ( ph /\ x e. A ) -> ( abs ` x ) = x )
156	151 155	eqtrd	|- ( ( ph /\ x e. A ) -> ( x ( ( abs o. - ) |` ( A X. A ) ) 0 ) = x )
157	156	breq1d	|- ( ( ph /\ x e. A ) -> ( ( x ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r <-> x < r ) )
158		eqid	|- ( x e. A |-> R ) = ( x e. A |-> R )
159	158	fvmpt2	|- ( ( x e. A /\ R e. CC ) -> ( ( x e. A |-> R ) ` x ) = R )
160	138 4 159	syl2anc	|- ( ( ph /\ x e. A ) -> ( ( x e. A |-> R ) ` x ) = R )
161	96	adantr	|- ( ( ph /\ x e. A ) -> C e. CC )
162	158 6 139 161	fvmptd3	|- ( ( ph /\ x e. A ) -> ( ( x e. A |-> R ) ` 0 ) = C )
163	160 162	oveq12d	|- ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) = ( R ( abs o. - ) C ) )
164	146	cnmetdval	|- ( ( R e. CC /\ C e. CC ) -> ( R ( abs o. - ) C ) = ( abs ` ( R - C ) ) )
165	4 161 164	syl2anc	|- ( ( ph /\ x e. A ) -> ( R ( abs o. - ) C ) = ( abs ` ( R - C ) ) )
166	163 165	eqtrd	|- ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> R ) ` x ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) = ( abs ` ( R - C ) ) )
167	166	breq1d	|- ( ( ph /\ x e. A ) -> ( ( ( ( x e. A |-> R ) ` x ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z <-> ( abs ` ( R - C ) ) < z ) )
168	157 167	imbi12d	|- ( ( ph /\ x e. A ) -> ( ( ( x ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r -> ( ( ( x e. A |-> R ) ` x ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z ) <-> ( x < r -> ( abs ` ( R - C ) ) < z ) ) )
169	168	ralbidva	|- ( ph -> ( A. x e. A ( ( x ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r -> ( ( ( x e. A |-> R ) ` x ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z ) <-> A. x e. A ( x < r -> ( abs ` ( R - C ) ) < z ) ) )
170	137 169	syl5bb	|- ( ph -> ( A. w e. A ( ( w ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r -> ( ( ( x e. A |-> R ) ` w ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z ) <-> A. x e. A ( x < r -> ( abs ` ( R - C ) ) < z ) ) )
171	170	rexbidv	|- ( ph -> ( E. r e. RR+ A. w e. A ( ( w ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r -> ( ( ( x e. A |-> R ) ` w ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z ) <-> E. r e. RR+ A. x e. A ( x < r -> ( abs ` ( R - C ) ) < z ) ) )
172	171	ralbidv	|- ( ph -> ( A. z e. RR+ E. r e. RR+ A. w e. A ( ( w ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r -> ( ( ( x e. A |-> R ) ` w ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z ) <-> A. z e. RR+ E. r e. RR+ A. x e. A ( x < r -> ( abs ` ( R - C ) ) < z ) ) )
173	4	fmpttd	|- ( ph -> ( x e. A |-> R ) : A --> CC )
174	173	biantrurd	|- ( ph -> ( A. z e. RR+ E. r e. RR+ A. w e. A ( ( w ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r -> ( ( ( x e. A |-> R ) ` w ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z ) <-> ( ( x e. A |-> R ) : A --> CC /\ A. z e. RR+ E. r e. RR+ A. w e. A ( ( w ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r -> ( ( ( x e. A |-> R ) ` w ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z ) ) ) )
175	120 172 174	3bitr2d	|- ( ph -> ( A. z e. RR+ E. t e. RR+ A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) <-> ( ( x e. A |-> R ) : A --> CC /\ A. z e. RR+ E. r e. RR+ A. w e. A ( ( w ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r -> ( ( ( x e. A |-> R ) ` w ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z ) ) ) )
176	7	eleq1d	|- ( x = ( 1 / y ) -> ( R e. CC <-> S e. CC ) )
177	95	adantr	|- ( ( ph /\ y e. B ) -> A. x e. A R e. CC )
178	176 177 52	rspcdva	|- ( ( ph /\ y e. B ) -> S e. CC )
179	178	ralrimiva	|- ( ph -> A. y e. B S e. CC )
180		rpssre	|- RR+ C_ RR
181	3 180	sstrdi	|- ( ph -> B C_ RR )
182		1red	|- ( ph -> 1 e. RR )
183	179 181 96 182	rlim3	|- ( ph -> ( ( y e. B |-> S ) ~~>r C <-> A. z e. RR+ E. t e. ( 1 [,) +oo ) A. y e. B ( t <_ y -> ( abs ` ( S - C ) ) < z ) ) )
184		0xr	|- 0 e. RR*
185		0lt1	|- 0 < 1
186		df-ioo	|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
187		df-ico	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
188		xrltletr	|- ( ( 0 e. RR* /\ 1 e. RR* /\ w e. RR* ) -> ( ( 0 < 1 /\ 1 <_ w ) -> 0 < w ) )
189	186 187 188	ixxss1	|- ( ( 0 e. RR* /\ 0 < 1 ) -> ( 1 [,) +oo ) C_ ( 0 (,) +oo ) )
190	184 185 189	mp2an	|- ( 1 [,) +oo ) C_ ( 0 (,) +oo )
191		ioorp	|- ( 0 (,) +oo ) = RR+
192	190 191	sseqtri	|- ( 1 [,) +oo ) C_ RR+
193		ssrexv	|- ( ( 1 [,) +oo ) C_ RR+ -> ( E. t e. ( 1 [,) +oo ) A. y e. B ( t <_ y -> ( abs ` ( S - C ) ) < z ) -> E. t e. RR+ A. y e. B ( t <_ y -> ( abs ` ( S - C ) ) < z ) ) )
194	192 193	ax-mp	|- ( E. t e. ( 1 [,) +oo ) A. y e. B ( t <_ y -> ( abs ` ( S - C ) ) < z ) -> E. t e. RR+ A. y e. B ( t <_ y -> ( abs ` ( S - C ) ) < z ) )
195		simplr	|- ( ( ( ph /\ t e. RR+ ) /\ y e. B ) -> t e. RR+ )
196	180 195	sselid	|- ( ( ( ph /\ t e. RR+ ) /\ y e. B ) -> t e. RR )
197	181	adantr	|- ( ( ph /\ t e. RR+ ) -> B C_ RR )
198	197	sselda	|- ( ( ( ph /\ t e. RR+ ) /\ y e. B ) -> y e. RR )
199		ltle	|- ( ( t e. RR /\ y e. RR ) -> ( t < y -> t <_ y ) )
200	196 198 199	syl2anc	|- ( ( ( ph /\ t e. RR+ ) /\ y e. B ) -> ( t < y -> t <_ y ) )
201	200	imim1d	|- ( ( ( ph /\ t e. RR+ ) /\ y e. B ) -> ( ( t <_ y -> ( abs ` ( S - C ) ) < z ) -> ( t < y -> ( abs ` ( S - C ) ) < z ) ) )
202	201	ralimdva	|- ( ( ph /\ t e. RR+ ) -> ( A. y e. B ( t <_ y -> ( abs ` ( S - C ) ) < z ) -> A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) ) )
203	202	reximdva	|- ( ph -> ( E. t e. RR+ A. y e. B ( t <_ y -> ( abs ` ( S - C ) ) < z ) -> E. t e. RR+ A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) ) )
204	194 203	syl5	|- ( ph -> ( E. t e. ( 1 [,) +oo ) A. y e. B ( t <_ y -> ( abs ` ( S - C ) ) < z ) -> E. t e. RR+ A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) ) )
205	204	ralimdv	|- ( ph -> ( A. z e. RR+ E. t e. ( 1 [,) +oo ) A. y e. B ( t <_ y -> ( abs ` ( S - C ) ) < z ) -> A. z e. RR+ E. t e. RR+ A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) ) )
206	183 205	sylbid	|- ( ph -> ( ( y e. B |-> S ) ~~>r C -> A. z e. RR+ E. t e. RR+ A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) ) )
207		ssrexv	|- ( RR+ C_ RR -> ( E. t e. RR+ A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) -> E. t e. RR A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) ) )
208	180 207	ax-mp	|- ( E. t e. RR+ A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) -> E. t e. RR A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) )
209	208	ralimi	|- ( A. z e. RR+ E. t e. RR+ A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) -> A. z e. RR+ E. t e. RR A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) )
210	179 181 96	rlim2lt	|- ( ph -> ( ( y e. B |-> S ) ~~>r C <-> A. z e. RR+ E. t e. RR A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) ) )
211	209 210	syl5ibr	|- ( ph -> ( A. z e. RR+ E. t e. RR+ A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) -> ( y e. B |-> S ) ~~>r C ) )
212	206 211	impbid	|- ( ph -> ( ( y e. B |-> S ) ~~>r C <-> A. z e. RR+ E. t e. RR+ A. y e. B ( t < y -> ( abs ` ( S - C ) ) < z ) ) )
213		cnxmet	|- ( abs o. - ) e. ( *Met ` CC )
214		xmetres2	|- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ A C_ CC ) -> ( ( abs o. - ) |` ( A X. A ) ) e. ( *Met ` A ) )
215	213 143 214	sylancr	|- ( ph -> ( ( abs o. - ) |` ( A X. A ) ) e. ( *Met ` A ) )
216	213	a1i	|- ( ph -> ( abs o. - ) e. ( *Met ` CC ) )
217		eqid	|- ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) )
218	8	cnfldtopn	|- J = ( MetOpen ` ( abs o. - ) )
219	217 218	metcnp2	|- ( ( ( ( abs o. - ) |` ( A X. A ) ) e. ( *Met ` A ) /\ ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. A ) -> ( ( x e. A |-> R ) e. ( ( ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) ) CnP J ) ` 0 ) <-> ( ( x e. A |-> R ) : A --> CC /\ A. z e. RR+ E. r e. RR+ A. w e. A ( ( w ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r -> ( ( ( x e. A |-> R ) ` w ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z ) ) ) )
220	215 216 2 219	syl3anc	|- ( ph -> ( ( x e. A |-> R ) e. ( ( ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) ) CnP J ) ` 0 ) <-> ( ( x e. A |-> R ) : A --> CC /\ A. z e. RR+ E. r e. RR+ A. w e. A ( ( w ( ( abs o. - ) |` ( A X. A ) ) 0 ) < r -> ( ( ( x e. A |-> R ) ` w ) ( abs o. - ) ( ( x e. A |-> R ) ` 0 ) ) < z ) ) ) )
221	175 212 220	3bitr4d	|- ( ph -> ( ( y e. B |-> S ) ~~>r C <-> ( x e. A |-> R ) e. ( ( ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) ) CnP J ) ` 0 ) ) )
222		eqid	|- ( ( abs o. - ) |` ( A X. A ) ) = ( ( abs o. - ) |` ( A X. A ) )
223	222 218 217	metrest	|- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ A C_ CC ) -> ( J |`t A ) = ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) ) )
224	213 143 223	sylancr	|- ( ph -> ( J |`t A ) = ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) ) )
225	9 224	syl5eq	|- ( ph -> K = ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) ) )
226	225	oveq1d	|- ( ph -> ( K CnP J ) = ( ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) ) CnP J ) )
227	226	fveq1d	|- ( ph -> ( ( K CnP J ) ` 0 ) = ( ( ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) ) CnP J ) ` 0 ) )
228	227	eleq2d	|- ( ph -> ( ( x e. A |-> R ) e. ( ( K CnP J ) ` 0 ) <-> ( x e. A |-> R ) e. ( ( ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) ) CnP J ) ` 0 ) ) )
229	221 228	bitr4d	|- ( ph -> ( ( y e. B |-> S ) ~~>r C <-> ( x e. A |-> R ) e. ( ( K CnP J ) ` 0 ) ) )