Step |
Hyp |
Ref |
Expression |
1 |
|
3simpa |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) |
2 |
|
3simpb |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) |
3 |
|
zsubcl |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 − 𝑁 ) ∈ ℤ ) |
4 |
3
|
anim2i |
⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝐾 ∈ ℤ ∧ ( 𝑀 − 𝑁 ) ∈ ℤ ) ) |
5 |
4
|
3impb |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ℤ ∧ ( 𝑀 − 𝑁 ) ∈ ℤ ) ) |
6 |
|
zsubcl |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 − 𝑦 ) ∈ ℤ ) |
7 |
6
|
adantl |
⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 − 𝑦 ) ∈ ℤ ) |
8 |
|
zcn |
⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ ) |
9 |
|
zcn |
⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ ) |
10 |
|
zcn |
⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ ) |
11 |
|
subdir |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( ( 𝑥 − 𝑦 ) · 𝐾 ) = ( ( 𝑥 · 𝐾 ) − ( 𝑦 · 𝐾 ) ) ) |
12 |
8 9 10 11
|
syl3an |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑥 − 𝑦 ) · 𝐾 ) = ( ( 𝑥 · 𝐾 ) − ( 𝑦 · 𝐾 ) ) ) |
13 |
12
|
3comr |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 − 𝑦 ) · 𝐾 ) = ( ( 𝑥 · 𝐾 ) − ( 𝑦 · 𝐾 ) ) ) |
14 |
13
|
3expb |
⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑥 − 𝑦 ) · 𝐾 ) = ( ( 𝑥 · 𝐾 ) − ( 𝑦 · 𝐾 ) ) ) |
15 |
|
oveq12 |
⊢ ( ( ( 𝑥 · 𝐾 ) = 𝑀 ∧ ( 𝑦 · 𝐾 ) = 𝑁 ) → ( ( 𝑥 · 𝐾 ) − ( 𝑦 · 𝐾 ) ) = ( 𝑀 − 𝑁 ) ) |
16 |
14 15
|
sylan9eq |
⊢ ( ( ( 𝐾 ∈ ℤ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) ∧ ( ( 𝑥 · 𝐾 ) = 𝑀 ∧ ( 𝑦 · 𝐾 ) = 𝑁 ) ) → ( ( 𝑥 − 𝑦 ) · 𝐾 ) = ( 𝑀 − 𝑁 ) ) |
17 |
16
|
ex |
⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( 𝑥 · 𝐾 ) = 𝑀 ∧ ( 𝑦 · 𝐾 ) = 𝑁 ) → ( ( 𝑥 − 𝑦 ) · 𝐾 ) = ( 𝑀 − 𝑁 ) ) ) |
18 |
17
|
3ad2antl1 |
⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( 𝑥 · 𝐾 ) = 𝑀 ∧ ( 𝑦 · 𝐾 ) = 𝑁 ) → ( ( 𝑥 − 𝑦 ) · 𝐾 ) = ( 𝑀 − 𝑁 ) ) ) |
19 |
1 2 5 7 18
|
dvds2lem |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ∥ ( 𝑀 − 𝑁 ) ) ) |