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 ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ M ∥ N ∧ N ∥ M → M = N

Proof

Step Hyp Ref Expression
1 dvdsabseq ⊢ M ∥ N ∧ N ∥ M → M = N
2 nn0re ⊢ M ∈ ℕ 0 → M ∈ ℝ
3 nn0ge0 ⊢ M ∈ ℕ 0 → 0 ≤ M
4 2 3 absidd ⊢ M ∈ ℕ 0 → M = M
5 4 adantr ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ 0 → M = M
6 5 eqcomd ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ 0 → M = M
7 6 adantr ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ M = N → M = M
8 simpr ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ M = N → M = N
9 nn0re ⊢ N ∈ ℕ 0 → N ∈ ℝ
10 nn0ge0 ⊢ N ∈ ℕ 0 → 0 ≤ N
11 9 10 absidd ⊢ N ∈ ℕ 0 → N = N
12 11 ad2antlr ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ M = N → N = N
13 7 8 12 3eqtrd ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ M = N → M = N
14 1 13 sylan2 ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ M ∥ N ∧ N ∥ M → M = N