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	|- ( ( A e. NN /\ B e. ZZ ) -> ( A / ( A gcd B ) ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		nnz	|- ( A e. NN -> A e. ZZ )
2	1	anim1i	|- ( ( A e. NN /\ B e. ZZ ) -> ( A e. ZZ /\ B e. ZZ ) )
3		gcddvds	|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
4	3	simpld	|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) || A )
5	2 4	syl	|- ( ( A e. NN /\ B e. ZZ ) -> ( A gcd B ) || A )
6		nnne0	|- ( A e. NN -> A =/= 0 )
7	6	neneqd	|- ( A e. NN -> -. A = 0 )
8	7	adantr	|- ( ( A e. NN /\ B e. ZZ ) -> -. A = 0 )
9	8	intnanrd	|- ( ( A e. NN /\ B e. ZZ ) -> -. ( A = 0 /\ B = 0 ) )
10		gcdn0cl	|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 /\ B = 0 ) ) -> ( A gcd B ) e. NN )
11	2 9 10	syl2anc	|- ( ( A e. NN /\ B e. ZZ ) -> ( A gcd B ) e. NN )
12		nndivdvds	|- ( ( A e. NN /\ ( A gcd B ) e. NN ) -> ( ( A gcd B ) || A <-> ( A / ( A gcd B ) ) e. NN ) )
13	11 12	syldan	|- ( ( A e. NN /\ B e. ZZ ) -> ( ( A gcd B ) || A <-> ( A / ( A gcd B ) ) e. NN ) )
14	5 13	mpbid	|- ( ( A e. NN /\ B e. ZZ ) -> ( A / ( A gcd B ) ) e. NN )