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 bitr4di ( ( ( 𝐾 + 1 ) ∈ ( ℤ𝑀 ) ∧ 𝑁 ∈ ( ℤ𝐾 ) ) → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑥 ∈ ( ( 𝑀 ... 𝐾 ) ∪ ( ( 𝐾 + 1 ) ... 𝑁 ) ) ) )
44 43 eqrdv ( ( ( 𝐾 + 1 ) ∈ ( ℤ𝑀 ) ∧ 𝑁 ∈ ( ℤ𝐾 ) ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... 𝐾 ) ∪ ( ( 𝐾 + 1 ) ... 𝑁 ) ) )