Metamath Proof Explorer

Theorem dvdsaddre2b

Description: Adding a multiple of the base does not affect divisibility. Variant of dvdsadd2b only requiring B to be a real number (not necessarily an integer). (Contributed by AV, 19-Jul-2021)

Ref Expression
Assertion dvdsaddre2b ⊢ A ∈ ℤ ∧ B ∈ ℝ ∧ C ∈ ℤ ∧ A ∥ C → A ∥ B ↔ A ∥ C + B

Proof

Step Hyp Ref Expression
1 dvdsadd2b ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ C → A ∥ B ↔ A ∥ C + B
2 1 a1d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A ∥ C → B ∈ ℝ → A ∥ B ↔ A ∥ C + B
3 2 3exp ⊢ A ∈ ℤ → B ∈ ℤ → C ∈ ℤ ∧ A ∥ C → B ∈ ℝ → A ∥ B ↔ A ∥ C + B
4 3 com24 ⊢ A ∈ ℤ → B ∈ ℝ → C ∈ ℤ ∧ A ∥ C → B ∈ ℤ → A ∥ B ↔ A ∥ C + B
5 4 3imp ⊢ A ∈ ℤ ∧ B ∈ ℝ ∧ C ∈ ℤ ∧ A ∥ C → B ∈ ℤ → A ∥ B ↔ A ∥ C + B
6 5 com12 ⊢ B ∈ ℤ → A ∈ ℤ ∧ B ∈ ℝ ∧ C ∈ ℤ ∧ A ∥ C → A ∥ B ↔ A ∥ C + B
7 dvdszrcl ⊢ A ∥ B → A ∈ ℤ ∧ B ∈ ℤ
8 pm2.24 ⊢ B ∈ ℤ → ¬ B ∈ ℤ → A ∥ C + B
9 7 8 simpl2im ⊢ A ∥ B → ¬ B ∈ ℤ → A ∥ C + B
10 9 com12 ⊢ ¬ B ∈ ℤ → A ∥ B → A ∥ C + B
11 10 adantr ⊢ ¬ B ∈ ℤ ∧ A ∈ ℤ ∧ B ∈ ℝ ∧ C ∈ ℤ ∧ A ∥ C → A ∥ B → A ∥ C + B
12 dvdszrcl ⊢ A ∥ C + B → A ∈ ℤ ∧ C + B ∈ ℤ
13 zcn ⊢ C ∈ ℤ → C ∈ ℂ
14 13 adantr ⊢ C ∈ ℤ ∧ B ∈ ℝ ∧ ¬ B ∈ ℤ → C ∈ ℂ
15 recn ⊢ B ∈ ℝ → B ∈ ℂ
16 15 ad2antrl ⊢ C ∈ ℤ ∧ B ∈ ℝ ∧ ¬ B ∈ ℤ → B ∈ ℂ
17 14 16 addcomd ⊢ C ∈ ℤ ∧ B ∈ ℝ ∧ ¬ B ∈ ℤ → C + B = B + C
18 eldif ⊢ B ∈ ℝ ∖ ℤ ↔ B ∈ ℝ ∧ ¬ B ∈ ℤ
19 nzadd ⊢ B ∈ ℝ ∖ ℤ ∧ C ∈ ℤ → B + C ∈ ℝ ∖ ℤ
20 19 eldifbd ⊢ B ∈ ℝ ∖ ℤ ∧ C ∈ ℤ → ¬ B + C ∈ ℤ
21 20 expcom ⊢ C ∈ ℤ → B ∈ ℝ ∖ ℤ → ¬ B + C ∈ ℤ
22 18 21 syl5bir ⊢ C ∈ ℤ → B ∈ ℝ ∧ ¬ B ∈ ℤ → ¬ B + C ∈ ℤ
23 22 imp ⊢ C ∈ ℤ ∧ B ∈ ℝ ∧ ¬ B ∈ ℤ → ¬ B + C ∈ ℤ
24 17 23 eqneltrd ⊢ C ∈ ℤ ∧ B ∈ ℝ ∧ ¬ B ∈ ℤ → ¬ C + B ∈ ℤ
25 24 exp32 ⊢ C ∈ ℤ → B ∈ ℝ → ¬ B ∈ ℤ → ¬ C + B ∈ ℤ
26 pm2.21 ⊢ ¬ C + B ∈ ℤ → C + B ∈ ℤ → A ∥ B
27 25 26 syl8 ⊢ C ∈ ℤ → B ∈ ℝ → ¬ B ∈ ℤ → C + B ∈ ℤ → A ∥ B
28 27 adantr ⊢ C ∈ ℤ ∧ A ∥ C → B ∈ ℝ → ¬ B ∈ ℤ → C + B ∈ ℤ → A ∥ B
29 28 com12 ⊢ B ∈ ℝ → C ∈ ℤ ∧ A ∥ C → ¬ B ∈ ℤ → C + B ∈ ℤ → A ∥ B
30 29 a1i ⊢ A ∈ ℤ → B ∈ ℝ → C ∈ ℤ ∧ A ∥ C → ¬ B ∈ ℤ → C + B ∈ ℤ → A ∥ B
31 30 3imp ⊢ A ∈ ℤ ∧ B ∈ ℝ ∧ C ∈ ℤ ∧ A ∥ C → ¬ B ∈ ℤ → C + B ∈ ℤ → A ∥ B
32 31 impcom ⊢ ¬ B ∈ ℤ ∧ A ∈ ℤ ∧ B ∈ ℝ ∧ C ∈ ℤ ∧ A ∥ C → C + B ∈ ℤ → A ∥ B
33 32 com12 ⊢ C + B ∈ ℤ → ¬ B ∈ ℤ ∧ A ∈ ℤ ∧ B ∈ ℝ ∧ C ∈ ℤ ∧ A ∥ C → A ∥ B
34 12 33 simpl2im ⊢ A ∥ C + B → ¬ B ∈ ℤ ∧ A ∈ ℤ ∧ B ∈ ℝ ∧ C ∈ ℤ ∧ A ∥ C → A ∥ B
35 34 com12 ⊢ ¬ B ∈ ℤ ∧ A ∈ ℤ ∧ B ∈ ℝ ∧ C ∈ ℤ ∧ A ∥ C → A ∥ C + B → A ∥ B
36 11 35 impbid ⊢ ¬ B ∈ ℤ ∧ A ∈ ℤ ∧ B ∈ ℝ ∧ C ∈ ℤ ∧ A ∥ C → A ∥ B ↔ A ∥ C + B
37 36 ex ⊢ ¬ B ∈ ℤ → A ∈ ℤ ∧ B ∈ ℝ ∧ C ∈ ℤ ∧ A ∥ C → A ∥ B ↔ A ∥ C + B
38 6 37 pm2.61i ⊢ A ∈ ℤ ∧ B ∈ ℝ ∧ C ∈ ℤ ∧ A ∥ C → A ∥ B ↔ A ∥ C + B