cnrefiisplem

Description: Lemma for cnrefiisp (some local definitions are used). (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	cnrefiisplem.a	$⊢ φ \to A \in ℂ$
	cnrefiisplem.n	$⊢ φ \to \neg A \in ℝ$
	cnrefiisplem.b	$⊢ φ \to B \in Fin$
	cnrefiisplem.c	$⊢ C = ℝ \cup B$
	cnrefiisplem.d	$⊢ D = \{\|ℑ (A)\|\} \cup ⋃_{y \in (B \cap ℂ) ∖ \{A\}} \{\|y - A\|\}$
	cnrefiisplem.x	$⊢ X = sup (D ℝ^{*} <)$
Assertion	cnrefiisplem	$⊢ φ \to \exists x \in ℝ^{+} \forall y \in C ((y \in ℂ \land y \neq A) \to x \leq \|y - A\|)$

Proof

Step	Hyp	Ref	Expression
1		cnrefiisplem.a	$⊢ φ \to A \in ℂ$
2		cnrefiisplem.n	$⊢ φ \to \neg A \in ℝ$
3		cnrefiisplem.b	$⊢ φ \to B \in Fin$
4		cnrefiisplem.c	$⊢ C = ℝ \cup B$
5		cnrefiisplem.d	$⊢ D = \{\|ℑ (A)\|\} \cup ⋃_{y \in (B \cap ℂ) ∖ \{A\}} \{\|y - A\|\}$
6		cnrefiisplem.x	$⊢ X = sup (D ℝ^{*} <)$
7		simpr	$⊢ (φ \land w = \|ℑ (A)\|) \to w = \|ℑ (A)\|$
8	1 2	absimnre	$⊢ φ \to \|ℑ (A)\| \in ℝ^{+}$
9	8	adantr	$⊢ (φ \land w = \|ℑ (A)\|) \to \|ℑ (A)\| \in ℝ^{+}$
10	7 9	eqeltrd	$⊢ (φ \land w = \|ℑ (A)\|) \to w \in ℝ^{+}$
11	10	adantlr	$⊢ ((φ \land w \in D) \land w = \|ℑ (A)\|) \to w \in ℝ^{+}$
12		simpll	$⊢ ((φ \land w \in D) \land w \neq \|ℑ (A)\|) \to φ$
13	5	eleq2i	$⊢ w \in D \leftrightarrow w \in (\{\|ℑ (A)\|\} \cup ⋃_{y \in (B \cap ℂ) ∖ \{A\}} \{\|y - A\|\})$
14	13	biimpi	$⊢ w \in D \to w \in (\{\|ℑ (A)\|\} \cup ⋃_{y \in (B \cap ℂ) ∖ \{A\}} \{\|y - A\|\})$
15		nelsn	$⊢ w \neq \|ℑ (A)\| \to \neg w \in \{\|ℑ (A)\|\}$
16		elunnel1	$⊢ (w \in (\{\|ℑ (A)\|\} \cup ⋃_{y \in (B \cap ℂ) ∖ \{A\}} \{\|y - A\|\}) \land \neg w \in \{\|ℑ (A)\|\}) \to w \in ⋃_{y \in (B \cap ℂ) ∖ \{A\}} \{\|y - A\|\}$
17	14 15 16	syl2an	$⊢ (w \in D \land w \neq \|ℑ (A)\|) \to w \in ⋃_{y \in (B \cap ℂ) ∖ \{A\}} \{\|y - A\|\}$
18		eliun	$⊢ w \in ⋃_{y \in (B \cap ℂ) ∖ \{A\}} \{\|y - A\|\} \leftrightarrow \exists y \in ((B \cap ℂ) ∖ \{A\}) w \in \{\|y - A\|\}$
19	17 18	sylib	$⊢ (w \in D \land w \neq \|ℑ (A)\|) \to \exists y \in ((B \cap ℂ) ∖ \{A\}) w \in \{\|y - A\|\}$
20		velsn	$⊢ w \in \{\|y - A\|\} \leftrightarrow w = \|y - A\|$
21	20	rexbii	$⊢ \exists y \in ((B \cap ℂ) ∖ \{A\}) w \in \{\|y - A\|\} \leftrightarrow \exists y \in ((B \cap ℂ) ∖ \{A\}) w = \|y - A\|$
22	19 21	sylib	$⊢ (w \in D \land w \neq \|ℑ (A)\|) \to \exists y \in ((B \cap ℂ) ∖ \{A\}) w = \|y - A\|$
23	22	adantll	$⊢ ((φ \land w \in D) \land w \neq \|ℑ (A)\|) \to \exists y \in ((B \cap ℂ) ∖ \{A\}) w = \|y - A\|$
24		simpr	$⊢ ((φ \land y \in ((B \cap ℂ) ∖ \{A\})) \land w = \|y - A\|) \to w = \|y - A\|$
25		eldifi	$⊢ y \in ((B \cap ℂ) ∖ \{A\}) \to y \in (B \cap ℂ)$
26	25	elin2d	$⊢ y \in ((B \cap ℂ) ∖ \{A\}) \to y \in ℂ$
27	26	ad2antlr	$⊢ ((φ \land y \in ((B \cap ℂ) ∖ \{A\})) \land w = \|y - A\|) \to y \in ℂ$
28	1	ad2antrr	$⊢ ((φ \land y \in ((B \cap ℂ) ∖ \{A\})) \land w = \|y - A\|) \to A \in ℂ$
29	27 28	subcld	$⊢ ((φ \land y \in ((B \cap ℂ) ∖ \{A\})) \land w = \|y - A\|) \to y - A \in ℂ$
30		eldifsni	$⊢ y \in ((B \cap ℂ) ∖ \{A\}) \to y \neq A$
31	30	ad2antlr	$⊢ ((φ \land y \in ((B \cap ℂ) ∖ \{A\})) \land w = \|y - A\|) \to y \neq A$
32	27 28 31	subne0d	$⊢ ((φ \land y \in ((B \cap ℂ) ∖ \{A\})) \land w = \|y - A\|) \to y - A \neq 0$
33	29 32	absrpcld	$⊢ ((φ \land y \in ((B \cap ℂ) ∖ \{A\})) \land w = \|y - A\|) \to \|y - A\| \in ℝ^{+}$
34	24 33	eqeltrd	$⊢ ((φ \land y \in ((B \cap ℂ) ∖ \{A\})) \land w = \|y - A\|) \to w \in ℝ^{+}$
35	34	rexlimdva2	$⊢ φ \to (\exists y \in ((B \cap ℂ) ∖ \{A\}) w = \|y - A\| \to w \in ℝ^{+})$
36	12 23 35	sylc	$⊢ ((φ \land w \in D) \land w \neq \|ℑ (A)\|) \to w \in ℝ^{+}$
37	11 36	pm2.61dane	$⊢ (φ \land w \in D) \to w \in ℝ^{+}$
38	37	ssd	$⊢ φ \to D \subseteq ℝ^{+}$
39		xrltso	$⊢ < Or ℝ^{*}$
40	39	a1i	$⊢ φ \to < Or ℝ^{*}$
41		snfi	$⊢ \{\|ℑ (A)\|\} \in Fin$
42	41	a1i	$⊢ φ \to \{\|ℑ (A)\|\} \in Fin$
43		inss1	$⊢ B \cap ℂ \subseteq B$
44	43	a1i	$⊢ φ \to B \cap ℂ \subseteq B$
45	44	ssdifssd	$⊢ φ \to (B \cap ℂ) ∖ \{A\} \subseteq B$
46	3 45	ssfid	$⊢ φ \to (B \cap ℂ) ∖ \{A\} \in Fin$
47		snfi	$⊢ \{\|y - A\|\} \in Fin$
48	47	rgenw	$⊢ \forall y \in ((B \cap ℂ) ∖ \{A\}) \{\|y - A\|\} \in Fin$
49		iunfi	$⊢ ((B \cap ℂ) ∖ \{A\} \in Fin \land \forall y \in ((B \cap ℂ) ∖ \{A\}) \{\|y - A\|\} \in Fin) \to ⋃_{y \in (B \cap ℂ) ∖ \{A\}} \{\|y - A\|\} \in Fin$
50	46 48 49	sylancl	$⊢ φ \to ⋃_{y \in (B \cap ℂ) ∖ \{A\}} \{\|y - A\|\} \in Fin$
51	42 50	unfid	$⊢ φ \to \{\|ℑ (A)\|\} \cup ⋃_{y \in (B \cap ℂ) ∖ \{A\}} \{\|y - A\|\} \in Fin$
52	5 51	eqeltrid	$⊢ φ \to D \in Fin$
53		fvex	$⊢ \|ℑ (A)\| \in V$
54	53	snid	$⊢ \|ℑ (A)\| \in \{\|ℑ (A)\|\}$
55		elun1	$⊢ \|ℑ (A)\| \in \{\|ℑ (A)\|\} \to \|ℑ (A)\| \in (\{\|ℑ (A)\|\} \cup ⋃_{y \in (B \cap ℂ) ∖ \{A\}} \{\|y - A\|\})$
56	54 55	ax-mp	$⊢ \|ℑ (A)\| \in (\{\|ℑ (A)\|\} \cup ⋃_{y \in (B \cap ℂ) ∖ \{A\}} \{\|y - A\|\})$
57	56 5	eleqtrri	$⊢ \|ℑ (A)\| \in D$
58	57	a1i	$⊢ φ \to \|ℑ (A)\| \in D$
59	58	ne0d	$⊢ φ \to D \neq \emptyset$
60		rpssxr	$⊢ ℝ^{+} \subseteq ℝ^{*}$
61	38 60	sstrdi	$⊢ φ \to D \subseteq ℝ^{*}$
62		fiinfcl	$⊢ (< Or ℝ^{} \land (D \in Fin \land D \neq \emptyset \land D \subseteq ℝ^{})) \to sup (D ℝ^{*} <) \in D$
63	40 52 59 61 62	syl13anc	$⊢ φ \to sup (D ℝ^{*} <) \in D$
64	6 63	eqeltrid	$⊢ φ \to X \in D$
65	38 64	sseldd	$⊢ φ \to X \in ℝ^{+}$
66	38 63	sseldd	$⊢ φ \to sup (D ℝ^{*} <) \in ℝ^{+}$
67	66	rpred	$⊢ φ \to sup (D ℝ^{*} <) \in ℝ$
68	67	adantr	$⊢ (φ \land y \in ℝ) \to sup (D ℝ^{*} <) \in ℝ$
69	1	imcld	$⊢ φ \to ℑ (A) \in ℝ$
70	69	recnd	$⊢ φ \to ℑ (A) \in ℂ$
71	70	adantr	$⊢ (φ \land y \in ℝ) \to ℑ (A) \in ℂ$
72	71	abscld	$⊢ (φ \land y \in ℝ) \to \|ℑ (A)\| \in ℝ$
73		recn	$⊢ y \in ℝ \to y \in ℂ$
74	73	adantl	$⊢ (φ \land y \in ℝ) \to y \in ℂ$
75	1	adantr	$⊢ (φ \land y \in ℝ) \to A \in ℂ$
76	74 75	subcld	$⊢ (φ \land y \in ℝ) \to y - A \in ℂ$
77	76	abscld	$⊢ (φ \land y \in ℝ) \to \|y - A\| \in ℝ$
78	61	adantr	$⊢ (φ \land y \in ℝ) \to D \subseteq ℝ^{*}$
79		infxrlb	$⊢ (D \subseteq ℝ^{} \land \|ℑ (A)\| \in D) \to sup (D ℝ^{} <) \leq \|ℑ (A)\|$
80	78 57 79	sylancl	$⊢ (φ \land y \in ℝ) \to sup (D ℝ^{*} <) \leq \|ℑ (A)\|$
81		simpr	$⊢ (φ \land y \in ℝ) \to y \in ℝ$
82	75 81	absimlere	$⊢ (φ \land y \in ℝ) \to \|ℑ (A)\| \leq \|y - A\|$
83	68 72 77 80 82	letrd	$⊢ (φ \land y \in ℝ) \to sup (D ℝ^{*} <) \leq \|y - A\|$
84	6 83	eqbrtrid	$⊢ (φ \land y \in ℝ) \to X \leq \|y - A\|$
85	84	ad4ant14	$⊢ (((φ \land y \in C) \land (y \in ℂ \land y \neq A)) \land y \in ℝ) \to X \leq \|y - A\|$
86	4	eleq2i	$⊢ y \in C \leftrightarrow y \in (ℝ \cup B)$
87		elunnel1	$⊢ (y \in (ℝ \cup B) \land \neg y \in ℝ) \to y \in B$
88	86 87	sylanb	$⊢ (y \in C \land \neg y \in ℝ) \to y \in B$
89	88	ad4ant24	$⊢ (((φ \land y \in C) \land (y \in ℂ \land y \neq A)) \land \neg y \in ℝ) \to y \in B$
90	61	ad2antrr	$⊢ ((φ \land (y \in ℂ \land y \neq A)) \land y \in B) \to D \subseteq ℝ^{*}$
91		simpr	$⊢ ((y \in ℂ \land y \neq A) \land y \in B) \to y \in B$
92		simpll	$⊢ ((y \in ℂ \land y \neq A) \land y \in B) \to y \in ℂ$
93	91 92	elind	$⊢ ((y \in ℂ \land y \neq A) \land y \in B) \to y \in (B \cap ℂ)$
94		nelsn	$⊢ y \neq A \to \neg y \in \{A\}$
95	94	ad2antlr	$⊢ ((y \in ℂ \land y \neq A) \land y \in B) \to \neg y \in \{A\}$
96	93 95	eldifd	$⊢ ((y \in ℂ \land y \neq A) \land y \in B) \to y \in ((B \cap ℂ) ∖ \{A\})$
97		fvex	$⊢ \|y - A\| \in V$
98	97	snid	$⊢ \|y - A\| \in \{\|y - A\|\}$
99		fvoveq1	$⊢ w = y \to \|w - A\| = \|y - A\|$
100	99	sneqd	$⊢ w = y \to \{\|w - A\|\} = \{\|y - A\|\}$
101	100	eliuni	$⊢ (y \in ((B \cap ℂ) ∖ \{A\}) \land \|y - A\| \in \{\|y - A\|\}) \to \|y - A\| \in ⋃_{w \in (B \cap ℂ) ∖ \{A\}} \{\|w - A\|\}$
102	96 98 101	sylancl	$⊢ ((y \in ℂ \land y \neq A) \land y \in B) \to \|y - A\| \in ⋃_{w \in (B \cap ℂ) ∖ \{A\}} \{\|w - A\|\}$
103	100	cbviunv	$⊢ ⋃_{w \in (B \cap ℂ) ∖ \{A\}} \{\|w - A\|\} = ⋃_{y \in (B \cap ℂ) ∖ \{A\}} \{\|y - A\|\}$
104	102 103	eleqtrdi	$⊢ ((y \in ℂ \land y \neq A) \land y \in B) \to \|y - A\| \in ⋃_{y \in (B \cap ℂ) ∖ \{A\}} \{\|y - A\|\}$
105		elun2	$⊢ \|y - A\| \in ⋃_{y \in (B \cap ℂ) ∖ \{A\}} \{\|y - A\|\} \to \|y - A\| \in (\{\|ℑ (A)\|\} \cup ⋃_{y \in (B \cap ℂ) ∖ \{A\}} \{\|y - A\|\})$
106	104 105	syl	$⊢ ((y \in ℂ \land y \neq A) \land y \in B) \to \|y - A\| \in (\{\|ℑ (A)\|\} \cup ⋃_{y \in (B \cap ℂ) ∖ \{A\}} \{\|y - A\|\})$
107	106 5	eleqtrrdi	$⊢ ((y \in ℂ \land y \neq A) \land y \in B) \to \|y - A\| \in D$
108	107	adantll	$⊢ ((φ \land (y \in ℂ \land y \neq A)) \land y \in B) \to \|y - A\| \in D$
109		infxrlb	$⊢ (D \subseteq ℝ^{} \land \|y - A\| \in D) \to sup (D ℝ^{} <) \leq \|y - A\|$
110	90 108 109	syl2anc	$⊢ ((φ \land (y \in ℂ \land y \neq A)) \land y \in B) \to sup (D ℝ^{*} <) \leq \|y - A\|$
111	6 110	eqbrtrid	$⊢ ((φ \land (y \in ℂ \land y \neq A)) \land y \in B) \to X \leq \|y - A\|$
112	111	adantllr	$⊢ (((φ \land y \in C) \land (y \in ℂ \land y \neq A)) \land y \in B) \to X \leq \|y - A\|$
113	89 112	syldan	$⊢ (((φ \land y \in C) \land (y \in ℂ \land y \neq A)) \land \neg y \in ℝ) \to X \leq \|y - A\|$
114	85 113	pm2.61dan	$⊢ ((φ \land y \in C) \land (y \in ℂ \land y \neq A)) \to X \leq \|y - A\|$
115	114	ex	$⊢ (φ \land y \in C) \to ((y \in ℂ \land y \neq A) \to X \leq \|y - A\|)$
116	115	ralrimiva	$⊢ φ \to \forall y \in C ((y \in ℂ \land y \neq A) \to X \leq \|y - A\|)$
117		breq1	$⊢ x = X \to (x \leq \|y - A\| \leftrightarrow X \leq \|y - A\|)$
118	117	imbi2d	$⊢ x = X \to (((y \in ℂ \land y \neq A) \to x \leq \|y - A\|) \leftrightarrow ((y \in ℂ \land y \neq A) \to X \leq \|y - A\|))$
119	118	ralbidv	$⊢ x = X \to (\forall y \in C ((y \in ℂ \land y \neq A) \to x \leq \|y - A\|) \leftrightarrow \forall y \in C ((y \in ℂ \land y \neq A) \to X \leq \|y - A\|))$
120	119	rspcev	$⊢ (X \in ℝ^{+} \land \forall y \in C ((y \in ℂ \land y \neq A) \to X \leq \|y - A\|)) \to \exists x \in ℝ^{+} \forall y \in C ((y \in ℂ \land y \neq A) \to x \leq \|y - A\|)$
121	65 116 120	syl2anc	$⊢ φ \to \exists x \in ℝ^{+} \forall y \in C ((y \in ℂ \land y \neq A) \to x \leq \|y - A\|)$

Metamath Proof Explorer

Theorem cnrefiisplem

Proof