Metamath Proof Explorer

Theorem ssfzo12bi

Description: Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 5-Nov-2018)

Ref Expression
Assertion ssfzo12bi 
|- ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) -> ( ( K ..^ L ) C_ ( M ..^ N ) <-> ( M <_ K /\ L <_ N ) ) )

Proof

Step Hyp Ref Expression
1 df-3an 
 |-  ( ( K e. ZZ /\ L e. ZZ /\ K < L ) <-> ( ( K e. ZZ /\ L e. ZZ ) /\ K < L ) )
2 1 biimpri 
 |-  ( ( ( K e. ZZ /\ L e. ZZ ) /\ K < L ) -> ( K e. ZZ /\ L e. ZZ /\ K < L ) )
3 2 3adant2 
 |-  ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) -> ( K e. ZZ /\ L e. ZZ /\ K < L ) )
4 ssfzo12 
 |-  ( ( K e. ZZ /\ L e. ZZ /\ K < L ) -> ( ( K ..^ L ) C_ ( M ..^ N ) -> ( M <_ K /\ L <_ N ) ) )
5 3 4 syl 
 |-  ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) -> ( ( K ..^ L ) C_ ( M ..^ N ) -> ( M <_ K /\ L <_ N ) ) )
6 elfzo2 
 |-  ( x e. ( K ..^ L ) <-> ( x e. ( ZZ>= ` K ) /\ L e. ZZ /\ x < L ) )
7 eluz2 
 |-  ( x e. ( ZZ>= ` K ) <-> ( K e. ZZ /\ x e. ZZ /\ K <_ x ) )
8 simprrl 
 |-  ( ( x e. ZZ /\ ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> M e. ZZ )
9 8 adantr 
 |-  ( ( ( x e. ZZ /\ ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) /\ ( M <_ K /\ K <_ x ) ) -> M e. ZZ )
10 simpll 
 |-  ( ( ( x e. ZZ /\ ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) /\ ( M <_ K /\ K <_ x ) ) -> x e. ZZ )
11 zre 
 |-  ( M e. ZZ -> M e. RR )
12 11 adantr 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> M e. RR )
13 12 adantl 
 |-  ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> M e. RR )
14 zre 
 |-  ( K e. ZZ -> K e. RR )
15 14 adantr 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> K e. RR )
16 15 adantr 
 |-  ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> K e. RR )
17 zre 
 |-  ( x e. ZZ -> x e. RR )
18 17 adantr 
 |-  ( ( x e. ZZ /\ ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> x e. RR )
19 letr 
 |-  ( ( M e. RR /\ K e. RR /\ x e. RR ) -> ( ( M <_ K /\ K <_ x ) -> M <_ x ) )
20 13 16 18 19 syl2an23an 
 |-  ( ( x e. ZZ /\ ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) -> ( ( M <_ K /\ K <_ x ) -> M <_ x ) )
21 20 imp 
 |-  ( ( ( x e. ZZ /\ ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) /\ ( M <_ K /\ K <_ x ) ) -> M <_ x )
22 9 10 21 3jca 
 |-  ( ( ( x e. ZZ /\ ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) ) /\ ( M <_ K /\ K <_ x ) ) -> ( M e. ZZ /\ x e. ZZ /\ M <_ x ) )
23 22 exp31 
 |-  ( x e. ZZ -> ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( M <_ K /\ K <_ x ) -> ( M e. ZZ /\ x e. ZZ /\ M <_ x ) ) ) )
24 23 com23 
 |-  ( x e. ZZ -> ( ( M <_ K /\ K <_ x ) -> ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( M e. ZZ /\ x e. ZZ /\ M <_ x ) ) ) )
25 24 expdimp 
 |-  ( ( x e. ZZ /\ M <_ K ) -> ( K <_ x -> ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( M e. ZZ /\ x e. ZZ /\ M <_ x ) ) ) )
26 25 impancom 
 |-  ( ( x e. ZZ /\ K <_ x ) -> ( M <_ K -> ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( M e. ZZ /\ x e. ZZ /\ M <_ x ) ) ) )
27 26 com13 
 |-  ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( M <_ K -> ( ( x e. ZZ /\ K <_ x ) -> ( M e. ZZ /\ x e. ZZ /\ M <_ x ) ) ) )
28 27 3adant3 
 |-  ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) -> ( M <_ K -> ( ( x e. ZZ /\ K <_ x ) -> ( M e. ZZ /\ x e. ZZ /\ M <_ x ) ) ) )
29 28 com12 
 |-  ( M <_ K -> ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) -> ( ( x e. ZZ /\ K <_ x ) -> ( M e. ZZ /\ x e. ZZ /\ M <_ x ) ) ) )
30 29 adantr 
 |-  ( ( M <_ K /\ L <_ N ) -> ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) -> ( ( x e. ZZ /\ K <_ x ) -> ( M e. ZZ /\ x e. ZZ /\ M <_ x ) ) ) )
31 30 impcom 
 |-  ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) -> ( ( x e. ZZ /\ K <_ x ) -> ( M e. ZZ /\ x e. ZZ /\ M <_ x ) ) )
32 31 com12 
 |-  ( ( x e. ZZ /\ K <_ x ) -> ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) -> ( M e. ZZ /\ x e. ZZ /\ M <_ x ) ) )
