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	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{Z}\right)\to \frac{A}{A\gcd B}\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		nnz	$$⊢A\in \mathbb{N}\to A\in \mathbb{Z}$$
2	1	anim1i	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{Z}\right)\to \left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)$$
3		gcddvds	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to \left(\left(A\gcd B\right)\parallel A\wedge \left(A\gcd B\right)\parallel B\right)$$
4	3	simpld	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to \left(A\gcd B\right)\parallel A$$
5	2 4	syl	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{Z}\right)\to \left(A\gcd B\right)\parallel A$$
6		nnne0	$$⊢A\in \mathbb{N}\to A\ne 0$$
7	6	neneqd	$$⊢A\in \mathbb{N}\to \neg A=0$$
8	7	adantr	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{Z}\right)\to \neg A=0$$
9	8	intnanrd	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{Z}\right)\to \neg \left(A=0\wedge B=0\right)$$
10		gcdn0cl	$$⊢\left(\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\wedge \neg \left(A=0\wedge B=0\right)\right)\to A\gcd B\in \mathbb{N}$$
11	2 9 10	syl2anc	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{Z}\right)\to A\gcd B\in \mathbb{N}$$
12		nndivdvds	$$⊢\left(A\in \mathbb{N}\wedge A\gcd B\in \mathbb{N}\right)\to \left(\left(A\gcd B\right)\parallel A\leftrightarrow \frac{A}{A\gcd B}\in \mathbb{N}\right)$$
13	11 12	syldan	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{Z}\right)\to \left(\left(A\gcd B\right)\parallel A\leftrightarrow \frac{A}{A\gcd B}\in \mathbb{N}\right)$$
14	5 13	mpbid	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{Z}\right)\to \frac{A}{A\gcd B}\in \mathbb{N}$$