Theorem eqsqrtd

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$$
	eqsqrtd.4	$$⊢\phi \to 0\le \Re \left(A\right)$$
	eqsqrtd.5	$$⊢\phi \to \neg \mathrm{i}A\in {ℝ}^{+}$$
Assertion	eqsqrtd	$$⊢\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		eqsqrtd.4	$$⊢\phi \to 0\le \Re \left(A\right)$$
5		eqsqrtd.5	$$⊢\phi \to \neg \mathrm{i}A\in {ℝ}^{+}$$
6		sqreu	$$⊢B\in ℂ\to \exists !x\in ℂ\left(x^2=B\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)$$
7		reurmo	$$⊢\exists !x\in ℂ\left(x^2=B\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\to {\exists }^{*}x\in ℂ\left(x^2=B\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)$$
8	2 6 7	3syl	$$⊢\phi \to {\exists }^{*}x\in ℂ\left(x^2=B\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)$$
9		df-nel	$$⊢\mathrm{i}A\notin {ℝ}^{+}\leftrightarrow \neg \mathrm{i}A\in {ℝ}^{+}$$
10	5 9	sylibr	$$⊢\phi \to \mathrm{i}A\notin {ℝ}^{+}$$
11	3 4 10	3jca	$$⊢\phi \to \left(A^2=B\wedge 0\le \Re \left(A\right)\wedge \mathrm{i}A\notin {ℝ}^{+}\right)$$
12		sqrtcl	$$⊢B\in ℂ\to \sqrt{B}\in ℂ$$
13	2 12	syl	$$⊢\phi \to \sqrt{B}\in ℂ$$
14		sqrtthlem	$$⊢B\in ℂ\to \left({\sqrt{B}}^2=B\wedge 0\le \Re \left(\sqrt{B}\right)\wedge \mathrm{i}\sqrt{B}\notin {ℝ}^{+}\right)$$
15	2 14	syl	$$⊢\phi \to \left({\sqrt{B}}^2=B\wedge 0\le \Re \left(\sqrt{B}\right)\wedge \mathrm{i}\sqrt{B}\notin {ℝ}^{+}\right)$$
16		oveq1	$$⊢x=A\to x^2=A^2$$
17	16	eqeq1d	$$⊢x=A\to \left(x^2=B\leftrightarrow A^2=B\right)$$
18		fveq2	$$⊢x=A\to \Re \left(x\right)=\Re \left(A\right)$$
19	18	breq2d	$$⊢x=A\to \left(0\le \Re \left(x\right)\leftrightarrow 0\le \Re \left(A\right)\right)$$
20		oveq2	$$⊢x=A\to \mathrm{i}x=\mathrm{i}A$$
21		neleq1	$$⊢\mathrm{i}x=\mathrm{i}A\to \left(\mathrm{i}x\notin {ℝ}^{+}\leftrightarrow \mathrm{i}A\notin {ℝ}^{+}\right)$$
22	20 21	syl	$$⊢x=A\to \left(\mathrm{i}x\notin {ℝ}^{+}\leftrightarrow \mathrm{i}A\notin {ℝ}^{+}\right)$$
23	17 19 22	3anbi123d	$$⊢x=A\to \left(\left(x^2=B\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\leftrightarrow \left(A^2=B\wedge 0\le \Re \left(A\right)\wedge \mathrm{i}A\notin {ℝ}^{+}\right)\right)$$
24		oveq1	$$⊢x=\sqrt{B}\to x^2={\sqrt{B}}^2$$
25	24	eqeq1d	$$⊢x=\sqrt{B}\to \left(x^2=B\leftrightarrow {\sqrt{B}}^2=B\right)$$
26		fveq2	$$⊢x=\sqrt{B}\to \Re \left(x\right)=\Re \left(\sqrt{B}\right)$$
27	26	breq2d	$$⊢x=\sqrt{B}\to \left(0\le \Re \left(x\right)\leftrightarrow 0\le \Re \left(\sqrt{B}\right)\right)$$
28		oveq2	$$⊢x=\sqrt{B}\to \mathrm{i}x=\mathrm{i}\sqrt{B}$$
29		neleq1	$$⊢\mathrm{i}x=\mathrm{i}\sqrt{B}\to \left(\mathrm{i}x\notin {ℝ}^{+}\leftrightarrow \mathrm{i}\sqrt{B}\notin {ℝ}^{+}\right)$$
30	28 29	syl	$$⊢x=\sqrt{B}\to \left(\mathrm{i}x\notin {ℝ}^{+}\leftrightarrow \mathrm{i}\sqrt{B}\notin {ℝ}^{+}\right)$$
31	25 27 30	3anbi123d	$$⊢x=\sqrt{B}\to \left(\left(x^2=B\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\leftrightarrow \left({\sqrt{B}}^2=B\wedge 0\le \Re \left(\sqrt{B}\right)\wedge \mathrm{i}\sqrt{B}\notin {ℝ}^{+}\right)\right)$$
32	23 31	rmoi	$$⊢\left({\exists }^{*}x\in ℂ\left(x^2=B\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\wedge \left(A\in ℂ\wedge \left(A^2=B\wedge 0\le \Re \left(A\right)\wedge \mathrm{i}A\notin {ℝ}^{+}\right)\right)\wedge \left(\sqrt{B}\in ℂ\wedge \left({\sqrt{B}}^2=B\wedge 0\le \Re \left(\sqrt{B}\right)\wedge \mathrm{i}\sqrt{B}\notin {ℝ}^{+}\right)\right)\right)\to A=\sqrt{B}$$
33	8 1 11 13 15 32	syl122anc	$$⊢\phi \to A=\sqrt{B}$$