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		simprr	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to D \in ℤ$
2	1	ad2antrr	$⊢ ((((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land D ∥ A) \land A ∥ (B - C)) \to D \in ℤ$
3		simp-4l	$⊢ ((((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land D ∥ A) \land A ∥ (B - C)) \to A \in ℤ$
4		simplr	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to B \in ℤ$
5	4	ad2antrr	$⊢ ((((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land D ∥ A) \land A ∥ (B - C)) \to B \in ℤ$
6		simprl	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to C \in ℤ$
7	6	ad2antrr	$⊢ ((((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land D ∥ A) \land A ∥ (B - C)) \to C \in ℤ$
8	5 7	zsubcld	$⊢ ((((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land D ∥ A) \land A ∥ (B - C)) \to B - C \in ℤ$
9		simplr	$⊢ ((((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land D ∥ A) \land A ∥ (B - C)) \to D ∥ A$
10		simpr	$⊢ ((((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land D ∥ A) \land A ∥ (B - C)) \to A ∥ (B - C)$
11	2 3 8 9 10	dvdstrd	$⊢ ((((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land D ∥ A) \land A ∥ (B - C)) \to D ∥ (B - C)$
12	11	ex	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land D ∥ A) \to (A ∥ (B - C) \to D ∥ (B - C))$
13	1	ad2antrr	$⊢ ((((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land D ∥ A) \land A ∥ (B - (- C))) \to D \in ℤ$
14		simp-4l	$⊢ ((((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land D ∥ A) \land A ∥ (B - (- C))) \to A \in ℤ$
15	4	ad2antrr	$⊢ ((((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land D ∥ A) \land A ∥ (B - (- C))) \to B \in ℤ$
16	6	ad2antrr	$⊢ ((((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land D ∥ A) \land A ∥ (B - (- C))) \to C \in ℤ$
17	16	znegcld	$⊢ ((((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land D ∥ A) \land A ∥ (B - (- C))) \to - C \in ℤ$
18	15 17	zsubcld	$⊢ ((((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land D ∥ A) \land A ∥ (B - (- C))) \to B - (- C) \in ℤ$
19		simplr	$⊢ ((((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land D ∥ A) \land A ∥ (B - (- C))) \to D ∥ A$
20		simpr	$⊢ ((((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land D ∥ A) \land A ∥ (B - (- C))) \to A ∥ (B - (- C))$
21	13 14 18 19 20	dvdstrd	$⊢ ((((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land D ∥ A) \land A ∥ (B - (- C))) \to D ∥ (B - (- C))$
22	21	ex	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land D ∥ A) \to (A ∥ (B - (- C)) \to D ∥ (B - (- C)))$
23	12 22	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))))$
24	23	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))))$
25	24	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