This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) = 𝐵 ↔ ( 𝐴 = ( √ ‘ 𝐵 ) ∨ 𝐴 = - ( √ ‘ 𝐵 ) ) ) )