Metamath Proof Explorer

Theorem fzunt1d

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

Ref Expression
Hypotheses fzunt1d.k ⊢φ→K∈ℤ
fzunt1d.l ⊢φ→L∈ℤ
fzunt1d.m ⊢φ→M∈ℤ
fzunt1d.n ⊢φ→N∈ℤ
fzunt1d.km ⊢φ→K≤M
fzunt1d.ml ⊢φ→M≤L
fzunt1d.ln ⊢φ→L≤N
Assertion fzunt1d ⊢φ→K…L∪M…N=K…N

Proof

Step Hyp Ref Expression
1 fzunt1d.k ⊢φ→K∈ℤ
2 fzunt1d.l ⊢φ→L∈ℤ
3 fzunt1d.m ⊢φ→M∈ℤ
4 fzunt1d.n ⊢φ→N∈ℤ
5 fzunt1d.km ⊢φ→K≤M
6 fzunt1d.ml ⊢φ→M≤L
7 fzunt1d.ln ⊢φ→L≤N
8 zre ⊢j∈ℤ→j∈ℝ
9 simplr ⊢φ∧j∈ℝ∧j≤L→j∈ℝ
10 2 ad2antrr ⊢φ∧j∈ℝ∧j≤L→L∈ℤ
11 10 zred ⊢φ∧j∈ℝ∧j≤L→L∈ℝ
12 4 ad2antrr ⊢φ∧j∈ℝ∧j≤L→N∈ℤ
13 12 zred ⊢φ∧j∈ℝ∧j≤L→N∈ℝ
14 simpr ⊢φ∧j∈ℝ∧j≤L→j≤L
15 7 ad2antrr ⊢φ∧j∈ℝ∧j≤L→L≤N
16 9 11 13 14 15 letrd ⊢φ∧j∈ℝ∧j≤L→j≤N
17 16 ex ⊢φ∧j∈ℝ→j≤L→j≤N
18 17 anim2d ⊢φ∧j∈ℝ→K≤j∧j≤L→K≤j∧j≤N
19 1 ad2antrr ⊢φ∧j∈ℝ∧M≤j→K∈ℤ
20 19 zred ⊢φ∧j∈ℝ∧M≤j→K∈ℝ
21 3 ad2antrr ⊢φ∧j∈ℝ∧M≤j→M∈ℤ
22 21 zred ⊢φ∧j∈ℝ∧M≤j→M∈ℝ
23 simplr ⊢φ∧j∈ℝ∧M≤j→j∈ℝ
24 5 ad2antrr ⊢φ∧j∈ℝ∧M≤j→K≤M
25 simpr ⊢φ∧j∈ℝ∧M≤j→M≤j
26 20 22 23 24 25 letrd ⊢φ∧j∈ℝ∧M≤j→K≤j
27 26 ex ⊢φ∧j∈ℝ→M≤j→K≤j
28 27 anim1d ⊢φ∧j∈ℝ→M≤j∧j≤N→K≤j∧j≤N
29 18 28 jaod ⊢φ∧j∈ℝ→K≤j∧j≤L∨M≤j∧j≤N→K≤j∧j≤N
30 orc ⊢K≤j→K≤j∨M≤j
31 orc ⊢K≤j→K≤j∨j≤N
32 30 31 jca ⊢K≤j→K≤j∨M≤j∧K≤j∨j≤N
33 32 ad2antrl ⊢φ∧j∈ℝ∧K≤j∧j≤N→K≤j∨M≤j∧K≤j∨j≤N
34 simpr ⊢φ∧j∈ℝ→j∈ℝ
35 2 adantr ⊢φ∧j∈ℝ→L∈ℤ
36 35 zred ⊢φ∧j∈ℝ→L∈ℝ
37 14 orcd ⊢φ∧j∈ℝ∧j≤L→j≤L∨M≤j
38 3 ad2antrr ⊢φ∧j∈ℝ∧L≤j→M∈ℤ
39 38 zred ⊢φ∧j∈ℝ∧L≤j→M∈ℝ
40 2 ad2antrr ⊢φ∧j∈ℝ∧L≤j→L∈ℤ
41 40 zred ⊢φ∧j∈ℝ∧L≤j→L∈ℝ
42 simplr ⊢φ∧j∈ℝ∧L≤j→j∈ℝ
43 6 ad2antrr ⊢φ∧j∈ℝ∧L≤j→M≤L
44 simpr ⊢φ∧j∈ℝ∧L≤j→L≤j
45 39 41 42 43 44 letrd ⊢φ∧j∈ℝ∧L≤j→M≤j
46 45 olcd ⊢φ∧j∈ℝ∧L≤j→j≤L∨M≤j
47 34 36 37 46 lecasei ⊢φ∧j∈ℝ→j≤L∨M≤j
48 47 adantr ⊢φ∧j∈ℝ∧K≤j∧j≤N→j≤L∨M≤j
49 simprr ⊢φ∧j∈ℝ∧K≤j∧j≤N→j≤N
50 49 olcd ⊢φ∧j∈ℝ∧K≤j∧j≤N→j≤L∨j≤N
51 48 50 jca ⊢φ∧j∈ℝ∧K≤j∧j≤N→j≤L∨M≤j∧j≤L∨j≤N
52 orddi ⊢K≤j∧j≤L∨M≤j∧j≤N↔K≤j∨M≤j∧K≤j∨j≤N∧j≤L∨M≤j∧j≤L∨j≤N
53 33 51 52 sylanbrc ⊢φ∧j∈ℝ∧K≤j∧j≤N→K≤j∧j≤L∨M≤j∧j≤N
54 53 ex ⊢φ∧j∈ℝ→K≤j∧j≤N→K≤j∧j≤L∨M≤j∧j≤N
55 29 54 impbid ⊢φ∧j∈ℝ→K≤j∧j≤L∨M≤j∧j≤N↔K≤j∧j≤N
56 8 55 sylan2 ⊢φ∧j∈ℤ→K≤j∧j≤L∨M≤j∧j≤N↔K≤j∧j≤N
57 56 pm5.32da ⊢φ→j∈ℤ∧K≤j∧j≤L∨M≤j∧j≤N↔j∈ℤ∧K≤j∧j≤N
58 elfz1 ⊢K∈ℤ∧L∈ℤ→j∈K…L↔j∈ℤ∧K≤j∧j≤L
59 1 2 58 syl2anc ⊢φ→j∈K…L↔j∈ℤ∧K≤j∧j≤L
60 3anass ⊢j∈ℤ∧K≤j∧j≤L↔j∈ℤ∧K≤j∧j≤L
61 59 60 bitrdi ⊢φ→j∈K…L↔j∈ℤ∧K≤j∧j≤L
62 elfz1 ⊢M∈ℤ∧N∈ℤ→j∈M…N↔j∈ℤ∧M≤j∧j≤N
63 3 4 62 syl2anc ⊢φ→j∈M…N↔j∈ℤ∧M≤j∧j≤N
64 3anass ⊢j∈ℤ∧M≤j∧j≤N↔j∈ℤ∧M≤j∧j≤N
65 63 64 bitrdi ⊢φ→j∈M…N↔j∈ℤ∧M≤j∧j≤N
66 61 65 orbi12d ⊢φ→j∈K…L∨j∈M…N↔j∈ℤ∧K≤j∧j≤L∨j∈ℤ∧M≤j∧j≤N
67 elun ⊢j∈K…L∪M…N↔j∈K…L∨j∈M…N
68 andi ⊢j∈ℤ∧K≤j∧j≤L∨M≤j∧j≤N↔j∈ℤ∧K≤j∧j≤L∨j∈ℤ∧M≤j∧j≤N
69 66 67 68 3bitr4g ⊢φ→j∈K…L∪M…N↔j∈ℤ∧K≤j∧j≤L∨M≤j∧j≤N
70 elfz1 ⊢K∈ℤ∧N∈ℤ→j∈K…N↔j∈ℤ∧K≤j∧j≤N
71 1 4 70 syl2anc ⊢φ→j∈K…N↔j∈ℤ∧K≤j∧j≤N
72 3anass ⊢j∈ℤ∧K≤j∧j≤N↔j∈ℤ∧K≤j∧j≤N
73 71 72 bitrdi ⊢φ→j∈K…N↔j∈ℤ∧K≤j∧j≤N
74 57 69 73 3bitr4d ⊢φ→j∈K…L∪M…N↔j∈K…N
75 74 eqrdv ⊢φ→K…L∪M…N=K…N