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 - 1 = ( 0 − 1 )
2 1 oveq2i ( 0 ... - 1 ) = ( 0 ... ( 0 − 1 ) )
3 neg1lt0 - 1 < 0
4 0z 0 ∈ ℤ
5 neg1z - 1 ∈ ℤ
6 fzn ( ( 0 ∈ ℤ ∧ - 1 ∈ ℤ ) → ( - 1 < 0 ↔ ( 0 ... - 1 ) = ∅ ) )
7 4 5 6 mp2an ( - 1 < 0 ↔ ( 0 ... - 1 ) = ∅ )
8 3 7 mpbi ( 0 ... - 1 ) = ∅
9 2 8 eqtr3i ( 0 ... ( 0 − 1 ) ) = ∅