dstregt0

Description: A complex number A that is not real, has a distance from the reals that is strictly larger than 0 . (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Hypothesis	dstregt0.1	$⊢ φ \to A \in (ℂ ∖ ℝ)$
	Assertion	dstregt0	$⊢ φ \to \exists x \in ℝ^{+} \forall y \in ℝ x < \|A - y\|$

Proof

Step	Hyp	Ref	Expression
1		dstregt0.1	$⊢ φ \to A \in (ℂ ∖ ℝ)$
2	1	eldifad	$⊢ φ \to A \in ℂ$
3	2	imcld	$⊢ φ \to ℑ (A) \in ℝ$
4	3	recnd	$⊢ φ \to ℑ (A) \in ℂ$
5	1	eldifbd	$⊢ φ \to \neg A \in ℝ$
6		reim0b	$⊢ A \in ℂ \to (A \in ℝ \leftrightarrow ℑ (A) = 0)$
7	2 6	syl	$⊢ φ \to (A \in ℝ \leftrightarrow ℑ (A) = 0)$
8	5 7	mtbid	$⊢ φ \to \neg ℑ (A) = 0$
9	8	neqned	$⊢ φ \to ℑ (A) \neq 0$
10	4 9	absrpcld	$⊢ φ \to \|ℑ (A)\| \in ℝ^{+}$
11	10	rphalfcld	$⊢ φ \to \frac{\|ℑ (A)\|}{2} \in ℝ^{+}$
12	2	adantr	$⊢ (φ \land y \in ℝ) \to A \in ℂ$
13		recn	$⊢ y \in ℝ \to y \in ℂ$
14	13	adantl	$⊢ (φ \land y \in ℝ) \to y \in ℂ$
15	12 14	imsubd	$⊢ (φ \land y \in ℝ) \to ℑ (A - y) = ℑ (A) - ℑ (y)$
16		simpr	$⊢ (φ \land y \in ℝ) \to y \in ℝ$
17	16	reim0d	$⊢ (φ \land y \in ℝ) \to ℑ (y) = 0$
18	17	oveq2d	$⊢ (φ \land y \in ℝ) \to ℑ (A) - ℑ (y) = ℑ (A) - 0$
19	4	adantr	$⊢ (φ \land y \in ℝ) \to ℑ (A) \in ℂ$
20	19	subid1d	$⊢ (φ \land y \in ℝ) \to ℑ (A) - 0 = ℑ (A)$
21	15 18 20	3eqtrrd	$⊢ (φ \land y \in ℝ) \to ℑ (A) = ℑ (A - y)$
22	21	fveq2d	$⊢ (φ \land y \in ℝ) \to \|ℑ (A)\| = \|ℑ (A - y)\|$
23	22	oveq1d	$⊢ (φ \land y \in ℝ) \to \frac{\|ℑ (A)\|}{2} = \frac{\|ℑ (A - y)\|}{2}$
24	21 19	eqeltrrd	$⊢ (φ \land y \in ℝ) \to ℑ (A - y) \in ℂ$
25	24	abscld	$⊢ (φ \land y \in ℝ) \to \|ℑ (A - y)\| \in ℝ$
26	25	rehalfcld	$⊢ (φ \land y \in ℝ) \to \frac{\|ℑ (A - y)\|}{2} \in ℝ$
27	12 14	subcld	$⊢ (φ \land y \in ℝ) \to A - y \in ℂ$
28	27	abscld	$⊢ (φ \land y \in ℝ) \to \|A - y\| \in ℝ$
29	9	adantr	$⊢ (φ \land y \in ℝ) \to ℑ (A) \neq 0$
30	21 29	eqnetrrd	$⊢ (φ \land y \in ℝ) \to ℑ (A - y) \neq 0$
31	24 30	absrpcld	$⊢ (φ \land y \in ℝ) \to \|ℑ (A - y)\| \in ℝ^{+}$
32		rphalflt	$⊢ \|ℑ (A - y)\| \in ℝ^{+} \to \frac{\|ℑ (A - y)\|}{2} < \|ℑ (A - y)\|$
33	31 32	syl	$⊢ (φ \land y \in ℝ) \to \frac{\|ℑ (A - y)\|}{2} < \|ℑ (A - y)\|$
34		absimle	$⊢ A - y \in ℂ \to \|ℑ (A - y)\| \leq \|A - y\|$
35	27 34	syl	$⊢ (φ \land y \in ℝ) \to \|ℑ (A - y)\| \leq \|A - y\|$
36	26 25 28 33 35	ltletrd	$⊢ (φ \land y \in ℝ) \to \frac{\|ℑ (A - y)\|}{2} < \|A - y\|$
37	23 36	eqbrtrd	$⊢ (φ \land y \in ℝ) \to \frac{\|ℑ (A)\|}{2} < \|A - y\|$
38	37	ralrimiva	$⊢ φ \to \forall y \in ℝ \frac{\|ℑ (A)\|}{2} < \|A - y\|$
39		breq1	$⊢ x = \frac{\|ℑ (A)\|}{2} \to (x < \|A - y\| \leftrightarrow \frac{\|ℑ (A)\|}{2} < \|A - y\|)$
40	39	ralbidv	$⊢ x = \frac{\|ℑ (A)\|}{2} \to (\forall y \in ℝ x < \|A - y\| \leftrightarrow \forall y \in ℝ \frac{\|ℑ (A)\|}{2} < \|A - y\|)$
41	40	rspcev	$⊢ (\frac{\|ℑ (A)\|}{2} \in ℝ^{+} \land \forall y \in ℝ \frac{\|ℑ (A)\|}{2} < \|A - y\|) \to \exists x \in ℝ^{+} \forall y \in ℝ x < \|A - y\|$
42	11 38 41	syl2anc	$⊢ φ \to \exists x \in ℝ^{+} \forall y \in ℝ x < \|A - y\|$

Metamath Proof Explorer

Theorem dstregt0

Proof