Metamath Proof Explorer

Theorem fzosplitsn

Description: Extending a half-open range by a singleton on the end. (Contributed by Stefan O'Rear, 23-Aug-2015)

Ref Expression
Assertion fzosplitsn ${⊢}{B}\in {ℤ}_{\ge {A}}\to \left({A}..^{B}+1\right)=\left({A}..^{B}\right)\cup \left\{{B}\right\}$

Proof

Step Hyp Ref Expression
1 id ${⊢}{B}\in {ℤ}_{\ge {A}}\to {B}\in {ℤ}_{\ge {A}}$
2 eluzelz ${⊢}{B}\in {ℤ}_{\ge {A}}\to {B}\in ℤ$
3 uzid ${⊢}{B}\in ℤ\to {B}\in {ℤ}_{\ge {B}}$
4 peano2uz ${⊢}{B}\in {ℤ}_{\ge {B}}\to {B}+1\in {ℤ}_{\ge {B}}$
5 2 3 4 3syl ${⊢}{B}\in {ℤ}_{\ge {A}}\to {B}+1\in {ℤ}_{\ge {B}}$
6 elfzuzb ${⊢}{B}\in \left({A}\dots {B}+1\right)↔\left({B}\in {ℤ}_{\ge {A}}\wedge {B}+1\in {ℤ}_{\ge {B}}\right)$
7 1 5 6 sylanbrc ${⊢}{B}\in {ℤ}_{\ge {A}}\to {B}\in \left({A}\dots {B}+1\right)$
8 fzosplit ${⊢}{B}\in \left({A}\dots {B}+1\right)\to \left({A}..^{B}+1\right)=\left({A}..^{B}\right)\cup \left({B}..^{B}+1\right)$
9 7 8 syl ${⊢}{B}\in {ℤ}_{\ge {A}}\to \left({A}..^{B}+1\right)=\left({A}..^{B}\right)\cup \left({B}..^{B}+1\right)$
10 fzosn ${⊢}{B}\in ℤ\to \left({B}..^{B}+1\right)=\left\{{B}\right\}$
11 2 10 syl ${⊢}{B}\in {ℤ}_{\ge {A}}\to \left({B}..^{B}+1\right)=\left\{{B}\right\}$
12 11 uneq2d ${⊢}{B}\in {ℤ}_{\ge {A}}\to \left({A}..^{B}\right)\cup \left({B}..^{B}+1\right)=\left({A}..^{B}\right)\cup \left\{{B}\right\}$
13 9 12 eqtrd ${⊢}{B}\in {ℤ}_{\ge {A}}\to \left({A}..^{B}+1\right)=\left({A}..^{B}\right)\cup \left\{{B}\right\}$