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	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to A+B-1\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		nncn	$$⊢A\in \mathbb{N}\to A\in ℂ$$
2		nncn	$$⊢B\in \mathbb{N}\to B\in ℂ$$
3		ax-1cn	$$⊢1\in ℂ$$
4		addsub	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge 1\in ℂ\right)\to A+B-1=A-1+B$$
5	3 4	mp3an3	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+B-1=A-1+B$$
6	1 2 5	syl2an	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to A+B-1=A-1+B$$
7		nnm1nn0	$$⊢A\in \mathbb{N}\to A-1\in {\mathbb{N}}_0$$
8		nn0nnaddcl	$$⊢\left(A-1\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to A-1+B\in \mathbb{N}$$
9	7 8	sylan	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to A-1+B\in \mathbb{N}$$
10	6 9	eqeltrd	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to A+B-1\in \mathbb{N}$$