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