Metamath Proof Explorer

Theorem fzosplitpr

Description: Extending a half-open integer range by an unordered pair at the end. (Contributed by Alexander van der Vekens, 22-Sep-2018)

Ref Expression
Assertion fzosplitpr ⊢ B ∈ ℤ ≥ A → A ..^ B + 2 = A ..^ B ∪ B B + 1

Proof

Step Hyp Ref Expression
1 df-2 ⊢ 2 = 1 + 1
2 1 a1i ⊢ B ∈ ℤ ≥ A → 2 = 1 + 1
3 2 oveq2d ⊢ B ∈ ℤ ≥ A → B + 2 = B + 1 + 1
4 eluzelcn ⊢ B ∈ ℤ ≥ A → B ∈ ℂ
5 1cnd ⊢ B ∈ ℤ ≥ A → 1 ∈ ℂ
6 add32r ⊢ B ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ → B + 1 + 1 = B + 1 + 1
7 4 5 5 6 syl3anc ⊢ B ∈ ℤ ≥ A → B + 1 + 1 = B + 1 + 1
8 3 7 eqtrd ⊢ B ∈ ℤ ≥ A → B + 2 = B + 1 + 1
9 8 oveq2d ⊢ B ∈ ℤ ≥ A → A ..^ B + 2 = A ..^ B + 1 + 1
10 peano2uz ⊢ B ∈ ℤ ≥ A → B + 1 ∈ ℤ ≥ A
11 fzosplitsn ⊢ B + 1 ∈ ℤ ≥ A → A ..^ B + 1 + 1 = A ..^ B + 1 ∪ B + 1
12 10 11 syl ⊢ B ∈ ℤ ≥ A → A ..^ B + 1 + 1 = A ..^ B + 1 ∪ B + 1
13 fzosplitsn ⊢ B ∈ ℤ ≥ A → A ..^ B + 1 = A ..^ B ∪ B
14 13 uneq1d ⊢ B ∈ ℤ ≥ A → A ..^ B + 1 ∪ B + 1 = A ..^ B ∪ B ∪ B + 1
15 unass ⊢ A ..^ B ∪ B ∪ B + 1 = A ..^ B ∪ B ∪ B + 1
16 15 a1i ⊢ B ∈ ℤ ≥ A → A ..^ B ∪ B ∪ B + 1 = A ..^ B ∪ B ∪ B + 1
17 df-pr ⊢ B B + 1 = B ∪ B + 1
18 17 eqcomi ⊢ B ∪ B + 1 = B B + 1
19 18 a1i ⊢ B ∈ ℤ ≥ A → B ∪ B + 1 = B B + 1
20 19 uneq2d ⊢ B ∈ ℤ ≥ A → A ..^ B ∪ B ∪ B + 1 = A ..^ B ∪ B B + 1
21 14 16 20 3eqtrd ⊢ B ∈ ℤ ≥ A → A ..^ B + 1 ∪ B + 1 = A ..^ B ∪ B B + 1
22 9 12 21 3eqtrd ⊢ B ∈ ℤ ≥ A → A ..^ B + 2 = A ..^ B ∪ B B + 1