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	⊢ 𝐴 ∈ ℂ
	binom2.2	⊢ 𝐵 ∈ ℂ
Assertion	subsq0i	⊢ ( ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = - 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		binom2.1	⊢ 𝐴 ∈ ℂ
2		binom2.2	⊢ 𝐵 ∈ ℂ
3	1	sqcli	⊢ ( 𝐴 ↑ 2 ) ∈ ℂ
4	2	sqcli	⊢ ( 𝐵 ↑ 2 ) ∈ ℂ
5	3 4	subeq0i	⊢ ( ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 ↔ ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) )
6	1 2	sqeqori	⊢ ( ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = - 𝐵 ) )
7	5 6	bitri	⊢ ( ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = - 𝐵 ) )