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	$$⊢A\in \mathbb{N}$$
Assertion	jm2.27dlem3	$$⊢A\in \left(1\dots A\right)$$

Proof

Step	Hyp	Ref	Expression
1		jm2.27dlem3.1	$$⊢A\in \mathbb{N}$$
2		elfz1end	$$⊢A\in \mathbb{N}\leftrightarrow A\in \left(1\dots A\right)$$
3	1 2	mpbi	$$⊢A\in \left(1\dots A\right)$$