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 
|- ( ph -> K e. ZZ )
fzuntgd.l 
|- ( ph -> L e. ZZ )
fzuntgd.m 
|- ( ph -> M e. ZZ )
fzuntgd.n 
|- ( ph -> N e. ZZ )
fzuntgd.km 
|- ( ph -> K <_ M )
fzuntgd.ml 
|- ( ph -> M <_ ( L + 1 ) )
fzuntgd.ln 
|- ( ph -> L <_ N )
Assertion fzuntgd 
|- ( ph -> ( ( K ... L ) u. ( M ... N ) ) = ( K ... N ) )

Proof

Step Hyp Ref Expression
1 fzuntgd.k 
 |-  ( ph -> K e. ZZ )
2 fzuntgd.l 
 |-  ( ph -> L e. ZZ )
3 fzuntgd.m 
 |-  ( ph -> M e. ZZ )
4 fzuntgd.n 
 |-  ( ph -> N e. ZZ )
5 fzuntgd.km 
 |-  ( ph -> K <_ M )
6 fzuntgd.ml 
 |-  ( ph -> M <_ ( L + 1 ) )
7 fzuntgd.ln 
 |-  ( ph -> L <_ N )
8 zre 
 |-  ( j e. ZZ -> j e. RR )
9 simplr 
 |-  ( ( ( ph /\ j e. RR ) /\ j <_ L ) -> j e. RR )
10 2 zred 
 |-  ( ph -> L e. RR )
11 10 ad2antrr 
 |-  ( ( ( ph /\ j e. RR ) /\ j <_ L ) -> L e. RR )
12 4 zred 
 |-  ( ph -> N e. RR )
13 12 ad2antrr 
 |-  ( ( ( ph /\ j e. RR ) /\ j <_ L ) -> N e. RR )
14 simpr 
 |-  ( ( ( ph /\ j e. RR ) /\ j <_ L ) -> j <_ L )
15 7 ad2antrr 
 |-  ( ( ( ph /\ j e. RR ) /\ j <_ L ) -> L <_ N )
16 9 11 13 14 15 letrd 
 |-  ( ( ( ph /\ j e. RR ) /\ j <_ L ) -> j <_ N )
17 16 ex 
 |-  ( ( ph /\ j e. RR ) -> ( j <_ L -> j <_ N ) )
18 17 anim2d 
 |-  ( ( ph /\ j e. RR ) -> ( ( K <_ j /\ j <_ L ) -> ( K <_ j /\ j <_ N ) ) )
19 1 zred 
 |-  ( ph -> K e. RR )
20 19 ad2antrr 
 |-  ( ( ( ph /\ j e. RR ) /\ M <_ j ) -> K e. RR )
21 3 zred 
 |-  ( ph -> M e. RR )
22 21 ad2antrr 
 |-  ( ( ( ph /\ j e. RR ) /\ M <_ j ) -> M e. RR )
23 simplr 
 |-  ( ( ( ph /\ j e. RR ) /\ M <_ j ) -> j e. RR )
24 5 ad2antrr 
 |-  ( ( ( ph /\ j e. RR ) /\ M <_ j ) -> K <_ M )
25 simpr 
 |-  ( ( ( ph /\ j e. RR ) /\ M <_ j ) -> M <_ j )
26 20 22 23 24 25 letrd 
 |-  ( ( ( ph /\ j e. RR ) /\ M <_ j ) -> K <_ j )
27 26 ex 
 |-  ( ( ph /\ j e. RR ) -> ( M <_ j -> K <_ j ) )
28 27 anim1d 
 |-  ( ( ph /\ j e. RR ) -> ( ( M <_ j /\ j <_ N ) -> ( K <_ j /\ j <_ N ) ) )
29 18 28 jaod 
 |-  ( ( ph /\ j e. RR ) -> ( ( ( K <_ j /\ j <_ L ) \/ ( M <_ j /\ j <_ N ) ) -> ( K <_ j /\ j <_ N ) ) )
30 8 29 sylan2 
 |-  ( ( ph /\ j e. ZZ ) -> ( ( ( 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 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( K <_ j /\ j <_ N ) ) -> ( ( K <_ j \/ M <_ j ) /\ ( K <_ j \/ j <_ N ) ) )
35 animorrl 
 |-  ( ( ( ph /\ j e. ZZ ) /\ j <_ L ) -> ( j <_ L \/ M <_ j ) )
36 21 ad2antrr 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( L + 1 ) <_ j ) -> M e. RR )
37 peano2re 
 |-  ( L e. RR -> ( L + 1 ) e. RR )
38 10 37 syl 
 |-  ( ph -> ( L + 1 ) e. RR )
39 38 ad2antrr 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( L + 1 ) <_ j ) -> ( L + 1 ) e. RR )
40 simplr 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( L + 1 ) <_ j ) -> j e. ZZ )
41 40 zred 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( L + 1 ) <_ j ) -> j e. RR )
42 6 ad2antrr 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( L + 1 ) <_ j ) -> M <_ ( L + 1 ) )
43 simpr 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( L + 1 ) <_ j ) -> ( L + 1 ) <_ j )
44 36 39 41 42 43 letrd 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( L + 1 ) <_ j ) -> M <_ j )
45 44 olcd 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( L + 1 ) <_ j ) -> ( j <_ L \/ M <_ j ) )
46 simpr 
 |-  ( ( ph /\ j e. ZZ ) -> j e. ZZ )
47 46 zred 
 |-  ( ( ph /\ j e. ZZ ) -> j e. RR )
48 2 adantr 
 |-  ( ( ph /\ j e. ZZ ) -> L e. ZZ )
