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

Metamath Proof Explorer

Theorem nnaddm1cl

Description: Closure of addition of positive integers minus one. (Contributed by NM, 6-Aug-2003) (Proof shortened by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion nnaddm1cl ⊢ A ∈ ℕ ∧ B ∈ ℕ → A + B - 1 ∈ ℕ

Proof

Step Hyp Ref Expression
1 nncn ⊢ A ∈ ℕ → A ∈ ℂ
2 nncn ⊢ B ∈ ℕ → B ∈ ℂ
3 ax-1cn ⊢ 1 ∈ ℂ
4 addsub ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ 1 ∈ ℂ → A + B - 1 = A - 1 + B
5 3 4 mp3an3 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B - 1 = A - 1 + B
6 1 2 5 syl2an ⊢ A ∈ ℕ ∧ B ∈ ℕ → A + B - 1 = A - 1 + B
7 nnm1nn0 ⊢ A ∈ ℕ → A − 1 ∈ ℕ 0
8 nn0nnaddcl ⊢ A − 1 ∈ ℕ 0 ∧ B ∈ ℕ → A - 1 + B ∈ ℕ
9 7 8 sylan ⊢ A ∈ ℕ ∧ B ∈ ℕ → A - 1 + B ∈ ℕ
10 6 9 eqeltrd ⊢ A ∈ ℕ ∧ B ∈ ℕ → A + B - 1 ∈ ℕ