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 ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐷 ∥ 𝐴 ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∨ 𝐴 ∥ ( 𝐵 − - 𝐶 ) ) ) ) → ( 𝐷 ∥ ( 𝐵 − 𝐶 ) ∨ 𝐷 ∥ ( 𝐵 − - 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 simprr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → 𝐷 ∈ ℤ )
2 1 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) → 𝐷 ∈ ℤ )
3 simp-4l ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) → 𝐴 ∈ ℤ )
4 simplr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → 𝐵 ∈ ℤ )
5 4 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) → 𝐵 ∈ ℤ )
6 simprl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → 𝐶 ∈ ℤ )
7 6 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) → 𝐶 ∈ ℤ )
8 5 7 zsubcld ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) → ( 𝐵 − 𝐶 ) ∈ ℤ )
9 simplr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) → 𝐷 ∥ 𝐴 )
10 simpr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) → 𝐴 ∥ ( 𝐵 − 𝐶 ) )
11 2 3 8 9 10 dvdstrd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) → 𝐷 ∥ ( 𝐵 − 𝐶 ) )
12 11 ex ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) → ( 𝐴 ∥ ( 𝐵 − 𝐶 ) → 𝐷 ∥ ( 𝐵 − 𝐶 ) ) )
13 1 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) ∧ 𝐴 ∥ ( 𝐵 − - 𝐶 ) ) → 𝐷 ∈ ℤ )
14 simp-4l ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) ∧ 𝐴 ∥ ( 𝐵 − - 𝐶 ) ) → 𝐴 ∈ ℤ )
15 4 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) ∧ 𝐴 ∥ ( 𝐵 − - 𝐶 ) ) → 𝐵 ∈ ℤ )
16 6 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) ∧ 𝐴 ∥ ( 𝐵 − - 𝐶 ) ) → 𝐶 ∈ ℤ )
17 16 znegcld ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) ∧ 𝐴 ∥ ( 𝐵 − - 𝐶 ) ) → - 𝐶 ∈ ℤ )
18 15 17 zsubcld ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) ∧ 𝐴 ∥ ( 𝐵 − - 𝐶 ) ) → ( 𝐵 − - 𝐶 ) ∈ ℤ )
19 simplr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) ∧ 𝐴 ∥ ( 𝐵 − - 𝐶 ) ) → 𝐷 ∥ 𝐴 )
20 simpr ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) ∧ 𝐴 ∥ ( 𝐵 − - 𝐶 ) ) → 𝐴 ∥ ( 𝐵 − - 𝐶 ) )
21 13 14 18 19 20 dvdstrd ⊢ ( ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) ∧ 𝐴 ∥ ( 𝐵 − - 𝐶 ) ) → 𝐷 ∥ ( 𝐵 − - 𝐶 ) )
22 21 ex ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) → ( 𝐴 ∥ ( 𝐵 − - 𝐶 ) → 𝐷 ∥ ( 𝐵 − - 𝐶 ) ) )
23 12 22 orim12d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝐷 ∥ 𝐴 ) → ( ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∨ 𝐴 ∥ ( 𝐵 − - 𝐶 ) ) → ( 𝐷 ∥ ( 𝐵 − 𝐶 ) ∨ 𝐷 ∥ ( 𝐵 − - 𝐶 ) ) ) )
24 23 expimpd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( ( 𝐷 ∥ 𝐴 ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∨ 𝐴 ∥ ( 𝐵 − - 𝐶 ) ) ) → ( 𝐷 ∥ ( 𝐵 − 𝐶 ) ∨ 𝐷 ∥ ( 𝐵 − - 𝐶 ) ) ) )
25 24 3impia ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐷 ∥ 𝐴 ∧ ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∨ 𝐴 ∥ ( 𝐵 − - 𝐶 ) ) ) ) → ( 𝐷 ∥ ( 𝐵 − 𝐶 ) ∨ 𝐷 ∥ ( 𝐵 − - 𝐶 ) ) )