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