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 e. CC
	binom2.2	|- B e. CC
Assertion	subsq0i	|- ( ( ( A ^ 2 ) - ( B ^ 2 ) ) = 0 <-> ( A = B \/ A = -u B ) )

Proof

Step	Hyp	Ref	Expression
1		binom2.1	|- A e. CC
2		binom2.2	|- B e. CC
3	1	sqcli	|- ( A ^ 2 ) e. CC
4	2	sqcli	|- ( B ^ 2 ) e. CC
5	3 4	subeq0i	|- ( ( ( A ^ 2 ) - ( B ^ 2 ) ) = 0 <-> ( A ^ 2 ) = ( B ^ 2 ) )
6	1 2	sqeqori	|- ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( A = B \/ A = -u B ) )
7	5 6	bitri	|- ( ( ( A ^ 2 ) - ( B ^ 2 ) ) = 0 <-> ( A = B \/ A = -u B ) )