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