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

Metamath Proof Explorer

Theorem nnnn0addcl

Description: A positive integer plus a nonnegative integer is a positive integer. (Contributed by NM, 20-Apr-2005) (Proof shortened by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion nnnn0addcl ⊢ M ∈ ℕ ∧ N ∈ ℕ 0 → M + N ∈ ℕ

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ N ∈ ℕ 0 ↔ N ∈ ℕ ∨ N = 0
2 nnaddcl ⊢ M ∈ ℕ ∧ N ∈ ℕ → M + N ∈ ℕ
3 oveq2 ⊢ N = 0 → M + N = M + 0
4 nncn ⊢ M ∈ ℕ → M ∈ ℂ
5 4 addridd ⊢ M ∈ ℕ → M + 0 = M
6 3 5 sylan9eqr ⊢ M ∈ ℕ ∧ N = 0 → M + N = M
7 simpl ⊢ M ∈ ℕ ∧ N = 0 → M ∈ ℕ
8 6 7 eqeltrd ⊢ M ∈ ℕ ∧ N = 0 → M + N ∈ ℕ
9 2 8 jaodan ⊢ M ∈ ℕ ∧ N ∈ ℕ ∨ N = 0 → M + N ∈ ℕ
10 1 9 sylan2b ⊢ M ∈ ℕ ∧ N ∈ ℕ 0 → M + N ∈ ℕ