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	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (N \in (0 \dots A) \to N \in (0 \dots A + B))$

Proof

Step	Hyp	Ref	Expression
1		nn0z	$⊢ A \in ℕ_{0} \to A \in ℤ$
2		uzid	$⊢ A \in ℤ \to A \in ℤ_{\geq A}$
3	1 2	syl	$⊢ A \in ℕ_{0} \to A \in ℤ_{\geq A}$
4		uzaddcl	$⊢ (A \in ℤ_{\geq A} \land B \in ℕ_{0}) \to A + B \in ℤ_{\geq A}$
5	3 4	sylan	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to A + B \in ℤ_{\geq A}$
6		fzss2	$⊢ A + B \in ℤ_{\geq A} \to (0 \dots A) \subseteq (0 \dots A + B)$
7	5 6	syl	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (0 \dots A) \subseteq (0 \dots A + B)$
8	7	sseld	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (N \in (0 \dots A) \to N \in (0 \dots A + B))$

Metamath Proof Explorer

Theorem elfz0add

Proof