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 ) → ( 𝐴 ..^ ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 ..^ 𝐵 ) ∪ ( 𝐵 ..^ ( 𝐵 + 𝐶 ) ) ) )