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	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\wedge \left(M\parallel N\wedge N\parallel M\right)\right)\to M=N$$

Proof

Step	Hyp	Ref	Expression
1		dvdsabseq	$$⊢\left(M\parallel N\wedge N\parallel M\right)\to \left|M\right|=\left|N\right|$$
2		nn0re	$$⊢M\in {\mathbb{N}}_0\to M\in ℝ$$
3		nn0ge0	$$⊢M\in {\mathbb{N}}_0\to 0\le M$$
4	2 3	absidd	$$⊢M\in {\mathbb{N}}_0\to \left|M\right|=M$$
5	4	adantr	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left|M\right|=M$$
6	5	eqcomd	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to M=\left|M\right|$$
7	6	adantr	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\wedge \left|M\right|=\left|N\right|\right)\to M=\left|M\right|$$
8		simpr	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\wedge \left|M\right|=\left|N\right|\right)\to \left|M\right|=\left|N\right|$$
9		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
10		nn0ge0	$$⊢N\in {\mathbb{N}}_0\to 0\le N$$
11	9 10	absidd	$$⊢N\in {\mathbb{N}}_0\to \left|N\right|=N$$
12	11	ad2antlr	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\wedge \left|M\right|=\left|N\right|\right)\to \left|N\right|=N$$
13	7 8 12	3eqtrd	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\wedge \left|M\right|=\left|N\right|\right)\to M=N$$
14	1 13	sylan2	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\wedge \left(M\parallel N\wedge N\parallel M\right)\right)\to M=N$$