Theorem sqsubswap

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

	Ref	Expression
Assertion	sqsubswap	|- ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) ^ 2 ) = ( ( B - A ) ^ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		subcl	|- ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
2		sqneg	|- ( ( A - B ) e. CC -> ( -u ( A - B ) ^ 2 ) = ( ( A - B ) ^ 2 ) )
3	1 2	syl	|- ( ( A e. CC /\ B e. CC ) -> ( -u ( A - B ) ^ 2 ) = ( ( A - B ) ^ 2 ) )
4		negsubdi2	|- ( ( A e. CC /\ B e. CC ) -> -u ( A - B ) = ( B - A ) )
5	4	oveq1d	|- ( ( A e. CC /\ B e. CC ) -> ( -u ( A - B ) ^ 2 ) = ( ( B - A ) ^ 2 ) )
6	3 5	eqtr3d	|- ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) ^ 2 ) = ( ( B - A ) ^ 2 ) )