Theorem rlimcnp 25144

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

Hypotheses

Ref	Expression
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

Ref	Expression
rlimcnp	⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘0)))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝜑,𝑥,𝑦   𝑦,𝑅   𝑥,𝑆

Allowed substitution hints:   𝑅(𝑥)   𝑆(𝑦)   𝐽(𝑥,𝑦)   𝐾(𝑥,𝑦)

Proof of Theorem rlimcnp

Dummy variables 𝑤 𝑟 𝑧 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rpreccl 12165	. . . . . . . . 9 ⊢ (𝑟 ∈ ℝ+ → (1 / 𝑟) ∈ ℝ+)
2	1	adantl 475	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (1 / 𝑟) ∈ ℝ+)
3		rpreccl 12165	. . . . . . . . . 10 ⊢ (𝑡 ∈ ℝ+ → (1 / 𝑡) ∈ ℝ+)
4	3	adantl 475	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (1 / 𝑡) ∈ ℝ+)
5		rpcnne0 12157	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ℝ+ → (𝑡 ∈ ℂ ∧ 𝑡 ≠ 0))
6	5	adantl 475	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝑡 ∈ ℂ ∧ 𝑡 ≠ 0))
7		recrec 11072	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 / (1 / 𝑡)) = 𝑡)
8	6, 7	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (1 / (1 / 𝑡)) = 𝑡)
9	8	eqcomd 2784	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑡 = (1 / (1 / 𝑡)))
10		oveq2 6930	. . . . . . . . . 10 ⊢ (𝑟 = (1 / 𝑡) → (1 / 𝑟) = (1 / (1 / 𝑡)))
11	10	rspceeqv 3529	. . . . . . . . 9 ⊢ (((1 / 𝑡) ∈ ℝ+ ∧ 𝑡 = (1 / (1 / 𝑡))) → ∃𝑟 ∈ ℝ+ 𝑡 = (1 / 𝑟))
12	4, 9, 11	syl2anc 579	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → ∃𝑟 ∈ ℝ+ 𝑡 = (1 / 𝑟))
13		simpr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 = (1 / 𝑟)) → 𝑡 = (1 / 𝑟))
14	13	breq1d 4896	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 = (1 / 𝑟)) → (𝑡 < 𝑦 ↔ (1 / 𝑟) < 𝑦))
15	14	imbi1d 333	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 = (1 / 𝑟)) → ((𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
16	15	ralbidv 3168	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 = (1 / 𝑟)) → (∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
17	2, 12, 16	rexxfrd 5121	. . . . . . 7 ⊢ (𝜑 → (∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
18	17	adantr 474	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) → (∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
19		simplr 759	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑟 ∈ ℝ+)
20		rlimcnp.b	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ⊆ ℝ+)
21	20	sselda 3821	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℝ+)
22	21	adantlr 705	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℝ+)
23		elrp 12139	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ ℝ+ ↔ (𝑟 ∈ ℝ ∧ 0 < 𝑟))
24		elrp 12139	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ+ ↔ (𝑦 ∈ ℝ ∧ 0 < 𝑦))
25		ltrec1 11264	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ ℝ ∧ 0 < 𝑟) ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → ((1 / 𝑟) < 𝑦 ↔ (1 / 𝑦) < 𝑟))
26	23, 24, 25	syl2anb 591	. . . . . . . . . . . . 13 ⊢ ((𝑟 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+) → ((1 / 𝑟) < 𝑦 ↔ (1 / 𝑦) < 𝑟))
27	19, 22, 26	syl2anc 579	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → ((1 / 𝑟) < 𝑦 ↔ (1 / 𝑦) < 𝑟))
28	27	imbi1d 333	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → (((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
29	28	ralbidva 3167	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
30	29	adantlr 705	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+) → (∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
31		rpcn 12149	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ)
32		rpne0 12155	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ≠ 0)
33	31, 32	recrecd 11148	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ+ → (1 / (1 / 𝑦)) = 𝑦)
34	21, 33	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / (1 / 𝑦)) = 𝑦)
35		simpr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵)
36	34, 35	eqeltrd 2859	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / (1 / 𝑦)) ∈ 𝐵)
37		eleq1 2847	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (1 / 𝑦) → (𝑥 ∈ 𝐴 ↔ (1 / 𝑦) ∈ 𝐴))
38		oveq2 6930	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (1 / 𝑦) → (1 / 𝑥) = (1 / (1 / 𝑦)))
39	38	eleq1d 2844	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (1 / 𝑦) → ((1 / 𝑥) ∈ 𝐵 ↔ (1 / (1 / 𝑦)) ∈ 𝐵))
40	37, 39	bibi12d 337	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (1 / 𝑦) → ((𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵) ↔ ((1 / 𝑦) ∈ 𝐴 ↔ (1 / (1 / 𝑦)) ∈ 𝐵)))
41		rlimcnp.d	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵))
42	41	ralrimiva 3148	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵))
43	42	adantr 474	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∀𝑥 ∈ ℝ+ (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵))
44		rpreccl 12165	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℝ+)
45	21, 44	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / 𝑦) ∈ ℝ+)
46	40, 43, 45	rspcdva 3517	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((1 / 𝑦) ∈ 𝐴 ↔ (1 / (1 / 𝑦)) ∈ 𝐵))
47	36, 46	mpbird 249	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / 𝑦) ∈ 𝐴)
48	45	rpne0d 12186	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / 𝑦) ≠ 0)
49		eldifsn 4550	. . . . . . . . . . . 12 ⊢ ((1 / 𝑦) ∈ (𝐴 ∖ {0}) ↔ ((1 / 𝑦) ∈ 𝐴 ∧ (1 / 𝑦) ≠ 0))
50	47, 48, 49	sylanbrc 578	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / 𝑦) ∈ (𝐴 ∖ {0}))
51		eldifi 3955	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴 ∖ {0}) → 𝑥 ∈ 𝐴)
52	51	adantl 475	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ∈ 𝐴)
53		rge0ssre 12594	. . . . . . . . . . . . . . . 16 ⊢ (0[,)+∞) ⊆ ℝ
54		rlimcnp.a	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ⊆ (0[,)+∞))
55	54	ssdifssd 3971	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 ∖ {0}) ⊆ (0[,)+∞))
56	55	sselda 3821	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ∈ (0[,)+∞))
57	53, 56	sseldi 3819	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ∈ ℝ)
58		0re 10378	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℝ
59		pnfxr 10430	. . . . . . . . . . . . . . . . . . 19 ⊢ +∞ ∈ ℝ*
60		elico2 12549	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 ∈ ℝ ∧ +∞ ∈ ℝ*) → (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < +∞)))
61	58, 59, 60	mp2an 682	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 < +∞))
62	61	simp2bi 1137	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (0[,)+∞) → 0 ≤ 𝑥)
63	56, 62	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 0 ≤ 𝑥)
64		eldifsni 4553	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴 ∖ {0}) → 𝑥 ≠ 0)
65	64	adantl 475	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ≠ 0)
66	57, 63, 65	ne0gt0d 10513	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 0 < 𝑥)
67	57, 66	elrpd 12178	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ∈ ℝ+)
68	67, 41	syldan 585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵))
69	52, 68	mpbid 224	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → (1 / 𝑥) ∈ 𝐵)
70		rpcn 12149	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ)
71		rpne0 12155	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ≠ 0)
72	70, 71	recrecd 11148	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ+ → (1 / (1 / 𝑥)) = 𝑥)
73	67, 72	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → (1 / (1 / 𝑥)) = 𝑥)
74	73	eqcomd 2784	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 = (1 / (1 / 𝑥)))
75		oveq2 6930	. . . . . . . . . . . . 13 ⊢ (𝑦 = (1 / 𝑥) → (1 / 𝑦) = (1 / (1 / 𝑥)))
76	75	rspceeqv 3529	. . . . . . . . . . . 12 ⊢ (((1 / 𝑥) ∈ 𝐵 ∧ 𝑥 = (1 / (1 / 𝑥))) → ∃𝑦 ∈ 𝐵 𝑥 = (1 / 𝑦))
77	69, 74, 76	syl2anc 579	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → ∃𝑦 ∈ 𝐵 𝑥 = (1 / 𝑦))
78		breq1 4889	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1 / 𝑦) → (𝑥 < 𝑟 ↔ (1 / 𝑦) < 𝑟))
79		rlimcnp.s	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (1 / 𝑦) → 𝑅 = 𝑆)
80	79	fvoveq1d 6944	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (1 / 𝑦) → (abs‘(𝑅 − 𝐶)) = (abs‘(𝑆 − 𝐶)))
81	80	breq1d 4896	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1 / 𝑦) → ((abs‘(𝑅 − 𝐶)) < 𝑧 ↔ (abs‘(𝑆 − 𝐶)) < 𝑧))
82	78, 81	imbi12d 336	. . . . . . . . . . . 12 ⊢ (𝑥 = (1 / 𝑦) → ((𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
83	82	adantl 475	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = (1 / 𝑦)) → ((𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
84	50, 77, 83	ralxfrd 5120	. . . . . . . . . 10 ⊢ (𝜑 → (∀𝑥 ∈ (𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
85	84	ad2antrr 716	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+) → (∀𝑥 ∈ (𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
86	30, 85	bitr4d 274	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+) → (∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑥 ∈ (𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)))
87		elsni 4415	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ {0} → 𝑥 = 0)
88	87	adantl 475	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → 𝑥 = 0)
89		rlimcnp.c	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 0 → 𝑅 = 𝐶)
90	88, 89	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → 𝑅 = 𝐶)
91	90	oveq1d 6937	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → (𝑅 − 𝐶) = (𝐶 − 𝐶))
92	89	eleq1d 2844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 0 → (𝑅 ∈ ℂ ↔ 𝐶 ∈ ℂ))
93		rlimcnp.r	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ ℂ)
94	93	ralrimiva 3148	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ)
95		rlimcnp.0	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ∈ 𝐴)
96	92, 94, 95	rspcdva 3517	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 ∈ ℂ)
97	96	subidd 10722	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐶 − 𝐶) = 0)
98	97	ad2antrr 716	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → (𝐶 − 𝐶) = 0)
99	91, 98	eqtrd 2814	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → (𝑅 − 𝐶) = 0)
100	99	abs00bd 14438	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → (abs‘(𝑅 − 𝐶)) = 0)
101		rpgt0 12151	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℝ+ → 0 < 𝑧)
102	101	ad2antlr 717	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → 0 < 𝑧)
103	100, 102	eqbrtrd 4908	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → (abs‘(𝑅 − 𝐶)) < 𝑧)
104	103	a1d 25	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))
105	104	ralrimiva 3148	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) → ∀𝑥 ∈ {0} (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))
106	105	adantr 474	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+) → ∀𝑥 ∈ {0} (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))
107	106	biantrud 527	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+) → (∀𝑥 ∈ (𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ (∀𝑥 ∈ (𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ∧ ∀𝑥 ∈ {0} (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))))
108		ralunb 4017	. . . . . . . . 9 ⊢ (∀𝑥 ∈ ((𝐴 ∖ {0}) ∪ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ (∀𝑥 ∈ (𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ∧ ∀𝑥 ∈ {0} (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)))
109	107, 108	syl6bbr 281	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+) → (∀𝑥 ∈ (𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ∀𝑥 ∈ ((𝐴 ∖ {0}) ∪ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)))
110		undif1 4267	. . . . . . . . . 10 ⊢ ((𝐴 ∖ {0}) ∪ {0}) = (𝐴 ∪ {0})
111	95	ad2antrr 716	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+) → 0 ∈ 𝐴)
112	111	snssd 4571	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+) → {0} ⊆ 𝐴)
113		ssequn2 4009	. . . . . . . . . . 11 ⊢ ({0} ⊆ 𝐴 ↔ (𝐴 ∪ {0}) = 𝐴)
114	112, 113	sylib 210	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+) → (𝐴 ∪ {0}) = 𝐴)
115	110, 114	syl5eq 2826	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+) → ((𝐴 ∖ {0}) ∪ {0}) = 𝐴)
116	115	raleqdv 3340	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+) → (∀𝑥 ∈ ((𝐴 ∖ {0}) ∪ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)))
117	86, 109, 116	3bitrd 297	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+) → (∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)))
118	117	rexbidva 3234	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) → (∃𝑟 ∈ ℝ+ ∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)))
119	18, 118	bitrd 271	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) → (∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)))
120	119	ralbidva 3167	. . . 4 ⊢ (𝜑 → (∀𝑧 ∈ ℝ+ ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑧 ∈ ℝ+ ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)))
121		nfv 1957	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟
122		nffvmpt1 6457	. . . . . . . . . . 11 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)
123		nfcv 2934	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(abs ∘ − )
124		nffvmpt1 6457	. . . . . . . . . . 11 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)
125	122, 123, 124	nfov 6952	. . . . . . . . . 10 ⊢ Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0))
126		nfcv 2934	. . . . . . . . . 10 ⊢ Ⅎ𝑥 <
127		nfcv 2934	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝑧
128	125, 126, 127	nfbr 4933	. . . . . . . . 9 ⊢ Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧
129	121, 128	nfim 1943	. . . . . . . 8 ⊢ Ⅎ𝑥((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)
130		nfv 1957	. . . . . . . 8 ⊢ Ⅎ𝑤((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)
131		oveq1 6929	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → (𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) = (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0))
132	131	breq1d 4896	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 ↔ (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟))
133		fveq2 6446	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑥 → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥))
134	133	oveq1d 6937	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) = (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)))
135	134	breq1d 4896	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → ((((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧 ↔ (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧))
136	132, 135	imbi12d 336	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)))
137	129, 130, 136	cbvral 3363	. . . . . . 7 ⊢ (∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 ((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧))
138		simpr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
139	95	adantr 474	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ∈ 𝐴)
140	138, 139	ovresd 7078	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) = (𝑥(abs ∘ − )0))
141	54, 53	syl6ss 3833	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
142		ax-resscn 10329	. . . . . . . . . . . . . . 15 ⊢ ℝ ⊆ ℂ
143	141, 142	syl6ss 3833	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
144	143	sselda 3821	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℂ)
145		0cnd 10369	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℂ)
146		eqid 2778	. . . . . . . . . . . . . 14 ⊢ (abs ∘ − ) = (abs ∘ − )
147	146	cnmetdval 22982	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑥(abs ∘ − )0) = (abs‘(𝑥 − 0)))
148	144, 145, 147	syl2anc 579	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥(abs ∘ − )0) = (abs‘(𝑥 − 0)))
149	144	subid1d 10723	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 − 0) = 𝑥)
150	149	fveq2d 6450	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝑥 − 0)) = (abs‘𝑥))
151	140, 148, 150	3eqtrd 2818	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) = (abs‘𝑥))
152	141	sselda 3821	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ)
153	54	sselda 3821	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ (0[,)+∞))
154	153, 62	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝑥)
155	152, 154	absidd 14569	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝑥) = 𝑥)
156	151, 155	eqtrd 2814	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) = 𝑥)
157	156	breq1d 4896	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 ↔ 𝑥 < 𝑟))
158		eqid 2778	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅)
159	158	fvmpt2 6552	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑅 ∈ ℂ) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅)
160	138, 93, 159	syl2anc 579	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅)
161	96	adantr 474	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
162	158, 89, 139, 161	fvmptd3 6564	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘0) = 𝐶)
163	160, 162	oveq12d 6940	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) = (𝑅(abs ∘ − )𝐶))
164	146	cnmetdval 22982	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶)))
165	93, 161, 164	syl2anc 579	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶)))
166	163, 165	eqtrd 2814	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) = (abs‘(𝑅 − 𝐶)))
167	166	breq1d 4896	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧 ↔ (abs‘(𝑅 − 𝐶)) < 𝑧))
168	157, 167	imbi12d 336	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)))
169	168	ralbidva 3167	. . . . . . 7 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)))
170	137, 169	syl5bb 275	. . . . . 6 ⊢ (𝜑 → (∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)))
171	170	rexbidv 3237	. . . . 5 ⊢ (𝜑 → (∃𝑟 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)))
172	171	ralbidv 3168	. . . 4 ⊢ (𝜑 → (∀𝑧 ∈ ℝ+ ∃𝑟 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∀𝑧 ∈ ℝ+ ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)))
173	93	fmpttd 6649	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ)
174	173	biantrurd 528	. . . 4 ⊢ (𝜑 → (∀𝑧 ∈ ℝ+ ∃𝑟 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑧 ∈ ℝ+ ∃𝑟 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧))))
175	120, 172, 174	3bitr2d 299	. . 3 ⊢ (𝜑 → (∀𝑧 ∈ ℝ+ ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑧 ∈ ℝ+ ∃𝑟 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧))))
176	79	eleq1d 2844	. . . . . . . 8 ⊢ (𝑥 = (1 / 𝑦) → (𝑅 ∈ ℂ ↔ 𝑆 ∈ ℂ))
177	94	adantr 474	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ)
178	176, 177, 47	rspcdva 3517	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑆 ∈ ℂ)
179	178	ralrimiva 3148	. . . . . 6 ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 𝑆 ∈ ℂ)
180		rpssre 12144	. . . . . . 7 ⊢ ℝ+ ⊆ ℝ
181	20, 180	syl6ss 3833	. . . . . 6 ⊢ (𝜑 → 𝐵 ⊆ ℝ)
182		1red 10377	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ)
183	179, 181, 96, 182	rlim3 14637	. . . . 5 ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ ∀𝑧 ∈ ℝ+ ∃𝑡 ∈ (1[,)+∞)∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
184		0xr 10423	. . . . . . . . . 10 ⊢ 0 ∈ ℝ*
185		0lt1 10897	. . . . . . . . . 10 ⊢ 0 < 1
186		df-ioo 12491	. . . . . . . . . . 11 ⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
187		df-ico 12493	. . . . . . . . . . 11 ⊢ [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
188		xrltletr 12300	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → ((0 < 1 ∧ 1 ≤ 𝑤) → 0 < 𝑤))
189	186, 187, 188	ixxss1 12505	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ* ∧ 0 < 1) → (1[,)+∞) ⊆ (0(,)+∞))
190	184, 185, 189	mp2an 682	. . . . . . . . 9 ⊢ (1[,)+∞) ⊆ (0(,)+∞)
191		ioorp 12563	. . . . . . . . 9 ⊢ (0(,)+∞) = ℝ+
192	190, 191	sseqtri 3856	. . . . . . . 8 ⊢ (1[,)+∞) ⊆ ℝ+
193		ssrexv 3886	. . . . . . . 8 ⊢ ((1[,)+∞) ⊆ ℝ+ → (∃𝑡 ∈ (1[,)+∞)∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
194	192, 193	ax-mp 5	. . . . . . 7 ⊢ (∃𝑡 ∈ (1[,)+∞)∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))
195		simplr 759	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑡 ∈ ℝ+)
196	180, 195	sseldi 3819	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑡 ∈ ℝ)
197	181	adantr 474	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐵 ⊆ ℝ)
198	197	sselda 3821	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℝ)
199		ltle 10465	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑡 < 𝑦 → 𝑡 ≤ 𝑦))
200	196, 198, 199	syl2anc 579	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → (𝑡 < 𝑦 → 𝑡 ≤ 𝑦))
201	200	imim1d 82	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → ((𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
202	201	ralimdva 3144	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
203	202	reximdva 3198	. . . . . . 7 ⊢ (𝜑 → (∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
204	194, 203	syl5 34	. . . . . 6 ⊢ (𝜑 → (∃𝑡 ∈ (1[,)+∞)∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
205	204	ralimdv 3145	. . . . 5 ⊢ (𝜑 → (∀𝑧 ∈ ℝ+ ∃𝑡 ∈ (1[,)+∞)∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∀𝑧 ∈ ℝ+ ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
206	183, 205	sylbid 232	. . . 4 ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 → ∀𝑧 ∈ ℝ+ ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
207		ssrexv 3886	. . . . . . 7 ⊢ (ℝ+ ⊆ ℝ → (∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
208	180, 207	ax-mp 5	. . . . . 6 ⊢ (∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))
209	208	ralimi 3134	. . . . 5 ⊢ (∀𝑧 ∈ ℝ+ ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∀𝑧 ∈ ℝ+ ∃𝑡 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))
210	179, 181, 96	rlim2lt 14636	. . . . 5 ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ ∀𝑧 ∈ ℝ+ ∃𝑡 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
211	209, 210	syl5ibr 238	. . . 4 ⊢ (𝜑 → (∀𝑧 ∈ ℝ+ ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → (𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶))
212	206, 211	impbid 204	. . 3 ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ ∀𝑧 ∈ ℝ+ ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)))
213		cnxmet 22984	. . . . 5 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
214		xmetres2 22574	. . . . 5 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ⊆ ℂ) → ((abs ∘ − ) ↾ (𝐴 × 𝐴)) ∈ (∞Met‘𝐴))
215	213, 143, 214	sylancr 581	. . . 4 ⊢ (𝜑 → ((abs ∘ − ) ↾ (𝐴 × 𝐴)) ∈ (∞Met‘𝐴))
216	213	a1i 11	. . . 4 ⊢ (𝜑 → (abs ∘ − ) ∈ (∞Met‘ℂ))
217		eqid 2778	. . . . 5 ⊢ (MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))) = (MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴)))
218		rlimcnp.j	. . . . . 6 ⊢ 𝐽 = (TopOpen‘ℂfld)
219	218	cnfldtopn 22993	. . . . 5 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
220	217, 219	metcnp2 22755	. . . 4 ⊢ ((((abs ∘ − ) ↾ (𝐴 × 𝐴)) ∈ (∞Met‘𝐴) ∧ (abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (((MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))) CnP 𝐽)‘0) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑧 ∈ ℝ+ ∃𝑟 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧))))
221	215, 216, 95, 220	syl3anc 1439	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (((MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))) CnP 𝐽)‘0) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑧 ∈ ℝ+ ∃𝑟 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧))))
222	175, 212, 221	3bitr4d 303	. 2 ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (((MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))) CnP 𝐽)‘0)))
223		rlimcnp.k	. . . . . 6 ⊢ 𝐾 = (𝐽 ↾t 𝐴)
224		eqid 2778	. . . . . . . 8 ⊢ ((abs ∘ − ) ↾ (𝐴 × 𝐴)) = ((abs ∘ − ) ↾ (𝐴 × 𝐴))
225	224, 219, 217	metrest 22737	. . . . . . 7 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ⊆ ℂ) → (𝐽 ↾t 𝐴) = (MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))))
226	213, 143, 225	sylancr 581	. . . . . 6 ⊢ (𝜑 → (𝐽 ↾t 𝐴) = (MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))))
227	223, 226	syl5eq 2826	. . . . 5 ⊢ (𝜑 → 𝐾 = (MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))))
228	227	oveq1d 6937	. . . 4 ⊢ (𝜑 → (𝐾 CnP 𝐽) = ((MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))) CnP 𝐽))
229	228	fveq1d 6448	. . 3 ⊢ (𝜑 → ((𝐾 CnP 𝐽)‘0) = (((MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))) CnP 𝐽)‘0))
230	229	eleq2d 2845	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘0) ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (((MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))) CnP 𝐽)‘0)))
231	222, 230	bitr4d 274	1 ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘0)))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1071   = wceq 1601   ∈ wcel 2107   ≠ wne 2969  ∀wral 3090  ∃wrex 3091   ∖ cdif 3789   ∪ cun 3790   ⊆ wss 3792  {csn 4398   class class class wbr 4886   ↦ cmpt 4965   × cxp 5353   ↾ cres 5357   ∘ ccom 5359  ⟶wf 6131  ‘cfv 6135  (class class class)co 6922  ℂcc 10270  ℝcr 10271  0cc0 10272  1c1 10273  +∞cpnf 10408  ℝ^*cxr 10410   < clt 10411   ≤ cle 10412   − cmin 10606   / cdiv 11032  ℝ⁺crp 12137  (,)cioo 12487  [,)cico 12489  abscabs 14381   ⇝_𝑟 crli 14624   ↾_t crest 16467  TopOpenctopn 16468  ∞Metcxmet 20127  MetOpencmopn 20132  ℂ_fldccnfld 20142   CnP ccnp 21437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-int 4711  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-oadd 7847  df-er 8026  df-map 8142  df-pm 8143  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-sup 8636  df-inf 8637  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-4 11440  df-5 11441  df-6 11442  df-7 11443  df-8 11444  df-9 11445  df-n0 11643  df-z 11729  df-dec 11846  df-uz 11993  df-q 12096  df-rp 12138  df-xneg 12257  df-xadd 12258  df-xmul 12259  df-ioo 12491  df-ico 12493  df-fz 12644  df-seq 13120  df-exp 13179  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383  df-rlim 14628  df-struct 16257  df-ndx 16258  df-slot 16259  df-base 16261  df-plusg 16351  df-mulr 16352  df-starv 16353  df-tset 16357  df-ple 16358  df-ds 16360  df-unif 16361  df-rest 16469  df-topn 16470  df-topgen 16490  df-psmet 20134  df-xmet 20135  df-met 20136  df-bl 20137  df-mopn 20138  df-cnfld 20143  df-top 21106  df-topon 21123  df-bases 21158  df-cnp 21440

This theorem is referenced by:  rlimcnp2  25145