cnplimcim - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > cnplimcim		GIF version

Theorem cnplimcim 14139

Description: If a function is continuous at 𝐵, its limit at 𝐵 equals the value of the function there. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 14-Jun-2023.)

**Hypotheses**
Ref	Expression
cnplimcim.k	⊢ 𝐾 = (MetOpen‘(abs ∘ − ))
cnplimcim.j	⊢ 𝐽 = (𝐾 ↾_t 𝐴)

**Assertion**
Ref	Expression
cnplimcim	⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵) → (𝐹:𝐴⟶ℂ ∧ (𝐹‘𝐵) ∈ (𝐹 lim_ℂ 𝐵))))

Proof of Theorem cnplimcim Dummy variables 𝑑 𝑒 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnplimcim.j	. . . . . 6 ⊢ 𝐽 = (𝐾 ↾_t 𝐴)
2		cnplimcim.k	. . . . . . . 8 ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))
3	2	cntoptopon 14035	. . . . . . 7 ⊢ 𝐾 ∈ (TopOn‘ℂ)
4		simpl 109	. . . . . . 7 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) → 𝐴 ⊆ ℂ)
5		resttopon 13674	. . . . . . 7 ⊢ ((𝐾 ∈ (TopOn‘ℂ) ∧ 𝐴 ⊆ ℂ) → (𝐾 ↾_t 𝐴) ∈ (TopOn‘𝐴))
6	3, 4, 5	sylancr 414	. . . . . 6 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) → (𝐾 ↾_t 𝐴) ∈ (TopOn‘𝐴))
7	1, 6	eqeltrid 2264	. . . . 5 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) → 𝐽 ∈ (TopOn‘𝐴))
8		cnpf2 13710	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝐴) ∧ 𝐾 ∈ (TopOn‘ℂ) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) → 𝐹:𝐴⟶ℂ)
9	8	3expia 1205	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝐴) ∧ 𝐾 ∈ (TopOn‘ℂ)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵) → 𝐹:𝐴⟶ℂ))
10	7, 3, 9	sylancl 413	. . . 4 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵) → 𝐹:𝐴⟶ℂ))
11	10	imp 124	. . 3 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) → 𝐹:𝐴⟶ℂ)
12		simplr 528	. . . . 5 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) → 𝐵 ∈ 𝐴)
13	11, 12	ffvelcdmd 5653	. . . 4 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) → (𝐹‘𝐵) ∈ ℂ)
14		simpr 110	. . . . . . 7 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵))
15		simpll 527	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹:𝐴⟶ℂ) → 𝐴 ⊆ ℂ)
16		cnxmet 14034	. . . . . . . . . . . 12 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
17		eqid 2177	. . . . . . . . . . . . 13 ⊢ ((abs ∘ − ) ↾ (𝐴 × 𝐴)) = ((abs ∘ − ) ↾ (𝐴 × 𝐴))
18		eqid 2177	. . . . . . . . . . . . 13 ⊢ (MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))) = (MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴)))
19	17, 2, 18	metrest 14009	. . . . . . . . . . . 12 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ⊆ ℂ) → (𝐾 ↾_t 𝐴) = (MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))))
20	16, 19	mpan 424	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ ℂ → (𝐾 ↾_t 𝐴) = (MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))))
21	1, 20	eqtrid 2222	. . . . . . . . . 10 ⊢ (𝐴 ⊆ ℂ → 𝐽 = (MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))))
22	15, 21	syl 14	. . . . . . . . 9 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹:𝐴⟶ℂ) → 𝐽 = (MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))))
23	2	a1i 9	. . . . . . . . 9 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹:𝐴⟶ℂ) → 𝐾 = (MetOpen‘(abs ∘ − )))
24		xmetres2 13882	. . . . . . . . . 10 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ⊆ ℂ) → ((abs ∘ − ) ↾ (𝐴 × 𝐴)) ∈ (∞Met‘𝐴))
25	16, 15, 24	sylancr 414	. . . . . . . . 9 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹:𝐴⟶ℂ) → ((abs ∘ − ) ↾ (𝐴 × 𝐴)) ∈ (∞Met‘𝐴))
26	16	a1i 9	. . . . . . . . 9 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹:𝐴⟶ℂ) → (abs ∘ − ) ∈ (∞Met‘ℂ))
27		simplr 528	. . . . . . . . 9 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹:𝐴⟶ℂ) → 𝐵 ∈ 𝐴)
28	22, 23, 25, 26, 27	metcnpd 14023	. . . . . . . 8 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹:𝐴⟶ℂ) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵) ↔ (𝐹:𝐴⟶ℂ ∧ ∀𝑒 ∈ ℝ⁺ ∃𝑑 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝐵((abs ∘ − ) ↾ (𝐴 × 𝐴))𝑧) < 𝑑 → ((𝐹‘𝐵)(abs ∘ − )(𝐹‘𝑧)) < 𝑒))))
29	11, 28	syldan 282	. . . . . . 7 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵) ↔ (𝐹:𝐴⟶ℂ ∧ ∀𝑒 ∈ ℝ⁺ ∃𝑑 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝐵((abs ∘ − ) ↾ (𝐴 × 𝐴))𝑧) < 𝑑 → ((𝐹‘𝐵)(abs ∘ − )(𝐹‘𝑧)) < 𝑒))))
30	14, 29	mpbid 147	. . . . . 6 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) → (𝐹:𝐴⟶ℂ ∧ ∀𝑒 ∈ ℝ⁺ ∃𝑑 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝐵((abs ∘ − ) ↾ (𝐴 × 𝐴))𝑧) < 𝑑 → ((𝐹‘𝐵)(abs ∘ − )(𝐹‘𝑧)) < 𝑒)))
31	30	simprd 114	. . . . 5 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) → ∀𝑒 ∈ ℝ⁺ ∃𝑑 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝐵((abs ∘ − ) ↾ (𝐴 × 𝐴))𝑧) < 𝑑 → ((𝐹‘𝐵)(abs ∘ − )(𝐹‘𝑧)) < 𝑒))
32	12	ad3antrrr 492	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → 𝐵 ∈ 𝐴)
33		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
34	32, 33	ovresd 6015	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → (𝐵((abs ∘ − ) ↾ (𝐴 × 𝐴))𝑧) = (𝐵(abs ∘ − )𝑧))
35	15, 27	sseldd 3157	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹:𝐴⟶ℂ) → 𝐵 ∈ ℂ)
36	11, 35	syldan 282	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) → 𝐵 ∈ ℂ)
37	36	ad3antrrr 492	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → 𝐵 ∈ ℂ)
38		simpll 527	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) → 𝐴 ⊆ ℂ)
39	38	ad3antrrr 492	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → 𝐴 ⊆ ℂ)
40	39, 33	sseldd 3157	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℂ)
41		eqid 2177	. . . . . . . . . . . . . . 15 ⊢ (abs ∘ − ) = (abs ∘ − )
42	41	cnmetdval 14032	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝐵(abs ∘ − )𝑧) = (abs‘(𝐵 − 𝑧)))
43	37, 40, 42	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → (𝐵(abs ∘ − )𝑧) = (abs‘(𝐵 − 𝑧)))
44	37, 40	abssubd 11202	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → (abs‘(𝐵 − 𝑧)) = (abs‘(𝑧 − 𝐵)))
45	34, 43, 44	3eqtrd 2214	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → (𝐵((abs ∘ − ) ↾ (𝐴 × 𝐴))𝑧) = (abs‘(𝑧 − 𝐵)))
46	45	breq1d 4014	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → ((𝐵((abs ∘ − ) ↾ (𝐴 × 𝐴))𝑧) < 𝑑 ↔ (abs‘(𝑧 − 𝐵)) < 𝑑))
47	46	biimprd 158	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → ((abs‘(𝑧 − 𝐵)) < 𝑑 → (𝐵((abs ∘ − ) ↾ (𝐴 × 𝐴))𝑧) < 𝑑))
48	47	adantld 278	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (𝐵((abs ∘ − ) ↾ (𝐴 × 𝐴))𝑧) < 𝑑))
49	13	ad3antrrr 492	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝐵) ∈ ℂ)
50	11	ad3antrrr 492	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → 𝐹:𝐴⟶ℂ)
51	50, 33	ffvelcdmd 5653	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℂ)
52	41	cnmetdval 14032	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝐵) ∈ ℂ ∧ (𝐹‘𝑧) ∈ ℂ) → ((𝐹‘𝐵)(abs ∘ − )(𝐹‘𝑧)) = (abs‘((𝐹‘𝐵) − (𝐹‘𝑧))))
53	49, 51, 52	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝐵)(abs ∘ − )(𝐹‘𝑧)) = (abs‘((𝐹‘𝐵) − (𝐹‘𝑧))))
54	49, 51	abssubd 11202	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → (abs‘((𝐹‘𝐵) − (𝐹‘𝑧))) = (abs‘((𝐹‘𝑧) − (𝐹‘𝐵))))
55	53, 54	eqtrd 2210	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝐵)(abs ∘ − )(𝐹‘𝑧)) = (abs‘((𝐹‘𝑧) − (𝐹‘𝐵))))
56	55	breq1d 4014	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝐵)(abs ∘ − )(𝐹‘𝑧)) < 𝑒 ↔ (abs‘((𝐹‘𝑧) − (𝐹‘𝐵))) < 𝑒))
57	56	biimpd 144	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → (((𝐹‘𝐵)(abs ∘ − )(𝐹‘𝑧)) < 𝑒 → (abs‘((𝐹‘𝑧) − (𝐹‘𝐵))) < 𝑒))
58	48, 57	imim12d 74	. . . . . . . 8 ⊢ ((((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑧 ∈ 𝐴) → (((𝐵((abs ∘ − ) ↾ (𝐴 × 𝐴))𝑧) < 𝑑 → ((𝐹‘𝐵)(abs ∘ − )(𝐹‘𝑧)) < 𝑒) → ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − (𝐹‘𝐵))) < 𝑒)))
59	58	ralimdva 2544	. . . . . . 7 ⊢ (((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) → (∀𝑧 ∈ 𝐴 ((𝐵((abs ∘ − ) ↾ (𝐴 × 𝐴))𝑧) < 𝑑 → ((𝐹‘𝐵)(abs ∘ − )(𝐹‘𝑧)) < 𝑒) → ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − (𝐹‘𝐵))) < 𝑒)))
60	59	reximdva 2579	. . . . . 6 ⊢ ((((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) ∧ 𝑒 ∈ ℝ⁺) → (∃𝑑 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝐵((abs ∘ − ) ↾ (𝐴 × 𝐴))𝑧) < 𝑑 → ((𝐹‘𝐵)(abs ∘ − )(𝐹‘𝑧)) < 𝑒) → ∃𝑑 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − (𝐹‘𝐵))) < 𝑒)))
61	60	ralimdva 2544	. . . . 5 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) → (∀𝑒 ∈ ℝ⁺ ∃𝑑 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝐵((abs ∘ − ) ↾ (𝐴 × 𝐴))𝑧) < 𝑑 → ((𝐹‘𝐵)(abs ∘ − )(𝐹‘𝑧)) < 𝑒) → ∀𝑒 ∈ ℝ⁺ ∃𝑑 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − (𝐹‘𝐵))) < 𝑒)))
62	31, 61	mpd 13	. . . 4 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) → ∀𝑒 ∈ ℝ⁺ ∃𝑑 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − (𝐹‘𝐵))) < 𝑒))
63	11, 38, 36	ellimc3ap 14133	. . . 4 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) → ((𝐹‘𝐵) ∈ (𝐹 lim_ℂ 𝐵) ↔ ((𝐹‘𝐵) ∈ ℂ ∧ ∀𝑒 ∈ ℝ⁺ ∃𝑑 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − (𝐹‘𝐵))) < 𝑒))))
64	13, 62, 63	mpbir2and 944	. . 3 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) → (𝐹‘𝐵) ∈ (𝐹 lim_ℂ 𝐵))
65	11, 64	jca 306	. 2 ⊢ (((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵)) → (𝐹:𝐴⟶ℂ ∧ (𝐹‘𝐵) ∈ (𝐹 lim_ℂ 𝐵)))
66	65	ex 115	1 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐵) → (𝐹:𝐴⟶ℂ ∧ (𝐹‘𝐵) ∈ (𝐹 lim_ℂ 𝐵))))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1353 ∈ wcel 2148 ∀wral 2455 ∃wrex 2456 ⊆ wss 3130 class class class wbr 4004 × cxp 4625 ↾ cres 4629 ∘ ccom 4631 ⟶wf 5213 ‘cfv 5217 (class class class)co 5875 ℂcc 7809 < clt 7992 − cmin 8128 # cap 8538 ℝ⁺crp 9653 abscabs 11006 ↾_t crest 12688 ∞Metcxmet 13443 MetOpencmopn 13448 TopOnctopon 13513 CnP ccnp 13689 lim_ℂ climc 14126

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4119 ax-sep 4122 ax-nul 4130 ax-pow 4175 ax-pr 4210 ax-un 4434 ax-setind 4537 ax-iinf 4588 ax-cnex 7902 ax-resscn 7903 ax-1cn 7904 ax-1re 7905 ax-icn 7906 ax-addcl 7907 ax-addrcl 7908 ax-mulcl 7909 ax-mulrcl 7910 ax-addcom 7911 ax-mulcom 7912 ax-addass 7913 ax-mulass 7914 ax-distr 7915 ax-i2m1 7916 ax-0lt1 7917 ax-1rid 7918 ax-0id 7919 ax-rnegex 7920 ax-precex 7921 ax-cnre 7922 ax-pre-ltirr 7923 ax-pre-ltwlin 7924 ax-pre-lttrn 7925 ax-pre-apti 7926 ax-pre-ltadd 7927 ax-pre-mulgt0 7928 ax-pre-mulext 7929 ax-arch 7930 ax-caucvg 7931

