Metamath Proof Explorer

Theorem fzo0end

Description: The endpoint of a zero-based half-open range. (Contributed by Stefan O'Rear, 27-Aug-2015) (Revised by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion fzo0end 
|- ( B e. NN -> ( B - 1 ) e. ( 0 ..^ B ) )

Proof

Step Hyp Ref Expression
1 lbfzo0 
 |-  ( 0 e. ( 0 ..^ B ) <-> B e. NN )
2 fzoend 
 |-  ( 0 e. ( 0 ..^ B ) -> ( B - 1 ) e. ( 0 ..^ B ) )
3 1 2 sylbir 
 |-  ( B e. NN -> ( B - 1 ) e. ( 0 ..^ B ) )