eqsqrtor

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

		Ref	Expression
	Assertion	eqsqrtor	$⊢ (A \in ℂ \land B \in ℂ) \to (A^{2} = B \leftrightarrow (A = \sqrt{B} \lor A = - \sqrt{B}))$

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

Metamath Proof Explorer