Step |
Hyp |
Ref |
Expression |
1 |
|
simprr |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ) → 𝐴 ∥ ( 𝐵 − 𝐶 ) ) |
2 |
|
zcn |
⊢ ( 𝐶 ∈ ℤ → 𝐶 ∈ ℂ ) |
3 |
2
|
ad2antrl |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ) → 𝐶 ∈ ℂ ) |
4 |
|
zcn |
⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ ) |
5 |
4
|
ad2antlr |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ) → 𝐵 ∈ ℂ ) |
6 |
3 5
|
negsubdi2d |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ) → - ( 𝐶 − 𝐵 ) = ( 𝐵 − 𝐶 ) ) |
7 |
1 6
|
breqtrrd |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ) → 𝐴 ∥ - ( 𝐶 − 𝐵 ) ) |
8 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ) → 𝐴 ∈ ℤ ) |
9 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ) → 𝐶 ∈ ℤ ) |
10 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ) → 𝐵 ∈ ℤ ) |
11 |
9 10
|
zsubcld |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ) → ( 𝐶 − 𝐵 ) ∈ ℤ ) |
12 |
|
dvdsnegb |
⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐶 − 𝐵 ) ∈ ℤ ) → ( 𝐴 ∥ ( 𝐶 − 𝐵 ) ↔ 𝐴 ∥ - ( 𝐶 − 𝐵 ) ) ) |
13 |
8 11 12
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ) → ( 𝐴 ∥ ( 𝐶 − 𝐵 ) ↔ 𝐴 ∥ - ( 𝐶 − 𝐵 ) ) ) |
14 |
7 13
|
mpbird |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐴 ∥ ( 𝐵 − 𝐶 ) ) ) → 𝐴 ∥ ( 𝐶 − 𝐵 ) ) |