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 ) ... 𝑁 ) ) ) |
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 ) ... 𝑁 ) ) ) |