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 ⊢ φ → K ∈ ℤ
fzuntd.m ⊢ φ → M ∈ ℤ
fzuntd.n ⊢ φ → N ∈ ℤ
fzuntd.km ⊢ φ → K ≤ M
fzuntd.mn ⊢ φ → M ≤ N
Assertion fzuntd ⊢ φ → K … M ∪ M … N = K … N

Proof

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