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	⊢ ( 𝜑 → 𝐴 ⊆ ( 0 [,) +∞ ) )
	rlimcnp.0	⊢ ( 𝜑 → 0 ∈ 𝐴 )
	rlimcnp.b	⊢ ( 𝜑 → 𝐵 ⊆ ℝ⁺ )
	rlimcnp.r	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑅 ∈ ℂ )
	rlimcnp.d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ( 𝑥 ∈ 𝐴 ↔ ( 1 / 𝑥 ) ∈ 𝐵 ) )
	rlimcnp.c	⊢ ( 𝑥 = 0 → 𝑅 = 𝐶 )
	rlimcnp.s	⊢ ( 𝑥 = ( 1 / 𝑦 ) → 𝑅 = 𝑆 )
	rlimcnp.j	⊢ 𝐽 = ( TopOpen ‘ ℂ_fld )
	rlimcnp.k	⊢ 𝐾 = ( 𝐽 ↾_t 𝐴 )
Assertion	rlimcnp	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) ⇝_𝑟 𝐶 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ 0 ) ) )

Proof

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

Metamath Proof Explorer

Theorem rlimcnp

Proof