Theorem congneg

Description: If two integers are congruent mod A , so are their negatives. (Contributed by Stefan O'Rear, 1-Oct-2014)

	Ref	Expression
Assertion	congneg	|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> A || ( -u B - -u C ) )

Proof

Step	Hyp	Ref	Expression
1		congsym	|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> A || ( C - B ) )
2		zcn	|- ( B e. ZZ -> B e. CC )
3		zcn	|- ( C e. ZZ -> C e. CC )
4		neg2sub	|- ( ( B e. CC /\ C e. CC ) -> ( -u B - -u C ) = ( C - B ) )
5	2 3 4	syl2an	|- ( ( B e. ZZ /\ C e. ZZ ) -> ( -u B - -u C ) = ( C - B ) )
6	5	ad2ant2lr	|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> ( -u B - -u C ) = ( C - B ) )
7	1 6	breqtrrd	|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> A || ( -u B - -u C ) )