# 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 ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\wedge \left({D}\parallel {A}\wedge \left({A}\parallel \left({B}-{C}\right)\vee {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\right)\right)\to \left({D}\parallel \left({B}-{C}\right)\vee {D}\parallel \left({B}-\left(-{C}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 simplr ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\wedge {A}\parallel \left({B}-{C}\right)\right)\to {D}\parallel {A}$
2 simpr ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\wedge {A}\parallel \left({B}-{C}\right)\right)\to {A}\parallel \left({B}-{C}\right)$
3 simprr ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\to {D}\in ℤ$
4 3 ad2antrr ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\wedge {A}\parallel \left({B}-{C}\right)\right)\to {D}\in ℤ$
5 simp-4l ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\wedge {A}\parallel \left({B}-{C}\right)\right)\to {A}\in ℤ$
6 simplr ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\to {B}\in ℤ$
7 6 ad2antrr ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\wedge {A}\parallel \left({B}-{C}\right)\right)\to {B}\in ℤ$
8 simprl ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\to {C}\in ℤ$
9 8 ad2antrr ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\wedge {A}\parallel \left({B}-{C}\right)\right)\to {C}\in ℤ$
10 7 9 zsubcld ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\wedge {A}\parallel \left({B}-{C}\right)\right)\to {B}-{C}\in ℤ$
11 dvdstr ${⊢}\left({D}\in ℤ\wedge {A}\in ℤ\wedge {B}-{C}\in ℤ\right)\to \left(\left({D}\parallel {A}\wedge {A}\parallel \left({B}-{C}\right)\right)\to {D}\parallel \left({B}-{C}\right)\right)$
12 4 5 10 11 syl3anc ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\wedge {A}\parallel \left({B}-{C}\right)\right)\to \left(\left({D}\parallel {A}\wedge {A}\parallel \left({B}-{C}\right)\right)\to {D}\parallel \left({B}-{C}\right)\right)$
13 1 2 12 mp2and ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\wedge {A}\parallel \left({B}-{C}\right)\right)\to {D}\parallel \left({B}-{C}\right)$
14 13 ex ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\to \left({A}\parallel \left({B}-{C}\right)\to {D}\parallel \left({B}-{C}\right)\right)$
15 simplr ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\wedge {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\to {D}\parallel {A}$
16 simpr ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\wedge {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\to {A}\parallel \left({B}-\left(-{C}\right)\right)$
17 3 ad2antrr ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\wedge {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\to {D}\in ℤ$
18 simp-4l ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\wedge {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\to {A}\in ℤ$
19 6 ad2antrr ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\wedge {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\to {B}\in ℤ$
20 8 ad2antrr ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\wedge {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\to {C}\in ℤ$
21 20 znegcld ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\wedge {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\to -{C}\in ℤ$
22 19 21 zsubcld ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\wedge {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\to {B}-\left(-{C}\right)\in ℤ$
23 dvdstr ${⊢}\left({D}\in ℤ\wedge {A}\in ℤ\wedge {B}-\left(-{C}\right)\in ℤ\right)\to \left(\left({D}\parallel {A}\wedge {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\to {D}\parallel \left({B}-\left(-{C}\right)\right)\right)$
24 17 18 22 23 syl3anc ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\wedge {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\to \left(\left({D}\parallel {A}\wedge {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\to {D}\parallel \left({B}-\left(-{C}\right)\right)\right)$
25 15 16 24 mp2and ${⊢}\left(\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\wedge {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\to {D}\parallel \left({B}-\left(-{C}\right)\right)$
26 25 ex ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\to \left({A}\parallel \left({B}-\left(-{C}\right)\right)\to {D}\parallel \left({B}-\left(-{C}\right)\right)\right)$
27 14 26 orim12d ${⊢}\left(\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\wedge {D}\parallel {A}\right)\to \left(\left({A}\parallel \left({B}-{C}\right)\vee {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\to \left({D}\parallel \left({B}-{C}\right)\vee {D}\parallel \left({B}-\left(-{C}\right)\right)\right)\right)$
28 27 expimpd ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\right)\to \left(\left({D}\parallel {A}\wedge \left({A}\parallel \left({B}-{C}\right)\vee {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\right)\to \left({D}\parallel \left({B}-{C}\right)\vee {D}\parallel \left({B}-\left(-{C}\right)\right)\right)\right)$
29 28 3impia ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\wedge \left({D}\parallel {A}\wedge \left({A}\parallel \left({B}-{C}\right)\vee {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\right)\right)\to \left({D}\parallel \left({B}-{C}\right)\vee {D}\parallel \left({B}-\left(-{C}\right)\right)\right)$