dvdsadd2b

Description: Adding a multiple of the base does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014)

		Ref	Expression
	Assertion	dvdsadd2b	$⊢ (A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \to (A ∥ B \leftrightarrow A ∥ (C + B))$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ B) \to A \in ℤ$
2		simpl3l	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ B) \to C \in ℤ$
3		simpl2	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ B) \to B \in ℤ$
4		simpl3r	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ B) \to A ∥ C$
5		simpr	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ B) \to A ∥ B$
6	1 2 3 4 5	dvds2addd	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ B) \to A ∥ (C + B)$
7		simpl1	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to A \in ℤ$
8		simp3l	$⊢ (A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \to C \in ℤ$
9		simp2	$⊢ (A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \to B \in ℤ$
10		zaddcl	$⊢ (C \in ℤ \land B \in ℤ) \to C + B \in ℤ$
11	8 9 10	syl2anc	$⊢ (A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \to C + B \in ℤ$
12	11	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to C + B \in ℤ$
13	8	znegcld	$⊢ (A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \to - C \in ℤ$
14	13	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to - C \in ℤ$
15		simpr	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to A ∥ (C + B)$
16		simpl3r	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to A ∥ C$
17		simpl3l	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to C \in ℤ$
18		dvdsnegb	$⊢ (A \in ℤ \land C \in ℤ) \to (A ∥ C \leftrightarrow A ∥ (- C))$
19	7 17 18	syl2anc	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to (A ∥ C \leftrightarrow A ∥ (- C))$
20	16 19	mpbid	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to A ∥ (- C)$
21	7 12 14 15 20	dvds2addd	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to A ∥ (C + B + (- C))$
22		simpl2	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to B \in ℤ$
23	10	ancoms	$⊢ (B \in ℤ \land C \in ℤ) \to C + B \in ℤ$
24	23	zcnd	$⊢ (B \in ℤ \land C \in ℤ) \to C + B \in ℂ$
25		zcn	$⊢ C \in ℤ \to C \in ℂ$
26	25	adantl	$⊢ (B \in ℤ \land C \in ℤ) \to C \in ℂ$
27	24 26	negsubd	$⊢ (B \in ℤ \land C \in ℤ) \to C + B + (- C) = C + B - C$
28		zcn	$⊢ B \in ℤ \to B \in ℂ$
29	28	adantr	$⊢ (B \in ℤ \land C \in ℤ) \to B \in ℂ$
30	26 29	pncan2d	$⊢ (B \in ℤ \land C \in ℤ) \to C + B - C = B$
31	27 30	eqtrd	$⊢ (B \in ℤ \land C \in ℤ) \to C + B + (- C) = B$
32	22 17 31	syl2anc	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to C + B + (- C) = B$
33	21 32	breqtrd	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to A ∥ B$
34	6 33	impbida	$⊢ (A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \to (A ∥ B \leftrightarrow A ∥ (C + B))$

Metamath Proof Explorer

Theorem dvdsadd2b

Proof