33 32 adantr 
 |-  ( ( ( x e. ZZ /\ K <_ x ) /\ x < L ) -> ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) -> ( M e. ZZ /\ x e. ZZ /\ M <_ x ) ) )
34 33 imp 
 |-  ( ( ( ( x e. ZZ /\ K <_ x ) /\ x < L ) /\ ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) ) -> ( M e. ZZ /\ x e. ZZ /\ M <_ x ) )
35 eluz2 
 |-  ( x e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ x e. ZZ /\ M <_ x ) )
36 34 35 sylibr 
 |-  ( ( ( ( x e. ZZ /\ K <_ x ) /\ x < L ) /\ ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) ) -> x e. ( ZZ>= ` M ) )
37 simpl2r 
 |-  ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) -> N e. ZZ )
38 37 adantl 
 |-  ( ( ( ( x e. ZZ /\ K <_ x ) /\ x < L ) /\ ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) ) -> N e. ZZ )
39 17 adantl 
 |-  ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ x e. ZZ ) -> x e. RR )
40 zre 
 |-  ( L e. ZZ -> L e. RR )
41 40 ad3antlr 
 |-  ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ x e. ZZ ) -> L e. RR )
42 zre 
 |-  ( N e. ZZ -> N e. RR )
43 42 adantl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> N e. RR )
44 43 adantl 
 |-  ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> N e. RR )
45 44 adantr 
 |-  ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ x e. ZZ ) -> N e. RR )
46 ltletr 
 |-  ( ( x e. RR /\ L e. RR /\ N e. RR ) -> ( ( x < L /\ L <_ N ) -> x < N ) )
47 39 41 45 46 syl3anc 
 |-  ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ x e. ZZ ) -> ( ( x < L /\ L <_ N ) -> x < N ) )
48 47 ex 
 |-  ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( x e. ZZ -> ( ( x < L /\ L <_ N ) -> x < N ) ) )
49 48 com23 
 |-  ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( x < L /\ L <_ N ) -> ( x e. ZZ -> x < N ) ) )
50 49 3adant3 
 |-  ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) -> ( ( x < L /\ L <_ N ) -> ( x e. ZZ -> x < N ) ) )
51 50 expcomd 
 |-  ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) -> ( L <_ N -> ( x < L -> ( x e. ZZ -> x < N ) ) ) )
52 51 adantld 
 |-  ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) -> ( ( M <_ K /\ L <_ N ) -> ( x < L -> ( x e. ZZ -> x < N ) ) ) )
53 52 imp 
 |-  ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) -> ( x < L -> ( x e. ZZ -> x < N ) ) )
54 53 com13 
 |-  ( x e. ZZ -> ( x < L -> ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) -> x < N ) ) )
55 54 adantr 
 |-  ( ( x e. ZZ /\ K <_ x ) -> ( x < L -> ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) -> x < N ) ) )
56 55 imp 
 |-  ( ( ( x e. ZZ /\ K <_ x ) /\ x < L ) -> ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) -> x < N ) )
57 56 imp 
 |-  ( ( ( ( x e. ZZ /\ K <_ x ) /\ x < L ) /\ ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) ) -> x < N )
58 elfzo2 
 |-  ( x e. ( M ..^ N ) <-> ( x e. ( ZZ>= ` M ) /\ N e. ZZ /\ x < N ) )
59 36 38 57 58 syl3anbrc 
 |-  ( ( ( ( x e. ZZ /\ K <_ x ) /\ x < L ) /\ ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) ) -> x e. ( M ..^ N ) )
60 59 exp31 
 |-  ( ( x e. ZZ /\ K <_ x ) -> ( x < L -> ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) -> x e. ( M ..^ N ) ) ) )
61 60 3adant1 
 |-  ( ( K e. ZZ /\ x e. ZZ /\ K <_ x ) -> ( x < L -> ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) -> x e. ( M ..^ N ) ) ) )
62 7 61 sylbi 
 |-  ( x e. ( ZZ>= ` K ) -> ( x < L -> ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) -> x e. ( M ..^ N ) ) ) )
63 62 imp 
 |-  ( ( x e. ( ZZ>= ` K ) /\ x < L ) -> ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) -> x e. ( M ..^ N ) ) )
64 63 3adant2 
 |-  ( ( x e. ( ZZ>= ` K ) /\ L e. ZZ /\ x < L ) -> ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) -> x e. ( M ..^ N ) ) )
65 6 64 sylbi 
 |-  ( x e. ( K ..^ L ) -> ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) -> x e. ( M ..^ N ) ) )
66 65 com12 
 |-  ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) -> ( x e. ( K ..^ L ) -> x e. ( M ..^ N ) ) )
67 66 ssrdv 
 |-  ( ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) /\ ( M <_ K /\ L <_ N ) ) -> ( K ..^ L ) C_ ( M ..^ N ) )
68 67 ex 
 |-  ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) -> ( ( M <_ K /\ L <_ N ) -> ( K ..^ L ) C_ ( M ..^ N ) ) )
69 5 68 impbid 
 |-  ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) -> ( ( K ..^ L ) C_ ( M ..^ N ) <-> ( M <_ K /\ L <_ N ) ) )