fzuntd

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

	Ref	Expression
Hypotheses	fzuntd.k	$⊢ φ \to K \in ℤ$
	fzuntd.m	$⊢ φ \to M \in ℤ$
	fzuntd.n	$⊢ φ \to N \in ℤ$
	fzuntd.km	$⊢ φ \to K \leq M$
	fzuntd.mn	$⊢ φ \to M \leq N$
Assertion	fzuntd	$⊢ φ \to (K \dots M) \cup (M \dots N) = (K \dots N)$

Proof

Step	Hyp	Ref	Expression
1		fzuntd.k	$⊢ φ \to K \in ℤ$
2		fzuntd.m	$⊢ φ \to M \in ℤ$
3		fzuntd.n	$⊢ φ \to N \in ℤ$
4		fzuntd.km	$⊢ φ \to K \leq M$
5		fzuntd.mn	$⊢ φ \to M \leq N$
6		simprl	$⊢ (φ \land (j \in ℤ \land j \leq M)) \to j \in ℤ$
7	6	zred	$⊢ (φ \land (j \in ℤ \land j \leq M)) \to j \in ℝ$
8	2	zred	$⊢ φ \to M \in ℝ$
9	8	adantr	$⊢ (φ \land (j \in ℤ \land j \leq M)) \to M \in ℝ$
10	3	zred	$⊢ φ \to N \in ℝ$
11	10	adantr	$⊢ (φ \land (j \in ℤ \land j \leq M)) \to N \in ℝ$
12		simprr	$⊢ (φ \land (j \in ℤ \land j \leq M)) \to j \leq M$
13	5	adantr	$⊢ (φ \land (j \in ℤ \land j \leq M)) \to M \leq N$
14	7 9 11 12 13	letrd	$⊢ (φ \land (j \in ℤ \land j \leq M)) \to j \leq N$
15	14	expr	$⊢ (φ \land j \in ℤ) \to (j \leq M \to j \leq N)$
16	15	anim2d	$⊢ (φ \land j \in ℤ) \to ((K \leq j \land j \leq M) \to (K \leq j \land j \leq N))$
17	1	zred	$⊢ φ \to K \in ℝ$
18	17	adantr	$⊢ (φ \land (j \in ℤ \land M \leq j)) \to K \in ℝ$
19	8	adantr	$⊢ (φ \land (j \in ℤ \land M \leq j)) \to M \in ℝ$
20		simprl	$⊢ (φ \land (j \in ℤ \land M \leq j)) \to j \in ℤ$
21	20	zred	$⊢ (φ \land (j \in ℤ \land M \leq j)) \to j \in ℝ$
22	4	adantr	$⊢ (φ \land (j \in ℤ \land M \leq j)) \to K \leq M$
23		simprr	$⊢ (φ \land (j \in ℤ \land M \leq j)) \to M \leq j$
24	18 19 21 22 23	letrd	$⊢ (φ \land (j \in ℤ \land M \leq j)) \to K \leq j$
25	24	expr	$⊢ (φ \land j \in ℤ) \to (M \leq j \to K \leq j)$
26	25	anim1d	$⊢ (φ \land j \in ℤ) \to ((M \leq j \land j \leq N) \to (K \leq j \land j \leq N))$
27	16 26	jaod	$⊢ (φ \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))$
28		orc	$⊢ K \leq j \to (K \leq j \lor M \leq j)$
29		orc	$⊢ K \leq j \to (K \leq j \lor j \leq N)$
30	28 29	jca	$⊢ K \leq j \to ((K \leq j \lor M \leq j) \land (K \leq j \lor j \leq N))$
31	30	ad2antrl	$⊢ ((φ \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))$
32		simpr	$⊢ (φ \land j \in ℤ) \to j \in ℤ$
33	32	zred	$⊢ (φ \land j \in ℤ) \to j \in ℝ$
34	8	adantr	$⊢ (φ \land j \in ℤ) \to M \in ℝ$
35	33 34	letrid	$⊢ (φ \land j \in ℤ) \to (j \leq M \lor M \leq j)$
36	35	adantr	$⊢ ((φ \land j \in ℤ) \land (K \leq j \land j \leq N)) \to (j \leq M \lor M \leq j)$
37		simprr	$⊢ ((φ \land j \in ℤ) \land (K \leq j \land j \leq N)) \to j \leq N$
38	37	olcd	$⊢ ((φ \land j \in ℤ) \land (K \leq j \land j \leq N)) \to (j \leq M \lor j \leq N)$
39	36 38	jca	$⊢ ((φ \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))$
40		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)))$
41	31 39 40	sylanbrc	$⊢ ((φ \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))$
42	41	ex	$⊢ (φ \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)))$
43	27 42	impbid	$⊢ (φ \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))$
44	43	pm5.32da	$⊢ φ \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)))$
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	1 2 45	syl2anc	$⊢ φ \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	$⊢ φ \to (j \in (K \dots M) \leftrightarrow (j \in ℤ \land (K \leq j \land j \leq M)))$
49		elfz1	$⊢ (M \in ℤ \land N \in ℤ) \to (j \in (M \dots N) \leftrightarrow (j \in ℤ \land M \leq j \land j \leq N))$
50	2 3 49	syl2anc	$⊢ φ \to (j \in (M \dots N) \leftrightarrow (j \in ℤ \land M \leq j \land j \leq N))$
51		3anass	$⊢ (j \in ℤ \land M \leq j \land j \leq N) \leftrightarrow (j \in ℤ \land (M \leq j \land j \leq N))$
52	50 51	bitrdi	$⊢ φ \to (j \in (M \dots N) \leftrightarrow (j \in ℤ \land (M \leq j \land j \leq N)))$
53	48 52	orbi12d	$⊢ φ \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))))$
54		elun	$⊢ j \in ((K \dots M) \cup (M \dots N)) \leftrightarrow (j \in (K \dots M) \lor j \in (M \dots N))$
55		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)))$
56	53 54 55	3bitr4g	$⊢ φ \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))))$
57		elfz1	$⊢ (K \in ℤ \land N \in ℤ) \to (j \in (K \dots N) \leftrightarrow (j \in ℤ \land K \leq j \land j \leq N))$
58	1 3 57	syl2anc	$⊢ φ \to (j \in (K \dots N) \leftrightarrow (j \in ℤ \land K \leq j \land j \leq N))$
59		3anass	$⊢ (j \in ℤ \land K \leq j \land j \leq N) \leftrightarrow (j \in ℤ \land (K \leq j \land j \leq N))$
60	58 59	bitrdi	$⊢ φ \to (j \in (K \dots N) \leftrightarrow (j \in ℤ \land (K \leq j \land j \leq N)))$
61	44 56 60	3bitr4d	$⊢ φ \to (j \in ((K \dots M) \cup (M \dots N)) \leftrightarrow j \in (K \dots N))$
62	61	eqrdv	$⊢ φ \to (K \dots M) \cup (M \dots N) = (K \dots N)$

Metamath Proof Explorer

Theorem fzuntd

Proof