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 ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... 𝐾 ) ∪ ( ( 𝐾 + 1 ) ... 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 elfzelz ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ℤ )
2 1 zred ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ℝ )
3 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝐾 ∈ ℤ )
4 3 adantl ⊢ ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐾 ∈ ℤ )
5 4 zred ⊢ ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐾 ∈ ℝ )
6 lelttric ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑥 ≤ 𝐾 ∨ 𝐾 < 𝑥 ) )
7 2 5 6 syl2anr ⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ≤ 𝐾 ∨ 𝐾 < 𝑥 ) )
8 elfzuz ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) )
9 elfz5 ⊢ ( ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ℤ ) → ( 𝑥 ∈ ( 𝑀 ... 𝐾 ) ↔ 𝑥 ≤ 𝐾 ) )
10 8 4 9 syl2anr ⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 ... 𝐾 ) ↔ 𝑥 ≤ 𝐾 ) )
11 simpl ⊢ ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
12 eluzelz ⊢ ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 + 1 ) ∈ ℤ )
13 11 12 syl ⊢ ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝐾 + 1 ) ∈ ℤ )
14 eluz ⊢ ( ( ( 𝐾 + 1 ) ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ↔ ( 𝐾 + 1 ) ≤ 𝑥 ) )
15 13 1 14 syl2an ⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ↔ ( 𝐾 + 1 ) ≤ 𝑥 ) )
16 elfzuz3 ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) )
17 16 adantl ⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) )
18 elfzuzb ⊢ ( 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) ) )
19 18 rbaib ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) → ( 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ↔ 𝑥 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) )
20 17 19 syl ⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ↔ 𝑥 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) )
21 zltp1le ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝐾 < 𝑥 ↔ ( 𝐾 + 1 ) ≤ 𝑥 ) )
22 4 1 21 syl2an ⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 < 𝑥 ↔ ( 𝐾 + 1 ) ≤ 𝑥 ) )
23 15 20 22 3bitr4d ⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ↔ 𝐾 < 𝑥 ) )
24 10 23 orbi12d ⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝑀 ... 𝐾 ) ∨ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) ↔ ( 𝑥 ≤ 𝐾 ∨ 𝐾 < 𝑥 ) ) )
25 7 24 mpbird ⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 ... 𝐾 ) ∨ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) )
26 elfzuz ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝐾 ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) )
27 26 adantl ⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝐾 ) ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) )
28 simpr ⊢ ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
29 elfzuz3 ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝐾 ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑥 ) )
30 uztrn ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑥 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) )
31 28 29 30 syl2an ⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝐾 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) )
32 elfzuzb ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) ) )
33 27 31 32 sylanbrc ⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝐾 ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) )
34 elfzuz ⊢ ( 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) → 𝑥 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) )
35 uztrn ⊢ ( ( 𝑥 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ∧ ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) )
36 34 11 35 syl2anr ⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) )
37 elfzuz3 ⊢ ( 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) )
38 37 adantl ⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) )
39 36 38 32 sylanbrc ⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) )
40 33 39 jaodan ⊢ ( ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝑀 ... 𝐾 ) ∨ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) )
41 25 40 impbida ⊢ ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑥 ∈ ( 𝑀 ... 𝐾 ) ∨ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) ) )
42 elun ⊢ ( 𝑥 ∈ ( ( 𝑀 ... 𝐾 ) ∪ ( ( 𝐾 + 1 ) ... 𝑁 ) ) ↔ ( 𝑥 ∈ ( 𝑀 ... 𝐾 ) ∨ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) )
43 41 42 syl6bbr ⊢ ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑥 ∈ ( ( 𝑀 ... 𝐾 ) ∪ ( ( 𝐾 + 1 ) ... 𝑁 ) ) ) )
44 43 eqrdv ⊢ ( ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... 𝐾 ) ∪ ( ( 𝐾 + 1 ) ... 𝑁 ) ) )