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