This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvdseq

Description: If two nonnegative integers divide each other, they must be equal. (Contributed by Mario Carneiro, 30-May-2014) (Proof shortened by AV, 7-Aug-2021)

Ref Expression
Assertion dvdseq 
|- ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( M || N /\ N || M ) ) -> M = N )

Proof

Step Hyp Ref Expression
1 dvdsabseq 
 |-  ( ( M || N /\ N || M ) -> ( abs ` M ) = ( abs ` N ) )
2 nn0re 
 |-  ( M e. NN0 -> M e. RR )
3 nn0ge0 
 |-  ( M e. NN0 -> 0 <_ M )
4 2 3 absidd 
 |-  ( M e. NN0 -> ( abs ` M ) = M )
5 4 adantr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( abs ` M ) = M )
6 5 eqcomd 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> M = ( abs ` M ) )
7 6 adantr 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( abs ` M ) = ( abs ` N ) ) -> M = ( abs ` M ) )
8 simpr 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( abs ` M ) = ( abs ` N ) ) -> ( abs ` M ) = ( abs ` N ) )
9 nn0re 
 |-  ( N e. NN0 -> N e. RR )
10 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
11 9 10 absidd 
 |-  ( N e. NN0 -> ( abs ` N ) = N )
12 11 ad2antlr 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( abs ` M ) = ( abs ` N ) ) -> ( abs ` N ) = N )
13 7 8 12 3eqtrd 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( abs ` M ) = ( abs ` N ) ) -> M = N )
14 1 13 sylan2 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( M || N /\ N || M ) ) -> M = N )