Theorem uzaddcl

Description: Addition closure law for an upper set of integers. (Contributed by NM, 4-Jun-2006)

	Ref	Expression
Assertion	uzaddcl	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge K\in {\mathbb{N}}_0\right)\to N+K\in {\mathbb{Z}}_{\ge M}$$

Proof

Step	Hyp	Ref	Expression
1		eluzelcn	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in ℂ$$
2		nn0cn	$$⊢k\in {\mathbb{N}}_0\to k\in ℂ$$
3		ax-1cn	$$⊢1\in ℂ$$
4		addass	$$⊢\left(N\in ℂ\wedge k\in ℂ\wedge 1\in ℂ\right)\to N+k+1=N+k+1$$
5	3 4	mp3an3	$$⊢\left(N\in ℂ\wedge k\in ℂ\right)\to N+k+1=N+k+1$$
6	1 2 5	syl2anr	$$⊢\left(k\in {\mathbb{N}}_0\wedge N\in {\mathbb{Z}}_{\ge M}\right)\to N+k+1=N+k+1$$
7	6	adantr	$$⊢\left(\left(k\in {\mathbb{N}}_0\wedge N\in {\mathbb{Z}}_{\ge M}\right)\wedge N+k\in {\mathbb{Z}}_{\ge M}\right)\to N+k+1=N+k+1$$
8		peano2uz	$$⊢N+k\in {\mathbb{Z}}_{\ge M}\to N+k+1\in {\mathbb{Z}}_{\ge M}$$
9	8	adantl	$$⊢\left(\left(k\in {\mathbb{N}}_0\wedge N\in {\mathbb{Z}}_{\ge M}\right)\wedge N+k\in {\mathbb{Z}}_{\ge M}\right)\to N+k+1\in {\mathbb{Z}}_{\ge M}$$
10	7 9	eqeltrrd	$$⊢\left(\left(k\in {\mathbb{N}}_0\wedge N\in {\mathbb{Z}}_{\ge M}\right)\wedge N+k\in {\mathbb{Z}}_{\ge M}\right)\to N+k+1\in {\mathbb{Z}}_{\ge M}$$
11	10	exp31	$$⊢k\in {\mathbb{N}}_0\to \left(N\in {\mathbb{Z}}_{\ge M}\to \left(N+k\in {\mathbb{Z}}_{\ge M}\to N+k+1\in {\mathbb{Z}}_{\ge M}\right)\right)$$
12	11	a2d	$$⊢k\in {\mathbb{N}}_0\to \left(\left(N\in {\mathbb{Z}}_{\ge M}\to N+k\in {\mathbb{Z}}_{\ge M}\right)\to \left(N\in {\mathbb{Z}}_{\ge M}\to N+k+1\in {\mathbb{Z}}_{\ge M}\right)\right)$$
13	1	addid1d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N+0=N$$
14	13	eleq1d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(N+0\in {\mathbb{Z}}_{\ge M}\leftrightarrow N\in {\mathbb{Z}}_{\ge M}\right)$$
15	14	ibir	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N+0\in {\mathbb{Z}}_{\ge M}$$
16		oveq2	$$⊢j=0\to N+j=N+0$$
17	16	eleq1d	$$⊢j=0\to \left(N+j\in {\mathbb{Z}}_{\ge M}\leftrightarrow N+0\in {\mathbb{Z}}_{\ge M}\right)$$
18	17	imbi2d	$$⊢j=0\to \left(\left(N\in {\mathbb{Z}}_{\ge M}\to N+j\in {\mathbb{Z}}_{\ge M}\right)\leftrightarrow \left(N\in {\mathbb{Z}}_{\ge M}\to N+0\in {\mathbb{Z}}_{\ge M}\right)\right)$$
19		oveq2	$$⊢j=k\to N+j=N+k$$
20	19	eleq1d	$$⊢j=k\to \left(N+j\in {\mathbb{Z}}_{\ge M}\leftrightarrow N+k\in {\mathbb{Z}}_{\ge M}\right)$$
21	20	imbi2d	$$⊢j=k\to \left(\left(N\in {\mathbb{Z}}_{\ge M}\to N+j\in {\mathbb{Z}}_{\ge M}\right)\leftrightarrow \left(N\in {\mathbb{Z}}_{\ge M}\to N+k\in {\mathbb{Z}}_{\ge M}\right)\right)$$
22		oveq2	$$⊢j=k+1\to N+j=N+k+1$$
23	22	eleq1d	$$⊢j=k+1\to \left(N+j\in {\mathbb{Z}}_{\ge M}\leftrightarrow N+k+1\in {\mathbb{Z}}_{\ge M}\right)$$
24	23	imbi2d	$$⊢j=k+1\to \left(\left(N\in {\mathbb{Z}}_{\ge M}\to N+j\in {\mathbb{Z}}_{\ge M}\right)\leftrightarrow \left(N\in {\mathbb{Z}}_{\ge M}\to N+k+1\in {\mathbb{Z}}_{\ge M}\right)\right)$$
25		oveq2	$$⊢j=K\to N+j=N+K$$
26	25	eleq1d	$$⊢j=K\to \left(N+j\in {\mathbb{Z}}_{\ge M}\leftrightarrow N+K\in {\mathbb{Z}}_{\ge M}\right)$$
27	26	imbi2d	$$⊢j=K\to \left(\left(N\in {\mathbb{Z}}_{\ge M}\to N+j\in {\mathbb{Z}}_{\ge M}\right)\leftrightarrow \left(N\in {\mathbb{Z}}_{\ge M}\to N+K\in {\mathbb{Z}}_{\ge M}\right)\right)$$
28	12 15 18 21 24 27	nn0indALT	$$⊢K\in {\mathbb{N}}_0\to \left(N\in {\mathbb{Z}}_{\ge M}\to N+K\in {\mathbb{Z}}_{\ge M}\right)$$
29	28	impcom	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge K\in {\mathbb{N}}_0\right)\to N+K\in {\mathbb{Z}}_{\ge M}$$