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∪BB+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 ⊢BB+1=B∪B+1
18 17 eqcomi ⊢B∪B+1=BB+1
19 18 a1i ⊢B∈ℤ≥A→B∪B+1=BB+1
20 19 uneq2d ⊢B∈ℤ≥A→A..^B∪B∪B+1=A..^B∪BB+1
21 14 16 20 3eqtrd ⊢B∈ℤ≥A→A..^B+1∪B+1=A..^B∪BB+1
22 9 12 21 3eqtrd ⊢B∈ℤ≥A→A..^B+2=A..^B∪BB+1