This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzsplit3

Description: Split a finite interval of integers into two parts. (Contributed by Thierry Arnoux, 2-May-2017)

Ref Expression
Assertion fzsplit3 ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... ( 𝐾 − 1 ) ) ∪ ( 𝐾 ... 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 elfzelz ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ℤ )
2 1 zred ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ℝ )
3 elfzelz ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ℤ )
4 3 zred ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ℝ )
5 1red ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 1 ∈ ℝ )
6 4 5 resubcld ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 − 1 ) ∈ ℝ )
7 lelttric ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝐾 − 1 ) ∈ ℝ ) → ( 𝑥 ≤ ( 𝐾 − 1 ) ∨ ( 𝐾 − 1 ) < 𝑥 ) )
8 2 6 7 syl2anr ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ≤ ( 𝐾 − 1 ) ∨ ( 𝐾 − 1 ) < 𝑥 ) )
9 elfzuz ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) )
10 1zzd ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 1 ∈ ℤ )
11 3 10 zsubcld ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 − 1 ) ∈ ℤ )
12 elfz5 ⊢ ( ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐾 − 1 ) ∈ ℤ ) → ( 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ↔ 𝑥 ≤ ( 𝐾 − 1 ) ) )
13 9 11 12 syl2anr ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ↔ 𝑥 ≤ ( 𝐾 − 1 ) ) )
14 elfzuz3 ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) )
15 14 adantl ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) )
16 elfzuzb ⊢ ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) ) )
17 16 rbaib ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) → ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) ↔ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) )
18 15 17 syl ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) ↔ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) )
19 eluz ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ↔ 𝐾 ≤ 𝑥 ) )
20 3 1 19 syl2an ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ↔ 𝐾 ≤ 𝑥 ) )
21 zlem1lt ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝐾 ≤ 𝑥 ↔ ( 𝐾 − 1 ) < 𝑥 ) )
22 3 1 21 syl2an ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 ≤ 𝑥 ↔ ( 𝐾 − 1 ) < 𝑥 ) )
23 18 20 22 3bitrd ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) ↔ ( 𝐾 − 1 ) < 𝑥 ) )
24 13 23 orbi12d ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ∨ 𝑥 ∈ ( 𝐾 ... 𝑁 ) ) ↔ ( 𝑥 ≤ ( 𝐾 − 1 ) ∨ ( 𝐾 − 1 ) < 𝑥 ) ) )
25 8 24 mpbird ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ∨ 𝑥 ∈ ( 𝐾 ... 𝑁 ) ) )
26 elfzuz ⊢ ( 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) )
27 26 adantl ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) )
28 elfzuz3 ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
29 28 adantr ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
30 elfzuz3 ⊢ ( 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) → ( 𝐾 − 1 ) ∈ ( ℤ≥ ‘ 𝑥 ) )
31 30 adantl ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( 𝐾 − 1 ) ∈ ( ℤ≥ ‘ 𝑥 ) )
32 peano2uz ⊢ ( ( 𝐾 − 1 ) ∈ ( ℤ≥ ‘ 𝑥 ) → ( ( 𝐾 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑥 ) )
33 31 32 syl ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( ( 𝐾 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑥 ) )
34 4 recnd ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ℂ )
35 5 recnd ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 1 ∈ ℂ )
36 34 35 npcand ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
37 36 eleq1d ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( ( ( 𝐾 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑥 ) ↔ 𝐾 ∈ ( ℤ≥ ‘ 𝑥 ) ) )
38 37 adantr ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( ( ( 𝐾 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑥 ) ↔ 𝐾 ∈ ( ℤ≥ ‘ 𝑥 ) ) )
39 33 38 mpbid ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑥 ) )
40 uztrn ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑥 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) )
41 29 39 40 syl2anc ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) )
42 elfzuzb ⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) ) )
43 27 41 42 sylanbrc ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) )
44 elfzuz ⊢ ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) )
45 elfzuz ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
46 uztrn ⊢ ( ( 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) )
47 44 45 46 syl2anr ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) )
48 elfzuz3 ⊢ ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) )
49 48 adantl ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑥 ) )
50 47 49 42 sylanbrc ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) )
51 43 50 jaodan ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ ( 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ∨ 𝑥 ∈ ( 𝐾 ... 𝑁 ) ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) )
52 25 51 impbida ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ∨ 𝑥 ∈ ( 𝐾 ... 𝑁 ) ) ) )
53 elun ⊢ ( 𝑥 ∈ ( ( 𝑀 ... ( 𝐾 − 1 ) ) ∪ ( 𝐾 ... 𝑁 ) ) ↔ ( 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ∨ 𝑥 ∈ ( 𝐾 ... 𝑁 ) ) )
54 52 53 bitr4di ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑥 ∈ ( ( 𝑀 ... ( 𝐾 − 1 ) ) ∪ ( 𝐾 ... 𝑁 ) ) ) )
55 54 eqrdv ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... ( 𝐾 − 1 ) ) ∪ ( 𝐾 ... 𝑁 ) ) )