Metamath Proof Explorer

Theorem fzpr

Description: A finite interval of integers with two elements. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion fzpr ⊢ M ∈ ℤ → M … M + 1 = M M + 1

Proof

Step Hyp Ref Expression
1 uzid ⊢ M ∈ ℤ → M ∈ ℤ ≥ M
2 elfzp1 ⊢ M ∈ ℤ ≥ M → m ∈ M … M + 1 ↔ m ∈ M … M ∨ m = M + 1
3 1 2 syl ⊢ M ∈ ℤ → m ∈ M … M + 1 ↔ m ∈ M … M ∨ m = M + 1
4 fzsn ⊢ M ∈ ℤ → M … M = M
5 4 eleq2d ⊢ M ∈ ℤ → m ∈ M … M ↔ m ∈ M
6 velsn ⊢ m ∈ M ↔ m = M
7 5 6 bitrdi ⊢ M ∈ ℤ → m ∈ M … M ↔ m = M
8 7 orbi1d ⊢ M ∈ ℤ → m ∈ M … M ∨ m = M + 1 ↔ m = M ∨ m = M + 1
9 3 8 bitrd ⊢ M ∈ ℤ → m ∈ M … M + 1 ↔ m = M ∨ m = M + 1
10 vex ⊢ m ∈ V
11 10 elpr ⊢ m ∈ M M + 1 ↔ m = M ∨ m = M + 1
12 9 11 bitr4di ⊢ M ∈ ℤ → m ∈ M … M + 1 ↔ m ∈ M M + 1
13 12 eqrdv ⊢ M ∈ ℤ → M … M + 1 = M M + 1