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 ∈ ℤ ≥ A → A ..^ B + 1 = A ..^ B ∪ B

Proof

Step Hyp Ref Expression
1 id ⊢ B ∈ ℤ ≥ A → B ∈ ℤ ≥ A
2 eluzelz ⊢ B ∈ ℤ ≥ A → B ∈ ℤ
3 uzid ⊢ B ∈ ℤ → B ∈ ℤ ≥ B
4 peano2uz ⊢ B ∈ ℤ ≥ B → B + 1 ∈ ℤ ≥ B
5 2 3 4 3syl ⊢ B ∈ ℤ ≥ A → B + 1 ∈ ℤ ≥ B
6 elfzuzb ⊢ B ∈ A … B + 1 ↔ B ∈ ℤ ≥ A ∧ B + 1 ∈ ℤ ≥ B
7 1 5 6 sylanbrc ⊢ B ∈ ℤ ≥ A → B ∈ A … B + 1
8 fzosplit ⊢ B ∈ A … B + 1 → A ..^ B + 1 = A ..^ B ∪ B ..^ B + 1
9 7 8 syl ⊢ B ∈ ℤ ≥ A → A ..^ B + 1 = A ..^ B ∪ B ..^ B + 1
10 fzosn ⊢ B ∈ ℤ → B ..^ B + 1 = B
11 2 10 syl ⊢ B ∈ ℤ ≥ A → B ..^ B + 1 = B
12 11 uneq2d ⊢ B ∈ ℤ ≥ A → A ..^ B ∪ B ..^ B + 1 = A ..^ B ∪ B
13 9 12 eqtrd ⊢ B ∈ ℤ ≥ A → A ..^ B + 1 = A ..^ B ∪ B