Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
fzuntd.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
fzuntd.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
fzuntd.km ⊢ ( 𝜑 → 𝐾 ≤ 𝑀 )
fzuntd.mn ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
Assertion fzuntd ( 𝜑 → ( ( 𝐾 ... 𝑀 ) ∪ ( 𝑀 ... 𝑁 ) ) = ( 𝐾 ... 𝑁 ) )

Proof

Step Hyp Ref Expression
1 fzuntd.k ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
2 fzuntd.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 fzuntd.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4 fzuntd.km ⊢ ( 𝜑 → 𝐾 ≤ 𝑀 )
5 fzuntd.mn ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
6 simprl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ 𝑗 ≤ 𝑀 ) ) → 𝑗 ∈ ℤ )
7 6 zred ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ 𝑗 ≤ 𝑀 ) ) → 𝑗 ∈ ℝ )
8 2 zred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
9 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ 𝑗 ≤ 𝑀 ) ) → 𝑀 ∈ ℝ )
10 3 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
11 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ 𝑗 ≤ 𝑀 ) ) → 𝑁 ∈ ℝ )
12 simprr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ 𝑗 ≤ 𝑀 ) ) → 𝑗 ≤ 𝑀 )
13 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ 𝑗 ≤ 𝑀 ) ) → 𝑀 ≤ 𝑁 )
14 7 9 11 12 13 letrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ 𝑗 ≤ 𝑀 ) ) → 𝑗 ≤ 𝑁 )
15 14 expr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) → ( 𝑗 ≤ 𝑀 → 𝑗 ≤ 𝑁 ) )
16 15 anim2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) → ( ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀 ) → ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
17 1 zred ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
18 17 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ) ) → 𝐾 ∈ ℝ )
19 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ) ) → 𝑀 ∈ ℝ )
20 simprl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ) ) → 𝑗 ∈ ℤ )
21 20 zred ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ) ) → 𝑗 ∈ ℝ )
22 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ) ) → 𝐾 ≤ 𝑀 )
23 simprr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ) ) → 𝑀 ≤ 𝑗 )
24 18 19 21 22 23 letrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ) ) → 𝐾 ≤ 𝑗 )
25 24 expr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) → ( 𝑀 ≤ 𝑗 → 𝐾 ≤ 𝑗 ) )
26 25 anim1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) → ( ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) → ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
27 16 26 jaod ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) → ( ( ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀 ) ∨ ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) → ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
28 orc ⊢ ( 𝐾 ≤ 𝑗 → ( 𝐾 ≤ 𝑗 ∨ 𝑀 ≤ 𝑗 ) )
29 orc ⊢ ( 𝐾 ≤ 𝑗 → ( 𝐾 ≤ 𝑗 ∨ 𝑗 ≤ 𝑁 ) )
30 28 29 jca ⊢ ( 𝐾 ≤ 𝑗 → ( ( 𝐾 ≤ 𝑗 ∨ 𝑀 ≤ 𝑗 ) ∧ ( 𝐾 ≤ 𝑗 ∨ 𝑗 ≤ 𝑁 ) ) )
31 30 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) → ( ( 𝐾 ≤ 𝑗 ∨ 𝑀 ≤ 𝑗 ) ∧ ( 𝐾 ≤ 𝑗 ∨ 𝑗 ≤ 𝑁 ) ) )
32 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) → 𝑗 ∈ ℤ )
33 32 zred ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) → 𝑗 ∈ ℝ )
34 8 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) → 𝑀 ∈ ℝ )
35 33 34 letrid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) → ( 𝑗 ≤ 𝑀 ∨ 𝑀 ≤ 𝑗 ) )
36 35 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) → ( 𝑗 ≤ 𝑀 ∨ 𝑀 ≤ 𝑗 ) )
37 simprr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) → 𝑗 ≤ 𝑁 )
38 37 olcd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) → ( 𝑗 ≤ 𝑀 ∨ 𝑗 ≤ 𝑁 ) )
39 36 38 jca ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) → ( ( 𝑗 ≤ 𝑀 ∨ 𝑀 ≤ 𝑗 ) ∧ ( 𝑗 ≤ 𝑀 ∨ 𝑗 ≤ 𝑁 ) ) )
40 orddi ⊢ ( ( ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀 ) ∨ ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) ↔ ( ( ( 𝐾 ≤ 𝑗 ∨ 𝑀 ≤ 𝑗 ) ∧ ( 𝐾 ≤ 𝑗 ∨ 𝑗 ≤ 𝑁 ) ) ∧ ( ( 𝑗 ≤ 𝑀 ∨ 𝑀 ≤ 𝑗 ) ∧ ( 𝑗 ≤ 𝑀 ∨ 𝑗 ≤ 𝑁 ) ) ) )
41 31 39 40 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) → ( ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀 ) ∨ ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
42 41 ex ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) → ( ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) → ( ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀 ) ∨ ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) ) )
43 27 42 impbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) → ( ( ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀 ) ∨ ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) ↔ ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
44 43 pm5.32da ⊢ ( 𝜑 → ( ( 𝑗 ∈ ℤ ∧ ( ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀 ) ∨ ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) ) ↔ ( 𝑗 ∈ ℤ ∧ ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) ) )
45 elfz1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑗 ∈ ( 𝐾 ... 𝑀 ) ↔ ( 𝑗 ∈ ℤ ∧ 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀 ) ) )
46 1 2 45 syl2anc ⊢ ( 𝜑 → ( 𝑗 ∈ ( 𝐾 ... 𝑀 ) ↔ ( 𝑗 ∈ ℤ ∧ 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀 ) ) )
47 3anass ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀 ) ↔ ( 𝑗 ∈ ℤ ∧ ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀 ) ) )
48 46 47 bitrdi ⊢ ( 𝜑 → ( 𝑗 ∈ ( 𝐾 ... 𝑀 ) ↔ ( 𝑗 ∈ ℤ ∧ ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀 ) ) ) )
49 elfz1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
50 2 3 49 syl2anc ⊢ ( 𝜑 → ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
51 3anass ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ↔ ( 𝑗 ∈ ℤ ∧ ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
52 50 51 bitrdi ⊢ ( 𝜑 → ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑗 ∈ ℤ ∧ ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) ) )
53 48 52 orbi12d ⊢ ( 𝜑 → ( ( 𝑗 ∈ ( 𝐾 ... 𝑀 ) ∨ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) ↔ ( ( 𝑗 ∈ ℤ ∧ ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀 ) ) ∨ ( 𝑗 ∈ ℤ ∧ ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) ) ) )
54 elun ⊢ ( 𝑗 ∈ ( ( 𝐾 ... 𝑀 ) ∪ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝑗 ∈ ( 𝐾 ... 𝑀 ) ∨ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) )
55 andi ⊢ ( ( 𝑗 ∈ ℤ ∧ ( ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀 ) ∨ ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) ) ↔ ( ( 𝑗 ∈ ℤ ∧ ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀 ) ) ∨ ( 𝑗 ∈ ℤ ∧ ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) ) )
56 53 54 55 3bitr4g ⊢ ( 𝜑 → ( 𝑗 ∈ ( ( 𝐾 ... 𝑀 ) ∪ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝑗 ∈ ℤ ∧ ( ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑀 ) ∨ ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) ) ) )
57 elfz1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑗 ∈ ( 𝐾 ... 𝑁 ) ↔ ( 𝑗 ∈ ℤ ∧ 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
58 1 3 57 syl2anc ⊢ ( 𝜑 → ( 𝑗 ∈ ( 𝐾 ... 𝑁 ) ↔ ( 𝑗 ∈ ℤ ∧ 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
59 3anass ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ↔ ( 𝑗 ∈ ℤ ∧ ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
60 58 59 bitrdi ⊢ ( 𝜑 → ( 𝑗 ∈ ( 𝐾 ... 𝑁 ) ↔ ( 𝑗 ∈ ℤ ∧ ( 𝐾 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) ) )
61 44 56 60 3bitr4d ⊢ ( 𝜑 → ( 𝑗 ∈ ( ( 𝐾 ... 𝑀 ) ∪ ( 𝑀 ... 𝑁 ) ) ↔ 𝑗 ∈ ( 𝐾 ... 𝑁 ) ) )
62 61 eqrdv ⊢ ( 𝜑 → ( ( 𝐾 ... 𝑀 ) ∪ ( 𝑀 ... 𝑁 ) ) = ( 𝐾 ... 𝑁 ) )