Theorem fzsplit

Description: Split a finite interval of integers into two parts. (Contributed by Jeff Madsen, 17-Jun-2010) (Revised by Mario Carneiro, 13-Apr-2016)

	Ref	Expression
Assertion	fzsplit	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... 𝐾 ) ∪ ( ( 𝐾 + 1 ) ... 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfzuz	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
2		peano2uz	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
3	1 2	syl	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
4		elfzuz3	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
5		fzsplit2	⊢ ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... 𝐾 ) ∪ ( ( 𝐾 + 1 ) ... 𝑁 ) ) )
6	3 4 5	syl2anc	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... 𝐾 ) ∪ ( ( 𝐾 + 1 ) ... 𝑁 ) ) )