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