Theorem eqsqrtor

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

	Ref	Expression
Assertion	eqsqrtor	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) = 𝐵 ↔ ( 𝐴 = ( √ ‘ 𝐵 ) ∨ 𝐴 = - ( √ ‘ 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		sqrtth	⊢ ( 𝐵 ∈ ℂ → ( ( √ ‘ 𝐵 ) ↑ 2 ) = 𝐵 )
2	1	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( √ ‘ 𝐵 ) ↑ 2 ) = 𝐵 )
3	2	eqeq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) = ( ( √ ‘ 𝐵 ) ↑ 2 ) ↔ ( 𝐴 ↑ 2 ) = 𝐵 ) )
4		sqrtcl	⊢ ( 𝐵 ∈ ℂ → ( √ ‘ 𝐵 ) ∈ ℂ )
5		sqeqor	⊢ ( ( 𝐴 ∈ ℂ ∧ ( √ ‘ 𝐵 ) ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) = ( ( √ ‘ 𝐵 ) ↑ 2 ) ↔ ( 𝐴 = ( √ ‘ 𝐵 ) ∨ 𝐴 = - ( √ ‘ 𝐵 ) ) ) )
6	4 5	sylan2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) = ( ( √ ‘ 𝐵 ) ↑ 2 ) ↔ ( 𝐴 = ( √ ‘ 𝐵 ) ∨ 𝐴 = - ( √ ‘ 𝐵 ) ) ) )
7	3 6	bitr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) = 𝐵 ↔ ( 𝐴 = ( √ ‘ 𝐵 ) ∨ 𝐴 = - ( √ ‘ 𝐵 ) ) ) )