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 ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℕ )

Proof

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 𝐵 ) ) ∈ ℕ )