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 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶 ) ) → ( 𝐴 ∥ 𝐵 ↔ 𝐴 ∥ ( 𝐶 + 𝐵 ) ) )

Proof

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