Metamath Proof Explorer

Theorem resqrtthlem

Description: Lemma for resqrtth . (Contributed by Mario Carneiro, 9-Jul-2013)

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

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 sqrtval 
 |-  ( A e. CC -> ( sqrt ` A ) = ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) )
3 2 eqcomd 
 |-  ( A e. CC -> ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) = ( sqrt ` A ) )
4 1 3 syl 
 |-  ( A e. RR -> ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) = ( sqrt ` A ) )
5 4 adantr 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) = ( sqrt ` A ) )
6 resqrtcl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` A ) e. RR )
7 6 recnd 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` A ) e. CC )
8 resqreu 
 |-  ( ( A e. RR /\ 0 <_ A ) -> E! x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
9 oveq1 
 |-  ( x = ( sqrt ` A ) -> ( x ^ 2 ) = ( ( sqrt ` A ) ^ 2 ) )
10 9 eqeq1d 
 |-  ( x = ( sqrt ` A ) -> ( ( x ^ 2 ) = A <-> ( ( sqrt ` A ) ^ 2 ) = A ) )
11 fveq2 
 |-  ( x = ( sqrt ` A ) -> ( Re ` x ) = ( Re ` ( sqrt ` A ) ) )
12 11 breq2d 
 |-  ( x = ( sqrt ` A ) -> ( 0 <_ ( Re ` x ) <-> 0 <_ ( Re ` ( sqrt ` A ) ) ) )
13 oveq2 
 |-  ( x = ( sqrt ` A ) -> ( _i x. x ) = ( _i x. ( sqrt ` A ) ) )
14 neleq1 
 |-  ( ( _i x. x ) = ( _i x. ( sqrt ` A ) ) -> ( ( _i x. x ) e/ RR+ <-> ( _i x. ( sqrt ` A ) ) e/ RR+ ) )
15 13 14 syl 
 |-  ( x = ( sqrt ` A ) -> ( ( _i x. x ) e/ RR+ <-> ( _i x. ( sqrt ` A ) ) e/ RR+ ) )
16 10 12 15 3anbi123d 
 |-  ( x = ( sqrt ` A ) -> ( ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) <-> ( ( ( sqrt ` A ) ^ 2 ) = A /\ 0 <_ ( Re ` ( sqrt ` A ) ) /\ ( _i x. ( sqrt ` A ) ) e/ RR+ ) ) )
17 16 riota2 
 |-  ( ( ( sqrt ` A ) e. CC /\ E! x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) -> ( ( ( ( sqrt ` A ) ^ 2 ) = A /\ 0 <_ ( Re ` ( sqrt ` A ) ) /\ ( _i x. ( sqrt ` A ) ) e/ RR+ ) <-> ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) = ( sqrt ` A ) ) )
18 7 8 17 syl2anc 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( ( ( sqrt ` A ) ^ 2 ) = A /\ 0 <_ ( Re ` ( sqrt ` A ) ) /\ ( _i x. ( sqrt ` A ) ) e/ RR+ ) <-> ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) = ( sqrt ` A ) ) )
19 5 18 mpbird 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( ( sqrt ` A ) ^ 2 ) = A /\ 0 <_ ( Re ` ( sqrt ` A ) ) /\ ( _i x. ( sqrt ` A ) ) e/ RR+ ) )