Metamath Proof Explorer

Theorem congsym

Description: Congruence mod A is a symmetric/commutative relation. (Contributed by Stefan O'Rear, 1-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 simprr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> A || ( B - C ) )
2 zcn 
 |-  ( C e. ZZ -> C e. CC )
3 2 ad2antrl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> C e. CC )
4 zcn 
 |-  ( B e. ZZ -> B e. CC )
5 4 ad2antlr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> B e. CC )
6 3 5 negsubdi2d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> -u ( C - B ) = ( B - C ) )
7 1 6 breqtrrd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> A || -u ( C - B ) )
8 simpll 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> A e. ZZ )
9 simprl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> C e. ZZ )
10 simplr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> B e. ZZ )
11 9 10 zsubcld 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> ( C - B ) e. ZZ )
12 dvdsnegb 
 |-  ( ( A e. ZZ /\ ( C - B ) e. ZZ ) -> ( A || ( C - B ) <-> A || -u ( C - B ) ) )
13 8 11 12 syl2anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> ( A || ( C - B ) <-> A || -u ( C - B ) ) )
14 7 13 mpbird 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> A || ( C - B ) )