This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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