Metamath Proof Explorer

Theorem fzoun

Description: A half-open integer range as union of two half-open integer ranges. (Contributed by AV, 23-Apr-2022)

Ref Expression
Assertion fzoun ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℕ 0 → A ..^ B + C = A ..^ B ∪ B ..^ B + C

Proof

Step Hyp Ref Expression
1 eluzel2 ⊢ B ∈ ℤ ≥ A → A ∈ ℤ
2 1 adantr ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℕ 0 → A ∈ ℤ
3 eluzelz ⊢ B ∈ ℤ ≥ A → B ∈ ℤ
4 nn0z ⊢ C ∈ ℕ 0 → C ∈ ℤ
5 zaddcl ⊢ B ∈ ℤ ∧ C ∈ ℤ → B + C ∈ ℤ
6 3 4 5 syl2an ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℕ 0 → B + C ∈ ℤ
7 3 adantr ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℕ 0 → B ∈ ℤ
8 eluzle ⊢ B ∈ ℤ ≥ A → A ≤ B
9 8 adantr ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℕ 0 → A ≤ B
10 nn0ge0 ⊢ C ∈ ℕ 0 → 0 ≤ C
11 10 adantl ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℕ 0 → 0 ≤ C
12 eluzelre ⊢ B ∈ ℤ ≥ A → B ∈ ℝ
13 nn0re ⊢ C ∈ ℕ 0 → C ∈ ℝ
14 addge01 ⊢ B ∈ ℝ ∧ C ∈ ℝ → 0 ≤ C ↔ B ≤ B + C
15 12 13 14 syl2an ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℕ 0 → 0 ≤ C ↔ B ≤ B + C
16 11 15 mpbid ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℕ 0 → B ≤ B + C
17 2 6 7 9 16 elfzd ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℕ 0 → B ∈ A … B + C
18 fzosplit ⊢ B ∈ A … B + C → A ..^ B + C = A ..^ B ∪ B ..^ B + C
19 17 18 syl ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℕ 0 → A ..^ B + C = A ..^ B ∪ B ..^ B + C