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 2 6 7 3jca ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℕ 0 → A ∈ ℤ ∧ B + C ∈ ℤ ∧ B ∈ ℤ
9 eluzle ⊢ B ∈ ℤ ≥ A → A ≤ B
10 9 adantr ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℕ 0 → A ≤ B
11 nn0ge0 ⊢ C ∈ ℕ 0 → 0 ≤ C
12 11 adantl ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℕ 0 → 0 ≤ C
13 eluzelre ⊢ B ∈ ℤ ≥ A → B ∈ ℝ
14 nn0re ⊢ C ∈ ℕ 0 → C ∈ ℝ
15 addge01 ⊢ B ∈ ℝ ∧ C ∈ ℝ → 0 ≤ C ↔ B ≤ B + C
16 13 14 15 syl2an ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℕ 0 → 0 ≤ C ↔ B ≤ B + C
17 12 16 mpbid ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℕ 0 → B ≤ B + C
18 10 17 jca ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℕ 0 → A ≤ B ∧ B ≤ B + C
19 elfz2 ⊢ B ∈ A … B + C ↔ A ∈ ℤ ∧ B + C ∈ ℤ ∧ B ∈ ℤ ∧ A ≤ B ∧ B ≤ B + C
20 8 18 19 sylanbrc ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℕ 0 → B ∈ A … B + C
21 fzosplit ⊢ B ∈ A … B + C → A ..^ B + C = A ..^ B ∪ B ..^ B + C
22 20 21 syl ⊢ B ∈ ℤ ≥ A ∧ C ∈ ℕ 0 → A ..^ B + C = A ..^ B ∪ B ..^ B + C