Step |
Hyp |
Ref |
Expression |
1 |
|
dvdsnegb |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ 𝑀 ∥ - 𝑁 ) ) |
2 |
|
znegcl |
⊢ ( 𝑁 ∈ ℤ → - 𝑁 ∈ ℤ ) |
3 |
|
dvdsadd |
⊢ ( ( 𝑀 ∈ ℤ ∧ - 𝑁 ∈ ℤ ) → ( 𝑀 ∥ - 𝑁 ↔ 𝑀 ∥ ( 𝑀 + - 𝑁 ) ) ) |
4 |
2 3
|
sylan2 |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ - 𝑁 ↔ 𝑀 ∥ ( 𝑀 + - 𝑁 ) ) ) |
5 |
|
zcn |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ ) |
6 |
|
zcn |
⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ ) |
7 |
|
negsub |
⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝑀 + - 𝑁 ) = ( 𝑀 − 𝑁 ) ) |
8 |
5 6 7
|
syl2an |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + - 𝑁 ) = ( 𝑀 − 𝑁 ) ) |
9 |
8
|
breq2d |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ ( 𝑀 + - 𝑁 ) ↔ 𝑀 ∥ ( 𝑀 − 𝑁 ) ) ) |
10 |
1 4 9
|
3bitrd |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ( 𝑀 − 𝑁 ) ) ) |