Metamath Proof Explorer

Theorem fzuntgd

Description: Union of two adjacent or overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024)

Ref Expression
Hypotheses fzuntgd.k ⊢ φ → K ∈ ℤ
fzuntgd.l ⊢ φ → L ∈ ℤ
fzuntgd.m ⊢ φ → M ∈ ℤ
fzuntgd.n ⊢ φ → N ∈ ℤ
fzuntgd.km ⊢ φ → K ≤ M
fzuntgd.ml ⊢ φ → M ≤ L + 1
fzuntgd.ln ⊢ φ → L ≤ N
Assertion fzuntgd ⊢ φ → K … L ∪ M … N = K … N

Proof

Step Hyp Ref Expression
1 fzuntgd.k ⊢ φ → K ∈ ℤ
2 fzuntgd.l ⊢ φ → L ∈ ℤ
3 fzuntgd.m ⊢ φ → M ∈ ℤ
4 fzuntgd.n ⊢ φ → N ∈ ℤ
5 fzuntgd.km ⊢ φ → K ≤ M
6 fzuntgd.ml ⊢ φ → M ≤ L + 1
7 fzuntgd.ln ⊢ φ → L ≤ N
8 zre ⊢ j ∈ ℤ → j ∈ ℝ
9 simplr ⊢ φ ∧ j ∈ ℝ ∧ j ≤ L → j ∈ ℝ
10 2 zred ⊢ φ → L ∈ ℝ
11 10 ad2antrr ⊢ φ ∧ j ∈ ℝ ∧ j ≤ L → L ∈ ℝ
12 4 zred ⊢ φ → N ∈ ℝ
13 12 ad2antrr ⊢ φ ∧ 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 zred ⊢ φ → K ∈ ℝ
20 19 ad2antrr ⊢ φ ∧ j ∈ ℝ ∧ M ≤ j → K ∈ ℝ
21 3 zred ⊢ φ → M ∈ ℝ
22 21 ad2antrr ⊢ φ ∧ 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 8 29 sylan2 ⊢ φ ∧ j ∈ ℤ → K ≤ j ∧ j ≤ L ∨ M ≤ j ∧ j ≤ N → K ≤ j ∧ j ≤ N
31 orc ⊢ K ≤ j → K ≤ j ∨ M ≤ j
32 orc ⊢ K ≤ j → K ≤ j ∨ j ≤ N
33 31 32 jca ⊢ K ≤ j → K ≤ j ∨ M ≤ j ∧ K ≤ j ∨ j ≤ N
34 33 ad2antrl ⊢ φ ∧ j ∈ ℤ ∧ K ≤ j ∧ j ≤ N → K ≤ j ∨ M ≤ j ∧ K ≤ j ∨ j ≤ N
35 animorrl ⊢ φ ∧ j ∈ ℤ ∧ j ≤ L → j ≤ L ∨ M ≤ j
36 21 ad2antrr ⊢ φ ∧ j ∈ ℤ ∧ L + 1 ≤ j → M ∈ ℝ
37 peano2re ⊢ L ∈ ℝ → L + 1 ∈ ℝ
38 10 37 syl ⊢ φ → L + 1 ∈ ℝ
39 38 ad2antrr ⊢ φ ∧ j ∈ ℤ ∧ L + 1 ≤ j → L + 1 ∈ ℝ
40 simplr ⊢ φ ∧ j ∈ ℤ ∧ L + 1 ≤ j → j ∈ ℤ
41 40 zred ⊢ φ ∧ j ∈ ℤ ∧ L + 1 ≤ j → j ∈ ℝ
42 6 ad2antrr ⊢ φ ∧ j ∈ ℤ ∧ L + 1 ≤ j → M ≤ L + 1
43 simpr ⊢ φ ∧ j ∈ ℤ ∧ L + 1 ≤ j → L + 1 ≤ j
44 36 39 41 42 43 letrd ⊢ φ ∧ j ∈ ℤ ∧ L + 1 ≤ j → M ≤ j
45 44 olcd ⊢ φ ∧ j ∈ ℤ ∧ L + 1 ≤ j → j ≤ L ∨ M ≤ j
46 simpr ⊢ φ ∧ j ∈ ℤ → j ∈ ℤ
47 46 zred ⊢ φ ∧ j ∈ ℤ → j ∈ ℝ
48 2 adantr ⊢ φ ∧ j ∈ ℤ → L ∈ ℤ
49 48 zred ⊢ φ ∧ j ∈ ℤ → L ∈ ℝ
50 lelttric ⊢ j ∈ ℝ ∧ L ∈ ℝ → j ≤ L ∨ L < j
51 47 49 50 syl2anc ⊢ φ ∧ j ∈ ℤ → j ≤ L ∨ L < j
52 zltp1le ⊢ L ∈ ℤ ∧ j ∈ ℤ → L < j ↔ L + 1 ≤ j
53 2 52 sylan ⊢ φ ∧ j ∈ ℤ → L < j ↔ L + 1 ≤ j
54 53 orbi2d ⊢ φ ∧ j ∈ ℤ → j ≤ L ∨ L < j ↔ j ≤ L ∨ L + 1 ≤ j
55 51 54 mpbid ⊢ φ ∧ j ∈ ℤ → j ≤ L ∨ L + 1 ≤ j
56 35 45 55 mpjaodan ⊢ φ ∧ j ∈ ℤ → j ≤ L ∨ M ≤ j
57 56 adantr ⊢ φ ∧ j ∈ ℤ ∧ K ≤ j ∧ j ≤ N → j ≤ L ∨ M ≤ j
58 simprr ⊢ φ ∧ j ∈ ℤ ∧ K ≤ j ∧ j ≤ N → j ≤ N
59 58 olcd ⊢ φ ∧ j ∈ ℤ ∧ K ≤ j ∧ j ≤ N → j ≤ L ∨ j ≤ N
60 57 59 jca ⊢ φ ∧ j ∈ ℤ ∧ K ≤ j ∧ j ≤ N → j ≤ L ∨ M ≤ j ∧ j ≤ L ∨ j ≤ N
61 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
62 34 60 61 sylanbrc ⊢ φ ∧ j ∈ ℤ ∧ K ≤ j ∧ j ≤ N → K ≤ j ∧ j ≤ L ∨ M ≤ j ∧ j ≤ N
63 62 ex ⊢ φ ∧ j ∈ ℤ → K ≤ j ∧ j ≤ N → K ≤ j ∧ j ≤ L ∨ M ≤ j ∧ j ≤ N
64 30 63 impbid ⊢ φ ∧ j ∈ ℤ → K ≤ j ∧ j ≤ L ∨ M ≤ j ∧ j ≤ N ↔ K ≤ j ∧ j ≤ N
65 64 pm5.32da ⊢ φ → j ∈ ℤ ∧ K ≤ j ∧ j ≤ L ∨ M ≤ j ∧ j ≤ N ↔ j ∈ ℤ ∧ K ≤ j ∧ j ≤ N
66 elfz1 ⊢ K ∈ ℤ ∧ L ∈ ℤ → j ∈ K … L ↔ j ∈ ℤ ∧ K ≤ j ∧ j ≤ L
67 1 2 66 syl2anc ⊢ φ → j ∈ K … L ↔ j ∈ ℤ ∧ K ≤ j ∧ j ≤ L
68 3anass ⊢ j ∈ ℤ ∧ K ≤ j ∧ j ≤ L ↔ j ∈ ℤ ∧ K ≤ j ∧ j ≤ L
69 67 68 bitrdi ⊢ φ → j ∈ K … L ↔ j ∈ ℤ ∧ K ≤ j ∧ j ≤ L
70 elfz1 ⊢ M ∈ ℤ ∧ N ∈ ℤ → j ∈ M … N ↔ j ∈ ℤ ∧ M ≤ j ∧ j ≤ N
71 3 4 70 syl2anc ⊢ φ → j ∈ M … N ↔ j ∈ ℤ ∧ M ≤ j ∧ j ≤ N
72 3anass ⊢ j ∈ ℤ ∧ M ≤ j ∧ j ≤ N ↔ j ∈ ℤ ∧ M ≤ j ∧ j ≤ N
73 71 72 bitrdi ⊢ φ → j ∈ M … N ↔ j ∈ ℤ ∧ M ≤ j ∧ j ≤ N
74 69 73 orbi12d ⊢ φ → j ∈ K … L ∨ j ∈ M … N ↔ j ∈ ℤ ∧ K ≤ j ∧ j ≤ L ∨ j ∈ ℤ ∧ M ≤ j ∧ j ≤ N
75 elun ⊢ j ∈ K … L ∪ M … N ↔ j ∈ K … L ∨ j ∈ M … N
76 andi ⊢ j ∈ ℤ ∧ K ≤ j ∧ j ≤ L ∨ M ≤ j ∧ j ≤ N ↔ j ∈ ℤ ∧ K ≤ j ∧ j ≤ L ∨ j ∈ ℤ ∧ M ≤ j ∧ j ≤ N
77 74 75 76 3bitr4g ⊢ φ → j ∈ K … L ∪ M … N ↔ j ∈ ℤ ∧ K ≤ j ∧ j ≤ L ∨ M ≤ j ∧ j ≤ N
78 elfz1 ⊢ K ∈ ℤ ∧ N ∈ ℤ → j ∈ K … N ↔ j ∈ ℤ ∧ K ≤ j ∧ j ≤ N
79 1 4 78 syl2anc ⊢ φ → j ∈ K … N ↔ j ∈ ℤ ∧ K ≤ j ∧ j ≤ N
80 3anass ⊢ j ∈ ℤ ∧ K ≤ j ∧ j ≤ N ↔ j ∈ ℤ ∧ K ≤ j ∧ j ≤ N
81 79 80 bitrdi ⊢ φ → j ∈ K … N ↔ j ∈ ℤ ∧ K ≤ j ∧ j ≤ N
82 65 77 81 3bitr4d ⊢ φ → j ∈ K … L ∪ M … N ↔ j ∈ K … N
83 82 eqrdv ⊢ φ → K … L ∪ M … N = K … N