Metamath Proof Explorer

Theorem fzosplitprm1

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

Ref Expression
Assertion fzosplitprm1 ⊢A∈ℤ∧B∈ℤ∧A<B→A..^B+1=A..^B−1∪B−1B

Proof

Step Hyp Ref Expression
1 simp1 ⊢A∈ℤ∧B∈ℤ∧A<B→A∈ℤ
2 peano2zm ⊢B∈ℤ→B−1∈ℤ
3 2 3ad2ant2 ⊢A∈ℤ∧B∈ℤ∧A<B→B−1∈ℤ
4 zltlem1 ⊢A∈ℤ∧B∈ℤ→A<B↔A≤B−1
5 4 biimp3a ⊢A∈ℤ∧B∈ℤ∧A<B→A≤B−1
6 eluz2 ⊢B−1∈ℤ≥A↔A∈ℤ∧B−1∈ℤ∧A≤B−1
7 1 3 5 6 syl3anbrc ⊢A∈ℤ∧B∈ℤ∧A<B→B−1∈ℤ≥A
8 fzosplitpr ⊢B−1∈ℤ≥A→A..^B-1+2=A..^B−1∪B−1B-1+1
9 7 8 syl ⊢A∈ℤ∧B∈ℤ∧A<B→A..^B-1+2=A..^B−1∪B−1B-1+1
10 zcn ⊢B∈ℤ→B∈ℂ
11 1cnd ⊢B∈ℤ→1∈ℂ
12 2cnd ⊢B∈ℤ→2∈ℂ
13 10 11 12 subadd23d ⊢B∈ℤ→B-1+2=B+2-1
14 2m1e1 ⊢2−1=1
15 14 oveq2i ⊢B+2-1=B+1
16 13 15 eqtr2di ⊢B∈ℤ→B+1=B-1+2
17 16 oveq2d ⊢B∈ℤ→A..^B+1=A..^B-1+2
18 npcan1 ⊢B∈ℂ→B-1+1=B
19 10 18 syl ⊢B∈ℤ→B-1+1=B
20 19 eqcomd ⊢B∈ℤ→B=B-1+1
21 20 preq2d ⊢B∈ℤ→B−1B=B−1B-1+1
22 21 uneq2d ⊢B∈ℤ→A..^B−1∪B−1B=A..^B−1∪B−1B-1+1
23 17 22 eqeq12d ⊢B∈ℤ→A..^B+1=A..^B−1∪B−1B↔A..^B-1+2=A..^B−1∪B−1B-1+1
24 23 3ad2ant2 ⊢A∈ℤ∧B∈ℤ∧A<B→A..^B+1=A..^B−1∪B−1B↔A..^B-1+2=A..^B−1∪B−1B-1+1
25 9 24 mpbird ⊢A∈ℤ∧B∈ℤ∧A<B→A..^B+1=A..^B−1∪B−1B