This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ ) )