Proof of Theorem dvdsaddre2b
| Step | Hyp | Ref
| Expression |
| 1 | | dvdsadd2b 16343 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵))) |
| 2 | 1 | a1d 25 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐵 ∈ ℝ → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵)))) |
| 3 | 2 | 3exp 1120 |
. . . . 5
⊢ (𝐴 ∈ ℤ → (𝐵 ∈ ℤ → ((𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶) → (𝐵 ∈ ℝ → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵)))))) |
| 4 | 3 | com24 95 |
. . . 4
⊢ (𝐴 ∈ ℤ → (𝐵 ∈ ℝ → ((𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶) → (𝐵 ∈ ℤ → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵)))))) |
| 5 | 4 | 3imp 1111 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐵 ∈ ℤ → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵)))) |
| 6 | 5 | com12 32 |
. 2
⊢ (𝐵 ∈ ℤ → ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵)))) |
| 7 | | dvdszrcl 16295 |
. . . . . . 7
⊢ (𝐴 ∥ 𝐵 → (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) |
| 8 | | pm2.24 124 |
. . . . . . 7
⊢ (𝐵 ∈ ℤ → (¬
𝐵 ∈ ℤ →
𝐴 ∥ (𝐶 + 𝐵))) |
| 9 | 7, 8 | simpl2im 503 |
. . . . . 6
⊢ (𝐴 ∥ 𝐵 → (¬ 𝐵 ∈ ℤ → 𝐴 ∥ (𝐶 + 𝐵))) |
| 10 | 9 | com12 32 |
. . . . 5
⊢ (¬
𝐵 ∈ ℤ →
(𝐴 ∥ 𝐵 → 𝐴 ∥ (𝐶 + 𝐵))) |
| 11 | 10 | adantr 480 |
. . . 4
⊢ ((¬
𝐵 ∈ ℤ ∧
(𝐴 ∈ ℤ ∧
𝐵 ∈ ℝ ∧
(𝐶 ∈ ℤ ∧
𝐴 ∥ 𝐶))) → (𝐴 ∥ 𝐵 → 𝐴 ∥ (𝐶 + 𝐵))) |
| 12 | | dvdszrcl 16295 |
. . . . . 6
⊢ (𝐴 ∥ (𝐶 + 𝐵) → (𝐴 ∈ ℤ ∧ (𝐶 + 𝐵) ∈ ℤ)) |
| 13 | | zcn 12618 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐶 ∈ ℤ → 𝐶 ∈
ℂ) |
| 14 | 13 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ ℤ ∧ (𝐵 ∈ ℝ ∧ ¬
𝐵 ∈ ℤ)) →
𝐶 ∈
ℂ) |
| 15 | | recn 11245 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
| 16 | 15 | ad2antrl 728 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ ℤ ∧ (𝐵 ∈ ℝ ∧ ¬
𝐵 ∈ ℤ)) →
𝐵 ∈
ℂ) |
| 17 | 14, 16 | addcomd 11463 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ ℤ ∧ (𝐵 ∈ ℝ ∧ ¬
𝐵 ∈ ℤ)) →
(𝐶 + 𝐵) = (𝐵 + 𝐶)) |
| 18 | | eldif 3961 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ (ℝ ∖
ℤ) ↔ (𝐵 ∈
ℝ ∧ ¬ 𝐵
∈ ℤ)) |
| 19 | | nzadd 12665 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ (ℝ ∖
ℤ) ∧ 𝐶 ∈
ℤ) → (𝐵 + 𝐶) ∈ (ℝ ∖
ℤ)) |
| 20 | 19 | eldifbd 3964 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ (ℝ ∖
ℤ) ∧ 𝐶 ∈
ℤ) → ¬ (𝐵 +
𝐶) ∈
ℤ) |
| 21 | 20 | expcom 413 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐶 ∈ ℤ → (𝐵 ∈ (ℝ ∖
ℤ) → ¬ (𝐵 +
𝐶) ∈
ℤ)) |
| 22 | 18, 21 | biimtrrid 243 |
. . . . . . . . . . . . . . . 16
⊢ (𝐶 ∈ ℤ → ((𝐵 ∈ ℝ ∧ ¬
𝐵 ∈ ℤ) →
¬ (𝐵 + 𝐶) ∈
ℤ)) |
| 23 | 22 | imp 406 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ ℤ ∧ (𝐵 ∈ ℝ ∧ ¬
𝐵 ∈ ℤ)) →
¬ (𝐵 + 𝐶) ∈
ℤ) |
| 24 | 17, 23 | eqneltrd 2861 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ ℤ ∧ (𝐵 ∈ ℝ ∧ ¬
𝐵 ∈ ℤ)) →
¬ (𝐶 + 𝐵) ∈
ℤ) |
| 25 | 24 | exp32 420 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ ℤ → (𝐵 ∈ ℝ → (¬
𝐵 ∈ ℤ →
¬ (𝐶 + 𝐵) ∈
ℤ))) |
| 26 | | pm2.21 123 |
. . . . . . . . . . . . 13
⊢ (¬
(𝐶 + 𝐵) ∈ ℤ → ((𝐶 + 𝐵) ∈ ℤ → 𝐴 ∥ 𝐵)) |
| 27 | 25, 26 | syl8 76 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ ℤ → (𝐵 ∈ ℝ → (¬
𝐵 ∈ ℤ →
((𝐶 + 𝐵) ∈ ℤ → 𝐴 ∥ 𝐵)))) |
| 28 | 27 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶) → (𝐵 ∈ ℝ → (¬ 𝐵 ∈ ℤ → ((𝐶 + 𝐵) ∈ ℤ → 𝐴 ∥ 𝐵)))) |
| 29 | 28 | com12 32 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ → ((𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶) → (¬ 𝐵 ∈ ℤ → ((𝐶 + 𝐵) ∈ ℤ → 𝐴 ∥ 𝐵)))) |
| 30 | 29 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℤ → (𝐵 ∈ ℝ → ((𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶) → (¬ 𝐵 ∈ ℤ → ((𝐶 + 𝐵) ∈ ℤ → 𝐴 ∥ 𝐵))))) |
| 31 | 30 | 3imp 1111 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (¬ 𝐵 ∈ ℤ → ((𝐶 + 𝐵) ∈ ℤ → 𝐴 ∥ 𝐵))) |
| 32 | 31 | impcom 407 |
. . . . . . 7
⊢ ((¬
𝐵 ∈ ℤ ∧
(𝐴 ∈ ℤ ∧
𝐵 ∈ ℝ ∧
(𝐶 ∈ ℤ ∧
𝐴 ∥ 𝐶))) → ((𝐶 + 𝐵) ∈ ℤ → 𝐴 ∥ 𝐵)) |
| 33 | 32 | com12 32 |
. . . . . 6
⊢ ((𝐶 + 𝐵) ∈ ℤ → ((¬ 𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶))) → 𝐴 ∥ 𝐵)) |
| 34 | 12, 33 | simpl2im 503 |
. . . . 5
⊢ (𝐴 ∥ (𝐶 + 𝐵) → ((¬ 𝐵 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶))) → 𝐴 ∥ 𝐵)) |
| 35 | 34 | com12 32 |
. . . 4
⊢ ((¬
𝐵 ∈ ℤ ∧
(𝐴 ∈ ℤ ∧
𝐵 ∈ ℝ ∧
(𝐶 ∈ ℤ ∧
𝐴 ∥ 𝐶))) → (𝐴 ∥ (𝐶 + 𝐵) → 𝐴 ∥ 𝐵)) |
| 36 | 11, 35 | impbid 212 |
. . 3
⊢ ((¬
𝐵 ∈ ℤ ∧
(𝐴 ∈ ℤ ∧
𝐵 ∈ ℝ ∧
(𝐶 ∈ ℤ ∧
𝐴 ∥ 𝐶))) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵))) |
| 37 | 36 | ex 412 |
. 2
⊢ (¬
𝐵 ∈ ℤ →
((𝐴 ∈ ℤ ∧
𝐵 ∈ ℝ ∧
(𝐶 ∈ ℤ ∧
𝐴 ∥ 𝐶)) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵)))) |
| 38 | 6, 37 | pm2.61i 182 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵))) |