Metamath Proof Explorer

Theorem acongsym

Description: Symmetry of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 congsym 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> A || ( C - B ) )
2 1 exp32 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( C e. ZZ -> ( A || ( B - C ) -> A || ( C - B ) ) ) )
3 2 3impia 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A || ( B - C ) -> A || ( C - B ) ) )
4 zcn 
 |-  ( B e. ZZ -> B e. CC )
5 4 3ad2ant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> B e. CC )
6 5 negnegd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> -u -u B = B )
7 6 oveq1d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( -u -u B - -u C ) = ( B - -u C ) )
8 4 negcld 
 |-  ( B e. ZZ -> -u B e. CC )
9 8 3ad2ant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> -u B e. CC )
10 zcn 
 |-  ( C e. ZZ -> C e. CC )
11 10 3ad2ant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> C e. CC )
12 9 11 neg2subd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( -u -u B - -u C ) = ( C - -u B ) )
13 7 12 eqtr3d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( B - -u C ) = ( C - -u B ) )
14 13 breq2d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A || ( B - -u C ) <-> A || ( C - -u B ) ) )
15 14 biimpd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A || ( B - -u C ) -> A || ( C - -u B ) ) )
16 3 15 orim12d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( A || ( B - C ) \/ A || ( B - -u C ) ) -> ( A || ( C - B ) \/ A || ( C - -u B ) ) ) )
17 16 imp 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( A || ( B - C ) \/ A || ( B - -u C ) ) ) -> ( A || ( C - B ) \/ A || ( C - -u B ) ) )