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