Metamath Proof Explorer

Theorem fzsuc2

Description: Join a successor to the end of a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Mar-2014)

Ref Expression
Assertion fzsuc2 ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M − 1 → M … N + 1 = M … N ∪ N + 1

Proof

Step Hyp Ref Expression
1 uzp1 ⊢ N ∈ ℤ ≥ M − 1 → N = M − 1 ∨ N ∈ ℤ ≥ M - 1 + 1
2 zcn ⊢ M ∈ ℤ → M ∈ ℂ
3 ax-1cn ⊢ 1 ∈ ℂ
4 npcan ⊢ M ∈ ℂ ∧ 1 ∈ ℂ → M - 1 + 1 = M
5 2 3 4 sylancl ⊢ M ∈ ℤ → M - 1 + 1 = M
6 5 oveq2d ⊢ M ∈ ℤ → M … M - 1 + 1 = M … M
7 uncom ⊢ ∅ ∪ M = M ∪ ∅
8 un0 ⊢ M ∪ ∅ = M
9 7 8 eqtri ⊢ ∅ ∪ M = M
10 zre ⊢ M ∈ ℤ → M ∈ ℝ
11 10 ltm1d ⊢ M ∈ ℤ → M − 1 < M
12 peano2zm ⊢ M ∈ ℤ → M − 1 ∈ ℤ
13 fzn ⊢ M ∈ ℤ ∧ M − 1 ∈ ℤ → M − 1 < M ↔ M … M − 1 = ∅
14 12 13 mpdan ⊢ M ∈ ℤ → M − 1 < M ↔ M … M − 1 = ∅
15 11 14 mpbid ⊢ M ∈ ℤ → M … M − 1 = ∅
16 5 sneqd ⊢ M ∈ ℤ → M - 1 + 1 = M
17 15 16 uneq12d ⊢ M ∈ ℤ → M … M − 1 ∪ M - 1 + 1 = ∅ ∪ M
18 fzsn ⊢ M ∈ ℤ → M … M = M
19 9 17 18 3eqtr4a ⊢ M ∈ ℤ → M … M − 1 ∪ M - 1 + 1 = M … M
20 6 19 eqtr4d ⊢ M ∈ ℤ → M … M - 1 + 1 = M … M − 1 ∪ M - 1 + 1
21 oveq1 ⊢ N = M − 1 → N + 1 = M - 1 + 1
22 21 oveq2d ⊢ N = M − 1 → M … N + 1 = M … M - 1 + 1
23 oveq2 ⊢ N = M − 1 → M … N = M … M − 1
24 21 sneqd ⊢ N = M − 1 → N + 1 = M - 1 + 1
25 23 24 uneq12d ⊢ N = M − 1 → M … N ∪ N + 1 = M … M − 1 ∪ M - 1 + 1
26 22 25 eqeq12d ⊢ N = M − 1 → M … N + 1 = M … N ∪ N + 1 ↔ M … M - 1 + 1 = M … M − 1 ∪ M - 1 + 1
27 20 26 syl5ibrcom ⊢ M ∈ ℤ → N = M − 1 → M … N + 1 = M … N ∪ N + 1
28 27 imp ⊢ M ∈ ℤ ∧ N = M − 1 → M … N + 1 = M … N ∪ N + 1
29 5 fveq2d ⊢ M ∈ ℤ → ℤ ≥ M - 1 + 1 = ℤ ≥ M
30 29 eleq2d ⊢ M ∈ ℤ → N ∈ ℤ ≥ M - 1 + 1 ↔ N ∈ ℤ ≥ M
31 30 biimpa ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M - 1 + 1 → N ∈ ℤ ≥ M
32 fzsuc ⊢ N ∈ ℤ ≥ M → M … N + 1 = M … N ∪ N + 1
33 31 32 syl ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M - 1 + 1 → M … N + 1 = M … N ∪ N + 1
34 28 33 jaodan ⊢ M ∈ ℤ ∧ N = M − 1 ∨ N ∈ ℤ ≥ M - 1 + 1 → M … N + 1 = M … N ∪ N + 1
35 1 34 sylan2 ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M − 1 → M … N + 1 = M … N ∪ N + 1