Metamath Proof Explorer

Theorem sqrtcvallem1

Description: Two ways of saying a complex number does not lie on the positive real axis. Lemma for sqrtcval . (Contributed by RP, 17-May-2024)

Ref Expression
Hypothesis sqrtcvallem1.1 
|- ( ph -> A e. CC )
Assertion sqrtcvallem1 
|- ( ph -> ( ( ( Im ` A ) = 0 -> ( Re ` A ) <_ 0 ) <-> -. A e. RR+ ) )

Proof

Step Hyp Ref Expression
1 sqrtcvallem1.1 
 |-  ( ph -> A e. CC )
2 eldif 
 |-  ( A e. ( CC \ RR+ ) <-> ( A e. CC /\ -. A e. RR+ ) )
3 2 a1i 
 |-  ( ph -> ( A e. ( CC \ RR+ ) <-> ( A e. CC /\ -. A e. RR+ ) ) )
4 imor 
 |-  ( ( ( Im ` A ) = 0 -> ( Re ` A ) <_ 0 ) <-> ( -. ( Im ` A ) = 0 \/ ( Re ` A ) <_ 0 ) )
5 1 biantrurd 
 |-  ( ph -> ( -. A e. RR <-> ( A e. CC /\ -. A e. RR ) ) )
6 reim0b 
 |-  ( A e. CC -> ( A e. RR <-> ( Im ` A ) = 0 ) )
7 1 6 syl 
 |-  ( ph -> ( A e. RR <-> ( Im ` A ) = 0 ) )
8 7 notbid 
 |-  ( ph -> ( -. A e. RR <-> -. ( Im ` A ) = 0 ) )
9 8 bicomd 
 |-  ( ph -> ( -. ( Im ` A ) = 0 <-> -. A e. RR ) )
10 eleq1 
 |-  ( x = A -> ( x e. RR <-> A e. RR ) )
11 10 notbid 
 |-  ( x = A -> ( -. x e. RR <-> -. A e. RR ) )
12 11 elrab 
 |-  ( A e. { x e. CC | -. x e. RR } <-> ( A e. CC /\ -. A e. RR ) )
13 12 a1i 
 |-  ( ph -> ( A e. { x e. CC | -. x e. RR } <-> ( A e. CC /\ -. A e. RR ) ) )
14 5 9 13 3bitr4d 
 |-  ( ph -> ( -. ( Im ` A ) = 0 <-> A e. { x e. CC | -. x e. RR } ) )
15 1 biantrurd 
 |-  ( ph -> ( -. 0 < ( Re ` A ) <-> ( A e. CC /\ -. 0 < ( Re ` A ) ) ) )
16 1 recld 
 |-  ( ph -> ( Re ` A ) e. RR )
17 0red 
 |-  ( ph -> 0 e. RR )
18 16 17 lenltd 
 |-  ( ph -> ( ( Re ` A ) <_ 0 <-> -. 0 < ( Re ` A ) ) )
19 fveq2 
 |-  ( x = A -> ( Re ` x ) = ( Re ` A ) )
20 19 breq2d 
 |-  ( x = A -> ( 0 < ( Re ` x ) <-> 0 < ( Re ` A ) ) )
21 20 notbid 
 |-  ( x = A -> ( -. 0 < ( Re ` x ) <-> -. 0 < ( Re ` A ) ) )
22 21 elrab 
 |-  ( A e. { x e. CC | -. 0 < ( Re ` x ) } <-> ( A e. CC /\ -. 0 < ( Re ` A ) ) )
23 22 a1i 
 |-  ( ph -> ( A e. { x e. CC | -. 0 < ( Re ` x ) } <-> ( A e. CC /\ -. 0 < ( Re ` A ) ) ) )
24 15 18 23 3bitr4d 
 |-  ( ph -> ( ( Re ` A ) <_ 0 <-> A e. { x e. CC | -. 0 < ( Re ` x ) } ) )
25 14 24 orbi12d 
 |-  ( ph -> ( ( -. ( Im ` A ) = 0 \/ ( Re ` A ) <_ 0 ) <-> ( A e. { x e. CC | -. x e. RR } \/ A e. { x e. CC | -. 0 < ( Re ` x ) } ) ) )
26 4 25 syl5bb 
 |-  ( ph -> ( ( ( Im ` A ) = 0 -> ( Re ` A ) <_ 0 ) <-> ( A e. { x e. CC | -. x e. RR } \/ A e. { x e. CC | -. 0 < ( Re ` x ) } ) ) )
27 elun 
 |-  ( A e. ( { x e. CC | -. x e. RR } u. { x e. CC | -. 0 < ( Re ` x ) } ) <-> ( A e. { x e. CC | -. x e. RR } \/ A e. { x e. CC | -. 0 < ( Re ` x ) } ) )
28 27 a1i 
 |-  ( ph -> ( A e. ( { x e. CC | -. x e. RR } u. { x e. CC | -. 0 < ( Re ` x ) } ) <-> ( A e. { x e. CC | -. x e. RR } \/ A e. { x e. CC | -. 0 < ( Re ` x ) } ) ) )
29 ianor 
 |-  ( -. ( x e. RR /\ 0 < ( Re ` x ) ) <-> ( -. x e. RR \/ -. 0 < ( Re ` x ) ) )
30 29 bicomi 
 |-  ( ( -. x e. RR \/ -. 0 < ( Re ` x ) ) <-> -. ( x e. RR /\ 0 < ( Re ` x ) ) )
31 elrp 
 |-  ( x e. RR+ <-> ( x e. RR /\ 0 < x ) )
32 rere 
 |-  ( x e. RR -> ( Re ` x ) = x )
33 32 breq2d 
 |-  ( x e. RR -> ( 0 < ( Re ` x ) <-> 0 < x ) )
