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 ) ) = (/)