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

Proof

Step Hyp Ref Expression
1 fzunt1d.k 
 |-  ( ph -> K e. ZZ )
2 fzunt1d.l 
 |-  ( ph -> L e. ZZ )
3 fzunt1d.m 
 |-  ( ph -> M e. ZZ )
4 fzunt1d.n 
 |-  ( ph -> N e. ZZ )
5 fzunt1d.km 
 |-  ( ph -> K <_ M )
6 fzunt1d.ml 
 |-  ( ph -> M <_ L )
7 fzunt1d.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 ad2antrr 
 |-  ( ( ( ph /\ j e. RR ) /\ j <_ L ) -> L e. ZZ )
11 10 zred 
 |-  ( ( ( ph /\ j e. RR ) /\ j <_ L ) -> L e. RR )
12 4 ad2antrr 
 |-  ( ( ( ph /\ j e. RR ) /\ j <_ L ) -> N e. ZZ )
13 12 zred 
 |-  ( ( ( 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 ad2antrr 
 |-  ( ( ( ph /\ j e. RR ) /\ M <_ j ) -> K e. ZZ )
20 19 zred 
 |-  ( ( ( ph /\ j e. RR ) /\ M <_ j ) -> K e. RR )
21 3 ad2antrr 
 |-  ( ( ( ph /\ j e. RR ) /\ M <_ j ) -> M e. ZZ )
22 21 zred 
 |-  ( ( ( 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 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 
 |-  ( ( ( ph /\ j e. RR ) /\ ( K <_ j /\ j <_ N ) ) -> ( ( K <_ j \/ M <_ j ) /\ ( K <_ j \/ j <_ N ) ) )
34 simpr 
 |-  ( ( ph /\ j e. RR ) -> j e. RR )
35 2 adantr 
 |-  ( ( ph /\ j e. RR ) -> L e. ZZ )
36 35 zred 
 |-  ( ( ph /\ j e. RR ) -> L e. RR )
37 14 orcd 
 |-  ( ( ( ph /\ j e. RR ) /\ j <_ L ) -> ( j <_ L \/ M <_ j ) )
38 3 ad2antrr 
 |-  ( ( ( ph /\ j e. RR ) /\ L <_ j ) -> M e. ZZ )
39 38 zred 
 |-  ( ( ( ph /\ j e. RR ) /\ L <_ j ) -> M e. RR )
40 2 ad2antrr 
 |-  ( ( ( ph /\ j e. RR ) /\ L <_ j ) -> L e. ZZ )
41 40 zred 
 |-  ( ( ( ph /\ j e. RR ) /\ L <_ j ) -> L e. RR )
42 simplr 
 |-  ( ( ( ph /\ j e. RR ) /\ L <_ j ) -> j e. RR )
43 6 ad2antrr 
 |-  ( ( ( ph /\ j e. RR ) /\ L <_ j ) -> M <_ L )
44 simpr 
 |-  ( ( ( ph /\ j e. RR ) /\ L <_ j ) -> L <_ j )
45 39 41 42 43 44 letrd 
 |-  ( ( ( ph /\ j e. RR ) /\ L <_ j ) -> M <_ j )
46 45 olcd 
 |-  ( ( ( ph /\ j e. RR ) /\ L <_ j ) -> ( j <_ L \/ M <_ j ) )
47 34 36 37 46 lecasei 
 |-  ( ( ph /\ j e. RR ) -> ( j <_ L \/ M <_ j ) )
48 47 adantr 
 |-  ( ( ( ph /\ j e. RR ) /\ ( K <_ j /\ j <_ N ) ) -> ( j <_ L \/ M <_ j ) )
49 simprr 
 |-  ( ( ( ph /\ j e. RR ) /\ ( K <_ j /\ j <_ N ) ) -> j <_ N )
50 49 olcd 
 |-  ( ( ( ph /\ j e. RR ) /\ ( K <_ j /\ j <_ N ) ) -> ( j <_ L \/ j <_ N ) )
51 48 50 jca 
 |-  ( ( ( ph /\ j e. RR ) /\ ( 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 
 |-  ( ( ( ph /\ j e. RR ) /\ ( K <_ j /\ j <_ N ) ) -> ( ( K <_ j /\ j <_ L ) \/ ( M <_ j /\ j <_ N ) ) )
54 53 ex 
 |-  ( ( ph /\ j e. RR ) -> ( ( K <_ j /\ j <_ N ) -> ( ( K <_ j /\ j <_ L ) \/ ( M <_ j /\ j <_ N ) ) ) )
55 29 54 impbid 
 |-  ( ( ph /\ j e. RR ) -> ( ( ( K <_ j /\ j <_ L ) \/ ( M <_ j /\ j <_ N ) ) <-> ( K <_ j /\ j <_ N ) ) )
56 8 55 sylan2 
 |-  ( ( ph /\ j e. ZZ ) -> ( ( ( K <_ j /\ j <_ L ) \/ ( M <_ j /\ j <_ N ) ) <-> ( K <_ j /\ j <_ N ) ) )
57 56 pm5.32da 
 |-  ( ph -> ( ( j e. ZZ /\ ( ( K <_ j /\ j <_ L ) \/ ( M <_ j /\ j <_ N ) ) ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ N ) ) ) )
58 elfz1 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> ( j e. ( K ... L ) <-> ( j e. ZZ /\ K <_ j /\ j <_ L ) ) )
59 1 2 58 syl2anc 
 |-  ( ph -> ( j e. ( K ... L ) <-> ( j e. ZZ /\ K <_ j /\ j <_ L ) ) )
60 3anass 
 |-  ( ( j e. ZZ /\ K <_ j /\ j <_ L ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ L ) ) )
61 59 60 bitrdi 
 |-  ( ph -> ( j e. ( K ... L ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ L ) ) ) )
62 elfz1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( j e. ( M ... N ) <-> ( j e. ZZ /\ M <_ j /\ j <_ N ) ) )
63 3 4 62 syl2anc 
 |-  ( ph -> ( j e. ( M ... N ) <-> ( j e. ZZ /\ M <_ j /\ j <_ N ) ) )
64 3anass 
 |-  ( ( j e. ZZ /\ M <_ j /\ j <_ N ) <-> ( j e. ZZ /\ ( M <_ j /\ j <_ N ) ) )
65 63 64 bitrdi 
 |-  ( ph -> ( j e. ( M ... N ) <-> ( j e. ZZ /\ ( M <_ j /\ j <_ N ) ) ) )
66 61 65 orbi12d 
 |-  ( ph -> ( ( j e. ( K ... L ) \/ j e. ( M ... N ) ) <-> ( ( j e. ZZ /\ ( K <_ j /\ j <_ L ) ) \/ ( j e. ZZ /\ ( M <_ j /\ j <_ N ) ) ) ) )
67 elun 
 |-  ( j e. ( ( K ... L ) u. ( M ... N ) ) <-> ( j e. ( K ... L ) \/ j e. ( M ... N ) ) )
68 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 ) ) ) )
69 66 67 68 3bitr4g 
 |-  ( ph -> ( j e. ( ( K ... L ) u. ( M ... N ) ) <-> ( j e. ZZ /\ ( ( K <_ j /\ j <_ L ) \/ ( M <_ j /\ j <_ N ) ) ) ) )
70 elfz1 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( j e. ( K ... N ) <-> ( j e. ZZ /\ K <_ j /\ j <_ N ) ) )
71 1 4 70 syl2anc 
 |-  ( ph -> ( j e. ( K ... N ) <-> ( j e. ZZ /\ K <_ j /\ j <_ N ) ) )
72 3anass 
 |-  ( ( j e. ZZ /\ K <_ j /\ j <_ N ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ N ) ) )
73 71 72 bitrdi 
 |-  ( ph -> ( j e. ( K ... N ) <-> ( j e. ZZ /\ ( K <_ j /\ j <_ N ) ) ) )
74 57 69 73 3bitr4d 
 |-  ( ph -> ( j e. ( ( K ... L ) u. ( M ... N ) ) <-> j e. ( K ... N ) ) )
75 74 eqrdv 
 |-  ( ph -> ( ( K ... L ) u. ( M ... N ) ) = ( K ... N ) )