Metamath Proof Explorer

Theorem risefall0lem

Description: Lemma for risefac0 and fallfac0 . Show a particular set of finite integers is empty. (Contributed by Scott Fenton, 5-Jan-2018)

Ref Expression
Assertion risefall0lem 
|- ( 0 ... ( 0 - 1 ) ) = (/)

Proof

Step Hyp Ref Expression
1 df-neg 
 |-  -u 1 = ( 0 - 1 )
2 1 oveq2i 
 |-  ( 0 ... -u 1 ) = ( 0 ... ( 0 - 1 ) )
3 neg1lt0 
 |-  -u 1 < 0
4 0z 
 |-  0 e. ZZ
5 neg1z 
 |-  -u 1 e. ZZ
6 fzn 
 |-  ( ( 0 e. ZZ /\ -u 1 e. ZZ ) -> ( -u 1 < 0 <-> ( 0 ... -u 1 ) = (/) ) )
7 4 5 6 mp2an 
 |-  ( -u 1 < 0 <-> ( 0 ... -u 1 ) = (/) )
8 3 7 mpbi 
 |-  ( 0 ... -u 1 ) = (/)
9 2 8 eqtr3i 
 |-  ( 0 ... ( 0 - 1 ) ) = (/)