Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dstregt0 Structured version   Visualization version   GIF version

Theorem dstregt0 42751
Description: A complex number 𝐴 that is not real, has a distance from the reals that is strictly larger than 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
dstregt0.1 (𝜑𝐴 ∈ (ℂ ∖ ℝ))
Assertion
Ref Expression
dstregt0 (𝜑 → ∃𝑥 ∈ ℝ+𝑦 ∈ ℝ 𝑥 < (abs‘(𝐴𝑦)))
Distinct variable groups:   𝑥,𝐴,𝑦   𝜑,𝑦
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem dstregt0
StepHypRef Expression
1 dstregt0.1 . . . . . . 7 (𝜑𝐴 ∈ (ℂ ∖ ℝ))
21eldifad 3900 . . . . . 6 (𝜑𝐴 ∈ ℂ)
32imcld 14850 . . . . 5 (𝜑 → (ℑ‘𝐴) ∈ ℝ)
43recnd 10950 . . . 4 (𝜑 → (ℑ‘𝐴) ∈ ℂ)
51eldifbd 3901 . . . . . 6 (𝜑 → ¬ 𝐴 ∈ ℝ)
6 reim0b 14774 . . . . . . 7 (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0))
72, 6syl 17 . . . . . 6 (𝜑 → (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0))
85, 7mtbid 323 . . . . 5 (𝜑 → ¬ (ℑ‘𝐴) = 0)
98neqned 2948 . . . 4 (𝜑 → (ℑ‘𝐴) ≠ 0)
104, 9absrpcld 15104 . . 3 (𝜑 → (abs‘(ℑ‘𝐴)) ∈ ℝ+)
1110rphalfcld 12729 . 2 (𝜑 → ((abs‘(ℑ‘𝐴)) / 2) ∈ ℝ+)
122adantr 480 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → 𝐴 ∈ ℂ)
13 recn 10908 . . . . . . . . 9 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
1413adantl 481 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
1512, 14imsubd 14872 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → (ℑ‘(𝐴𝑦)) = ((ℑ‘𝐴) − (ℑ‘𝑦)))
16 simpr 484 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
1716reim0d 14880 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (ℑ‘𝑦) = 0)
1817oveq2d 7276 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((ℑ‘𝐴) − (ℑ‘𝑦)) = ((ℑ‘𝐴) − 0))
194adantr 480 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (ℑ‘𝐴) ∈ ℂ)
2019subid1d 11267 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → ((ℑ‘𝐴) − 0) = (ℑ‘𝐴))
2115, 18, 203eqtrrd 2782 . . . . . 6 ((𝜑𝑦 ∈ ℝ) → (ℑ‘𝐴) = (ℑ‘(𝐴𝑦)))
2221fveq2d 6765 . . . . 5 ((𝜑𝑦 ∈ ℝ) → (abs‘(ℑ‘𝐴)) = (abs‘(ℑ‘(𝐴𝑦))))
2322oveq1d 7275 . . . 4 ((𝜑𝑦 ∈ ℝ) → ((abs‘(ℑ‘𝐴)) / 2) = ((abs‘(ℑ‘(𝐴𝑦))) / 2))
2421, 19eqeltrrd 2838 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → (ℑ‘(𝐴𝑦)) ∈ ℂ)
2524abscld 15092 . . . . . 6 ((𝜑𝑦 ∈ ℝ) → (abs‘(ℑ‘(𝐴𝑦))) ∈ ℝ)
2625rehalfcld 12166 . . . . 5 ((𝜑𝑦 ∈ ℝ) → ((abs‘(ℑ‘(𝐴𝑦))) / 2) ∈ ℝ)
2712, 14subcld 11278 . . . . . 6 ((𝜑𝑦 ∈ ℝ) → (𝐴𝑦) ∈ ℂ)
2827abscld 15092 . . . . 5 ((𝜑𝑦 ∈ ℝ) → (abs‘(𝐴𝑦)) ∈ ℝ)
299adantr 480 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ) → (ℑ‘𝐴) ≠ 0)
3021, 29eqnetrrd 3010 . . . . . . 7 ((𝜑𝑦 ∈ ℝ) → (ℑ‘(𝐴𝑦)) ≠ 0)
3124, 30absrpcld 15104 . . . . . 6 ((𝜑𝑦 ∈ ℝ) → (abs‘(ℑ‘(𝐴𝑦))) ∈ ℝ+)
32 rphalflt 12704 . . . . . 6 ((abs‘(ℑ‘(𝐴𝑦))) ∈ ℝ+ → ((abs‘(ℑ‘(𝐴𝑦))) / 2) < (abs‘(ℑ‘(𝐴𝑦))))
3331, 32syl 17 . . . . 5 ((𝜑𝑦 ∈ ℝ) → ((abs‘(ℑ‘(𝐴𝑦))) / 2) < (abs‘(ℑ‘(𝐴𝑦))))
34 absimle 14965 . . . . . 6 ((𝐴𝑦) ∈ ℂ → (abs‘(ℑ‘(𝐴𝑦))) ≤ (abs‘(𝐴𝑦)))
3527, 34syl 17 . . . . 5 ((𝜑𝑦 ∈ ℝ) → (abs‘(ℑ‘(𝐴𝑦))) ≤ (abs‘(𝐴𝑦)))
3626, 25, 28, 33, 35ltletrd 11081 . . . 4 ((𝜑𝑦 ∈ ℝ) → ((abs‘(ℑ‘(𝐴𝑦))) / 2) < (abs‘(𝐴𝑦)))
3723, 36eqbrtrd 5097 . . 3 ((𝜑𝑦 ∈ ℝ) → ((abs‘(ℑ‘𝐴)) / 2) < (abs‘(𝐴𝑦)))
3837ralrimiva 3106 . 2 (𝜑 → ∀𝑦 ∈ ℝ ((abs‘(ℑ‘𝐴)) / 2) < (abs‘(𝐴𝑦)))
39 breq1 5078 . . . 4 (𝑥 = ((abs‘(ℑ‘𝐴)) / 2) → (𝑥 < (abs‘(𝐴𝑦)) ↔ ((abs‘(ℑ‘𝐴)) / 2) < (abs‘(𝐴𝑦))))
4039ralbidv 3119 . . 3 (𝑥 = ((abs‘(ℑ‘𝐴)) / 2) → (∀𝑦 ∈ ℝ 𝑥 < (abs‘(𝐴𝑦)) ↔ ∀𝑦 ∈ ℝ ((abs‘(ℑ‘𝐴)) / 2) < (abs‘(𝐴𝑦))))
4140rspcev 3557 . 2 ((((abs‘(ℑ‘𝐴)) / 2) ∈ ℝ+ ∧ ∀𝑦 ∈ ℝ ((abs‘(ℑ‘𝐴)) / 2) < (abs‘(𝐴𝑦))) → ∃𝑥 ∈ ℝ+𝑦 ∈ ℝ 𝑥 < (abs‘(𝐴𝑦)))
4211, 38, 41syl2anc 583 1 (𝜑 → ∃𝑥 ∈ ℝ+𝑦 ∈ ℝ 𝑥 < (abs‘(𝐴𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395   = wceq 1539  wcel 2107  wne 2941  wral 3062  wrex 3063  cdif 3885   class class class wbr 5075  cfv 6423  (class class class)co 7260  cc 10816  cr 10817  0cc0 10818   < clt 10956  cle 10957  cmin 11151   / cdiv 11578  2c2 11974  +crp 12675  cim 14753  abscabs 14889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7571  ax-cnex 10874  ax-resscn 10875  ax-1cn 10876  ax-icn 10877  ax-addcl 10878  ax-addrcl 10879  ax-mulcl 10880  ax-mulrcl 10881  ax-mulcom 10882  ax-addass 10883  ax-mulass 10884  ax-distr 10885  ax-i2m1 10886  ax-1ne0 10887  ax-1rid 10888  ax-rnegex 10889  ax-rrecex 10890  ax-cnre 10891  ax-pre-lttri 10892  ax-pre-lttrn 10893  ax-pre-ltadd 10894  ax-pre-mulgt0 10895  ax-pre-sup 10896
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3429  df-sbc 3717  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4842  df-iun 4928  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5485  df-eprel 5491  df-po 5499  df-so 5500  df-fr 5540  df-we 5542  df-xp 5591  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-res 5597  df-ima 5598  df-pred 6196  df-ord 6259  df-on 6260  df-lim 6261  df-suc 6262  df-iota 6381  df-fun 6425  df-fn 6426  df-f 6427  df-f1 6428  df-fo 6429  df-f1o 6430  df-fv 6431  df-riota 7217  df-ov 7263  df-oprab 7264  df-mpo 7265  df-om 7693  df-2nd 7810  df-frecs 8073  df-wrecs 8104  df-recs 8178  df-rdg 8217  df-er 8461  df-en 8697  df-dom 8698  df-sdom 8699  df-sup 9147  df-pnf 10958  df-mnf 10959  df-xr 10960  df-ltxr 10961  df-le 10962  df-sub 11153  df-neg 11154  df-div 11579  df-nn 11920  df-2 11982  df-3 11983  df-n0 12180  df-z 12266  df-uz 12528  df-rp 12676  df-seq 13666  df-exp 13727  df-cj 14754  df-re 14755  df-im 14756  df-sqrt 14890  df-abs 14891
This theorem is referenced by:  limcrecl  43102
  Copyright terms: Public domain W3C validator