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 
|- ( ph -> K e. ZZ )
fzuntd.m 
|- ( ph -> M e. ZZ )
fzuntd.n 
|- ( ph -> N e. ZZ )
fzuntd.km 
|- ( ph -> K <_ M )
fzuntd.mn 
|- ( ph -> M <_ N )
Assertion fzuntd 
|- ( ph -> ( ( K ... M ) u. ( M ... N ) ) = ( K ... N ) )

Proof

Step Hyp Ref Expression
1 fzuntd.k 
 |-  ( ph -> K e. ZZ )
2 fzuntd.m 
 |-  ( ph -> M e. ZZ )
3 fzuntd.n 
 |-  ( ph -> N e. ZZ )
4 fzuntd.km 
 |-  ( ph -> K <_ M )
5 fzuntd.mn 
 |-  ( ph -> M <_ N )
6 simprl 
 |-  ( ( ph /\ ( j e. ZZ /\ j <_ M ) ) -> j e. ZZ )
7 6 zred 
 |-  ( ( ph /\ ( j e. ZZ /\ j <_ M ) ) -> j e. RR )
8 2 zred 
 |-  ( ph -> M e. RR )
9 8 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ j <_ M ) ) -> M e. RR )
10 3 zred 
 |-  ( ph -> N e. RR )
11 10 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ j <_ M ) ) -> N e. RR )
12 simprr 
 |-  ( ( ph /\ ( j e. ZZ /\ j <_ M ) ) -> j <_ M )
13 5 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ j <_ M ) ) -> M <_ N )
14 7 9 11 12 13 letrd 
 |-  ( ( ph /\ ( j e. ZZ /\ j <_ M ) ) -> j <_ N )
15 14 expr 
 |-  ( ( ph /\ j e. ZZ ) -> ( j <_ M -> j <_ N ) )
16 15 anim2d 
 |-  ( ( ph /\ j e. ZZ ) -> ( ( K <_ j /\ j <_ M ) -> ( K <_ j /\ j <_ N ) ) )
17 1 zred 
 |-  ( ph -> K e. RR )
18 17 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ M <_ j ) ) -> K e. RR )
19 8 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ M <_ j ) ) -> M e. RR )
20 simprl 
 |-  ( ( ph /\ ( j e. ZZ /\ M <_ j ) ) -> j e. ZZ )
21 20 zred 
 |-  ( ( ph /\ ( j e. ZZ /\ M <_ j ) ) -> j e. RR )
22 4 adantr 
 |-  ( ( ph /\ ( j e. ZZ /\ M <_ j ) ) -> K <_ M )
23 simprr 
 |-  ( ( ph /\ ( j e. ZZ /\ M <_ j ) ) -> M <_ j )
24 18 19 21 22 23 letrd 
 |-  ( ( ph /\ ( j e. ZZ /\ M <_ j ) ) -> K <_ j )
25 24 expr 
 |-  ( ( ph /\ j e. ZZ ) -> ( M <_ j -> K <_ j ) )
26 25 anim1d 
 |-  ( ( ph /\ j e. ZZ ) -> ( ( M <_ j /\ j <_ N ) -> ( K <_ j /\ j <_ N ) ) )
