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 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
fzunt1d.l ⊢ ( 𝜑 → 𝐿 ∈ ℤ )
fzunt1d.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
fzunt1d.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
fzunt1d.km ⊢ ( 𝜑 → 𝐾 ≤ 𝑀 )
fzunt1d.ml ⊢ ( 𝜑 → 𝑀 ≤ 𝐿 )
fzunt1d.ln ⊢ ( 𝜑 → 𝐿 ≤ 𝑁 )
Assertion fzunt1d ( 𝜑 → ( ( 𝐾 ... 𝐿 ) ∪ ( 𝑀 ... 𝑁 ) ) = ( 𝐾 ... 𝑁 ) )

Proof

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