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 − 1 B

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 − 1 B - 1 + 1
9 7 8 syl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ A < B → A ..^ B - 1 + 2 = A ..^ B − 1 ∪ B − 1 B - 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 − 1 B = B − 1 B - 1 + 1
22 21 uneq2d ⊢ B ∈ ℤ → A ..^ B − 1 ∪ B − 1 B = A ..^ B − 1 ∪ B − 1 B - 1 + 1
23 17 22 eqeq12d ⊢ B ∈ ℤ → A ..^ B + 1 = A ..^ B − 1 ∪ B − 1 B ↔ A ..^ B - 1 + 2 = A ..^ B − 1 ∪ B − 1 B - 1 + 1
24 23 3ad2ant2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ A < B → A ..^ B + 1 = A ..^ B − 1 ∪ B − 1 B ↔ A ..^ B - 1 + 2 = A ..^ B − 1 ∪ B − 1 B - 1 + 1
25 9 24 mpbird ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ A < B → A ..^ B + 1 = A ..^ B − 1 ∪ B − 1 B