49 48 zred 
 |-  ( ( ph /\ j e. ZZ ) -> L e. RR )
50 lelttric 
 |-  ( ( j e. RR /\ L e. RR ) -> ( j <_ L \/ L < j ) )
51 47 49 50 syl2anc 
 |-  ( ( ph /\ j e. ZZ ) -> ( j <_ L \/ L < j ) )
52 zltp1le 
 |-  ( ( L e. ZZ /\ j e. ZZ ) -> ( L < j <-> ( L + 1 ) <_ j ) )
53 2 52 sylan 
 |-  ( ( ph /\ j e. ZZ ) -> ( L < j <-> ( L + 1 ) <_ j ) )
54 53 orbi2d 
 |-  ( ( ph /\ j e. ZZ ) -> ( ( j <_ L \/ L < j ) <-> ( j <_ L \/ ( L + 1 ) <_ j ) ) )
55 51 54 mpbid 
 |-  ( ( ph /\ j e. ZZ ) -> ( j <_ L \/ ( L + 1 ) <_ j ) )
56 35 45 55 mpjaodan 
 |-  ( ( ph /\ j e. ZZ ) -> ( j <_ L \/ M <_ j ) )
57 56 adantr 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( K <_ j /\ j <_ N ) ) -> ( j <_ L \/ M <_ j ) )
58 simprr 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( K <_ j /\ j <_ N ) ) -> j <_ N )
59 58 olcd 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( K <_ j /\ j <_ N ) ) -> ( j <_ L \/ j <_ N ) )
60 57 59 jca 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( 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 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( K <_ j /\ j <_ N ) ) -> ( ( K <_ j /\ j <_ L ) \/ ( M <_ j /\ j <_ N ) ) )
63 62 ex 
 |-  ( ( ph /\ j e. ZZ ) -> ( ( K <_ j /\ j <_ N ) -> ( ( K <_ j /\ j <_ L ) \/ ( M <_ j /\ j <_ N ) ) ) )
64 30 63 impbid 
 |-  ( ( ph /\ j e. ZZ ) -> ( ( ( K <_ j /\ j <_ L ) \/ ( M <_ j /\ j <_ N ) ) <-> ( K <_ j /\ j <_ N ) ) )
65 64 pm5.32da 
 |-  ( ph -> ( ( j e. ZZ /\ ( ( K <_ j /\ j <_ L ) \/ ( M <_ j /\ j <_ N ) ) ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ N ) ) ) )
66 elfz1 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> ( j e. ( K ... L ) <-> ( j e. ZZ /\ K <_ j /\ j <_ L ) ) )
67 1 2 66 syl2anc 
 |-  ( ph -> ( j e. ( K ... L ) <-> ( j e. ZZ /\ K <_ j /\ j <_ L ) ) )
68 3anass 
 |-  ( ( j e. ZZ /\ K <_ j /\ j <_ L ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ L ) ) )
69 67 68 bitrdi 
 |-  ( ph -> ( j e. ( K ... L ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ L ) ) ) )
70 elfz1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( j e. ( M ... N ) <-> ( j e. ZZ /\ M <_ j /\ j <_ N ) ) )
71 3 4 70 syl2anc 
 |-  ( ph -> ( j e. ( M ... N ) <-> ( j e. ZZ /\ M <_ j /\ j <_ N ) ) )
72 3anass 
 |-  ( ( j e. ZZ /\ M <_ j /\ j <_ N ) <-> ( j e. ZZ /\ ( M <_ j /\ j <_ N ) ) )
73 71 72 bitrdi 
 |-  ( ph -> ( j e. ( M ... N ) <-> ( j e. ZZ /\ ( M <_ j /\ j <_ N ) ) ) )
74 69 73 orbi12d 
 |-  ( ph -> ( ( j e. ( K ... L ) \/ j e. ( M ... N ) ) <-> ( ( j e. ZZ /\ ( K <_ j /\ j <_ L ) ) \/ ( j e. ZZ /\ ( M <_ j /\ j <_ N ) ) ) ) )
75 elun 
 |-  ( j e. ( ( K ... L ) u. ( M ... N ) ) <-> ( j e. ( K ... L ) \/ j e. ( M ... N ) ) )
76 andi 
 |-  ( ( j e. ZZ /\ ( ( K <_ j /\ j <_ L ) \/ ( M <_ j /\ j <_ N ) ) ) <-> ( ( j e. ZZ /\ ( K <_ j /\ j <_ L ) ) \/ ( j e. ZZ /\ ( M <_ j /\ j <_ N ) ) ) )
77 74 75 76 3bitr4g 
 |-  ( ph -> ( j e. ( ( K ... L ) u. ( M ... N ) ) <-> ( j e. ZZ /\ ( ( K <_ j /\ j <_ L ) \/ ( M <_ j /\ j <_ N ) ) ) ) )
78 elfz1 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( j e. ( K ... N ) <-> ( j e. ZZ /\ K <_ j /\ j <_ N ) ) )
79 1 4 78 syl2anc 
 |-  ( ph -> ( j e. ( K ... N ) <-> ( j e. ZZ /\ K <_ j /\ j <_ N ) ) )
80 3anass 
 |-  ( ( j e. ZZ /\ K <_ j /\ j <_ N ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ N ) ) )
81 79 80 bitrdi 
 |-  ( ph -> ( j e. ( K ... N ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ N ) ) ) )
82 65 77 81 3bitr4d 
 |-  ( ph -> ( j e. ( ( K ... L ) u. ( M ... N ) ) <-> j e. ( K ... N ) ) )
83 82 eqrdv 
 |-  ( ph -> ( ( K ... L ) u. ( M ... N ) ) = ( K ... N ) )