Metamath Proof Explorer

Theorem nndivides

Description: Definition of the divides relation for positive integers. (Contributed by AV, 26-Jul-2021)

Ref Expression
Assertion nndivides 
|- ( ( M e. NN /\ N e. NN ) -> ( M || N <-> E. n e. NN ( n x. M ) = N ) )

Proof

Step Hyp Ref Expression
1 nndiv 
 |-  ( ( M e. NN /\ N e. NN ) -> ( E. n e. NN ( M x. n ) = N <-> ( N / M ) e. NN ) )
2 nncn 
 |-  ( n e. NN -> n e. CC )
3 2 adantl 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) -> n e. CC )
4 nncn 
 |-  ( M e. NN -> M e. CC )
5 4 ad2antrr 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) -> M e. CC )
6 3 5 mulcomd 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) -> ( n x. M ) = ( M x. n ) )
7 6 eqeq1d 
 |-  ( ( ( M e. NN /\ N e. NN ) /\ n e. NN ) -> ( ( n x. M ) = N <-> ( M x. n ) = N ) )
8 7 rexbidva 
 |-  ( ( M e. NN /\ N e. NN ) -> ( E. n e. NN ( n x. M ) = N <-> E. n e. NN ( M x. n ) = N ) )
9 nndivdvds 
 |-  ( ( N e. NN /\ M e. NN ) -> ( M || N <-> ( N / M ) e. NN ) )
10 9 ancoms 
 |-  ( ( M e. NN /\ N e. NN ) -> ( M || N <-> ( N / M ) e. NN ) )
11 1 8 10 3bitr4rd 
 |-  ( ( M e. NN /\ N e. NN ) -> ( M || N <-> E. n e. NN ( n x. M ) = N ) )