This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐶 ∈ ℕ0 ) → ( 𝐴 ..^ ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 ..^ 𝐵 ) ∪ ( 𝐵 ..^ ( 𝐵 + 𝐶 ) ) ) )

Proof

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