Theorem elfz0add

Description: An element of a finite set of sequential nonnegative integers is an element of an extended finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 28-Mar-2018) (Proof shortened by OpenAI, 25-Mar-2020)

	Ref	Expression
Assertion	elfz0add	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(N\in \left(0\dots A\right)\to N\in \left(0\dots A+B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0z	$$⊢A\in {\mathbb{N}}_0\to A\in \mathbb{Z}$$
2		uzid	$$⊢A\in \mathbb{Z}\to A\in {\mathbb{Z}}_{\ge A}$$
3	1 2	syl	$$⊢A\in {\mathbb{N}}_0\to A\in {\mathbb{Z}}_{\ge A}$$
4		uzaddcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge A}\wedge B\in {\mathbb{N}}_0\right)\to A+B\in {\mathbb{Z}}_{\ge A}$$
5	3 4	sylan	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to A+B\in {\mathbb{Z}}_{\ge A}$$
6		fzss2	$$⊢A+B\in {\mathbb{Z}}_{\ge A}\to \left(0\dots A\right)\subseteq \left(0\dots A+B\right)$$
7	5 6	syl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(0\dots A\right)\subseteq \left(0\dots A+B\right)$$
8	7	sseld	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(N\in \left(0\dots A\right)\to N\in \left(0\dots A+B\right)\right)$$