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	$⊢ N \in ℤ_{\geq M} \to ℤ_{\geq M} = (M \dots N - 1) \cup ℤ_{\geq N}$

Proof

Step	Hyp	Ref	Expression
1		eluzelre	$⊢ N \in ℤ_{\geq M} \to N \in ℝ$
2		eluzelre	$⊢ k \in ℤ_{\geq M} \to k \in ℝ$
3		lelttric	$⊢ (N \in ℝ \land k \in ℝ) \to (N \leq k \lor k < N)$
4	1 2 3	syl2an	$⊢ (N \in ℤ_{\geq M} \land k \in ℤ_{\geq M}) \to (N \leq k \lor k < N)$
5		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
6		eluzelz	$⊢ k \in ℤ_{\geq M} \to k \in ℤ$
7		eluz	$⊢ (N \in ℤ \land k \in ℤ) \to (k \in ℤ_{\geq N} \leftrightarrow N \leq k)$
8	5 6 7	syl2an	$⊢ (N \in ℤ_{\geq M} \land k \in ℤ_{\geq M}) \to (k \in ℤ_{\geq N} \leftrightarrow N \leq k)$
9		eluzle	$⊢ k \in ℤ_{\geq M} \to M \leq k$
10	6 9	jca	$⊢ k \in ℤ_{\geq M} \to (k \in ℤ \land M \leq k)$
11	10	adantl	$⊢ (N \in ℤ_{\geq M} \land k \in ℤ_{\geq M}) \to (k \in ℤ \land M \leq k)$
12		eluzel2	$⊢ k \in ℤ_{\geq M} \to M \in ℤ$
13		elfzm11	$⊢ (M \in ℤ \land N \in ℤ) \to (k \in (M \dots N - 1) \leftrightarrow (k \in ℤ \land M \leq k \land k < N))$
14		df-3an	$⊢ (k \in ℤ \land M \leq k \land k < N) \leftrightarrow ((k \in ℤ \land M \leq k) \land k < N)$
15	13 14	bitrdi	$⊢ (M \in ℤ \land N \in ℤ) \to (k \in (M \dots N - 1) \leftrightarrow ((k \in ℤ \land M \leq k) \land k < N))$
16	12 5 15	syl2anr	$⊢ (N \in ℤ_{\geq M} \land k \in ℤ_{\geq M}) \to (k \in (M \dots N - 1) \leftrightarrow ((k \in ℤ \land M \leq k) \land k < N))$
17	11 16	mpbirand	$⊢ (N \in ℤ_{\geq M} \land k \in ℤ_{\geq M}) \to (k \in (M \dots N - 1) \leftrightarrow k < N)$
18	8 17	orbi12d	$⊢ (N \in ℤ_{\geq M} \land k \in ℤ_{\geq M}) \to ((k \in ℤ_{\geq N} \lor k \in (M \dots N - 1)) \leftrightarrow (N \leq k \lor k < N))$
19	4 18	mpbird	$⊢ (N \in ℤ_{\geq M} \land k \in ℤ_{\geq M}) \to (k \in ℤ_{\geq N} \lor k \in (M \dots N - 1))$
20	19	orcomd	$⊢ (N \in ℤ_{\geq M} \land k \in ℤ_{\geq M}) \to (k \in (M \dots N - 1) \lor k \in ℤ_{\geq N})$
21	20	ex	$⊢ N \in ℤ_{\geq M} \to (k \in ℤ_{\geq M} \to (k \in (M \dots N - 1) \lor k \in ℤ_{\geq N}))$
22		elfzuz	$⊢ k \in (M \dots N - 1) \to k \in ℤ_{\geq M}$
23	22	a1i	$⊢ N \in ℤ_{\geq M} \to (k \in (M \dots N - 1) \to k \in ℤ_{\geq M})$
24		uztrn	$⊢ (k \in ℤ_{\geq N} \land N \in ℤ_{\geq M}) \to k \in ℤ_{\geq M}$
25	24	expcom	$⊢ N \in ℤ_{\geq M} \to (k \in ℤ_{\geq N} \to k \in ℤ_{\geq M})$
26	23 25	jaod	$⊢ N \in ℤ_{\geq M} \to ((k \in (M \dots N - 1) \lor k \in ℤ_{\geq N}) \to k \in ℤ_{\geq M})$
27	21 26	impbid	$⊢ N \in ℤ_{\geq M} \to (k \in ℤ_{\geq M} \leftrightarrow (k \in (M \dots N - 1) \lor k \in ℤ_{\geq N}))$
28		elun	$⊢ k \in ((M \dots N - 1) \cup ℤ_{\geq N}) \leftrightarrow (k \in (M \dots N - 1) \lor k \in ℤ_{\geq N})$
29	27 28	bitr4di	$⊢ N \in ℤ_{\geq M} \to (k \in ℤ_{\geq M} \leftrightarrow k \in ((M \dots N - 1) \cup ℤ_{\geq N}))$
30	29	eqrdv	$⊢ N \in ℤ_{\geq M} \to ℤ_{\geq M} = (M \dots N - 1) \cup ℤ_{\geq N}$

Metamath Proof Explorer

Theorem uzsplit

Proof