Theorem eqsqrtor

Description: Solve an equation containing a square. (Contributed by Mario Carneiro, 23-Apr-2015)

	Ref	Expression
Assertion	eqsqrtor	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^2=B\leftrightarrow \left(A=\sqrt{B}\vee A=-\sqrt{B}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sqrtth	$$⊢B\in ℂ\to {\sqrt{B}}^2=B$$
2	1	adantl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\sqrt{B}}^2=B$$
3	2	eqeq2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^2={\sqrt{B}}^2\leftrightarrow A^2=B\right)$$
4		sqrtcl	$$⊢B\in ℂ\to \sqrt{B}\in ℂ$$
5		sqeqor	$$⊢\left(A\in ℂ\wedge \sqrt{B}\in ℂ\right)\to \left(A^2={\sqrt{B}}^2\leftrightarrow \left(A=\sqrt{B}\vee A=-\sqrt{B}\right)\right)$$
6	4 5	sylan2	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^2={\sqrt{B}}^2\leftrightarrow \left(A=\sqrt{B}\vee A=-\sqrt{B}\right)\right)$$
7	3 6	bitr3d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A^2=B\leftrightarrow \left(A=\sqrt{B}\vee A=-\sqrt{B}\right)\right)$$