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