Theorem elfz1end

Description: A nonempty finite range of integers contains its end point. (Contributed by Stefan O'Rear, 10-Oct-2014)

	Ref	Expression
Assertion	elfz1end	$$⊢A\in \mathbb{N}\leftrightarrow A\in \left(1\dots A\right)$$

Proof

Step	Hyp	Ref	Expression
1		elnnuz	$$⊢A\in \mathbb{N}\leftrightarrow A\in {\mathbb{Z}}_{\ge 1}$$
2	1	biimpi	$$⊢A\in \mathbb{N}\to A\in {\mathbb{Z}}_{\ge 1}$$
3		nnz	$$⊢A\in \mathbb{N}\to A\in \mathbb{Z}$$
4		uzid	$$⊢A\in \mathbb{Z}\to A\in {\mathbb{Z}}_{\ge A}$$
5	3 4	syl	$$⊢A\in \mathbb{N}\to A\in {\mathbb{Z}}_{\ge A}$$
6		eluzfz	$$⊢\left(A\in {\mathbb{Z}}_{\ge 1}\wedge A\in {\mathbb{Z}}_{\ge A}\right)\to A\in \left(1\dots A\right)$$
7	2 5 6	syl2anc	$$⊢A\in \mathbb{N}\to A\in \left(1\dots A\right)$$
8		elfznn	$$⊢A\in \left(1\dots A\right)\to A\in \mathbb{N}$$
9	7 8	impbii	$$⊢A\in \mathbb{N}\leftrightarrow A\in \left(1\dots A\right)$$