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 M0N0MNNMM=N

Proof

Step Hyp Ref Expression
1 dvdsabseq MNNMM=N
2 nn0re M0M
3 nn0ge0 M00M
4 2 3 absidd M0M=M
5 4 adantr M0N0M=M
6 5 eqcomd M0N0M=M
7 6 adantr M0N0M=NM=M
8 simpr M0N0M=NM=N
9 nn0re N0N
10 nn0ge0 N00N
11 9 10 absidd N0N=N
12 11 ad2antlr M0N0M=NN=N
13 7 8 12 3eqtrd M0N0M=NM=N
14 1 13 sylan2 M0N0MNNMM=N