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	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑀 ∥ 𝑁 ∧ 𝑁 ∥ 𝑀 ) ) → 𝑀 = 𝑁 )

Proof

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