Metamath Proof Explorer

Theorem divgcdnnr

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 divgcdnnr ⊢ A ∈ ℕ ∧ B ∈ ℤ → A B gcd A ∈ ℕ

Proof

Step Hyp Ref Expression
1 nnz ⊢ A ∈ ℕ → A ∈ ℤ
2 gcdcom ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B = B gcd A
3 1 2 sylan ⊢ A ∈ ℕ ∧ B ∈ ℤ → A gcd B = B gcd A
4 3 eqcomd ⊢ A ∈ ℕ ∧ B ∈ ℤ → B gcd A = A gcd B
5 4 oveq2d ⊢ A ∈ ℕ ∧ B ∈ ℤ → A B gcd A = A A gcd B
6 divgcdnn ⊢ A ∈ ℕ ∧ B ∈ ℤ → A A gcd B ∈ ℕ
7 5 6 eqeltrd ⊢ A ∈ ℕ ∧ B ∈ ℤ → A B gcd A ∈ ℕ