Theorem uzsplit

Description: Express an upper integer set as the disjoint (see uzdisj ) union of the first N values and the rest. (Contributed by Mario Carneiro, 24-Apr-2014)

	Ref	Expression
Assertion	uzsplit	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑀 ) = ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ ( ℤ≥ ‘ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eluzelre	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℝ )
2		eluzelre	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℝ )
3		lelttric	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑁 ≤ 𝑘 ∨ 𝑘 < 𝑁 ) )
4	1 2 3	syl2an	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑁 ≤ 𝑘 ∨ 𝑘 < 𝑁 ) )
5		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
6		eluzelz	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℤ )
7		eluz	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ 𝑁 ≤ 𝑘 ) )
8	5 6 7	syl2an	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ 𝑁 ≤ 𝑘 ) )
9		eluzle	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑘 )
10	6 9	jca	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) )
11	10	adantl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) )
12		eluzel2	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
13		elfzm11	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ↔ ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < 𝑁 ) ) )
14		df-3an	⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < 𝑁 ) ↔ ( ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑘 < 𝑁 ) )
15	13 14	syl6bb	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ↔ ( ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑘 < 𝑁 ) ) )
16	12 5 15	syl2anr	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ↔ ( ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑘 < 𝑁 ) ) )
17	11 16	mpbirand	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ↔ 𝑘 < 𝑁 ) )
18	8 17	orbi12d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ∨ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) ↔ ( 𝑁 ≤ 𝑘 ∨ 𝑘 < 𝑁 ) ) )
19	4 18	mpbird	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ∨ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) )
20	19	orcomd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) )
21	20	ex	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) )
22		elfzuz	⊢ ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
23	22	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
24		uztrn	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
25	24	expcom	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
26	23 25	jaod	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
27	21 26	impbid	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) )
28		elun	⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ ( ℤ≥ ‘ 𝑁 ) ) ↔ ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) )
29	27 28	syl6bbr	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑘 ∈ ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ ( ℤ≥ ‘ 𝑁 ) ) ) )
30	29	eqrdv	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑀 ) = ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ ( ℤ≥ ‘ 𝑁 ) ) )