Metamath Proof Explorer

Theorem divgcdnnr

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

Proof

Step Hyp Ref Expression
1 nnz 
 |-  ( A e. NN -> A e. ZZ )
2 gcdcom 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) = ( B gcd A ) )
3 1 2 sylan 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( A gcd B ) = ( B gcd A ) )
4 3 eqcomd 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( B gcd A ) = ( A gcd B ) )
5 4 oveq2d 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( A / ( B gcd A ) ) = ( A / ( A gcd B ) ) )
6 divgcdnn 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( A / ( A gcd B ) ) e. NN )
7 5 6 eqeltrd 
 |-  ( ( A e. NN /\ B e. ZZ ) -> ( A / ( B gcd A ) ) e. NN )