Metamath Proof Explorer

Theorem dvdsacongtr

Description: Alternating congruence passes from a base to a dividing base. (Contributed by Stefan O'Rear, 4-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 simprr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> D e. ZZ )
2 1 ad2antrr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) /\ A || ( B - C ) ) -> D e. ZZ )
3 simp-4l 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) /\ A || ( B - C ) ) -> A e. ZZ )
4 simplr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> B e. ZZ )
5 4 ad2antrr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) /\ A || ( B - C ) ) -> B e. ZZ )
6 simprl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> C e. ZZ )
7 6 ad2antrr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) /\ A || ( B - C ) ) -> C e. ZZ )
8 5 7 zsubcld 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) /\ A || ( B - C ) ) -> ( B - C ) e. ZZ )
9 simplr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) /\ A || ( B - C ) ) -> D || A )
10 simpr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) /\ A || ( B - C ) ) -> A || ( B - C ) )
11 2 3 8 9 10 dvdstrd 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) /\ A || ( B - C ) ) -> D || ( B - C ) )
12 11 ex 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) -> ( A || ( B - C ) -> D || ( B - C ) ) )
13 1 ad2antrr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) /\ A || ( B - -u C ) ) -> D e. ZZ )
14 simp-4l 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) /\ A || ( B - -u C ) ) -> A e. ZZ )
15 4 ad2antrr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) /\ A || ( B - -u C ) ) -> B e. ZZ )
16 6 ad2antrr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) /\ A || ( B - -u C ) ) -> C e. ZZ )
17 16 znegcld 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) /\ A || ( B - -u C ) ) -> -u C e. ZZ )
18 15 17 zsubcld 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) /\ A || ( B - -u C ) ) -> ( B - -u C ) e. ZZ )
19 simplr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) /\ A || ( B - -u C ) ) -> D || A )
20 simpr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) /\ A || ( B - -u C ) ) -> A || ( B - -u C ) )
21 13 14 18 19 20 dvdstrd 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) /\ A || ( B - -u C ) ) -> D || ( B - -u C ) )
22 21 ex 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) -> ( A || ( B - -u C ) -> D || ( B - -u C ) ) )
23 12 22 orim12d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ D || A ) -> ( ( A || ( B - C ) \/ A || ( B - -u C ) ) -> ( D || ( B - C ) \/ D || ( B - -u C ) ) ) )
24 23 expimpd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( ( D || A /\ ( A || ( B - C ) \/ A || ( B - -u C ) ) ) -> ( D || ( B - C ) \/ D || ( B - -u C ) ) ) )
25 24 3impia 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( D || A /\ ( A || ( B - C ) \/ A || ( B - -u C ) ) ) ) -> ( D || ( B - C ) \/ D || ( B - -u C ) ) )