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	⊢ ( 𝐴 ∈ ℕ ↔ 𝐴 ∈ ( 1 ... 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elnnuz	⊢ ( 𝐴 ∈ ℕ ↔ 𝐴 ∈ ( ℤ≥ ‘ 1 ) )
2	1	biimpi	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ( ℤ≥ ‘ 1 ) )
3		nnz	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
4		uzid	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ( ℤ≥ ‘ 𝐴 ) )
5	3 4	syl	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ( ℤ≥ ‘ 𝐴 ) )
6		eluzfz	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝐴 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝐴 ∈ ( 1 ... 𝐴 ) )
7	2 5 6	syl2anc	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ( 1 ... 𝐴 ) )
8		elfznn	⊢ ( 𝐴 ∈ ( 1 ... 𝐴 ) → 𝐴 ∈ ℕ )
9	7 8	impbii	⊢ ( 𝐴 ∈ ℕ ↔ 𝐴 ∈ ( 1 ... 𝐴 ) )