This theorem depends on definitions: df-bi 117 df-stab 831 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2740 df-sbc 2964 df-csb 3059 df-dif 3132 df-un 3134 df-in 3136 df-ss 3143 df-nul 3424 df-if 3536 df-pw 3578 df-sn 3599 df-pr 3600 df-op 3602 df-uni 3811 df-int 3846 df-iun 3889 df-br 4005 df-opab 4066 df-mpt 4067 df-tr 4103 df-id 4294 df-po 4297 df-iso 4298 df-iord 4367 df-on 4369 df-ilim 4370 df-suc 4372 df-iom 4591 df-xp 4633 df-rel 4634 df-cnv 4635 df-co 4636 df-dm 4637 df-rn 4638 df-res 4639 df-ima 4640 df-iota 5179 df-fun 5219 df-fn 5220 df-f 5221 df-f1 5222 df-fo 5223 df-f1o 5224 df-fv 5225 df-isom 5226 df-riota 5831 df-ov 5878 df-oprab 5879 df-mpo 5880 df-1st 6141 df-2nd 6142 df-recs 6306 df-frec 6392 df-map 6650 df-pm 6651 df-sup 6983 df-inf 6984 df-pnf 7994 df-mnf 7995 df-xr 7996 df-ltxr 7997 df-le 7998 df-sub 8130 df-neg 8131 df-reap 8532 df-ap 8539 df-div 8630 df-inn 8920 df-2 8978 df-3 8979 df-4 8980 df-n0 9177 df-z 9254 df-uz 9529 df-q 9620 df-rp 9654 df-xneg 9772 df-xadd 9773 df-seqfrec 10446 df-exp 10520 df-cj 10851 df-re 10852 df-im 10853 df-rsqrt 11007 df-abs 11008 df-rest 12690 df-topgen 12709 df-psmet 13450 df-xmet 13451 df-met 13452 df-bl 13453 df-mopn 13454 df-top 13501 df-topon 13514 df-bases 13546 df-cnp 13692 df-limced 14128

This theorem is referenced by: cnplimccntop 14142 cnlimcim 14143

W3C validator