Metamath Proof Explorer

Theorem divgcdnn

Description: A positive integer divided by the gcd of it and another integer is a positive integer. (Contributed by AV, 10-Jul-2021)

Ref Expression
Assertion divgcdnn ⊢ A ∈ ℕ ∧ B ∈ ℤ → A A gcd B ∈ ℕ

Proof

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