Description: There are no integers between 1 and 0. (Contributed by Jeff Madsen, 16-Jun-2010) (Proof shortened by Mario Carneiro, 28-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fz10 | ⊢ ( 1 ... 0 ) = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0lt1 | ⊢ 0 < 1 | |
2 | 1z | ⊢ 1 ∈ ℤ | |
3 | 0z | ⊢ 0 ∈ ℤ | |
4 | fzn | ⊢ ( ( 1 ∈ ℤ ∧ 0 ∈ ℤ ) → ( 0 < 1 ↔ ( 1 ... 0 ) = ∅ ) ) | |
5 | 2 3 4 | mp2an | ⊢ ( 0 < 1 ↔ ( 1 ... 0 ) = ∅ ) |
6 | 1 5 | mpbi | ⊢ ( 1 ... 0 ) = ∅ |