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

Metamath Proof Explorer

Theorem subsq0i

Description: The two solutions to the difference of squares set equal to zero. (Contributed by NM, 25-Apr-2006)

Ref Expression
Hypotheses binom2.1 ⊢ A ∈ ℂ
binom2.2 ⊢ B ∈ ℂ
Assertion subsq0i ⊢ A 2 − B 2 = 0 ↔ A = B ∨ A = − B

Proof

Step Hyp Ref Expression
1 binom2.1 ⊢ A ∈ ℂ
2 binom2.2 ⊢ B ∈ ℂ
3 1 sqcli ⊢ A 2 ∈ ℂ
4 2 sqcli ⊢ B 2 ∈ ℂ
5 3 4 subeq0i ⊢ A 2 − B 2 = 0 ↔ A 2 = B 2
6 1 2 sqeqori ⊢ A 2 = B 2 ↔ A = B ∨ A = − B
7 5 6 bitri ⊢ A 2 − B 2 = 0 ↔ A = B ∨ A = − B