# Metamath Proof Explorer

## Theorem fzsplit2

Description: Split a finite interval of integers into two parts. (Contributed by Mario Carneiro, 13-Apr-2016)

Ref Expression
Assertion fzsplit2 ${⊢}\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\to \left({M}\dots {N}\right)=\left({M}\dots {K}\right)\cup \left({K}+1\dots {N}\right)$

### Proof

Step Hyp Ref Expression
1 elfzelz ${⊢}{x}\in \left({M}\dots {N}\right)\to {x}\in ℤ$
2 1 zred ${⊢}{x}\in \left({M}\dots {N}\right)\to {x}\in ℝ$
3 eluzel2 ${⊢}{N}\in {ℤ}_{\ge {K}}\to {K}\in ℤ$
4 3 adantl ${⊢}\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\to {K}\in ℤ$
5 4 zred ${⊢}\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\to {K}\in ℝ$
6 lelttric ${⊢}\left({x}\in ℝ\wedge {K}\in ℝ\right)\to \left({x}\le {K}\vee {K}<{x}\right)$
7 2 5 6 syl2anr ${⊢}\left(\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\wedge {x}\in \left({M}\dots {N}\right)\right)\to \left({x}\le {K}\vee {K}<{x}\right)$
8 elfzuz ${⊢}{x}\in \left({M}\dots {N}\right)\to {x}\in {ℤ}_{\ge {M}}$
9 elfz5 ${⊢}\left({x}\in {ℤ}_{\ge {M}}\wedge {K}\in ℤ\right)\to \left({x}\in \left({M}\dots {K}\right)↔{x}\le {K}\right)$
10 8 4 9 syl2anr ${⊢}\left(\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\wedge {x}\in \left({M}\dots {N}\right)\right)\to \left({x}\in \left({M}\dots {K}\right)↔{x}\le {K}\right)$
11 simpl ${⊢}\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\to {K}+1\in {ℤ}_{\ge {M}}$
12 eluzelz ${⊢}{K}+1\in {ℤ}_{\ge {M}}\to {K}+1\in ℤ$
13 11 12 syl ${⊢}\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\to {K}+1\in ℤ$
14 eluz ${⊢}\left({K}+1\in ℤ\wedge {x}\in ℤ\right)\to \left({x}\in {ℤ}_{\ge \left({K}+1\right)}↔{K}+1\le {x}\right)$
15 13 1 14 syl2an ${⊢}\left(\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\wedge {x}\in \left({M}\dots {N}\right)\right)\to \left({x}\in {ℤ}_{\ge \left({K}+1\right)}↔{K}+1\le {x}\right)$
16 elfzuz3 ${⊢}{x}\in \left({M}\dots {N}\right)\to {N}\in {ℤ}_{\ge {x}}$
17 16 adantl ${⊢}\left(\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\wedge {x}\in \left({M}\dots {N}\right)\right)\to {N}\in {ℤ}_{\ge {x}}$
18 elfzuzb ${⊢}{x}\in \left({K}+1\dots {N}\right)↔\left({x}\in {ℤ}_{\ge \left({K}+1\right)}\wedge {N}\in {ℤ}_{\ge {x}}\right)$
19 18 rbaib ${⊢}{N}\in {ℤ}_{\ge {x}}\to \left({x}\in \left({K}+1\dots {N}\right)↔{x}\in {ℤ}_{\ge \left({K}+1\right)}\right)$
20 17 19 syl ${⊢}\left(\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\wedge {x}\in \left({M}\dots {N}\right)\right)\to \left({x}\in \left({K}+1\dots {N}\right)↔{x}\in {ℤ}_{\ge \left({K}+1\right)}\right)$
21 zltp1le ${⊢}\left({K}\in ℤ\wedge {x}\in ℤ\right)\to \left({K}<{x}↔{K}+1\le {x}\right)$
22 4 1 21 syl2an ${⊢}\left(\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\wedge {x}\in \left({M}\dots {N}\right)\right)\to \left({K}<{x}↔{K}+1\le {x}\right)$
23 15 20 22 3bitr4d ${⊢}\left(\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\wedge {x}\in \left({M}\dots {N}\right)\right)\to \left({x}\in \left({K}+1\dots {N}\right)↔{K}<{x}\right)$
24 10 23 orbi12d ${⊢}\left(\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\wedge {x}\in \left({M}\dots {N}\right)\right)\to \left(\left({x}\in \left({M}\dots {K}\right)\vee {x}\in \left({K}+1\dots {N}\right)\right)↔\left({x}\le {K}\vee {K}<{x}\right)\right)$
25 7 24 mpbird ${⊢}\left(\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\wedge {x}\in \left({M}\dots {N}\right)\right)\to \left({x}\in \left({M}\dots {K}\right)\vee {x}\in \left({K}+1\dots {N}\right)\right)$
26 elfzuz ${⊢}{x}\in \left({M}\dots {K}\right)\to {x}\in {ℤ}_{\ge {M}}$
27 26 adantl ${⊢}\left(\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\wedge {x}\in \left({M}\dots {K}\right)\right)\to {x}\in {ℤ}_{\ge {M}}$
28 simpr ${⊢}\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\to {N}\in {ℤ}_{\ge {K}}$
29 elfzuz3 ${⊢}{x}\in \left({M}\dots {K}\right)\to {K}\in {ℤ}_{\ge {x}}$
30 uztrn ${⊢}\left({N}\in {ℤ}_{\ge {K}}\wedge {K}\in {ℤ}_{\ge {x}}\right)\to {N}\in {ℤ}_{\ge {x}}$
31 28 29 30 syl2an ${⊢}\left(\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\wedge {x}\in \left({M}\dots {K}\right)\right)\to {N}\in {ℤ}_{\ge {x}}$
32 elfzuzb ${⊢}{x}\in \left({M}\dots {N}\right)↔\left({x}\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {x}}\right)$
33 27 31 32 sylanbrc ${⊢}\left(\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\wedge {x}\in \left({M}\dots {K}\right)\right)\to {x}\in \left({M}\dots {N}\right)$
34 elfzuz ${⊢}{x}\in \left({K}+1\dots {N}\right)\to {x}\in {ℤ}_{\ge \left({K}+1\right)}$
35 uztrn ${⊢}\left({x}\in {ℤ}_{\ge \left({K}+1\right)}\wedge {K}+1\in {ℤ}_{\ge {M}}\right)\to {x}\in {ℤ}_{\ge {M}}$
36 34 11 35 syl2anr ${⊢}\left(\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\wedge {x}\in \left({K}+1\dots {N}\right)\right)\to {x}\in {ℤ}_{\ge {M}}$
37 elfzuz3 ${⊢}{x}\in \left({K}+1\dots {N}\right)\to {N}\in {ℤ}_{\ge {x}}$
38 37 adantl ${⊢}\left(\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\wedge {x}\in \left({K}+1\dots {N}\right)\right)\to {N}\in {ℤ}_{\ge {x}}$
39 36 38 32 sylanbrc ${⊢}\left(\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\wedge {x}\in \left({K}+1\dots {N}\right)\right)\to {x}\in \left({M}\dots {N}\right)$
40 33 39 jaodan ${⊢}\left(\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\wedge \left({x}\in \left({M}\dots {K}\right)\vee {x}\in \left({K}+1\dots {N}\right)\right)\right)\to {x}\in \left({M}\dots {N}\right)$
41 25 40 impbida ${⊢}\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\to \left({x}\in \left({M}\dots {N}\right)↔\left({x}\in \left({M}\dots {K}\right)\vee {x}\in \left({K}+1\dots {N}\right)\right)\right)$
42 elun ${⊢}{x}\in \left(\left({M}\dots {K}\right)\cup \left({K}+1\dots {N}\right)\right)↔\left({x}\in \left({M}\dots {K}\right)\vee {x}\in \left({K}+1\dots {N}\right)\right)$
43 41 42 syl6bbr ${⊢}\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\to \left({x}\in \left({M}\dots {N}\right)↔{x}\in \left(\left({M}\dots {K}\right)\cup \left({K}+1\dots {N}\right)\right)\right)$
44 43 eqrdv ${⊢}\left({K}+1\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)\to \left({M}\dots {N}\right)=\left({M}\dots {K}\right)\cup \left({K}+1\dots {N}\right)$