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 biimtrrid ⊢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