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 \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ) \land (D ∥ A \land (A ∥ (B - C) \lor A ∥ (B - (- C))))) \to (D ∥ (B - C) \lor D ∥ (B - (- C)))$

Proof

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

Metamath Proof Explorer

Theorem dvdsacongtr

Proof