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 𝐴 ∈ ℂ
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 ↔ ( 𝐴 = 𝐵𝐴 = - 𝐵 ) )