Step |
Hyp |
Ref |
Expression |
1 |
|
lcmdvds |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) → ( 𝑀 lcm 𝑁 ) ∥ 𝐾 ) ) |
2 |
|
dvdslcm |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ ( 𝑀 lcm 𝑁 ) ∧ 𝑁 ∥ ( 𝑀 lcm 𝑁 ) ) ) |
3 |
2
|
simpld |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∥ ( 𝑀 lcm 𝑁 ) ) |
4 |
3
|
3adant1 |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∥ ( 𝑀 lcm 𝑁 ) ) |
5 |
|
simp2 |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℤ ) |
6 |
|
lcmcl |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) ∈ ℕ0 ) |
7 |
6
|
nn0zd |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) ∈ ℤ ) |
8 |
7
|
3adant1 |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) ∈ ℤ ) |
9 |
|
simp1 |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐾 ∈ ℤ ) |
10 |
|
dvdstr |
⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑀 lcm 𝑁 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑀 ∥ ( 𝑀 lcm 𝑁 ) ∧ ( 𝑀 lcm 𝑁 ) ∥ 𝐾 ) → 𝑀 ∥ 𝐾 ) ) |
11 |
5 8 9 10
|
syl3anc |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ∥ ( 𝑀 lcm 𝑁 ) ∧ ( 𝑀 lcm 𝑁 ) ∥ 𝐾 ) → 𝑀 ∥ 𝐾 ) ) |
12 |
4 11
|
mpand |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 lcm 𝑁 ) ∥ 𝐾 → 𝑀 ∥ 𝐾 ) ) |
13 |
2
|
simprd |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∥ ( 𝑀 lcm 𝑁 ) ) |
14 |
13
|
3adant1 |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∥ ( 𝑀 lcm 𝑁 ) ) |
15 |
|
dvdstr |
⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑀 lcm 𝑁 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑁 ∥ ( 𝑀 lcm 𝑁 ) ∧ ( 𝑀 lcm 𝑁 ) ∥ 𝐾 ) → 𝑁 ∥ 𝐾 ) ) |
16 |
15
|
3com13 |
⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 lcm 𝑁 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 ∥ ( 𝑀 lcm 𝑁 ) ∧ ( 𝑀 lcm 𝑁 ) ∥ 𝐾 ) → 𝑁 ∥ 𝐾 ) ) |
17 |
8 16
|
syld3an2 |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 ∥ ( 𝑀 lcm 𝑁 ) ∧ ( 𝑀 lcm 𝑁 ) ∥ 𝐾 ) → 𝑁 ∥ 𝐾 ) ) |
18 |
14 17
|
mpand |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 lcm 𝑁 ) ∥ 𝐾 → 𝑁 ∥ 𝐾 ) ) |
19 |
12 18
|
jcad |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 lcm 𝑁 ) ∥ 𝐾 → ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) ) ) |
20 |
1 19
|
impbid |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) ↔ ( 𝑀 lcm 𝑁 ) ∥ 𝐾 ) ) |