Metamath Proof Explorer

Theorem fz0n

Description: The sequence ( 0 ... ( N - 1 ) ) is empty iff N is zero. (Contributed by Scott Fenton, 16-May-2014)

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

Proof

Step Hyp Ref Expression
1 0z 
 |-  0 e. ZZ
2 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
3 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
4 2 3 syl 
 |-  ( N e. NN0 -> ( N - 1 ) e. ZZ )
5 fzn 
 |-  ( ( 0 e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( ( N - 1 ) < 0 <-> ( 0 ... ( N - 1 ) ) = (/) ) )
6 1 4 5 sylancr 
 |-  ( N e. NN0 -> ( ( N - 1 ) < 0 <-> ( 0 ... ( N - 1 ) ) = (/) ) )
7 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
8 nnge1 
 |-  ( N e. NN -> 1 <_ N )
9 nnre 
 |-  ( N e. NN -> N e. RR )
10 1re 
 |-  1 e. RR
11 subge0 
 |-  ( ( N e. RR /\ 1 e. RR ) -> ( 0 <_ ( N - 1 ) <-> 1 <_ N ) )
12 0re 
 |-  0 e. RR
13 resubcl 
 |-  ( ( N e. RR /\ 1 e. RR ) -> ( N - 1 ) e. RR )
14 lenlt 
 |-  ( ( 0 e. RR /\ ( N - 1 ) e. RR ) -> ( 0 <_ ( N - 1 ) <-> -. ( N - 1 ) < 0 ) )
15 12 13 14 sylancr 
 |-  ( ( N e. RR /\ 1 e. RR ) -> ( 0 <_ ( N - 1 ) <-> -. ( N - 1 ) < 0 ) )
16 11 15 bitr3d 
 |-  ( ( N e. RR /\ 1 e. RR ) -> ( 1 <_ N <-> -. ( N - 1 ) < 0 ) )
17 9 10 16 sylancl 
 |-  ( N e. NN -> ( 1 <_ N <-> -. ( N - 1 ) < 0 ) )
18 8 17 mpbid 
 |-  ( N e. NN -> -. ( N - 1 ) < 0 )
19 nnne0 
 |-  ( N e. NN -> N =/= 0 )
20 19 neneqd 
 |-  ( N e. NN -> -. N = 0 )
21 18 20 2falsed 
 |-  ( N e. NN -> ( ( N - 1 ) < 0 <-> N = 0 ) )
22 oveq1 
 |-  ( N = 0 -> ( N - 1 ) = ( 0 - 1 ) )
23 df-neg 
 |-  -u 1 = ( 0 - 1 )
24 22 23 eqtr4di 
 |-  ( N = 0 -> ( N - 1 ) = -u 1 )
25 neg1lt0 
 |-  -u 1 < 0
26 24 25 eqbrtrdi 
 |-  ( N = 0 -> ( N - 1 ) < 0 )
27 id 
 |-  ( N = 0 -> N = 0 )
28 26 27 2thd 
 |-  ( N = 0 -> ( ( N - 1 ) < 0 <-> N = 0 ) )
29 21 28 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( ( N - 1 ) < 0 <-> N = 0 ) )
30 7 29 sylbi 
 |-  ( N e. NN0 -> ( ( N - 1 ) < 0 <-> N = 0 ) )
31 6 30 bitr3d 
 |-  ( N e. NN0 -> ( ( 0 ... ( N - 1 ) ) = (/) <-> N = 0 ) )