34 33 bicomd 
 |-  ( x e. RR -> ( 0 < x <-> 0 < ( Re ` x ) ) )
35 34 pm5.32i 
 |-  ( ( x e. RR /\ 0 < x ) <-> ( x e. RR /\ 0 < ( Re ` x ) ) )
36 31 35 bitri 
 |-  ( x e. RR+ <-> ( x e. RR /\ 0 < ( Re ` x ) ) )
37 30 36 xchbinxr 
 |-  ( ( -. x e. RR \/ -. 0 < ( Re ` x ) ) <-> -. x e. RR+ )
38 37 rabbii 
 |-  { x e. CC | ( -. x e. RR \/ -. 0 < ( Re ` x ) ) } = { x e. CC | -. x e. RR+ }
39 unrab 
 |-  ( { x e. CC | -. x e. RR } u. { x e. CC | -. 0 < ( Re ` x ) } ) = { x e. CC | ( -. x e. RR \/ -. 0 < ( Re ` x ) ) }
40 dfdif2 
 |-  ( CC \ RR+ ) = { x e. CC | -. x e. RR+ }
41 38 39 40 3eqtr4i 
 |-  ( { x e. CC | -. x e. RR } u. { x e. CC | -. 0 < ( Re ` x ) } ) = ( CC \ RR+ )
42 41 a1i 
 |-  ( ph -> ( { x e. CC | -. x e. RR } u. { x e. CC | -. 0 < ( Re ` x ) } ) = ( CC \ RR+ ) )
43 42 eleq2d 
 |-  ( ph -> ( A e. ( { x e. CC | -. x e. RR } u. { x e. CC | -. 0 < ( Re ` x ) } ) <-> A e. ( CC \ RR+ ) ) )
44 26 28 43 3bitr2d 
 |-  ( ph -> ( ( ( Im ` A ) = 0 -> ( Re ` A ) <_ 0 ) <-> A e. ( CC \ RR+ ) ) )
45 1 biantrurd 
 |-  ( ph -> ( -. A e. RR+ <-> ( A e. CC /\ -. A e. RR+ ) ) )
46 3 44 45 3bitr4d 
 |-  ( ph -> ( ( ( Im ` A ) = 0 -> ( Re ` A ) <_ 0 ) <-> -. A e. RR+ ) )