fzuntgd

Description: Union of two adjacent or overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024)

	Ref	Expression
Hypotheses	fzuntgd.k	$⊢ φ \to K \in ℤ$
	fzuntgd.l	$⊢ φ \to L \in ℤ$
	fzuntgd.m	$⊢ φ \to M \in ℤ$
	fzuntgd.n	$⊢ φ \to N \in ℤ$
	fzuntgd.km	$⊢ φ \to K \leq M$
	fzuntgd.ml	$⊢ φ \to M \leq L + 1$
	fzuntgd.ln	$⊢ φ \to L \leq N$
Assertion	fzuntgd	$⊢ φ \to (K \dots L) \cup (M \dots N) = (K \dots N)$

Proof

Step	Hyp	Ref	Expression
1		fzuntgd.k	$⊢ φ \to K \in ℤ$
2		fzuntgd.l	$⊢ φ \to L \in ℤ$
3		fzuntgd.m	$⊢ φ \to M \in ℤ$
4		fzuntgd.n	$⊢ φ \to N \in ℤ$
5		fzuntgd.km	$⊢ φ \to K \leq M$
6		fzuntgd.ml	$⊢ φ \to M \leq L + 1$
7		fzuntgd.ln	$⊢ φ \to L \leq N$
8		zre	$⊢ j \in ℤ \to j \in ℝ$
9		simplr	$⊢ ((φ \land j \in ℝ) \land j \leq L) \to j \in ℝ$
10	2	zred	$⊢ φ \to L \in ℝ$
11	10	ad2antrr	$⊢ ((φ \land j \in ℝ) \land j \leq L) \to L \in ℝ$
12	4	zred	$⊢ φ \to N \in ℝ$
13	12	ad2antrr	$⊢ ((φ \land j \in ℝ) \land j \leq L) \to N \in ℝ$
14		simpr	$⊢ ((φ \land j \in ℝ) \land j \leq L) \to j \leq L$
15	7	ad2antrr	$⊢ ((φ \land j \in ℝ) \land j \leq L) \to L \leq N$
16	9 11 13 14 15	letrd	$⊢ ((φ \land j \in ℝ) \land j \leq L) \to j \leq N$
17	16	ex	$⊢ (φ \land j \in ℝ) \to (j \leq L \to j \leq N)$
18	17	anim2d	$⊢ (φ \land j \in ℝ) \to ((K \leq j \land j \leq L) \to (K \leq j \land j \leq N))$
19	1	zred	$⊢ φ \to K \in ℝ$
20	19	ad2antrr	$⊢ ((φ \land j \in ℝ) \land M \leq j) \to K \in ℝ$
21	3	zred	$⊢ φ \to M \in ℝ$
22	21	ad2antrr	$⊢ ((φ \land j \in ℝ) \land M \leq j) \to M \in ℝ$
23		simplr	$⊢ ((φ \land j \in ℝ) \land M \leq j) \to j \in ℝ$
24	5	ad2antrr	$⊢ ((φ \land j \in ℝ) \land M \leq j) \to K \leq M$
25		simpr	$⊢ ((φ \land j \in ℝ) \land M \leq j) \to M \leq j$
26	20 22 23 24 25	letrd	$⊢ ((φ \land j \in ℝ) \land M \leq j) \to K \leq j$
27	26	ex	$⊢ (φ \land j \in ℝ) \to (M \leq j \to K \leq j)$
28	27	anim1d	$⊢ (φ \land j \in ℝ) \to ((M \leq j \land j \leq N) \to (K \leq j \land j \leq N))$
29	18 28	jaod	$⊢ (φ \land j \in ℝ) \to (((K \leq j \land j \leq L) \lor (M \leq j \land j \leq N)) \to (K \leq j \land j \leq N))$
30	8 29	sylan2	$⊢ (φ \land j \in ℤ) \to (((K \leq j \land j \leq L) \lor (M \leq j \land j \leq N)) \to (K \leq j \land j \leq N))$
31		orc	$⊢ K \leq j \to (K \leq j \lor M \leq j)$
32		orc	$⊢ K \leq j \to (K \leq j \lor j \leq N)$
33	31 32	jca	$⊢ K \leq j \to ((K \leq j \lor M \leq j) \land (K \leq j \lor j \leq N))$
34	33	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))$
35		animorrl	$⊢ ((φ \land j \in ℤ) \land j \leq L) \to (j \leq L \lor M \leq j)$
36	21	ad2antrr	$⊢ ((φ \land j \in ℤ) \land L + 1 \leq j) \to M \in ℝ$
37		peano2re	$⊢ L \in ℝ \to L + 1 \in ℝ$
38	10 37	syl	$⊢ φ \to L + 1 \in ℝ$
39	38	ad2antrr	$⊢ ((φ \land j \in ℤ) \land L + 1 \leq j) \to L + 1 \in ℝ$
40		simplr	$⊢ ((φ \land j \in ℤ) \land L + 1 \leq j) \to j \in ℤ$
41	40	zred	$⊢ ((φ \land j \in ℤ) \land L + 1 \leq j) \to j \in ℝ$
42	6	ad2antrr	$⊢ ((φ \land j \in ℤ) \land L + 1 \leq j) \to M \leq L + 1$
43		simpr	$⊢ ((φ \land j \in ℤ) \land L + 1 \leq j) \to L + 1 \leq j$
44	36 39 41 42 43	letrd	$⊢ ((φ \land j \in ℤ) \land L + 1 \leq j) \to M \leq j$
45	44	olcd	$⊢ ((φ \land j \in ℤ) \land L + 1 \leq j) \to (j \leq L \lor M \leq j)$
46		simpr	$⊢ (φ \land j \in ℤ) \to j \in ℤ$
47	46	zred	$⊢ (φ \land j \in ℤ) \to j \in ℝ$
48	2	adantr	$⊢ (φ \land j \in ℤ) \to L \in ℤ$
49	48	zred	$⊢ (φ \land j \in ℤ) \to L \in ℝ$
50		lelttric	$⊢ (j \in ℝ \land L \in ℝ) \to (j \leq L \lor L < j)$
51	47 49 50	syl2anc	$⊢ (φ \land j \in ℤ) \to (j \leq L \lor L < j)$
52		zltp1le	$⊢ (L \in ℤ \land j \in ℤ) \to (L < j \leftrightarrow L + 1 \leq j)$
53	2 52	sylan	$⊢ (φ \land j \in ℤ) \to (L < j \leftrightarrow L + 1 \leq j)$
54	53	orbi2d	$⊢ (φ \land j \in ℤ) \to ((j \leq L \lor L < j) \leftrightarrow (j \leq L \lor L + 1 \leq j))$
55	51 54	mpbid	$⊢ (φ \land j \in ℤ) \to (j \leq L \lor L + 1 \leq j)$
56	35 45 55	mpjaodan	$⊢ (φ \land j \in ℤ) \to (j \leq L \lor M \leq j)$
57	56	adantr	$⊢ ((φ \land j \in ℤ) \land (K \leq j \land j \leq N)) \to (j \leq L \lor M \leq j)$
58		simprr	$⊢ ((φ \land j \in ℤ) \land (K \leq j \land j \leq N)) \to j \leq N$
59	58	olcd	$⊢ ((φ \land j \in ℤ) \land (K \leq j \land j \leq N)) \to (j \leq L \lor j \leq N)$
60	57 59	jca	$⊢ ((φ \land j \in ℤ) \land (K \leq j \land j \leq N)) \to ((j \leq L \lor M \leq j) \land (j \leq L \lor j \leq N))$
61		orddi	$⊢ ((K \leq j \land j \leq L) \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 L \lor M \leq j) \land (j \leq L \lor j \leq N)))$
62	34 60 61	sylanbrc	$⊢ ((φ \land j \in ℤ) \land (K \leq j \land j \leq N)) \to ((K \leq j \land j \leq L) \lor (M \leq j \land j \leq N))$
63	62	ex	$⊢ (φ \land j \in ℤ) \to ((K \leq j \land j \leq N) \to ((K \leq j \land j \leq L) \lor (M \leq j \land j \leq N)))$
64	30 63	impbid	$⊢ (φ \land j \in ℤ) \to (((K \leq j \land j \leq L) \lor (M \leq j \land j \leq N)) \leftrightarrow (K \leq j \land j \leq N))$
65	64	pm5.32da	$⊢ φ \to ((j \in ℤ \land ((K \leq j \land j \leq L) \lor (M \leq j \land j \leq N))) \leftrightarrow (j \in ℤ \land (K \leq j \land j \leq N)))$
66		elfz1	$⊢ (K \in ℤ \land L \in ℤ) \to (j \in (K \dots L) \leftrightarrow (j \in ℤ \land K \leq j \land j \leq L))$
67	1 2 66	syl2anc	$⊢ φ \to (j \in (K \dots L) \leftrightarrow (j \in ℤ \land K \leq j \land j \leq L))$
68		3anass	$⊢ (j \in ℤ \land K \leq j \land j \leq L) \leftrightarrow (j \in ℤ \land (K \leq j \land j \leq L))$
69	67 68	bitrdi	$⊢ φ \to (j \in (K \dots L) \leftrightarrow (j \in ℤ \land (K \leq j \land j \leq L)))$
70		elfz1	$⊢ (M \in ℤ \land N \in ℤ) \to (j \in (M \dots N) \leftrightarrow (j \in ℤ \land M \leq j \land j \leq N))$
71	3 4 70	syl2anc	$⊢ φ \to (j \in (M \dots N) \leftrightarrow (j \in ℤ \land M \leq j \land j \leq N))$
72		3anass	$⊢ (j \in ℤ \land M \leq j \land j \leq N) \leftrightarrow (j \in ℤ \land (M \leq j \land j \leq N))$
73	71 72	bitrdi	$⊢ φ \to (j \in (M \dots N) \leftrightarrow (j \in ℤ \land (M \leq j \land j \leq N)))$
74	69 73	orbi12d	$⊢ φ \to ((j \in (K \dots L) \lor j \in (M \dots N)) \leftrightarrow ((j \in ℤ \land (K \leq j \land j \leq L)) \lor (j \in ℤ \land (M \leq j \land j \leq N))))$
75		elun	$⊢ j \in ((K \dots L) \cup (M \dots N)) \leftrightarrow (j \in (K \dots L) \lor j \in (M \dots N))$
76		andi	$⊢ (j \in ℤ \land ((K \leq j \land j \leq L) \lor (M \leq j \land j \leq N))) \leftrightarrow ((j \in ℤ \land (K \leq j \land j \leq L)) \lor (j \in ℤ \land (M \leq j \land j \leq N)))$
77	74 75 76	3bitr4g	$⊢ φ \to (j \in ((K \dots L) \cup (M \dots N)) \leftrightarrow (j \in ℤ \land ((K \leq j \land j \leq L) \lor (M \leq j \land j \leq N))))$
78		elfz1	$⊢ (K \in ℤ \land N \in ℤ) \to (j \in (K \dots N) \leftrightarrow (j \in ℤ \land K \leq j \land j \leq N))$
79	1 4 78	syl2anc	$⊢ φ \to (j \in (K \dots N) \leftrightarrow (j \in ℤ \land K \leq j \land j \leq N))$
80		3anass	$⊢ (j \in ℤ \land K \leq j \land j \leq N) \leftrightarrow (j \in ℤ \land (K \leq j \land j \leq N))$
81	79 80	bitrdi	$⊢ φ \to (j \in (K \dots N) \leftrightarrow (j \in ℤ \land (K \leq j \land j \leq N)))$
82	65 77 81	3bitr4d	$⊢ φ \to (j \in ((K \dots L) \cup (M \dots N)) \leftrightarrow j \in (K \dots N))$
83	82	eqrdv	$⊢ φ \to (K \dots L) \cup (M \dots N) = (K \dots N)$

Metamath Proof Explorer

Theorem fzuntgd

Proof