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 ⊢ φ → K ∈ ℤ
fzunt1d.l ⊢ φ → L ∈ ℤ
fzunt1d.m ⊢ φ → M ∈ ℤ
fzunt1d.n ⊢ φ → N ∈ ℤ
fzunt1d.km ⊢ φ → K ≤ M
fzunt1d.ml ⊢ φ → M ≤ L
fzunt1d.ln ⊢ φ → L ≤ N
Assertion fzunt1d ⊢ φ → K … L ∪ M … N = K … N

Proof

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