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

Proof

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