Step |
Hyp |
Ref |
Expression |
1 |
|
nnz |
⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ ) |
2 |
1
|
anim1i |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) |
3 |
|
gcddvds |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) ) |
4 |
3
|
simpld |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ) |
5 |
2 4
|
syl |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ) |
6 |
|
nnne0 |
⊢ ( 𝐴 ∈ ℕ → 𝐴 ≠ 0 ) |
7 |
6
|
neneqd |
⊢ ( 𝐴 ∈ ℕ → ¬ 𝐴 = 0 ) |
8 |
7
|
adantr |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ) → ¬ 𝐴 = 0 ) |
9 |
8
|
intnanrd |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ) → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) |
10 |
|
gcdn0cl |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ ) |
11 |
2 9 10
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ ) |
12 |
|
nndivdvds |
⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ↔ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ ) ) |
13 |
11 12
|
syldan |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ↔ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ ) ) |
14 |
5 13
|
mpbid |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ ) |