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		dvds2add	$⊢ (A \in ℤ \land C \in ℤ \land B \in ℤ) \to ((A ∥ C \land A ∥ B) \to A ∥ (C + B))$
7	6	imp	$⊢ ((A \in ℤ \land C \in ℤ \land B \in ℤ) \land (A ∥ C \land A ∥ B)) \to A ∥ (C + B)$
8	1 2 3 4 5 7	syl32anc	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ B) \to A ∥ (C + B)$
9		simpl1	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to A \in ℤ$
10		simp3l	$⊢ (A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \to C \in ℤ$
11		simp2	$⊢ (A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \to B \in ℤ$
12		zaddcl	$⊢ (C \in ℤ \land B \in ℤ) \to C + B \in ℤ$
13	10 11 12	syl2anc	$⊢ (A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \to C + B \in ℤ$
14	13	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to C + B \in ℤ$
15	10	znegcld	$⊢ (A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \to - C \in ℤ$
16	15	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to - C \in ℤ$
17		simpr	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to A ∥ (C + B)$
18		simpl3r	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to A ∥ C$
19		simpl3l	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to C \in ℤ$
20		dvdsnegb	$⊢ (A \in ℤ \land C \in ℤ) \to (A ∥ C \leftrightarrow A ∥ (- C))$
21	9 19 20	syl2anc	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to (A ∥ C \leftrightarrow A ∥ (- C))$
22	18 21	mpbid	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to A ∥ (- C)$
23		dvds2add	$⊢ (A \in ℤ \land C + B \in ℤ \land - C \in ℤ) \to ((A ∥ (C + B) \land A ∥ (- C)) \to A ∥ (C + B + (- C)))$
24	23	imp	$⊢ ((A \in ℤ \land C + B \in ℤ \land - C \in ℤ) \land (A ∥ (C + B) \land A ∥ (- C))) \to A ∥ (C + B + (- C))$
25	9 14 16 17 22 24	syl32anc	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to A ∥ (C + B + (- C))$
26		simpl2	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to B \in ℤ$
27	12	ancoms	$⊢ (B \in ℤ \land C \in ℤ) \to C + B \in ℤ$
28	27	zcnd	$⊢ (B \in ℤ \land C \in ℤ) \to C + B \in ℂ$
29		zcn	$⊢ C \in ℤ \to C \in ℂ$
30	29	adantl	$⊢ (B \in ℤ \land C \in ℤ) \to C \in ℂ$
31	28 30	negsubd	$⊢ (B \in ℤ \land C \in ℤ) \to C + B + (- C) = C + B - C$
32		zcn	$⊢ B \in ℤ \to B \in ℂ$
33	32	adantr	$⊢ (B \in ℤ \land C \in ℤ) \to B \in ℂ$
34	30 33	pncan2d	$⊢ (B \in ℤ \land C \in ℤ) \to C + B - C = B$
35	31 34	eqtrd	$⊢ (B \in ℤ \land C \in ℤ) \to C + B + (- C) = B$
36	26 19 35	syl2anc	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to C + B + (- C) = B$
37	25 36	breqtrd	$⊢ ((A \in ℤ \land B \in ℤ \land (C \in ℤ \land A ∥ C)) \land A ∥ (C + B)) \to A ∥ B$
38	8 37	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