Theorem rlimcld2

Description: If D is a closed set in the topology of the complex numbers (stated here in basic form), and all the elements of the sequence lie in D , then the limit of the sequence also lies in D . (Contributed by Mario Carneiro, 10-May-2016)

	Ref	Expression
Hypotheses	rlimcld2.1	⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
	rlimcld2.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 )
	rlimcld2.3	⊢ ( 𝜑 → 𝐷 ⊆ ℂ )
	rlimcld2.4	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ 𝐷 ) ) → 𝑅 ∈ ℝ+ )
	rlimcld2.5	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ 𝐷 ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑅 ≤ ( abs ‘ ( 𝑧 − 𝑦 ) ) )
	rlimcld2.6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐷 )
Assertion	rlimcld2	⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		rlimcld2.1	⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
2		rlimcld2.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 )
3		rlimcld2.3	⊢ ( 𝜑 → 𝐷 ⊆ ℂ )
4		rlimcld2.4	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ 𝐷 ) ) → 𝑅 ∈ ℝ+ )
5		rlimcld2.5	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ 𝐷 ) ) ∧ 𝑧 ∈ 𝐷 ) → 𝑅 ≤ ( abs ‘ ( 𝑧 − 𝑦 ) ) )
6		rlimcld2.6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐷 )
7	6	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐷 )
8	7	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐷 )
9	2	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 )
10		rlimcl	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 → 𝐶 ∈ ℂ )
11	9 10	syl	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) → 𝐶 ∈ ℂ )
12		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) → ¬ 𝐶 ∈ 𝐷 )
13	11 12	eldifd	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) → 𝐶 ∈ ( ℂ ∖ 𝐷 ) )
14	4	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( ℂ ∖ 𝐷 ) 𝑅 ∈ ℝ+ )
15	14	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) → ∀ 𝑦 ∈ ( ℂ ∖ 𝐷 ) 𝑅 ∈ ℝ+ )
16		nfcsb1v	⊢ Ⅎ 𝑦 ⦋ 𝐶 / 𝑦 ⦌ 𝑅
17	16	nfel1	⊢ Ⅎ 𝑦 ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ∈ ℝ+
18		csbeq1a	⊢ ( 𝑦 = 𝐶 → 𝑅 = ⦋ 𝐶 / 𝑦 ⦌ 𝑅 )
19	18	eleq1d	⊢ ( 𝑦 = 𝐶 → ( 𝑅 ∈ ℝ+ ↔ ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ∈ ℝ+ ) )
20	17 19	rspc	⊢ ( 𝐶 ∈ ( ℂ ∖ 𝐷 ) → ( ∀ 𝑦 ∈ ( ℂ ∖ 𝐷 ) 𝑅 ∈ ℝ+ → ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ∈ ℝ+ ) )
21	13 15 20	sylc	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) → ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ∈ ℝ+ )
22	8 21 9	rlimi	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) → ∃ 𝑟 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑟 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ) )
23	21	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ∈ ℝ+ )
24	23	rpred	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ∈ ℝ )
25	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ⊆ ℂ )
26	6	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐷 )
27	25 26	sseldd	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
28	11	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
29	27 28	subcld	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
30	29	abscld	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) ∈ ℝ )
31	5	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ 𝐷 ) ) → ∀ 𝑧 ∈ 𝐷 𝑅 ≤ ( abs ‘ ( 𝑧 − 𝑦 ) ) )
32	31	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( ℂ ∖ 𝐷 ) ∀ 𝑧 ∈ 𝐷 𝑅 ≤ ( abs ‘ ( 𝑧 − 𝑦 ) ) )
33	32	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) → ∀ 𝑦 ∈ ( ℂ ∖ 𝐷 ) ∀ 𝑧 ∈ 𝐷 𝑅 ≤ ( abs ‘ ( 𝑧 − 𝑦 ) ) )
34		nfcv	⊢ Ⅎ 𝑦 𝐷
35		nfcv	⊢ Ⅎ 𝑦 ≤
36		nfcv	⊢ Ⅎ 𝑦 ( abs ‘ ( 𝑧 − 𝐶 ) )
37	16 35 36	nfbr	⊢ Ⅎ 𝑦 ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ≤ ( abs ‘ ( 𝑧 − 𝐶 ) )
38	34 37	nfralw	⊢ Ⅎ 𝑦 ∀ 𝑧 ∈ 𝐷 ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ≤ ( abs ‘ ( 𝑧 − 𝐶 ) )
39		oveq2	⊢ ( 𝑦 = 𝐶 → ( 𝑧 − 𝑦 ) = ( 𝑧 − 𝐶 ) )
40	39	fveq2d	⊢ ( 𝑦 = 𝐶 → ( abs ‘ ( 𝑧 − 𝑦 ) ) = ( abs ‘ ( 𝑧 − 𝐶 ) ) )
41	18 40	breq12d	⊢ ( 𝑦 = 𝐶 → ( 𝑅 ≤ ( abs ‘ ( 𝑧 − 𝑦 ) ) ↔ ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ≤ ( abs ‘ ( 𝑧 − 𝐶 ) ) ) )
42	41	ralbidv	⊢ ( 𝑦 = 𝐶 → ( ∀ 𝑧 ∈ 𝐷 𝑅 ≤ ( abs ‘ ( 𝑧 − 𝑦 ) ) ↔ ∀ 𝑧 ∈ 𝐷 ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ≤ ( abs ‘ ( 𝑧 − 𝐶 ) ) ) )
43	38 42	rspc	⊢ ( 𝐶 ∈ ( ℂ ∖ 𝐷 ) → ( ∀ 𝑦 ∈ ( ℂ ∖ 𝐷 ) ∀ 𝑧 ∈ 𝐷 𝑅 ≤ ( abs ‘ ( 𝑧 − 𝑦 ) ) → ∀ 𝑧 ∈ 𝐷 ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ≤ ( abs ‘ ( 𝑧 − 𝐶 ) ) ) )
44	13 33 43	sylc	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) → ∀ 𝑧 ∈ 𝐷 ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ≤ ( abs ‘ ( 𝑧 − 𝐶 ) ) )
45	44	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑧 ∈ 𝐷 ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ≤ ( abs ‘ ( 𝑧 − 𝐶 ) ) )
46		fvoveq1	⊢ ( 𝑧 = 𝐵 → ( abs ‘ ( 𝑧 − 𝐶 ) ) = ( abs ‘ ( 𝐵 − 𝐶 ) ) )
47	46	breq2d	⊢ ( 𝑧 = 𝐵 → ( ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ≤ ( abs ‘ ( 𝑧 − 𝐶 ) ) ↔ ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )
48	47	rspcv	⊢ ( 𝐵 ∈ 𝐷 → ( ∀ 𝑧 ∈ 𝐷 ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ≤ ( abs ‘ ( 𝑧 − 𝐶 ) ) → ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )
49	26 45 48	sylc	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) )
50	24 30 49	lensymd	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ¬ ( abs ‘ ( 𝐵 − 𝐶 ) ) < ⦋ 𝐶 / 𝑦 ⦌ 𝑅 )
51		id	⊢ ( ( 𝑟 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ) → ( 𝑟 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ) )
52	51	imp	⊢ ( ( ( 𝑟 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ) ∧ 𝑟 ≤ 𝑥 ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ⦋ 𝐶 / 𝑦 ⦌ 𝑅 )
53	50 52	nsyl	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ¬ ( ( 𝑟 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ) ∧ 𝑟 ≤ 𝑥 ) )
54	53	nrexdv	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ 𝑟 ∈ ℝ ) → ¬ ∃ 𝑥 ∈ 𝐴 ( ( 𝑟 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ) ∧ 𝑟 ≤ 𝑥 ) )
55		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
56	55 6	dmmptd	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
57		rlimss	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
58	2 57	syl	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
59	56 58	eqsstrrd	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
60		ressxr	⊢ ℝ ⊆ ℝ*
61	59 60	sstrdi	⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
62		supxrunb1	⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑟 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑟 ≤ 𝑥 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) )
63	61 62	syl	⊢ ( 𝜑 → ( ∀ 𝑟 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑟 ≤ 𝑥 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) )
64	1 63	mpbird	⊢ ( 𝜑 → ∀ 𝑟 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑟 ≤ 𝑥 )
65	64	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) → ∀ 𝑟 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑟 ≤ 𝑥 )
66	65	r19.21bi	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ 𝑟 ∈ ℝ ) → ∃ 𝑥 ∈ 𝐴 𝑟 ≤ 𝑥 )
67		r19.29	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑟 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ) ∧ ∃ 𝑥 ∈ 𝐴 𝑟 ≤ 𝑥 ) → ∃ 𝑥 ∈ 𝐴 ( ( 𝑟 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ) ∧ 𝑟 ≤ 𝑥 ) )
68	67	expcom	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑟 ≤ 𝑥 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑟 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ) → ∃ 𝑥 ∈ 𝐴 ( ( 𝑟 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ) ∧ 𝑟 ≤ 𝑥 ) ) )
69	66 68	syl	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ 𝑟 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑟 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ) → ∃ 𝑥 ∈ 𝐴 ( ( 𝑟 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ) ∧ 𝑟 ≤ 𝑥 ) ) )
70	54 69	mtod	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) ∧ 𝑟 ∈ ℝ ) → ¬ ∀ 𝑥 ∈ 𝐴 ( 𝑟 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ) )
71	70	nrexdv	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝐷 ) → ¬ ∃ 𝑟 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑟 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ⦋ 𝐶 / 𝑦 ⦌ 𝑅 ) )
72	22 71	condan	⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )