Metamath Proof Explorer

Theorem elfzomin

Description: Membership of an integer in the smallest open range of integers. (Contributed by Alexander van der Vekens, 22-Sep-2018)

Ref Expression
Assertion elfzomin 
|- ( Z e. ZZ -> Z e. ( Z ..^ ( Z + 1 ) ) )

Proof

Step Hyp Ref Expression
1 snidg 
 |-  ( Z e. ZZ -> Z e. { Z } )
2 fzosn 
 |-  ( Z e. ZZ -> ( Z ..^ ( Z + 1 ) ) = { Z } )
3 1 2 eleqtrrd 
 |-  ( Z e. ZZ -> Z e. ( Z ..^ ( Z + 1 ) ) )