fzsplit2

Description: Split a finite interval of integers into two parts. (Contributed by Mario Carneiro, 13-Apr-2016)

		Ref	Expression
	Assertion	fzsplit2	$⊢ (K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \to (M \dots N) = (M \dots K) \cup (K + 1 \dots N)$

Proof

Step	Hyp	Ref	Expression
1		elfzelz	$⊢ x \in (M \dots N) \to x \in ℤ$
2	1	zred	$⊢ x \in (M \dots N) \to x \in ℝ$
3		eluzel2	$⊢ N \in ℤ_{\geq K} \to K \in ℤ$
4	3	adantl	$⊢ (K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \to K \in ℤ$
5	4	zred	$⊢ (K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \to K \in ℝ$
6		lelttric	$⊢ (x \in ℝ \land K \in ℝ) \to (x \leq K \lor K < x)$
7	2 5 6	syl2anr	$⊢ ((K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \land x \in (M \dots N)) \to (x \leq K \lor K < x)$
8		elfzuz	$⊢ x \in (M \dots N) \to x \in ℤ_{\geq M}$
9		elfz5	$⊢ (x \in ℤ_{\geq M} \land K \in ℤ) \to (x \in (M \dots K) \leftrightarrow x \leq K)$
10	8 4 9	syl2anr	$⊢ ((K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \land x \in (M \dots N)) \to (x \in (M \dots K) \leftrightarrow x \leq K)$
11		simpl	$⊢ (K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \to K + 1 \in ℤ_{\geq M}$
12		eluzelz	$⊢ K + 1 \in ℤ_{\geq M} \to K + 1 \in ℤ$
13	11 12	syl	$⊢ (K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \to K + 1 \in ℤ$
14		eluz	$⊢ (K + 1 \in ℤ \land x \in ℤ) \to (x \in ℤ_{\geq (K + 1)} \leftrightarrow K + 1 \leq x)$
15	13 1 14	syl2an	$⊢ ((K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \land x \in (M \dots N)) \to (x \in ℤ_{\geq (K + 1)} \leftrightarrow K + 1 \leq x)$
16		elfzuz3	$⊢ x \in (M \dots N) \to N \in ℤ_{\geq x}$
17	16	adantl	$⊢ ((K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \land x \in (M \dots N)) \to N \in ℤ_{\geq x}$
18		elfzuzb	$⊢ x \in (K + 1 \dots N) \leftrightarrow (x \in ℤ_{\geq (K + 1)} \land N \in ℤ_{\geq x})$
19	18	rbaib	$⊢ N \in ℤ_{\geq x} \to (x \in (K + 1 \dots N) \leftrightarrow x \in ℤ_{\geq (K + 1)})$
20	17 19	syl	$⊢ ((K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \land x \in (M \dots N)) \to (x \in (K + 1 \dots N) \leftrightarrow x \in ℤ_{\geq (K + 1)})$
21		zltp1le	$⊢ (K \in ℤ \land x \in ℤ) \to (K < x \leftrightarrow K + 1 \leq x)$
22	4 1 21	syl2an	$⊢ ((K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \land x \in (M \dots N)) \to (K < x \leftrightarrow K + 1 \leq x)$
23	15 20 22	3bitr4d	$⊢ ((K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \land x \in (M \dots N)) \to (x \in (K + 1 \dots N) \leftrightarrow K < x)$
24	10 23	orbi12d	$⊢ ((K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \land x \in (M \dots N)) \to ((x \in (M \dots K) \lor x \in (K + 1 \dots N)) \leftrightarrow (x \leq K \lor K < x))$
25	7 24	mpbird	$⊢ ((K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \land x \in (M \dots N)) \to (x \in (M \dots K) \lor x \in (K + 1 \dots N))$
26		elfzuz	$⊢ x \in (M \dots K) \to x \in ℤ_{\geq M}$
27	26	adantl	$⊢ ((K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \land x \in (M \dots K)) \to x \in ℤ_{\geq M}$
28		simpr	$⊢ (K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \to N \in ℤ_{\geq K}$
29		elfzuz3	$⊢ x \in (M \dots K) \to K \in ℤ_{\geq x}$
30		uztrn	$⊢ (N \in ℤ_{\geq K} \land K \in ℤ_{\geq x}) \to N \in ℤ_{\geq x}$
31	28 29 30	syl2an	$⊢ ((K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \land x \in (M \dots K)) \to N \in ℤ_{\geq x}$
32		elfzuzb	$⊢ x \in (M \dots N) \leftrightarrow (x \in ℤ_{\geq M} \land N \in ℤ_{\geq x})$
33	27 31 32	sylanbrc	$⊢ ((K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \land x \in (M \dots K)) \to x \in (M \dots N)$
34		elfzuz	$⊢ x \in (K + 1 \dots N) \to x \in ℤ_{\geq (K + 1)}$
35		uztrn	$⊢ (x \in ℤ_{\geq (K + 1)} \land K + 1 \in ℤ_{\geq M}) \to x \in ℤ_{\geq M}$
36	34 11 35	syl2anr	$⊢ ((K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \land x \in (K + 1 \dots N)) \to x \in ℤ_{\geq M}$
37		elfzuz3	$⊢ x \in (K + 1 \dots N) \to N \in ℤ_{\geq x}$
38	37	adantl	$⊢ ((K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \land x \in (K + 1 \dots N)) \to N \in ℤ_{\geq x}$
39	36 38 32	sylanbrc	$⊢ ((K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \land x \in (K + 1 \dots N)) \to x \in (M \dots N)$
40	33 39	jaodan	$⊢ ((K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \land (x \in (M \dots K) \lor x \in (K + 1 \dots N))) \to x \in (M \dots N)$
41	25 40	impbida	$⊢ (K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \to (x \in (M \dots N) \leftrightarrow (x \in (M \dots K) \lor x \in (K + 1 \dots N)))$
42		elun	$⊢ x \in ((M \dots K) \cup (K + 1 \dots N)) \leftrightarrow (x \in (M \dots K) \lor x \in (K + 1 \dots N))$
43	41 42	bitr4di	$⊢ (K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \to (x \in (M \dots N) \leftrightarrow x \in ((M \dots K) \cup (K + 1 \dots N)))$
44	43	eqrdv	$⊢ (K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \to (M \dots N) = (M \dots K) \cup (K + 1 \dots N)$

Metamath Proof Explorer

Theorem fzsplit2

Proof