Metamath Proof Explorer

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 e. NN
Assertion jm2.27dlem3 
|- A e. ( 1 ... A )

Proof

Step Hyp Ref Expression
1 jm2.27dlem3.1 
 |-  A e. NN
2 elfz1end 
 |-  ( A e. NN <-> A e. ( 1 ... A ) )
3 1 2 mpbi 
 |-  A e. ( 1 ... A )