Metamath Proof Explorer


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