27 16 26 jaod 
 |-  ( ( ph /\ j e. ZZ ) -> ( ( ( 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 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( K <_ j /\ j <_ N ) ) -> ( ( K <_ j \/ M <_ j ) /\ ( K <_ j \/ j <_ N ) ) )
32 simpr 
 |-  ( ( ph /\ j e. ZZ ) -> j e. ZZ )
33 32 zred 
 |-  ( ( ph /\ j e. ZZ ) -> j e. RR )
34 8 adantr 
 |-  ( ( ph /\ j e. ZZ ) -> M e. RR )
35 33 34 letrid 
 |-  ( ( ph /\ j e. ZZ ) -> ( j <_ M \/ M <_ j ) )
36 35 adantr 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( K <_ j /\ j <_ N ) ) -> ( j <_ M \/ M <_ j ) )
37 simprr 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( K <_ j /\ j <_ N ) ) -> j <_ N )
38 37 olcd 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( K <_ j /\ j <_ N ) ) -> ( j <_ M \/ j <_ N ) )
39 36 38 jca 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( 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 
 |-  ( ( ( ph /\ j e. ZZ ) /\ ( K <_ j /\ j <_ N ) ) -> ( ( K <_ j /\ j <_ M ) \/ ( M <_ j /\ j <_ N ) ) )
42 41 ex 
 |-  ( ( ph /\ j e. ZZ ) -> ( ( K <_ j /\ j <_ N ) -> ( ( K <_ j /\ j <_ M ) \/ ( M <_ j /\ j <_ N ) ) ) )
43 27 42 impbid 
 |-  ( ( ph /\ j e. ZZ ) -> ( ( ( K <_ j /\ j <_ M ) \/ ( M <_ j /\ j <_ N ) ) <-> ( K <_ j /\ j <_ N ) ) )
44 43 pm5.32da 
 |-  ( ph -> ( ( j e. ZZ /\ ( ( K <_ j /\ j <_ M ) \/ ( M <_ j /\ j <_ N ) ) ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ N ) ) ) )
45 elfz1 
 |-  ( ( K e. ZZ /\ M e. ZZ ) -> ( j e. ( K ... M ) <-> ( j e. ZZ /\ K <_ j /\ j <_ M ) ) )
46 1 2 45 syl2anc 
 |-  ( ph -> ( 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 
 |-  ( ph -> ( j e. ( K ... M ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ M ) ) ) )
49 elfz1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( j e. ( M ... N ) <-> ( j e. ZZ /\ M <_ j /\ j <_ N ) ) )
50 2 3 49 syl2anc 
 |-  ( ph -> ( j e. ( M ... N ) <-> ( j e. ZZ /\ M <_ j /\ j <_ N ) ) )
51 3anass 
 |-  ( ( j e. ZZ /\ M <_ j /\ j <_ N ) <-> ( j e. ZZ /\ ( M <_ j /\ j <_ N ) ) )
52 50 51 bitrdi 
 |-  ( ph -> ( j e. ( M ... N ) <-> ( j e. ZZ /\ ( M <_ j /\ j <_ N ) ) ) )
53 48 52 orbi12d 
 |-  ( ph -> ( ( j e. ( K ... M ) \/ j e. ( M ... N ) ) <-> ( ( j e. ZZ /\ ( K <_ j /\ j <_ M ) ) \/ ( j e. ZZ /\ ( M <_ j /\ j <_ N ) ) ) ) )
54 elun 
 |-  ( j e. ( ( K ... M ) u. ( M ... N ) ) <-> ( j e. ( K ... M ) \/ j e. ( M ... N ) ) )
55 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 ) ) ) )
56 53 54 55 3bitr4g 
 |-  ( ph -> ( j e. ( ( K ... M ) u. ( M ... N ) ) <-> ( j e. ZZ /\ ( ( K <_ j /\ j <_ M ) \/ ( M <_ j /\ j <_ N ) ) ) ) )
57 elfz1 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( j e. ( K ... N ) <-> ( j e. ZZ /\ K <_ j /\ j <_ N ) ) )
58 1 3 57 syl2anc 
 |-  ( ph -> ( j e. ( K ... N ) <-> ( j e. ZZ /\ K <_ j /\ j <_ N ) ) )
59 3anass 
 |-  ( ( j e. ZZ /\ K <_ j /\ j <_ N ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ N ) ) )
60 58 59 bitrdi 
 |-  ( ph -> ( j e. ( K ... N ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ N ) ) ) )
61 44 56 60 3bitr4d 
 |-  ( ph -> ( j e. ( ( K ... M ) u. ( M ... N ) ) <-> j e. ( K ... N ) ) )
62 61 eqrdv 
 |-  ( ph -> ( ( K ... M ) u. ( M ... N ) ) = ( K ... N ) )