Metamath Proof Explorer


Theorem znnsub

Description: The positive difference of unequal integers is a positive integer. (Generalization of nnsub .) (Contributed by NM, 11-May-2004)

Ref Expression
Assertion znnsub ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ ( 𝑁𝑀 ) ∈ ℕ ) )

Proof

Step Hyp Ref Expression
1 zre ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
2 zre ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
3 posdif ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 < 𝑁 ↔ 0 < ( 𝑁𝑀 ) ) )
4 1 2 3 syl2an ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ 0 < ( 𝑁𝑀 ) ) )
5 zsubcl ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁𝑀 ) ∈ ℤ )
6 5 ancoms ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁𝑀 ) ∈ ℤ )
7 6 biantrurd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 < ( 𝑁𝑀 ) ↔ ( ( 𝑁𝑀 ) ∈ ℤ ∧ 0 < ( 𝑁𝑀 ) ) ) )
8 4 7 bitrd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ ( ( 𝑁𝑀 ) ∈ ℤ ∧ 0 < ( 𝑁𝑀 ) ) ) )
9 elnnz ( ( 𝑁𝑀 ) ∈ ℕ ↔ ( ( 𝑁𝑀 ) ∈ ℤ ∧ 0 < ( 𝑁𝑀 ) ) )
10 8 9 bitr4di ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ ( 𝑁𝑀 ) ∈ ℕ ) )