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 ⊢ M ∈ ℤ ∧ N ∈ ℤ → M < N ↔ N − M ∈ ℕ

Proof

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