Metamath Proof Explorer

Theorem sqrtneg

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

Ref Expression
Assertion sqrtneg 
|- ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` -u A ) = ( _i x. ( sqrt ` A ) ) )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 1 adantr 
 |-  ( ( A e. RR /\ 0 <_ A ) -> A e. CC )
3 2 negcld 
 |-  ( ( A e. RR /\ 0 <_ A ) -> -u A e. CC )
4 sqrtval 
 |-  ( -u A e. CC -> ( sqrt ` -u A ) = ( iota_ x e. CC ( ( x ^ 2 ) = -u A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) )
5 3 4 syl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` -u A ) = ( iota_ x e. CC ( ( x ^ 2 ) = -u A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) )
6 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+ ) )
7 ax-icn 
 |-  _i e. CC
8 resqrtcl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` A ) e. RR )
9 8 recnd 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` A ) e. CC )
10 mulcl 
 |-  ( ( _i e. CC /\ ( sqrt ` A ) e. CC ) -> ( _i x. ( sqrt ` A ) ) e. CC )
11 7 9 10 sylancr 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( _i x. ( sqrt ` A ) ) e. CC )
12 oveq1 
 |-  ( x = ( _i x. ( sqrt ` A ) ) -> ( x ^ 2 ) = ( ( _i x. ( sqrt ` A ) ) ^ 2 ) )
13 12 eqeq1d 
 |-  ( x = ( _i x. ( sqrt ` A ) ) -> ( ( x ^ 2 ) = -u A <-> ( ( _i x. ( sqrt ` A ) ) ^ 2 ) = -u A ) )
14 fveq2 
 |-  ( x = ( _i x. ( sqrt ` A ) ) -> ( Re ` x ) = ( Re ` ( _i x. ( sqrt ` A ) ) ) )
15 14 breq2d 
 |-  ( x = ( _i x. ( sqrt ` A ) ) -> ( 0 <_ ( Re ` x ) <-> 0 <_ ( Re ` ( _i x. ( sqrt ` A ) ) ) ) )
16 oveq2 
 |-  ( x = ( _i x. ( sqrt ` A ) ) -> ( _i x. x ) = ( _i x. ( _i x. ( sqrt ` A ) ) ) )
17 neleq1 
 |-  ( ( _i x. x ) = ( _i x. ( _i x. ( sqrt ` A ) ) ) -> ( ( _i x. x ) e/ RR+ <-> ( _i x. ( _i x. ( sqrt ` A ) ) ) e/ RR+ ) )
18 16 17 syl 
 |-  ( x = ( _i x. ( sqrt ` A ) ) -> ( ( _i x. x ) e/ RR+ <-> ( _i x. ( _i x. ( sqrt ` A ) ) ) e/ RR+ ) )
19 13 15 18 3anbi123d 
 |-  ( x = ( _i x. ( sqrt ` A ) ) -> ( ( ( x ^ 2 ) = -u A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) <-> ( ( ( _i x. ( sqrt ` A ) ) ^ 2 ) = -u A /\ 0 <_ ( Re ` ( _i x. ( sqrt ` A ) ) ) /\ ( _i x. ( _i x. ( sqrt ` A ) ) ) e/ RR+ ) ) )
20 19 rspcev 
 |-  ( ( ( _i x. ( sqrt ` A ) ) e. CC /\ ( ( ( _i x. ( sqrt ` A ) ) ^ 2 ) = -u A /\ 0 <_ ( Re ` ( _i x. ( sqrt ` A ) ) ) /\ ( _i x. ( _i x. ( sqrt ` A ) ) ) e/ RR+ ) ) -> E. x e. CC ( ( x ^ 2 ) = -u A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
21 11 6 20 syl2anc 
 |-  ( ( A e. RR /\ 0 <_ A ) -> E. x e. CC ( ( x ^ 2 ) = -u A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
22 sqrmo 
 |-  ( -u A e. CC -> E* x e. CC ( ( x ^ 2 ) = -u A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
23 3 22 syl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> E* x e. CC ( ( x ^ 2 ) = -u A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
24 reu5 
 |-  ( E! x e. CC ( ( x ^ 2 ) = -u A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) <-> ( E. x e. CC ( ( x ^ 2 ) = -u A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) /\ E* x e. CC ( ( x ^ 2 ) = -u A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) )
25 21 23 24 sylanbrc 
 |-  ( ( A e. RR /\ 0 <_ A ) -> E! x e. CC ( ( x ^ 2 ) = -u A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
26 19 riota2 
 |-  ( ( ( _i x. ( sqrt ` A ) ) e. CC /\ E! x e. CC ( ( x ^ 2 ) = -u A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) -> ( ( ( ( _i x. ( sqrt ` A ) ) ^ 2 ) = -u A /\ 0 <_ ( Re ` ( _i x. ( sqrt ` A ) ) ) /\ ( _i x. ( _i x. ( sqrt ` A ) ) ) e/ RR+ ) <-> ( iota_ x e. CC ( ( x ^ 2 ) = -u A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) = ( _i x. ( sqrt ` A ) ) ) )
27 11 25 26 syl2anc 
 |-  ( ( 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+ ) <-> ( iota_ x e. CC ( ( x ^ 2 ) = -u A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) = ( _i x. ( sqrt ` A ) ) ) )
28 6 27 mpbid 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( iota_ x e. CC ( ( x ^ 2 ) = -u A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) = ( _i x. ( sqrt ` A ) ) )
29 5 28 eqtrd 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` -u A ) = ( _i x. ( sqrt ` A ) ) )