Metamath Proof Explorer

Theorem nndiv

Description: Two ways to express " A divides B " for positive integers. (Contributed by NM, 3-Feb-2004) (Proof shortened by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion nndiv 
|- ( ( A e. NN /\ B e. NN ) -> ( E. x e. NN ( A x. x ) = B <-> ( B / A ) e. NN ) )

Proof

Step Hyp Ref Expression
1 risset 
 |-  ( ( B / A ) e. NN <-> E. x e. NN x = ( B / A ) )
2 eqcom 
 |-  ( x = ( B / A ) <-> ( B / A ) = x )
3 nncn 
 |-  ( B e. NN -> B e. CC )
4 3 ad2antlr 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ x e. NN ) -> B e. CC )
5 nncn 
 |-  ( A e. NN -> A e. CC )
6 5 ad2antrr 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ x e. NN ) -> A e. CC )
7 nncn 
 |-  ( x e. NN -> x e. CC )
8 7 adantl 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ x e. NN ) -> x e. CC )
9 nnne0 
 |-  ( A e. NN -> A =/= 0 )
10 9 ad2antrr 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ x e. NN ) -> A =/= 0 )
11 4 6 8 10 divmuld 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ x e. NN ) -> ( ( B / A ) = x <-> ( A x. x ) = B ) )
12 2 11 bitrid 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ x e. NN ) -> ( x = ( B / A ) <-> ( A x. x ) = B ) )
13 12 rexbidva 
 |-  ( ( A e. NN /\ B e. NN ) -> ( E. x e. NN x = ( B / A ) <-> E. x e. NN ( A x. x ) = B ) )
14 1 13 bitr2id 
 |-  ( ( A e. NN /\ B e. NN ) -> ( E. x e. NN ( A x. x ) = B <-> ( B / A ) e. NN ) )