fzunt

Description: Union of two adjacent finite sets of sequential integers that share a common endpoint. (Suggested by NM, 21-Jul-2005.) (Contributed by RP, 14-Dec-2024)

		Ref	Expression
	Assertion	fzunt	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \leq M \land M \leq N)) \to (K \dots M) \cup (M \dots N) = (K \dots N)$

Proof

Step	Hyp	Ref	Expression
1		zre	$⊢ K \in ℤ \to K \in ℝ$
2		zre	$⊢ M \in ℤ \to M \in ℝ$
3		zre	$⊢ N \in ℤ \to N \in ℝ$
4		zre	$⊢ j \in ℤ \to j \in ℝ$
5		simprl	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land (j \in ℝ \land j \leq M)) \to j \in ℝ$
6		simpl2	$⊢ ((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \to M \in ℝ$
7	6	adantr	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land (j \in ℝ \land j \leq M)) \to M \in ℝ$
8		simpll3	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land (j \in ℝ \land j \leq M)) \to N \in ℝ$
9		simprr	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land (j \in ℝ \land j \leq M)) \to j \leq M$
10		simprr	$⊢ ((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \to M \leq N$
11	10	adantr	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land (j \in ℝ \land j \leq M)) \to M \leq N$
12	5 7 8 9 11	letrd	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land (j \in ℝ \land j \leq M)) \to j \leq N$
13	12	expr	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land j \in ℝ) \to (j \leq M \to j \leq N)$
14	13	anim2d	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land j \in ℝ) \to ((K \leq j \land j \leq M) \to (K \leq j \land j \leq N))$
15		simpll1	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land (j \in ℝ \land M \leq j)) \to K \in ℝ$
16	6	adantr	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land (j \in ℝ \land M \leq j)) \to M \in ℝ$
17		simprl	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land (j \in ℝ \land M \leq j)) \to j \in ℝ$
18		simprl	$⊢ ((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \to K \leq M$
19	18	adantr	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land (j \in ℝ \land M \leq j)) \to K \leq M$
20		simprr	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land (j \in ℝ \land M \leq j)) \to M \leq j$
21	15 16 17 19 20	letrd	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land (j \in ℝ \land M \leq j)) \to K \leq j$
22	21	expr	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land j \in ℝ) \to (M \leq j \to K \leq j)$
23	22	anim1d	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land j \in ℝ) \to ((M \leq j \land j \leq N) \to (K \leq j \land j \leq N))$
24	14 23	jaod	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land j \in ℝ) \to (((K \leq j \land j \leq M) \lor (M \leq j \land j \leq N)) \to (K \leq j \land j \leq N))$
25		orc	$⊢ K \leq j \to (K \leq j \lor M \leq j)$
26		orc	$⊢ K \leq j \to (K \leq j \lor j \leq N)$
27	25 26	jca	$⊢ K \leq j \to ((K \leq j \lor M \leq j) \land (K \leq j \lor j \leq N))$
28	27	ad2antrl	$⊢ ((((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land j \in ℝ) \land (K \leq j \land j \leq N)) \to ((K \leq j \lor M \leq j) \land (K \leq j \lor j \leq N))$
29		letric	$⊢ (j \in ℝ \land M \in ℝ) \to (j \leq M \lor M \leq j)$
30	29	ancoms	$⊢ (M \in ℝ \land j \in ℝ) \to (j \leq M \lor M \leq j)$
31	6 30	sylan	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land j \in ℝ) \to (j \leq M \lor M \leq j)$
32	31	adantr	$⊢ ((((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land j \in ℝ) \land (K \leq j \land j \leq N)) \to (j \leq M \lor M \leq j)$
33		simprr	$⊢ ((((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land j \in ℝ) \land (K \leq j \land j \leq N)) \to j \leq N$
34	33	olcd	$⊢ ((((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land j \in ℝ) \land (K \leq j \land j \leq N)) \to (j \leq M \lor j \leq N)$
35	32 34	jca	$⊢ ((((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land j \in ℝ) \land (K \leq j \land j \leq N)) \to ((j \leq M \lor M \leq j) \land (j \leq M \lor j \leq N))$
36		orddi	$⊢ ((K \leq j \land j \leq M) \lor (M \leq j \land j \leq N)) \leftrightarrow (((K \leq j \lor M \leq j) \land (K \leq j \lor j \leq N)) \land ((j \leq M \lor M \leq j) \land (j \leq M \lor j \leq N)))$
37	28 35 36	sylanbrc	$⊢ ((((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land j \in ℝ) \land (K \leq j \land j \leq N)) \to ((K \leq j \land j \leq M) \lor (M \leq j \land j \leq N))$
38	37	ex	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land j \in ℝ) \to ((K \leq j \land j \leq N) \to ((K \leq j \land j \leq M) \lor (M \leq j \land j \leq N)))$
39	24 38	impbid	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land j \in ℝ) \to (((K \leq j \land j \leq M) \lor (M \leq j \land j \leq N)) \leftrightarrow (K \leq j \land j \leq N))$
40	4 39	sylan2	$⊢ (((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \land j \in ℤ) \to (((K \leq j \land j \leq M) \lor (M \leq j \land j \leq N)) \leftrightarrow (K \leq j \land j \leq N))$
41	40	pm5.32da	$⊢ ((K \in ℝ \land M \in ℝ \land N \in ℝ) \land (K \leq M \land M \leq N)) \to ((j \in ℤ \land ((K \leq j \land j \leq M) \lor (M \leq j \land j \leq N))) \leftrightarrow (j \in ℤ \land (K \leq j \land j \leq N)))$
42	1 2 3 41	syl3anl	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \leq M \land M \leq N)) \to ((j \in ℤ \land ((K \leq j \land j \leq M) \lor (M \leq j \land j \leq N))) \leftrightarrow (j \in ℤ \land (K \leq j \land j \leq N)))$
43		simp1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \in ℤ$
44		simp2	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M \in ℤ$
45		elfz1	$⊢ (K \in ℤ \land M \in ℤ) \to (j \in (K \dots M) \leftrightarrow (j \in ℤ \land K \leq j \land j \leq M))$
46	43 44 45	syl2anc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (j \in (K \dots M) \leftrightarrow (j \in ℤ \land K \leq j \land j \leq M))$
47		3anass	$⊢ (j \in ℤ \land K \leq j \land j \leq M) \leftrightarrow (j \in ℤ \land (K \leq j \land j \leq M))$
48	46 47	bitrdi	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (j \in (K \dots M) \leftrightarrow (j \in ℤ \land (K \leq j \land j \leq M)))$
49		simp3	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to N \in ℤ$
50		elfz1	$⊢ (M \in ℤ \land N \in ℤ) \to (j \in (M \dots N) \leftrightarrow (j \in ℤ \land M \leq j \land j \leq N))$
51	44 49 50	syl2anc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (j \in (M \dots N) \leftrightarrow (j \in ℤ \land M \leq j \land j \leq N))$
52		3anass	$⊢ (j \in ℤ \land M \leq j \land j \leq N) \leftrightarrow (j \in ℤ \land (M \leq j \land j \leq N))$
53	51 52	bitrdi	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (j \in (M \dots N) \leftrightarrow (j \in ℤ \land (M \leq j \land j \leq N)))$
54	48 53	orbi12d	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((j \in (K \dots M) \lor j \in (M \dots N)) \leftrightarrow ((j \in ℤ \land (K \leq j \land j \leq M)) \lor (j \in ℤ \land (M \leq j \land j \leq N))))$
55		elun	$⊢ j \in ((K \dots M) \cup (M \dots N)) \leftrightarrow (j \in (K \dots M) \lor j \in (M \dots N))$
56		andi	$⊢ (j \in ℤ \land ((K \leq j \land j \leq M) \lor (M \leq j \land j \leq N))) \leftrightarrow ((j \in ℤ \land (K \leq j \land j \leq M)) \lor (j \in ℤ \land (M \leq j \land j \leq N)))$
57	54 55 56	3bitr4g	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (j \in ((K \dots M) \cup (M \dots N)) \leftrightarrow (j \in ℤ \land ((K \leq j \land j \leq M) \lor (M \leq j \land j \leq N))))$
58	57	adantr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \leq M \land M \leq N)) \to (j \in ((K \dots M) \cup (M \dots N)) \leftrightarrow (j \in ℤ \land ((K \leq j \land j \leq M) \lor (M \leq j \land j \leq N))))$
59		elfz1	$⊢ (K \in ℤ \land N \in ℤ) \to (j \in (K \dots N) \leftrightarrow (j \in ℤ \land K \leq j \land j \leq N))$
60	43 49 59	syl2anc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (j \in (K \dots N) \leftrightarrow (j \in ℤ \land K \leq j \land j \leq N))$
61		3anass	$⊢ (j \in ℤ \land K \leq j \land j \leq N) \leftrightarrow (j \in ℤ \land (K \leq j \land j \leq N))$
62	60 61	bitrdi	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (j \in (K \dots N) \leftrightarrow (j \in ℤ \land (K \leq j \land j \leq N)))$
63	62	adantr	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \leq M \land M \leq N)) \to (j \in (K \dots N) \leftrightarrow (j \in ℤ \land (K \leq j \land j \leq N)))$
64	42 58 63	3bitr4d	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \leq M \land M \leq N)) \to (j \in ((K \dots M) \cup (M \dots N)) \leftrightarrow j \in (K \dots N))$
65	64	eqrdv	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (K \leq M \land M \leq N)) \to (K \dots M) \cup (M \dots N) = (K \dots N)$

Metamath Proof Explorer

Theorem fzunt

Proof