Theorem 1elfz0hash

Description: 1 is an element of the finite set of sequential nonnegative integers bounded by the size of a nonempty finite set. (Contributed by AV, 9-May-2020)

	Ref	Expression
Assertion	1elfz0hash	$$⊢\left(A\in \mathrm{Fin}\wedge A\ne \varnothing \right)\to 1\in \left(0\dots \left|A\right|\right)$$

Proof

Step	Hyp	Ref	Expression
1		1nn0	$$⊢1\in {\mathbb{N}}_0$$
2	1	a1i	$$⊢\left(A\in \mathrm{Fin}\wedge A\ne \varnothing \right)\to 1\in {\mathbb{N}}_0$$
3		hashcl	$$⊢A\in \mathrm{Fin}\to \left|A\right|\in {\mathbb{N}}_0$$
4	3	adantr	$$⊢\left(A\in \mathrm{Fin}\wedge A\ne \varnothing \right)\to \left|A\right|\in {\mathbb{N}}_0$$
5		hashge1	$$⊢\left(A\in \mathrm{Fin}\wedge A\ne \varnothing \right)\to 1\le \left|A\right|$$
6		elfz2nn0	$$⊢1\in \left(0\dots \left|A\right|\right)\leftrightarrow \left(1\in {\mathbb{N}}_0\wedge \left|A\right|\in {\mathbb{N}}_0\wedge 1\le \left|A\right|\right)$$
7	2 4 5 6	syl3anbrc	$$⊢\left(A\in \mathrm{Fin}\wedge A\ne \varnothing \right)\to 1\in \left(0\dots \left|A\right|\right)$$