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