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 
|- ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K <_ M /\ M <_ N ) ) -> ( ( K ... M ) u. ( M ... N ) ) = ( K ... N ) )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( K e. ZZ -> K e. RR )
2 zre 
 |-  ( M e. ZZ -> M e. RR )
3 zre 
 |-  ( N e. ZZ -> N e. RR )
4 zre 
 |-  ( j e. ZZ -> j e. RR )
5 simprl 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ ( j e. RR /\ j <_ M ) ) -> j e. RR )
6 simpl2 
 |-  ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) -> M e. RR )
7 6 adantr 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ ( j e. RR /\ j <_ M ) ) -> M e. RR )
8 simpll3 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ ( j e. RR /\ j <_ M ) ) -> N e. RR )
9 simprr 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ ( j e. RR /\ j <_ M ) ) -> j <_ M )
10 simprr 
 |-  ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) -> M <_ N )
11 10 adantr 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ ( j e. RR /\ j <_ M ) ) -> M <_ N )
12 5 7 8 9 11 letrd 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ ( j e. RR /\ j <_ M ) ) -> j <_ N )
13 12 expr 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ j e. RR ) -> ( j <_ M -> j <_ N ) )
14 13 anim2d 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ j e. RR ) -> ( ( K <_ j /\ j <_ M ) -> ( K <_ j /\ j <_ N ) ) )
15 simpll1 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ ( j e. RR /\ M <_ j ) ) -> K e. RR )
16 6 adantr 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ ( j e. RR /\ M <_ j ) ) -> M e. RR )
17 simprl 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ ( j e. RR /\ M <_ j ) ) -> j e. RR )
18 simprl 
 |-  ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) -> K <_ M )
19 18 adantr 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ ( j e. RR /\ M <_ j ) ) -> K <_ M )
20 simprr 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ ( j e. RR /\ M <_ j ) ) -> M <_ j )
21 15 16 17 19 20 letrd 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ ( j e. RR /\ M <_ j ) ) -> K <_ j )
22 21 expr 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ j e. RR ) -> ( M <_ j -> K <_ j ) )
23 22 anim1d 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ j e. RR ) -> ( ( M <_ j /\ j <_ N ) -> ( K <_ j /\ j <_ N ) ) )
24 14 23 jaod 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ j e. RR ) -> ( ( ( K <_ j /\ j <_ M ) \/ ( M <_ j /\ j <_ N ) ) -> ( K <_ j /\ j <_ N ) ) )
25 orc 
 |-  ( K <_ j -> ( K <_ j \/ M <_ j ) )
26 orc 
 |-  ( K <_ j -> ( K <_ j \/ j <_ N ) )
27 25 26 jca 
 |-  ( K <_ j -> ( ( K <_ j \/ M <_ j ) /\ ( K <_ j \/ j <_ N ) ) )
28 27 ad2antrl 
 |-  ( ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ j e. RR ) /\ ( K <_ j /\ j <_ N ) ) -> ( ( K <_ j \/ M <_ j ) /\ ( K <_ j \/ j <_ N ) ) )
29 letric 
 |-  ( ( j e. RR /\ M e. RR ) -> ( j <_ M \/ M <_ j ) )
30 29 ancoms 
 |-  ( ( M e. RR /\ j e. RR ) -> ( j <_ M \/ M <_ j ) )
31 6 30 sylan 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ j e. RR ) -> ( j <_ M \/ M <_ j ) )
32 31 adantr 
 |-  ( ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ j e. RR ) /\ ( K <_ j /\ j <_ N ) ) -> ( j <_ M \/ M <_ j ) )
33 simprr 
 |-  ( ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ j e. RR ) /\ ( K <_ j /\ j <_ N ) ) -> j <_ N )
34 33 olcd 
 |-  ( ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ j e. RR ) /\ ( K <_ j /\ j <_ N ) ) -> ( j <_ M \/ j <_ N ) )
35 32 34 jca 
 |-  ( ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ j e. RR ) /\ ( K <_ j /\ j <_ N ) ) -> ( ( j <_ M \/ M <_ j ) /\ ( j <_ M \/ j <_ N ) ) )
36 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 ) ) ) )
37 28 35 36 sylanbrc 
 |-  ( ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ j e. RR ) /\ ( K <_ j /\ j <_ N ) ) -> ( ( K <_ j /\ j <_ M ) \/ ( M <_ j /\ j <_ N ) ) )
