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 ABxAx=BBA

Proof

Step Hyp Ref Expression
1 risset BAxx=BA
2 eqcom x=BABA=x
3 nncn BB
4 3 ad2antlr ABxB
5 nncn AA
6 5 ad2antrr ABxA
7 nncn xx
8 7 adantl ABxx
9 nnne0 AA0
10 9 ad2antrr ABxA0
11 4 6 8 10 divmuld ABxBA=xAx=B
12 2 11 bitrid ABxx=BAAx=B
13 12 rexbidva ABxx=BAxAx=B
14 1 13 bitr2id ABxAx=BBA