Theorem 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	$$⊢\phi \to A\in \left(ℂ\setminus ℝ\right)$$
Assertion	dstregt0	$$⊢\phi \to \exists x\in {ℝ}^{+}\forall y\in ℝx<\left|A-y\right|$$

Proof

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