Metamath Proof Explorer

Theorem fzunt

Description: Union of two adjacent finite sets of sequential integers that share a common endpoint. (Suggested by NM, 21-Jul-2005.) (Contributed by RP, 14-Dec-2024)

Ref Expression
Assertion fzunt ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁 ) ) → ( ( 𝐾 ... 𝑀 ) ∪ ( 𝑀 ... 𝑁 ) ) = ( 𝐾 ... 𝑁 ) )

Proof

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