Step |
Hyp |
Ref |
Expression |
1 |
|
nnz |
⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℤ ) |
2 |
|
nnz |
⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ ) |
3 |
|
nnz |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ ) |
4 |
1 2 3
|
3anim123i |
⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) |
5 |
|
nnne0 |
⊢ ( 𝑀 ∈ ℕ → 𝑀 ≠ 0 ) |
6 |
5
|
neneqd |
⊢ ( 𝑀 ∈ ℕ → ¬ 𝑀 = 0 ) |
7 |
6
|
3ad2ant2 |
⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ¬ 𝑀 = 0 ) |
8 |
7
|
intnanrd |
⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) |
9 |
|
dvdslegcd |
⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ≤ ( 𝑀 gcd 𝑁 ) ) ) |
10 |
4 8 9
|
syl2anc |
⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ≤ ( 𝑀 gcd 𝑁 ) ) ) |