Metamath Proof Explorer

Theorem fzosplitsnm1

Description: Removing a singleton from a half-open integer range at the end. (Contributed by Alexander van der Vekens, 23-Mar-2018)

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

Proof

Step Hyp Ref Expression
1 eluzelz ⊢ B ∈ ℤ ≥ A + 1 → B ∈ ℤ
2 1 zcnd ⊢ B ∈ ℤ ≥ A + 1 → B ∈ ℂ
3 2 adantl ⊢ A ∈ ℤ ∧ B ∈ ℤ ≥ A + 1 → B ∈ ℂ
4 ax-1cn ⊢ 1 ∈ ℂ
5 npcan ⊢ B ∈ ℂ ∧ 1 ∈ ℂ → B - 1 + 1 = B
6 5 eqcomd ⊢ B ∈ ℂ ∧ 1 ∈ ℂ → B = B - 1 + 1
7 3 4 6 sylancl ⊢ A ∈ ℤ ∧ B ∈ ℤ ≥ A + 1 → B = B - 1 + 1
8 7 oveq2d ⊢ A ∈ ℤ ∧ B ∈ ℤ ≥ A + 1 → A ..^ B = A ..^ B - 1 + 1
9 eluzp1m1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ≥ A + 1 → B − 1 ∈ ℤ ≥ A
10 1 adantl ⊢ A ∈ ℤ ∧ B ∈ ℤ ≥ A + 1 → B ∈ ℤ
11 peano2zm ⊢ B ∈ ℤ → B − 1 ∈ ℤ
12 uzid ⊢ B − 1 ∈ ℤ → B − 1 ∈ ℤ ≥ B − 1
13 peano2uz ⊢ B − 1 ∈ ℤ ≥ B − 1 → B - 1 + 1 ∈ ℤ ≥ B − 1
14 10 11 12 13 4syl ⊢ A ∈ ℤ ∧ B ∈ ℤ ≥ A + 1 → B - 1 + 1 ∈ ℤ ≥ B − 1
15 elfzuzb ⊢ B − 1 ∈ A … B - 1 + 1 ↔ B − 1 ∈ ℤ ≥ A ∧ B - 1 + 1 ∈ ℤ ≥ B − 1
16 9 14 15 sylanbrc ⊢ A ∈ ℤ ∧ B ∈ ℤ ≥ A + 1 → B − 1 ∈ A … B - 1 + 1
17 fzosplit ⊢ B − 1 ∈ A … B - 1 + 1 → A ..^ B - 1 + 1 = A ..^ B − 1 ∪ B − 1 ..^ B - 1 + 1
18 16 17 syl ⊢ A ∈ ℤ ∧ B ∈ ℤ ≥ A + 1 → A ..^ B - 1 + 1 = A ..^ B − 1 ∪ B − 1 ..^ B - 1 + 1
19 1 11 syl ⊢ B ∈ ℤ ≥ A + 1 → B − 1 ∈ ℤ
20 19 adantl ⊢ A ∈ ℤ ∧ B ∈ ℤ ≥ A + 1 → B − 1 ∈ ℤ
21 fzosn ⊢ B − 1 ∈ ℤ → B − 1 ..^ B - 1 + 1 = B − 1
22 20 21 syl ⊢ A ∈ ℤ ∧ B ∈ ℤ ≥ A + 1 → B − 1 ..^ B - 1 + 1 = B − 1
23 22 uneq2d ⊢ A ∈ ℤ ∧ B ∈ ℤ ≥ A + 1 → A ..^ B − 1 ∪ B − 1 ..^ B - 1 + 1 = A ..^ B − 1 ∪ B − 1
24 8 18 23 3eqtrd ⊢ A ∈ ℤ ∧ B ∈ ℤ ≥ A + 1 → A ..^ B = A ..^ B − 1 ∪ B − 1