Metamath Proof Explorer

Theorem fz1n

Description: A 1-based finite set of sequential integers is empty iff it ends at index 0 . (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion fz1n 
|- ( N e. NN0 -> ( ( 1 ... N ) = (/) <-> N = 0 ) )

Proof

Step Hyp Ref Expression
1 1z 
 |-  1 e. ZZ
2 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
3 fzn 
 |-  ( ( 1 e. ZZ /\ N e. ZZ ) -> ( N < 1 <-> ( 1 ... N ) = (/) ) )
4 1 2 3 sylancr 
 |-  ( N e. NN0 -> ( N < 1 <-> ( 1 ... N ) = (/) ) )
5 nn0lt10b 
 |-  ( N e. NN0 -> ( N < 1 <-> N = 0 ) )
6 4 5 bitr3d 
 |-  ( N e. NN0 -> ( ( 1 ... N ) = (/) <-> N = 0 ) )