Metamath Proof Explorer

Theorem sqrtneglem

Description: The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013)

Ref Expression
Assertion sqrtneglem 
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( ( _i x. ( sqrt ` A ) ) ^ 2 ) = -u A /\ 0 <_ ( Re ` ( _i x. ( sqrt ` A ) ) ) /\ ( _i x. ( _i x. ( sqrt ` A ) ) ) e/ RR+ ) )

Proof

Step Hyp Ref Expression
1 ax-icn 
 |-  _i e. CC
2 resqrtcl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` A ) e. RR )
3 recn 
 |-  ( ( sqrt ` A ) e. RR -> ( sqrt ` A ) e. CC )
4 2 3 syl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` A ) e. CC )
5 sqmul 
 |-  ( ( _i e. CC /\ ( sqrt ` A ) e. CC ) -> ( ( _i x. ( sqrt ` A ) ) ^ 2 ) = ( ( _i ^ 2 ) x. ( ( sqrt ` A ) ^ 2 ) ) )
6 1 4 5 sylancr 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( _i x. ( sqrt ` A ) ) ^ 2 ) = ( ( _i ^ 2 ) x. ( ( sqrt ` A ) ^ 2 ) ) )
7 i2 
 |-  ( _i ^ 2 ) = -u 1
8 7 a1i 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( _i ^ 2 ) = -u 1 )
9 resqrtth 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( sqrt ` A ) ^ 2 ) = A )
10 8 9 oveq12d 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( _i ^ 2 ) x. ( ( sqrt ` A ) ^ 2 ) ) = ( -u 1 x. A ) )
11 recn 
 |-  ( A e. RR -> A e. CC )
12 11 adantr 
 |-  ( ( A e. RR /\ 0 <_ A ) -> A e. CC )
13 12 mulm1d 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( -u 1 x. A ) = -u A )
14 6 10 13 3eqtrd 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( _i x. ( sqrt ` A ) ) ^ 2 ) = -u A )
15 renegcl 
 |-  ( ( sqrt ` A ) e. RR -> -u ( sqrt ` A ) e. RR )
16 0re 
 |-  0 e. RR
17 reim0 
 |-  ( -u ( sqrt ` A ) e. RR -> ( Im ` -u ( sqrt ` A ) ) = 0 )
18 recn 
 |-  ( -u ( sqrt ` A ) e. RR -> -u ( sqrt ` A ) e. CC )
19 imre 
 |-  ( -u ( sqrt ` A ) e. CC -> ( Im ` -u ( sqrt ` A ) ) = ( Re ` ( -u _i x. -u ( sqrt ` A ) ) ) )
20 18 19 syl 
 |-  ( -u ( sqrt ` A ) e. RR -> ( Im ` -u ( sqrt ` A ) ) = ( Re ` ( -u _i x. -u ( sqrt ` A ) ) ) )
21 17 20 eqtr3d 
 |-  ( -u ( sqrt ` A ) e. RR -> 0 = ( Re ` ( -u _i x. -u ( sqrt ` A ) ) ) )
22 eqle 
 |-  ( ( 0 e. RR /\ 0 = ( Re ` ( -u _i x. -u ( sqrt ` A ) ) ) ) -> 0 <_ ( Re ` ( -u _i x. -u ( sqrt ` A ) ) ) )
23 16 21 22 sylancr 
 |-  ( -u ( sqrt ` A ) e. RR -> 0 <_ ( Re ` ( -u _i x. -u ( sqrt ` A ) ) ) )
24 2 15 23 3syl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> 0 <_ ( Re ` ( -u _i x. -u ( sqrt ` A ) ) ) )
25 mul2neg 
 |-  ( ( _i e. CC /\ ( sqrt ` A ) e. CC ) -> ( -u _i x. -u ( sqrt ` A ) ) = ( _i x. ( sqrt ` A ) ) )
26 1 4 25 sylancr 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( -u _i x. -u ( sqrt ` A ) ) = ( _i x. ( sqrt ` A ) ) )
27 26 fveq2d 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( Re ` ( -u _i x. -u ( sqrt ` A ) ) ) = ( Re ` ( _i x. ( sqrt ` A ) ) ) )
28 24 27 breqtrd 
 |-  ( ( A e. RR /\ 0 <_ A ) -> 0 <_ ( Re ` ( _i x. ( sqrt ` A ) ) ) )
