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 ) )