Theorem eqsqrt2d

Description: A deduction for showing that a number equals the square root of another. (Contributed by Mario Carneiro, 3-Apr-2015)

	Ref	Expression
Hypotheses	eqsqrtd.1	|- ( ph -> A e. CC )
	eqsqrtd.2	|- ( ph -> B e. CC )
	eqsqrtd.3	|- ( ph -> ( A ^ 2 ) = B )
	eqsqrt2d.4	|- ( ph -> 0 < ( Re ` A ) )
Assertion	eqsqrt2d	|- ( ph -> A = ( sqrt ` B ) )

Proof

Step	Hyp	Ref	Expression
1		eqsqrtd.1	|- ( ph -> A e. CC )
2		eqsqrtd.2	|- ( ph -> B e. CC )
3		eqsqrtd.3	|- ( ph -> ( A ^ 2 ) = B )
4		eqsqrt2d.4	|- ( ph -> 0 < ( Re ` A ) )
5		0re	|- 0 e. RR
6	1	recld	|- ( ph -> ( Re ` A ) e. RR )
7		ltle	|- ( ( 0 e. RR /\ ( Re ` A ) e. RR ) -> ( 0 < ( Re ` A ) -> 0 <_ ( Re ` A ) ) )
8	5 6 7	sylancr	|- ( ph -> ( 0 < ( Re ` A ) -> 0 <_ ( Re ` A ) ) )
9	4 8	mpd	|- ( ph -> 0 <_ ( Re ` A ) )
10		reim	|- ( A e. CC -> ( Re ` A ) = ( Im ` ( _i x. A ) ) )
11	1 10	syl	|- ( ph -> ( Re ` A ) = ( Im ` ( _i x. A ) ) )
12	4	gt0ne0d	|- ( ph -> ( Re ` A ) =/= 0 )
13	11 12	eqnetrrd	|- ( ph -> ( Im ` ( _i x. A ) ) =/= 0 )
14		rpre	|- ( ( _i x. A ) e. RR+ -> ( _i x. A ) e. RR )
15	14	reim0d	|- ( ( _i x. A ) e. RR+ -> ( Im ` ( _i x. A ) ) = 0 )
16	15	necon3ai	|- ( ( Im ` ( _i x. A ) ) =/= 0 -> -. ( _i x. A ) e. RR+ )
17	13 16	syl	|- ( ph -> -. ( _i x. A ) e. RR+ )
18	1 2 3 9 17	eqsqrtd	|- ( ph -> A = ( sqrt ` B ) )