29 ixi 
 |-  ( _i x. _i ) = -u 1
30 29 oveq1i 
 |-  ( ( _i x. _i ) x. ( sqrt ` A ) ) = ( -u 1 x. ( sqrt ` A ) )
31 mulass 
 |-  ( ( _i e. CC /\ _i e. CC /\ ( sqrt ` A ) e. CC ) -> ( ( _i x. _i ) x. ( sqrt ` A ) ) = ( _i x. ( _i x. ( sqrt ` A ) ) ) )
32 1 1 31 mp3an12 
 |-  ( ( sqrt ` A ) e. CC -> ( ( _i x. _i ) x. ( sqrt ` A ) ) = ( _i x. ( _i x. ( sqrt ` A ) ) ) )
33 mulm1 
 |-  ( ( sqrt ` A ) e. CC -> ( -u 1 x. ( sqrt ` A ) ) = -u ( sqrt ` A ) )
34 30 32 33 3eqtr3a 
 |-  ( ( sqrt ` A ) e. CC -> ( _i x. ( _i x. ( sqrt ` A ) ) ) = -u ( sqrt ` A ) )
35 4 34 syl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( _i x. ( _i x. ( sqrt ` A ) ) ) = -u ( sqrt ` A ) )
36 sqrtge0 
 |-  ( ( A e. RR /\ 0 <_ A ) -> 0 <_ ( sqrt ` A ) )
37 le0neg2 
 |-  ( ( sqrt ` A ) e. RR -> ( 0 <_ ( sqrt ` A ) <-> -u ( sqrt ` A ) <_ 0 ) )
38 lenlt 
 |-  ( ( -u ( sqrt ` A ) e. RR /\ 0 e. RR ) -> ( -u ( sqrt ` A ) <_ 0 <-> -. 0 < -u ( sqrt ` A ) ) )
39 15 16 38 sylancl 
 |-  ( ( sqrt ` A ) e. RR -> ( -u ( sqrt ` A ) <_ 0 <-> -. 0 < -u ( sqrt ` A ) ) )
40 37 39 bitrd 
 |-  ( ( sqrt ` A ) e. RR -> ( 0 <_ ( sqrt ` A ) <-> -. 0 < -u ( sqrt ` A ) ) )
41 2 40 syl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( 0 <_ ( sqrt ` A ) <-> -. 0 < -u ( sqrt ` A ) ) )
42 36 41 mpbid 
 |-  ( ( A e. RR /\ 0 <_ A ) -> -. 0 < -u ( sqrt ` A ) )
43 elrp 
 |-  ( -u ( sqrt ` A ) e. RR+ <-> ( -u ( sqrt ` A ) e. RR /\ 0 < -u ( sqrt ` A ) ) )
44 2 15 syl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> -u ( sqrt ` A ) e. RR )
45 44 biantrurd 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( 0 < -u ( sqrt ` A ) <-> ( -u ( sqrt ` A ) e. RR /\ 0 < -u ( sqrt ` A ) ) ) )
46 43 45 bitr4id 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( -u ( sqrt ` A ) e. RR+ <-> 0 < -u ( sqrt ` A ) ) )
47 42 46 mtbird 
 |-  ( ( A e. RR /\ 0 <_ A ) -> -. -u ( sqrt ` A ) e. RR+ )
48 35 47 eqneltrd 
 |-  ( ( A e. RR /\ 0 <_ A ) -> -. ( _i x. ( _i x. ( sqrt ` A ) ) ) e. RR+ )
49 df-nel 
 |-  ( ( _i x. ( _i x. ( sqrt ` A ) ) ) e/ RR+ <-> -. ( _i x. ( _i x. ( sqrt ` A ) ) ) e. RR+ )
50 48 49 sylibr 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( _i x. ( _i x. ( sqrt ` A ) ) ) e/ RR+ )
51 14 28 50 3jca 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( ( _i x. ( sqrt ` A ) ) ^ 2 ) = -u A /\ 0 <_ ( Re ` ( _i x. ( sqrt ` A ) ) ) /\ ( _i x. ( _i x. ( sqrt ` A ) ) ) e/ RR+ ) )