fzsplit3

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

		Ref	Expression
	Assertion	fzsplit3	$⊢ K \in (M \dots N) \to (M \dots N) = (M \dots K - 1) \cup (K \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		elfzelz	$⊢ K \in (M \dots N) \to K \in ℤ$
4	3	zred	$⊢ K \in (M \dots N) \to K \in ℝ$
5		1red	$⊢ K \in (M \dots N) \to 1 \in ℝ$
6	4 5	resubcld	$⊢ K \in (M \dots N) \to K - 1 \in ℝ$
7		lelttric	$⊢ (x \in ℝ \land K - 1 \in ℝ) \to (x \leq K - 1 \lor K - 1 < x)$
8	2 6 7	syl2anr	$⊢ (K \in (M \dots N) \land x \in (M \dots N)) \to (x \leq K - 1 \lor K - 1 < x)$
9		elfzuz	$⊢ x \in (M \dots N) \to x \in ℤ_{\geq M}$
10		1zzd	$⊢ K \in (M \dots N) \to 1 \in ℤ$
11	3 10	zsubcld	$⊢ K \in (M \dots N) \to K - 1 \in ℤ$
12		elfz5	$⊢ (x \in ℤ_{\geq M} \land K - 1 \in ℤ) \to (x \in (M \dots K - 1) \leftrightarrow x \leq K - 1)$
13	9 11 12	syl2anr	$⊢ (K \in (M \dots N) \land x \in (M \dots N)) \to (x \in (M \dots K - 1) \leftrightarrow x \leq K - 1)$
14		elfzuz3	$⊢ x \in (M \dots N) \to N \in ℤ_{\geq x}$
15	14	adantl	$⊢ (K \in (M \dots N) \land x \in (M \dots N)) \to N \in ℤ_{\geq x}$
16		elfzuzb	$⊢ x \in (K \dots N) \leftrightarrow (x \in ℤ_{\geq K} \land N \in ℤ_{\geq x})$
17	16	rbaib	$⊢ N \in ℤ_{\geq x} \to (x \in (K \dots N) \leftrightarrow x \in ℤ_{\geq K})$
18	15 17	syl	$⊢ (K \in (M \dots N) \land x \in (M \dots N)) \to (x \in (K \dots N) \leftrightarrow x \in ℤ_{\geq K})$
19		eluz	$⊢ (K \in ℤ \land x \in ℤ) \to (x \in ℤ_{\geq K} \leftrightarrow K \leq x)$
20	3 1 19	syl2an	$⊢ (K \in (M \dots N) \land x \in (M \dots N)) \to (x \in ℤ_{\geq K} \leftrightarrow K \leq x)$
21		zlem1lt	$⊢ (K \in ℤ \land x \in ℤ) \to (K \leq x \leftrightarrow K - 1 < x)$
22	3 1 21	syl2an	$⊢ (K \in (M \dots N) \land x \in (M \dots N)) \to (K \leq x \leftrightarrow K - 1 < x)$
23	18 20 22	3bitrd	$⊢ (K \in (M \dots N) \land x \in (M \dots N)) \to (x \in (K \dots N) \leftrightarrow K - 1 < x)$
24	13 23	orbi12d	$⊢ (K \in (M \dots N) \land x \in (M \dots N)) \to ((x \in (M \dots K - 1) \lor x \in (K \dots N)) \leftrightarrow (x \leq K - 1 \lor K - 1 < x))$
25	8 24	mpbird	$⊢ (K \in (M \dots N) \land x \in (M \dots N)) \to (x \in (M \dots K - 1) \lor x \in (K \dots N))$
26		elfzuz	$⊢ x \in (M \dots K - 1) \to x \in ℤ_{\geq M}$
27	26	adantl	$⊢ (K \in (M \dots N) \land x \in (M \dots K - 1)) \to x \in ℤ_{\geq M}$
28		elfzuz3	$⊢ K \in (M \dots N) \to N \in ℤ_{\geq K}$
29	28	adantr	$⊢ (K \in (M \dots N) \land x \in (M \dots K - 1)) \to N \in ℤ_{\geq K}$
30		elfzuz3	$⊢ x \in (M \dots K - 1) \to K - 1 \in ℤ_{\geq x}$
31	30	adantl	$⊢ (K \in (M \dots N) \land x \in (M \dots K - 1)) \to K - 1 \in ℤ_{\geq x}$
32		peano2uz	$⊢ K - 1 \in ℤ_{\geq x} \to K - 1 + 1 \in ℤ_{\geq x}$
33	31 32	syl	$⊢ (K \in (M \dots N) \land x \in (M \dots K - 1)) \to K - 1 + 1 \in ℤ_{\geq x}$
34	4	recnd	$⊢ K \in (M \dots N) \to K \in ℂ$
35	5	recnd	$⊢ K \in (M \dots N) \to 1 \in ℂ$
36	34 35	npcand	$⊢ K \in (M \dots N) \to K - 1 + 1 = K$
37	36	eleq1d	$⊢ K \in (M \dots N) \to (K - 1 + 1 \in ℤ_{\geq x} \leftrightarrow K \in ℤ_{\geq x})$
38	37	adantr	$⊢ (K \in (M \dots N) \land x \in (M \dots K - 1)) \to (K - 1 + 1 \in ℤ_{\geq x} \leftrightarrow K \in ℤ_{\geq x})$
39	33 38	mpbid	$⊢ (K \in (M \dots N) \land x \in (M \dots K - 1)) \to K \in ℤ_{\geq x}$
40		uztrn	$⊢ (N \in ℤ_{\geq K} \land K \in ℤ_{\geq x}) \to N \in ℤ_{\geq x}$
41	29 39 40	syl2anc	$⊢ (K \in (M \dots N) \land x \in (M \dots K - 1)) \to N \in ℤ_{\geq x}$
42		elfzuzb	$⊢ x \in (M \dots N) \leftrightarrow (x \in ℤ_{\geq M} \land N \in ℤ_{\geq x})$
43	27 41 42	sylanbrc	$⊢ (K \in (M \dots N) \land x \in (M \dots K - 1)) \to x \in (M \dots N)$
44		elfzuz	$⊢ x \in (K \dots N) \to x \in ℤ_{\geq K}$
45		elfzuz	$⊢ K \in (M \dots N) \to K \in ℤ_{\geq M}$
46		uztrn	$⊢ (x \in ℤ_{\geq K} \land K \in ℤ_{\geq M}) \to x \in ℤ_{\geq M}$
47	44 45 46	syl2anr	$⊢ (K \in (M \dots N) \land x \in (K \dots N)) \to x \in ℤ_{\geq M}$
48		elfzuz3	$⊢ x \in (K \dots N) \to N \in ℤ_{\geq x}$
49	48	adantl	$⊢ (K \in (M \dots N) \land x \in (K \dots N)) \to N \in ℤ_{\geq x}$
50	47 49 42	sylanbrc	$⊢ (K \in (M \dots N) \land x \in (K \dots N)) \to x \in (M \dots N)$
51	43 50	jaodan	$⊢ (K \in (M \dots N) \land (x \in (M \dots K - 1) \lor x \in (K \dots N))) \to x \in (M \dots N)$
52	25 51	impbida	$⊢ K \in (M \dots N) \to (x \in (M \dots N) \leftrightarrow (x \in (M \dots K - 1) \lor x \in (K \dots N)))$
53		elun	$⊢ x \in ((M \dots K - 1) \cup (K \dots N)) \leftrightarrow (x \in (M \dots K - 1) \lor x \in (K \dots N))$
54	52 53	bitr4di	$⊢ K \in (M \dots N) \to (x \in (M \dots N) \leftrightarrow x \in ((M \dots K - 1) \cup (K \dots N)))$
55	54	eqrdv	$⊢ K \in (M \dots N) \to (M \dots N) = (M \dots K - 1) \cup (K \dots N)$

Metamath Proof Explorer

Theorem fzsplit3

Proof