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

Metamath Proof Explorer

Theorem sqsubswap

Description: Swap the order of subtraction in a square. (Contributed by Scott Fenton, 10-Jun-2013)

Ref Expression
Assertion sqsubswap ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B 2 = B − A 2

Proof

Step Hyp Ref Expression
1 subcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ∈ ℂ
2 sqneg ⊢ A − B ∈ ℂ → − A − B 2 = A − B 2
3 1 2 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A − B 2 = A − B 2
4 negsubdi2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A − B = B − A
5 4 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A − B 2 = B − A 2
6 3 5 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B 2 = B − A 2