Metamath Proof Explorer

Theorem 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∈ℤ∧B∈ℤ∧C∈ℤ∧A∥C→A∥B↔A∥C+B

Proof

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