This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fztp

Description: A finite interval of integers with three elements. (Contributed by NM, 13-Sep-2011) (Revised by Mario Carneiro, 7-Mar-2014)

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

Proof

Step Hyp Ref Expression
1 uzid ⊢ M ∈ ℤ → M ∈ ℤ ≥ M
2 peano2uz ⊢ M ∈ ℤ ≥ M → M + 1 ∈ ℤ ≥ M
3 fzsuc ⊢ M + 1 ∈ ℤ ≥ M → M … M + 1 + 1 = M … M + 1 ∪ M + 1 + 1
4 1 2 3 3syl ⊢ M ∈ ℤ → M … M + 1 + 1 = M … M + 1 ∪ M + 1 + 1
5 zcn ⊢ M ∈ ℤ → M ∈ ℂ
6 ax-1cn ⊢ 1 ∈ ℂ
7 addass ⊢ M ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ → M + 1 + 1 = M + 1 + 1
8 6 6 7 mp3an23 ⊢ M ∈ ℂ → M + 1 + 1 = M + 1 + 1
9 5 8 syl ⊢ M ∈ ℤ → M + 1 + 1 = M + 1 + 1
10 df-2 ⊢ 2 = 1 + 1
11 10 oveq2i ⊢ M + 2 = M + 1 + 1
12 9 11 eqtr4di ⊢ M ∈ ℤ → M + 1 + 1 = M + 2
13 12 oveq2d ⊢ M ∈ ℤ → M … M + 1 + 1 = M … M + 2
14 fzpr ⊢ M ∈ ℤ → M … M + 1 = M M + 1
15 12 sneqd ⊢ M ∈ ℤ → M + 1 + 1 = M + 2
16 14 15 uneq12d ⊢ M ∈ ℤ → M … M + 1 ∪ M + 1 + 1 = M M + 1 ∪ M + 2
17 df-tp ⊢ M M + 1 M + 2 = M M + 1 ∪ M + 2
18 16 17 eqtr4di ⊢ M ∈ ℤ → M … M + 1 ∪ M + 1 + 1 = M M + 1 M + 2
19 4 13 18 3eqtr3d ⊢ M ∈ ℤ → M … M + 2 = M M + 1 M + 2