Theorem 2elfz3nn0

Description: If there are two elements in a finite set of sequential integers starting at 0, these two elements as well as the upper bound are nonnegative integers. (Contributed by Alexander van der Vekens, 7-Apr-2018)

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

Proof

Step	Hyp	Ref	Expression
1		elfznn0	$$⊢A\in \left(0\dots N\right)\to A\in {\mathbb{N}}_0$$
2		elfz2nn0	$$⊢B\in \left(0\dots N\right)\leftrightarrow \left(B\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\wedge B\le N\right)$$
3		3anass	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\leftrightarrow \left(A\in {\mathbb{N}}_0\wedge \left(B\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\right)$$
4	3	simplbi2com	$$⊢\left(B\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left(A\in {\mathbb{N}}_0\to \left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\right)$$
5	4	3adant3	$$⊢\left(B\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\wedge B\le N\right)\to \left(A\in {\mathbb{N}}_0\to \left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\right)$$
6	2 5	sylbi	$$⊢B\in \left(0\dots N\right)\to \left(A\in {\mathbb{N}}_0\to \left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\right)$$
7	1 6	mpan9	$$⊢\left(A\in \left(0\dots N\right)\wedge B\in \left(0\dots N\right)\right)\to \left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)$$