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

Metamath Proof Explorer

Theorem nnsubi

Description: Subtraction of positive integers. (Contributed by NM, 19-Aug-2001)

Ref Expression
Hypotheses nnsub.1 ⊢ A ∈ ℕ
nnsub.2 ⊢ B ∈ ℕ
Assertion nnsubi ⊢ A < B ↔ B − A ∈ ℕ

Proof

Step Hyp Ref Expression
1 nnsub.1 ⊢ A ∈ ℕ
2 nnsub.2 ⊢ B ∈ ℕ
3 nnsub ⊢ A ∈ ℕ ∧ B ∈ ℕ → A < B ↔ B − A ∈ ℕ
4 1 2 3 mp2an ⊢ A < B ↔ B − A ∈ ℕ