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	⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ℝ ) )
Assertion	dstregt0	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐴 − 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dstregt0.1	⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ℝ ) )
2	1	eldifad	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
3	2	imcld	⊢ ( 𝜑 → ( ℑ ‘ 𝐴 ) ∈ ℝ )
4	3	recnd	⊢ ( 𝜑 → ( ℑ ‘ 𝐴 ) ∈ ℂ )
5	1	eldifbd	⊢ ( 𝜑 → ¬ 𝐴 ∈ ℝ )
6		reim0b	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( ℑ ‘ 𝐴 ) = 0 ) )
7	2 6	syl	⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ↔ ( ℑ ‘ 𝐴 ) = 0 ) )
8	5 7	mtbid	⊢ ( 𝜑 → ¬ ( ℑ ‘ 𝐴 ) = 0 )
9	8	neqned	⊢ ( 𝜑 → ( ℑ ‘ 𝐴 ) ≠ 0 )
10	4 9	absrpcld	⊢ ( 𝜑 → ( abs ‘ ( ℑ ‘ 𝐴 ) ) ∈ ℝ+ )
11	10	rphalfcld	⊢ ( 𝜑 → ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) ∈ ℝ+ )
12	2	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐴 ∈ ℂ )
13		recn	⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
15	12 14	imsubd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ℑ ‘ ( 𝐴 − 𝑦 ) ) = ( ( ℑ ‘ 𝐴 ) − ( ℑ ‘ 𝑦 ) ) )
16		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
17	16	reim0d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ℑ ‘ 𝑦 ) = 0 )
18	17	oveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ℑ ‘ 𝐴 ) − ( ℑ ‘ 𝑦 ) ) = ( ( ℑ ‘ 𝐴 ) − 0 ) )
19	4	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ℑ ‘ 𝐴 ) ∈ ℂ )
20	19	subid1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ℑ ‘ 𝐴 ) − 0 ) = ( ℑ ‘ 𝐴 ) )
21	15 18 20	3eqtrrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ℑ ‘ 𝐴 ) = ( ℑ ‘ ( 𝐴 − 𝑦 ) ) )
22	21	fveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( abs ‘ ( ℑ ‘ 𝐴 ) ) = ( abs ‘ ( ℑ ‘ ( 𝐴 − 𝑦 ) ) ) )
23	22	oveq1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) = ( ( abs ‘ ( ℑ ‘ ( 𝐴 − 𝑦 ) ) ) / 2 ) )
24	21 19	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ℑ ‘ ( 𝐴 − 𝑦 ) ) ∈ ℂ )
25	24	abscld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( abs ‘ ( ℑ ‘ ( 𝐴 − 𝑦 ) ) ) ∈ ℝ )
26	25	rehalfcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( abs ‘ ( ℑ ‘ ( 𝐴 − 𝑦 ) ) ) / 2 ) ∈ ℝ )
27	12 14	subcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐴 − 𝑦 ) ∈ ℂ )
28	27	abscld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( abs ‘ ( 𝐴 − 𝑦 ) ) ∈ ℝ )
29	9	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ℑ ‘ 𝐴 ) ≠ 0 )
30	21 29	eqnetrrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ℑ ‘ ( 𝐴 − 𝑦 ) ) ≠ 0 )
31	24 30	absrpcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( abs ‘ ( ℑ ‘ ( 𝐴 − 𝑦 ) ) ) ∈ ℝ+ )
32		rphalflt	⊢ ( ( abs ‘ ( ℑ ‘ ( 𝐴 − 𝑦 ) ) ) ∈ ℝ+ → ( ( abs ‘ ( ℑ ‘ ( 𝐴 − 𝑦 ) ) ) / 2 ) < ( abs ‘ ( ℑ ‘ ( 𝐴 − 𝑦 ) ) ) )
33	31 32	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( abs ‘ ( ℑ ‘ ( 𝐴 − 𝑦 ) ) ) / 2 ) < ( abs ‘ ( ℑ ‘ ( 𝐴 − 𝑦 ) ) ) )
34		absimle	⊢ ( ( 𝐴 − 𝑦 ) ∈ ℂ → ( abs ‘ ( ℑ ‘ ( 𝐴 − 𝑦 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑦 ) ) )
35	27 34	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( abs ‘ ( ℑ ‘ ( 𝐴 − 𝑦 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑦 ) ) )
36	26 25 28 33 35	ltletrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( abs ‘ ( ℑ ‘ ( 𝐴 − 𝑦 ) ) ) / 2 ) < ( abs ‘ ( 𝐴 − 𝑦 ) ) )
37	23 36	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) < ( abs ‘ ( 𝐴 − 𝑦 ) ) )
38	37	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) < ( abs ‘ ( 𝐴 − 𝑦 ) ) )
39		breq1	⊢ ( 𝑥 = ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) → ( 𝑥 < ( abs ‘ ( 𝐴 − 𝑦 ) ) ↔ ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) < ( abs ‘ ( 𝐴 − 𝑦 ) ) ) )
40	39	ralbidv	⊢ ( 𝑥 = ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) → ( ∀ 𝑦 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐴 − 𝑦 ) ) ↔ ∀ 𝑦 ∈ ℝ ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) < ( abs ‘ ( 𝐴 − 𝑦 ) ) ) )
41	40	rspcev	⊢ ( ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) ∈ ℝ+ ∧ ∀ 𝑦 ∈ ℝ ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) < ( abs ‘ ( 𝐴 − 𝑦 ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐴 − 𝑦 ) ) )
42	11 38 41	syl2anc	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐴 − 𝑦 ) ) )