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	$$⊢\phi \to A\in ℂ$$
	eqsqrtd.2	$$⊢\phi \to B\in ℂ$$
	eqsqrtd.3	$$⊢\phi \to A^2=B$$
	eqsqrt2d.4	$$⊢\phi \to 0<\Re \left(A\right)$$
Assertion	eqsqrt2d	$$⊢\phi \to A=\sqrt{B}$$

Proof

Step	Hyp	Ref	Expression
1		eqsqrtd.1	$$⊢\phi \to A\in ℂ$$
2		eqsqrtd.2	$$⊢\phi \to B\in ℂ$$
3		eqsqrtd.3	$$⊢\phi \to A^2=B$$
4		eqsqrt2d.4	$$⊢\phi \to 0<\Re \left(A\right)$$
5		0re	$$⊢0\in ℝ$$
6	1	recld	$$⊢\phi \to \Re \left(A\right)\in ℝ$$
7		ltle	$$⊢\left(0\in ℝ\wedge \Re \left(A\right)\in ℝ\right)\to \left(0<\Re \left(A\right)\to 0\le \Re \left(A\right)\right)$$
8	5 6 7	sylancr	$$⊢\phi \to \left(0<\Re \left(A\right)\to 0\le \Re \left(A\right)\right)$$
9	4 8	mpd	$$⊢\phi \to 0\le \Re \left(A\right)$$
10		reim	$$⊢A\in ℂ\to \Re \left(A\right)=\Im \left(\mathrm{i}A\right)$$
11	1 10	syl	$$⊢\phi \to \Re \left(A\right)=\Im \left(\mathrm{i}A\right)$$
12	4	gt0ne0d	$$⊢\phi \to \Re \left(A\right)\ne 0$$
13	11 12	eqnetrrd	$$⊢\phi \to \Im \left(\mathrm{i}A\right)\ne 0$$
14		rpre	$$⊢\mathrm{i}A\in {ℝ}^{+}\to \mathrm{i}A\in ℝ$$
15	14	reim0d	$$⊢\mathrm{i}A\in {ℝ}^{+}\to \Im \left(\mathrm{i}A\right)=0$$
16	15	necon3ai	$$⊢\Im \left(\mathrm{i}A\right)\ne 0\to \neg \mathrm{i}A\in {ℝ}^{+}$$
17	13 16	syl	$$⊢\phi \to \neg \mathrm{i}A\in {ℝ}^{+}$$
18	1 2 3 9 17	eqsqrtd	$$⊢\phi \to A=\sqrt{B}$$