Theorem jm2.27dlem3

Description: Lemma for rmydioph . Infer membership of the endpoint of a range. (Contributed by Stefan O'Rear, 11-Oct-2014)

	Ref	Expression
Hypothesis	jm2.27dlem3.1	⊢ 𝐴 ∈ ℕ
Assertion	jm2.27dlem3	⊢ 𝐴 ∈ ( 1 ... 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		jm2.27dlem3.1	⊢ 𝐴 ∈ ℕ
2		elfz1end	⊢ ( 𝐴 ∈ ℕ ↔ 𝐴 ∈ ( 1 ... 𝐴 ) )
3	1 2	mpbi	⊢ 𝐴 ∈ ( 1 ... 𝐴 )