unblimceq0lem

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

Proof

Step	Hyp	Ref	Expression
1		unblimceq0lem.0	$⊢ φ \to S \subseteq ℂ$
2		unblimceq0lem.1	$⊢ φ \to F : S ⟶ ℂ$
3		unblimceq0lem.2	$⊢ φ \to A \in ℂ$
4		unblimceq0lem.3	$⊢ φ \to \forall b \in ℝ^{+} \forall d \in ℝ^{+} \exists x \in S (\|x - A\| < d \land b \leq \|F (x)\|)$
5		breq1	$⊢ b = if (A \in S, \|F (A)\| + c, c) \to (b \leq \|F (x)\| \leftrightarrow if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|)$
6	5	anbi2d	$⊢ b = if (A \in S, \|F (A)\| + c, c) \to ((\|x - A\| < d \land b \leq \|F (x)\|) \leftrightarrow (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))$
7	6	rexbidv	$⊢ b = if (A \in S, \|F (A)\| + c, c) \to (\exists x \in S (\|x - A\| < d \land b \leq \|F (x)\|) \leftrightarrow \exists x \in S (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))$
8	7	ralbidv	$⊢ b = if (A \in S, \|F (A)\| + c, c) \to (\forall d \in ℝ^{+} \exists x \in S (\|x - A\| < d \land b \leq \|F (x)\|) \leftrightarrow \forall d \in ℝ^{+} \exists x \in S (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))$
9	4	adantr	$⊢ (φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to \forall b \in ℝ^{+} \forall d \in ℝ^{+} \exists x \in S (\|x - A\| < d \land b \leq \|F (x)\|)$
10	2	ad2antrr	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land A \in S) \to F : S ⟶ ℂ$
11		simpr	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land A \in S) \to A \in S$
12	10 11	ffvelrnd	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land A \in S) \to F (A) \in ℂ$
13	12	abscld	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land A \in S) \to \|F (A)\| \in ℝ$
14		simprl	$⊢ (φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to c \in ℝ^{+}$
15	14	rpred	$⊢ (φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to c \in ℝ$
16	15	adantr	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land A \in S) \to c \in ℝ$
17	13 16	readdcld	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land A \in S) \to \|F (A)\| + c \in ℝ$
18	12	absge0d	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land A \in S) \to 0 \leq \|F (A)\|$
19	14	rpgt0d	$⊢ (φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to 0 < c$
20	19	adantr	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land A \in S) \to 0 < c$
21	13 16 18 20	addgegt0d	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land A \in S) \to 0 < \|F (A)\| + c$
22	17 21	elrpd	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land A \in S) \to \|F (A)\| + c \in ℝ^{+}$
23		simplrl	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land \neg A \in S) \to c \in ℝ^{+}$
24	22 23	ifclda	$⊢ (φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to if (A \in S, \|F (A)\| + c, c) \in ℝ^{+}$
25	8 9 24	rspcdva	$⊢ (φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to \forall d \in ℝ^{+} \exists x \in S (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|)$
26		simprr	$⊢ (φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to d \in ℝ^{+}$
27		rsp	$⊢ \forall d \in ℝ^{+} \exists x \in S (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|) \to (d \in ℝ^{+} \to \exists x \in S (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))$
28	25 26 27	sylc	$⊢ (φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to \exists x \in S (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|)$
29		simprl	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \to x \in S$
30		neeq1	$⊢ y = x \to (y \neq A \leftrightarrow x \neq A)$
31		fvoveq1	$⊢ y = x \to \|y - A\| = \|x - A\|$
32	31	breq1d	$⊢ y = x \to (\|y - A\| < d \leftrightarrow \|x - A\| < d)$
33		2fveq3	$⊢ y = x \to \|F (y)\| = \|F (x)\|$
34	33	breq2d	$⊢ y = x \to (c \leq \|F (y)\| \leftrightarrow c \leq \|F (x)\|)$
35	30 32 34	3anbi123d	$⊢ y = x \to ((y \neq A \land \|y - A\| < d \land c \leq \|F (y)\|) \leftrightarrow (x \neq A \land \|x - A\| < d \land c \leq \|F (x)\|))$
36	35	adantl	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land y = x) \to ((y \neq A \land \|y - A\| < d \land c \leq \|F (y)\|) \leftrightarrow (x \neq A \land \|x - A\| < d \land c \leq \|F (x)\|))$
37	17	adantlr	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to \|F (A)\| + c \in ℝ$
38	2	ad2antrr	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \to F : S ⟶ ℂ$
39	38 29	ffvelrnd	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \to F (x) \in ℂ$
40	39	abscld	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \to \|F (x)\| \in ℝ$
41	40	adantr	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to \|F (x)\| \in ℝ$
42		simpr	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to A \in S$
43	42	iftrued	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to if (A \in S, \|F (A)\| + c, c) = \|F (A)\| + c$
44	43	eqcomd	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to \|F (A)\| + c = if (A \in S, \|F (A)\| + c, c)$
45		simprrr	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \to if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|$
46	45	adantr	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|$
47	44 46	eqbrtrd	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to \|F (A)\| + c \leq \|F (x)\|$
48	37 41 47	lensymd	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to \neg \|F (x)\| < \|F (A)\| + c$
49		2fveq3	$⊢ x = A \to \|F (x)\| = \|F (A)\|$
50	49	adantl	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land A \in S) \land x = A) \to \|F (x)\| = \|F (A)\|$
51	16 13	ltaddposd	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land A \in S) \to (0 < c \leftrightarrow \|F (A)\| < \|F (A)\| + c)$
52	20 51	mpbid	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land A \in S) \to \|F (A)\| < \|F (A)\| + c$
53	52	adantr	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land A \in S) \land x = A) \to \|F (A)\| < \|F (A)\| + c$
54	50 53	eqbrtrd	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land A \in S) \land x = A) \to \|F (x)\| < \|F (A)\| + c$
55	54	ex	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land A \in S) \to (x = A \to \|F (x)\| < \|F (A)\| + c)$
56	55	adantlr	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to (x = A \to \|F (x)\| < \|F (A)\| + c)$
57	56	necon3bd	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to (\neg \|F (x)\| < \|F (A)\| + c \to x \neq A)$
58	48 57	mpd	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to x \neq A$
59		simprrl	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \to \|x - A\| < d$
60	59	adantr	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to \|x - A\| < d$
61	16	adantlr	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to c \in ℝ$
62	12	adantlr	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to F (A) \in ℂ$
63	62	absge0d	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to 0 \leq \|F (A)\|$
64	13	adantlr	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to \|F (A)\| \in ℝ$
65	61 64	addge02d	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to (0 \leq \|F (A)\| \leftrightarrow c \leq \|F (A)\| + c)$
66	63 65	mpbid	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to c \leq \|F (A)\| + c$
67	61 37 41 66 47	letrd	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to c \leq \|F (x)\|$
68	58 60 67	3jca	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land A \in S) \to (x \neq A \land \|x - A\| < d \land c \leq \|F (x)\|)$
69		simpr	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land \neg A \in S) \to \neg A \in S$
70		simpr	$⊢ ((((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land \neg A \in S) \land x = A) \to x = A$
71	29	adantr	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land \neg A \in S) \to x \in S$
72	71	adantr	$⊢ ((((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land \neg A \in S) \land x = A) \to x \in S$
73	70 72	eqeltrrd	$⊢ ((((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land \neg A \in S) \land x = A) \to A \in S$
74	73	ex	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land \neg A \in S) \to (x = A \to A \in S)$
75	74	necon3bd	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land \neg A \in S) \to (\neg A \in S \to x \neq A)$
76	69 75	mpd	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land \neg A \in S) \to x \neq A$
77	59	adantr	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land \neg A \in S) \to \|x - A\| < d$
78	69	iffalsed	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land \neg A \in S) \to if (A \in S, \|F (A)\| + c, c) = c$
79	78	eqcomd	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land \neg A \in S) \to c = if (A \in S, \|F (A)\| + c, c)$
80	45	adantr	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land \neg A \in S) \to if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|$
81	79 80	eqbrtrd	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land \neg A \in S) \to c \leq \|F (x)\|$
82	76 77 81	3jca	$⊢ (((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \land \neg A \in S) \to (x \neq A \land \|x - A\| < d \land c \leq \|F (x)\|)$
83	68 82	pm2.61dan	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \to (x \neq A \land \|x - A\| < d \land c \leq \|F (x)\|)$
84	29 36 83	rspcedvd	$⊢ ((φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \land (x \in S \land (\|x - A\| < d \land if (A \in S, \|F (A)\| + c, c) \leq \|F (x)\|))) \to \exists y \in S (y \neq A \land \|y - A\| < d \land c \leq \|F (y)\|)$
85	28 84	rexlimddv	$⊢ (φ \land (c \in ℝ^{+} \land d \in ℝ^{+})) \to \exists y \in S (y \neq A \land \|y - A\| < d \land c \leq \|F (y)\|)$
86	85	ralrimivva	$⊢ φ \to \forall c \in ℝ^{+} \forall d \in ℝ^{+} \exists y \in S (y \neq A \land \|y - A\| < d \land c \leq \|F (y)\|)$

Metamath Proof Explorer

Theorem unblimceq0lem

Proof