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	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝑁 ∈ ( 0 ... 𝐴 ) → 𝑁 ∈ ( 0 ... ( 𝐴 + 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		nn0z	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℤ )
2		uzid	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ( ℤ≥ ‘ 𝐴 ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ( ℤ≥ ‘ 𝐴 ) )
4		uzaddcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 + 𝐵 ) ∈ ( ℤ≥ ‘ 𝐴 ) )
5	3 4	sylan	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 + 𝐵 ) ∈ ( ℤ≥ ‘ 𝐴 ) )
6		fzss2	⊢ ( ( 𝐴 + 𝐵 ) ∈ ( ℤ≥ ‘ 𝐴 ) → ( 0 ... 𝐴 ) ⊆ ( 0 ... ( 𝐴 + 𝐵 ) ) )
7	5 6	syl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 0 ... 𝐴 ) ⊆ ( 0 ... ( 𝐴 + 𝐵 ) ) )
8	7	sseld	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝑁 ∈ ( 0 ... 𝐴 ) → 𝑁 ∈ ( 0 ... ( 𝐴 + 𝐵 ) ) ) )