Metamath Proof Explorer

Theorem fzuntgd

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

Ref Expression
Hypotheses fzuntgd.k ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
fzuntgd.l ⊢ ( 𝜑 → 𝐿 ∈ ℤ )
fzuntgd.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
fzuntgd.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
fzuntgd.km ⊢ ( 𝜑 → 𝐾 ≤ 𝑀 )
fzuntgd.ml ⊢ ( 𝜑 → 𝑀 ≤ ( 𝐿 + 1 ) )
fzuntgd.ln ⊢ ( 𝜑 → 𝐿 ≤ 𝑁 )
Assertion fzuntgd ( 𝜑 → ( ( 𝐾 ... 𝐿 ) ∪ ( 𝑀 ... 𝑁 ) ) = ( 𝐾 ... 𝑁 ) )

Proof

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