This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ ( 𝐴 − 𝑦 ) ) )