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\in ℂ$$
	binom2.2	$$⊢B\in ℂ$$
Assertion	subsq0i	$$⊢A^2-B^2=0\leftrightarrow \left(A=B\vee A=-B\right)$$

Proof

Step	Hyp	Ref	Expression
1		binom2.1	$$⊢A\in ℂ$$
2		binom2.2	$$⊢B\in ℂ$$
3	1	sqcli	$$⊢A^2\in ℂ$$
4	2	sqcli	$$⊢B^2\in ℂ$$
5	3 4	subeq0i	$$⊢A^2-B^2=0\leftrightarrow A^2=B^2$$
6	1 2	sqeqori	$$⊢A^2=B^2\leftrightarrow \left(A=B\vee A=-B\right)$$
7	5 6	bitri	$$⊢A^2-B^2=0\leftrightarrow \left(A=B\vee A=-B\right)$$