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 
|- ( ( 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 )