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	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → 1 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		1nn0	⊢ 1 ∈ ℕ0
2	1	a1i	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → 1 ∈ ℕ0 )
3		hashcl	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
4	3	adantr	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
5		hashge1	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → 1 ≤ ( ♯ ‘ 𝐴 ) )
6		elfz2nn0	⊢ ( 1 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ↔ ( 1 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ 1 ≤ ( ♯ ‘ 𝐴 ) ) )
7	2 4 5 6	syl3anbrc	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → 1 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )