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 
|- ( ph -> A e. ( CC \ RR ) )
Assertion dstregt0 
|- ( ph -> E. x e. RR+ A. y e. RR x < ( abs ` ( A - y ) ) )

Proof

Step Hyp Ref Expression
1 dstregt0.1 
 |-  ( ph -> A e. ( CC \ RR ) )
2 1 eldifad 
 |-  ( ph -> A e. CC )
3 2 imcld 
 |-  ( ph -> ( Im ` A ) e. RR )
4 3 recnd 
 |-  ( ph -> ( Im ` A ) e. CC )
5 1 eldifbd 
 |-  ( ph -> -. A e. RR )
6 reim0b 
 |-  ( A e. CC -> ( A e. RR <-> ( Im ` A ) = 0 ) )
7 2 6 syl 
 |-  ( ph -> ( A e. RR <-> ( Im ` A ) = 0 ) )
8 5 7 mtbid 
 |-  ( ph -> -. ( Im ` A ) = 0 )
9 8 neqned 
 |-  ( ph -> ( Im ` A ) =/= 0 )
10 4 9 absrpcld 
 |-  ( ph -> ( abs ` ( Im ` A ) ) e. RR+ )
11 10 rphalfcld 
 |-  ( ph -> ( ( abs ` ( Im ` A ) ) / 2 ) e. RR+ )
12 2 adantr 
 |-  ( ( ph /\ y e. RR ) -> A e. CC )
13 recn 
 |-  ( y e. RR -> y e. CC )
14 13 adantl 
 |-  ( ( ph /\ y e. RR ) -> y e. CC )
15 12 14 imsubd 
 |-  ( ( ph /\ y e. RR ) -> ( Im ` ( A - y ) ) = ( ( Im ` A ) - ( Im ` y ) ) )
16 simpr 
 |-  ( ( ph /\ y e. RR ) -> y e. RR )
17 16 reim0d 
 |-  ( ( ph /\ y e. RR ) -> ( Im ` y ) = 0 )
18 17 oveq2d 
 |-  ( ( ph /\ y e. RR ) -> ( ( Im ` A ) - ( Im ` y ) ) = ( ( Im ` A ) - 0 ) )
19 4 adantr 
 |-  ( ( ph /\ y e. RR ) -> ( Im ` A ) e. CC )
20 19 subid1d 
 |-  ( ( ph /\ y e. RR ) -> ( ( Im ` A ) - 0 ) = ( Im ` A ) )
21 15 18 20 3eqtrrd 
 |-  ( ( ph /\ y e. RR ) -> ( Im ` A ) = ( Im ` ( A - y ) ) )
22 21 fveq2d 
 |-  ( ( ph /\ y e. RR ) -> ( abs ` ( Im ` A ) ) = ( abs ` ( Im ` ( A - y ) ) ) )
23 22 oveq1d 
 |-  ( ( ph /\ y e. RR ) -> ( ( abs ` ( Im ` A ) ) / 2 ) = ( ( abs ` ( Im ` ( A - y ) ) ) / 2 ) )
24 21 19 eqeltrrd 
 |-  ( ( ph /\ y e. RR ) -> ( Im ` ( A - y ) ) e. CC )
25 24 abscld 
 |-  ( ( ph /\ y e. RR ) -> ( abs ` ( Im ` ( A - y ) ) ) e. RR )
26 25 rehalfcld 
 |-  ( ( ph /\ y e. RR ) -> ( ( abs ` ( Im ` ( A - y ) ) ) / 2 ) e. RR )
27 12 14 subcld 
 |-  ( ( ph /\ y e. RR ) -> ( A - y ) e. CC )
28 27 abscld 
 |-  ( ( ph /\ y e. RR ) -> ( abs ` ( A - y ) ) e. RR )
29 9 adantr 
 |-  ( ( ph /\ y e. RR ) -> ( Im ` A ) =/= 0 )
30 21 29 eqnetrrd 
 |-  ( ( ph /\ y e. RR ) -> ( Im ` ( A - y ) ) =/= 0 )
31 24 30 absrpcld 
 |-  ( ( ph /\ y e. RR ) -> ( abs ` ( Im ` ( A - y ) ) ) e. RR+ )
32 rphalflt 
 |-  ( ( abs ` ( Im ` ( A - y ) ) ) e. RR+ -> ( ( abs ` ( Im ` ( A - y ) ) ) / 2 ) < ( abs ` ( Im ` ( A - y ) ) ) )
33 31 32 syl 
 |-  ( ( ph /\ y e. RR ) -> ( ( abs ` ( Im ` ( A - y ) ) ) / 2 ) < ( abs ` ( Im ` ( A - y ) ) ) )
34 absimle 
 |-  ( ( A - y ) e. CC -> ( abs ` ( Im ` ( A - y ) ) ) <_ ( abs ` ( A - y ) ) )
35 27 34 syl 
 |-  ( ( ph /\ y e. RR ) -> ( abs ` ( Im ` ( A - y ) ) ) <_ ( abs ` ( A - y ) ) )
36 26 25 28 33 35 ltletrd 
 |-  ( ( ph /\ y e. RR ) -> ( ( abs ` ( Im ` ( A - y ) ) ) / 2 ) < ( abs ` ( A - y ) ) )
37 23 36 eqbrtrd 
 |-  ( ( ph /\ y e. RR ) -> ( ( abs ` ( Im ` A ) ) / 2 ) < ( abs ` ( A - y ) ) )
38 37 ralrimiva 
 |-  ( ph -> A. y e. RR ( ( abs ` ( Im ` A ) ) / 2 ) < ( abs ` ( A - y ) ) )
39 breq1 
 |-  ( x = ( ( abs ` ( Im ` A ) ) / 2 ) -> ( x < ( abs ` ( A - y ) ) <-> ( ( abs ` ( Im ` A ) ) / 2 ) < ( abs ` ( A - y ) ) ) )
40 39 ralbidv 
 |-  ( x = ( ( abs ` ( Im ` A ) ) / 2 ) -> ( A. y e. RR x < ( abs ` ( A - y ) ) <-> A. y e. RR ( ( abs ` ( Im ` A ) ) / 2 ) < ( abs ` ( A - y ) ) ) )
41 40 rspcev 
 |-  ( ( ( ( abs ` ( Im ` A ) ) / 2 ) e. RR+ /\ A. y e. RR ( ( abs ` ( Im ` A ) ) / 2 ) < ( abs ` ( A - y ) ) ) -> E. x e. RR+ A. y e. RR x < ( abs ` ( A - y ) ) )
42 11 38 41 syl2anc 
 |-  ( ph -> E. x e. RR+ A. y e. RR x < ( abs ` ( A - y ) ) )