unblimceq0

Description: If F is unbounded near A it has no limit at A . (Contributed by Asger C. Ipsen, 12-May-2021)

	Ref	Expression
Hypotheses	unblimceq0.0	$⊢ φ \to S \subseteq ℂ$
	unblimceq0.1	$⊢ φ \to F : S ⟶ ℂ$
	unblimceq0.2	$⊢ φ \to A \in ℂ$
	unblimceq0.3	$⊢ φ \to \forall b \in ℝ^{+} \forall d \in ℝ^{+} \exists x \in S (\|x - A\| < d \land b \leq \|F (x)\|)$
Assertion	unblimceq0	$⊢ φ \to F {lim}_{ℂ} A = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		unblimceq0.0	$⊢ φ \to S \subseteq ℂ$
2		unblimceq0.1	$⊢ φ \to F : S ⟶ ℂ$
3		unblimceq0.2	$⊢ φ \to A \in ℂ$
4		unblimceq0.3	$⊢ φ \to \forall b \in ℝ^{+} \forall d \in ℝ^{+} \exists x \in S (\|x - A\| < d \land b \leq \|F (x)\|)$
5		1rp	$⊢ 1 \in ℝ^{+}$
6	5	a1i	$⊢ (φ \land y \in ℂ) \to 1 \in ℝ^{+}$
7		breq2	$⊢ e = 1 \to (\|F (z) - y\| < e \leftrightarrow \|F (z) - y\| < 1)$
8	7	imbi2d	$⊢ e = 1 \to (((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < e) \leftrightarrow ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < 1))$
9	8	rexralbidv	$⊢ e = 1 \to (\exists c \in ℝ^{+} \forall z \in S ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < e) \leftrightarrow \exists c \in ℝ^{+} \forall z \in S ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < 1))$
10	9	notbid	$⊢ e = 1 \to (\neg \exists c \in ℝ^{+} \forall z \in S ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < e) \leftrightarrow \neg \exists c \in ℝ^{+} \forall z \in S ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < 1))$
11	10	adantl	$⊢ ((φ \land y \in ℂ) \land e = 1) \to (\neg \exists c \in ℝ^{+} \forall z \in S ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < e) \leftrightarrow \neg \exists c \in ℝ^{+} \forall z \in S ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < 1))$
12		simprr1	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to z \neq A$
13		simprr2	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to \|z - A\| < c$
14	12 13	jca	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to (z \neq A \land \|z - A\| < c)$
15		1red	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to 1 \in ℝ$
16	2	ad2antrr	$⊢ ((φ \land y \in ℂ) \land c \in ℝ^{+}) \to F : S ⟶ ℂ$
17	16	adantr	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to F : S ⟶ ℂ$
18		simprl	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to z \in S$
19	17 18	ffvelrnd	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to F (z) \in ℂ$
20		simplr	$⊢ ((φ \land y \in ℂ) \land c \in ℝ^{+}) \to y \in ℂ$
21	20	adantr	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to y \in ℂ$
22	19 21	subcld	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to F (z) - y \in ℂ$
23	22	abscld	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to \|F (z) - y\| \in ℝ$
24	19	abscld	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to \|F (z)\| \in ℝ$
25	20	abscld	$⊢ ((φ \land y \in ℂ) \land c \in ℝ^{+}) \to \|y\| \in ℝ$
26	25	adantr	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to \|y\| \in ℝ$
27	24 26	resubcld	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to \|F (z)\| - \|y\| \in ℝ$
28		1cnd	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to 1 \in ℂ$
29	26	recnd	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to \|y\| \in ℂ$
30	28 29	pncand	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to 1 + \|y\| - \|y\| = 1$
31		1red	$⊢ ((φ \land y \in ℂ) \land c \in ℝ^{+}) \to 1 \in ℝ$
32	31 25	readdcld	$⊢ ((φ \land y \in ℂ) \land c \in ℝ^{+}) \to 1 + \|y\| \in ℝ$
33	32	adantr	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to 1 + \|y\| \in ℝ$
34		simprr3	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to 1 + \|y\| \leq \|F (z)\|$
35	33 24 26 34	lesub1dd	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to 1 + \|y\| - \|y\| \leq \|F (z)\| - \|y\|$
36	30 35	eqbrtrrd	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to 1 \leq \|F (z)\| - \|y\|$
37	19 21	abs2difd	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to \|F (z)\| - \|y\| \leq \|F (z) - y\|$
38	15 27 23 36 37	letrd	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to 1 \leq \|F (z) - y\|$
39	15 23 38	lensymd	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to \neg \|F (z) - y\| < 1$
40	14 39	jcnd	$⊢ (((φ \land y \in ℂ) \land c \in ℝ^{+}) \land (z \in S \land (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))) \to \neg ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < 1)$
41		breq2	$⊢ d = c \to (\|z - A\| < d \leftrightarrow \|z - A\| < c)$
42	41	3anbi2d	$⊢ d = c \to ((z \neq A \land \|z - A\| < d \land 1 + \|y\| \leq \|F (z)\|) \leftrightarrow (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))$
43	42	rexbidv	$⊢ d = c \to (\exists z \in S (z \neq A \land \|z - A\| < d \land 1 + \|y\| \leq \|F (z)\|) \leftrightarrow \exists z \in S (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|))$
44		breq1	$⊢ a = 1 + \|y\| \to (a \leq \|F (z)\| \leftrightarrow 1 + \|y\| \leq \|F (z)\|)$
45	44	3anbi3d	$⊢ a = 1 + \|y\| \to ((z \neq A \land \|z - A\| < d \land a \leq \|F (z)\|) \leftrightarrow (z \neq A \land \|z - A\| < d \land 1 + \|y\| \leq \|F (z)\|))$
46	45	rexbidv	$⊢ a = 1 + \|y\| \to (\exists z \in S (z \neq A \land \|z - A\| < d \land a \leq \|F (z)\|) \leftrightarrow \exists z \in S (z \neq A \land \|z - A\| < d \land 1 + \|y\| \leq \|F (z)\|))$
47	46	ralbidv	$⊢ a = 1 + \|y\| \to (\forall d \in ℝ^{+} \exists z \in S (z \neq A \land \|z - A\| < d \land a \leq \|F (z)\|) \leftrightarrow \forall d \in ℝ^{+} \exists z \in S (z \neq A \land \|z - A\| < d \land 1 + \|y\| \leq \|F (z)\|))$
48	1 2 3 4	unblimceq0lem	$⊢ φ \to \forall a \in ℝ^{+} \forall d \in ℝ^{+} \exists z \in S (z \neq A \land \|z - A\| < d \land a \leq \|F (z)\|)$
49	48	ad2antrr	$⊢ ((φ \land y \in ℂ) \land c \in ℝ^{+}) \to \forall a \in ℝ^{+} \forall d \in ℝ^{+} \exists z \in S (z \neq A \land \|z - A\| < d \land a \leq \|F (z)\|)$
50		0lt1	$⊢ 0 < 1$
51	50	a1i	$⊢ ((φ \land y \in ℂ) \land c \in ℝ^{+}) \to 0 < 1$
52	20	absge0d	$⊢ ((φ \land y \in ℂ) \land c \in ℝ^{+}) \to 0 \leq \|y\|$
53	31 25 51 52	addgtge0d	$⊢ ((φ \land y \in ℂ) \land c \in ℝ^{+}) \to 0 < 1 + \|y\|$
54	32 53	elrpd	$⊢ ((φ \land y \in ℂ) \land c \in ℝ^{+}) \to 1 + \|y\| \in ℝ^{+}$
55	47 49 54	rspcdva	$⊢ ((φ \land y \in ℂ) \land c \in ℝ^{+}) \to \forall d \in ℝ^{+} \exists z \in S (z \neq A \land \|z - A\| < d \land 1 + \|y\| \leq \|F (z)\|)$
56		simpr	$⊢ ((φ \land y \in ℂ) \land c \in ℝ^{+}) \to c \in ℝ^{+}$
57	43 55 56	rspcdva	$⊢ ((φ \land y \in ℂ) \land c \in ℝ^{+}) \to \exists z \in S (z \neq A \land \|z - A\| < c \land 1 + \|y\| \leq \|F (z)\|)$
58	40 57	reximddv	$⊢ ((φ \land y \in ℂ) \land c \in ℝ^{+}) \to \exists z \in S \neg ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < 1)$
59		rexnal	$⊢ \exists z \in S \neg ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < 1) \leftrightarrow \neg \forall z \in S ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < 1)$
60	58 59	sylib	$⊢ ((φ \land y \in ℂ) \land c \in ℝ^{+}) \to \neg \forall z \in S ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < 1)$
61	60	nrexdv	$⊢ (φ \land y \in ℂ) \to \neg \exists c \in ℝ^{+} \forall z \in S ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < 1)$
62	6 11 61	rspcedvd	$⊢ (φ \land y \in ℂ) \to \exists e \in ℝ^{+} \neg \exists c \in ℝ^{+} \forall z \in S ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < e)$
63		rexnal	$⊢ \exists e \in ℝ^{+} \neg \exists c \in ℝ^{+} \forall z \in S ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < e) \leftrightarrow \neg \forall e \in ℝ^{+} \exists c \in ℝ^{+} \forall z \in S ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < e)$
64	62 63	sylib	$⊢ (φ \land y \in ℂ) \to \neg \forall e \in ℝ^{+} \exists c \in ℝ^{+} \forall z \in S ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < e)$
65	64	ex	$⊢ φ \to (y \in ℂ \to \neg \forall e \in ℝ^{+} \exists c \in ℝ^{+} \forall z \in S ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < e))$
66		imnan	$⊢ (y \in ℂ \to \neg \forall e \in ℝ^{+} \exists c \in ℝ^{+} \forall z \in S ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < e)) \leftrightarrow \neg (y \in ℂ \land \forall e \in ℝ^{+} \exists c \in ℝ^{+} \forall z \in S ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < e))$
67	65 66	sylib	$⊢ φ \to \neg (y \in ℂ \land \forall e \in ℝ^{+} \exists c \in ℝ^{+} \forall z \in S ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < e))$
68	2 1 3	ellimc3	$⊢ φ \to (y \in (F {lim}_{ℂ} A) \leftrightarrow (y \in ℂ \land \forall e \in ℝ^{+} \exists c \in ℝ^{+} \forall z \in S ((z \neq A \land \|z - A\| < c) \to \|F (z) - y\| < e)))$
69	67 68	mtbird	$⊢ φ \to \neg y \in (F {lim}_{ℂ} A)$
70	69	eq0rdv	$⊢ φ \to F {lim}_{ℂ} A = \emptyset$

Metamath Proof Explorer

Theorem unblimceq0

Proof