38 37 ex 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ j e. RR ) -> ( ( K <_ j /\ j <_ N ) -> ( ( K <_ j /\ j <_ M ) \/ ( M <_ j /\ j <_ N ) ) ) )
39 24 38 impbid 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ j e. RR ) -> ( ( ( K <_ j /\ j <_ M ) \/ ( M <_ j /\ j <_ N ) ) <-> ( K <_ j /\ j <_ N ) ) )
40 4 39 sylan2 
 |-  ( ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) /\ j e. ZZ ) -> ( ( ( K <_ j /\ j <_ M ) \/ ( M <_ j /\ j <_ N ) ) <-> ( K <_ j /\ j <_ N ) ) )
41 40 pm5.32da 
 |-  ( ( ( K e. RR /\ M e. RR /\ N e. RR ) /\ ( K <_ M /\ M <_ N ) ) -> ( ( j e. ZZ /\ ( ( K <_ j /\ j <_ M ) \/ ( M <_ j /\ j <_ N ) ) ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ N ) ) ) )
42 1 2 3 41 syl3anl 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K <_ M /\ M <_ N ) ) -> ( ( j e. ZZ /\ ( ( K <_ j /\ j <_ M ) \/ ( M <_ j /\ j <_ N ) ) ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ N ) ) ) )
43 simp1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> K e. ZZ )
44 simp2 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> M e. ZZ )
45 elfz1 
 |-  ( ( K e. ZZ /\ M e. ZZ ) -> ( j e. ( K ... M ) <-> ( j e. ZZ /\ K <_ j /\ j <_ M ) ) )
46 43 44 45 syl2anc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( j e. ( K ... M ) <-> ( j e. ZZ /\ K <_ j /\ j <_ M ) ) )
47 3anass 
 |-  ( ( j e. ZZ /\ K <_ j /\ j <_ M ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ M ) ) )
48 46 47 bitrdi 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( j e. ( K ... M ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ M ) ) ) )
49 simp3 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> N e. ZZ )
50 elfz1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( j e. ( M ... N ) <-> ( j e. ZZ /\ M <_ j /\ j <_ N ) ) )
51 44 49 50 syl2anc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( j e. ( M ... N ) <-> ( j e. ZZ /\ M <_ j /\ j <_ N ) ) )
52 3anass 
 |-  ( ( j e. ZZ /\ M <_ j /\ j <_ N ) <-> ( j e. ZZ /\ ( M <_ j /\ j <_ N ) ) )
53 51 52 bitrdi 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( j e. ( M ... N ) <-> ( j e. ZZ /\ ( M <_ j /\ j <_ N ) ) ) )
54 48 53 orbi12d 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( j e. ( K ... M ) \/ j e. ( M ... N ) ) <-> ( ( j e. ZZ /\ ( K <_ j /\ j <_ M ) ) \/ ( j e. ZZ /\ ( M <_ j /\ j <_ N ) ) ) ) )
55 elun 
 |-  ( j e. ( ( K ... M ) u. ( M ... N ) ) <-> ( j e. ( K ... M ) \/ j e. ( M ... N ) ) )
56 andi 
 |-  ( ( j e. ZZ /\ ( ( K <_ j /\ j <_ M ) \/ ( M <_ j /\ j <_ N ) ) ) <-> ( ( j e. ZZ /\ ( K <_ j /\ j <_ M ) ) \/ ( j e. ZZ /\ ( M <_ j /\ j <_ N ) ) ) )
57 54 55 56 3bitr4g 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( j e. ( ( K ... M ) u. ( M ... N ) ) <-> ( j e. ZZ /\ ( ( K <_ j /\ j <_ M ) \/ ( M <_ j /\ j <_ N ) ) ) ) )
58 57 adantr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K <_ M /\ M <_ N ) ) -> ( j e. ( ( K ... M ) u. ( M ... N ) ) <-> ( j e. ZZ /\ ( ( K <_ j /\ j <_ M ) \/ ( M <_ j /\ j <_ N ) ) ) ) )
59 elfz1 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( j e. ( K ... N ) <-> ( j e. ZZ /\ K <_ j /\ j <_ N ) ) )
60 43 49 59 syl2anc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( j e. ( K ... N ) <-> ( j e. ZZ /\ K <_ j /\ j <_ N ) ) )
61 3anass 
 |-  ( ( j e. ZZ /\ K <_ j /\ j <_ N ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ N ) ) )
62 60 61 bitrdi 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( j e. ( K ... N ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ N ) ) ) )
63 62 adantr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K <_ M /\ M <_ N ) ) -> ( j e. ( K ... N ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ N ) ) ) )
64 42 58 63 3bitr4d 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K <_ M /\ M <_ N ) ) -> ( j e. ( ( K ... M ) u. ( M ... N ) ) <-> j e. ( K ... N ) ) )
65 64 eqrdv 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K <_ M /\ M <_ N ) ) -> ( ( K ... M ) u. ( M ... N ) ) = ( K ... N ) )