Metamath Proof Explorer

Theorem ssfzo12

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

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

Proof

Step Hyp Ref Expression
1 fzolb2 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> ( K e. ( K ..^ L ) <-> K < L ) )
2 1 biimp3ar 
 |-  ( ( K e. ZZ /\ L e. ZZ /\ K < L ) -> K e. ( K ..^ L ) )
3 fzoend 
 |-  ( K e. ( K ..^ L ) -> ( L - 1 ) e. ( K ..^ L ) )
4 ssel2 
 |-  ( ( ( K ..^ L ) C_ ( M ..^ N ) /\ K e. ( K ..^ L ) ) -> K e. ( M ..^ N ) )
5 ssel2 
 |-  ( ( ( K ..^ L ) C_ ( M ..^ N ) /\ ( L - 1 ) e. ( K ..^ L ) ) -> ( L - 1 ) e. ( M ..^ N ) )
6 elfzolt2 
 |-  ( ( L - 1 ) e. ( M ..^ N ) -> ( L - 1 ) < N )
7 simp2 
 |-  ( ( K e. ZZ /\ L e. ZZ /\ K < L ) -> L e. ZZ )
8 elfzoel2 
 |-  ( K e. ( M ..^ N ) -> N e. ZZ )
9 zlem1lt 
 |-  ( ( L e. ZZ /\ N e. ZZ ) -> ( L <_ N <-> ( L - 1 ) < N ) )
10 7 8 9 syl2anr 
 |-  ( ( K e. ( M ..^ N ) /\ ( K e. ZZ /\ L e. ZZ /\ K < L ) ) -> ( L <_ N <-> ( L - 1 ) < N ) )
11 elfzole1 
 |-  ( K e. ( M ..^ N ) -> M <_ K )
12 pm3.2 
 |-  ( M <_ K -> ( L <_ N -> ( M <_ K /\ L <_ N ) ) )
13 11 12 syl 
 |-  ( K e. ( M ..^ N ) -> ( L <_ N -> ( M <_ K /\ L <_ N ) ) )
14 13 adantr 
 |-  ( ( K e. ( M ..^ N ) /\ ( K e. ZZ /\ L e. ZZ /\ K < L ) ) -> ( L <_ N -> ( M <_ K /\ L <_ N ) ) )
15 10 14 sylbird 
 |-  ( ( K e. ( M ..^ N ) /\ ( K e. ZZ /\ L e. ZZ /\ K < L ) ) -> ( ( L - 1 ) < N -> ( M <_ K /\ L <_ N ) ) )
16 15 ex 
 |-  ( K e. ( M ..^ N ) -> ( ( K e. ZZ /\ L e. ZZ /\ K < L ) -> ( ( L - 1 ) < N -> ( M <_ K /\ L <_ N ) ) ) )
17 16 com13 
 |-  ( ( L - 1 ) < N -> ( ( K e. ZZ /\ L e. ZZ /\ K < L ) -> ( K e. ( M ..^ N ) -> ( M <_ K /\ L <_ N ) ) ) )
18 5 6 17 3syl 
 |-  ( ( ( K ..^ L ) C_ ( M ..^ N ) /\ ( L - 1 ) e. ( K ..^ L ) ) -> ( ( K e. ZZ /\ L e. ZZ /\ K < L ) -> ( K e. ( M ..^ N ) -> ( M <_ K /\ L <_ N ) ) ) )
19 18 ex 
 |-  ( ( K ..^ L ) C_ ( M ..^ N ) -> ( ( L - 1 ) e. ( K ..^ L ) -> ( ( K e. ZZ /\ L e. ZZ /\ K < L ) -> ( K e. ( M ..^ N ) -> ( M <_ K /\ L <_ N ) ) ) ) )
20 19 com24 
 |-  ( ( K ..^ L ) C_ ( M ..^ N ) -> ( K e. ( M ..^ N ) -> ( ( K e. ZZ /\ L e. ZZ /\ K < L ) -> ( ( L - 1 ) e. ( K ..^ L ) -> ( M <_ K /\ L <_ N ) ) ) ) )
21 4 20 syl5com 
 |-  ( ( ( K ..^ L ) C_ ( M ..^ N ) /\ K e. ( K ..^ L ) ) -> ( ( K ..^ L ) C_ ( M ..^ N ) -> ( ( K e. ZZ /\ L e. ZZ /\ K < L ) -> ( ( L - 1 ) e. ( K ..^ L ) -> ( M <_ K /\ L <_ N ) ) ) ) )
22 21 ex 
 |-  ( ( K ..^ L ) C_ ( M ..^ N ) -> ( K e. ( K ..^ L ) -> ( ( K ..^ L ) C_ ( M ..^ N ) -> ( ( K e. ZZ /\ L e. ZZ /\ K < L ) -> ( ( L - 1 ) e. ( K ..^ L ) -> ( M <_ K /\ L <_ N ) ) ) ) ) )
23 22 pm2.43a 
 |-  ( ( K ..^ L ) C_ ( M ..^ N ) -> ( K e. ( K ..^ L ) -> ( ( K e. ZZ /\ L e. ZZ /\ K < L ) -> ( ( L - 1 ) e. ( K ..^ L ) -> ( M <_ K /\ L <_ N ) ) ) ) )
24 23 com14 
 |-  ( ( L - 1 ) e. ( K ..^ L ) -> ( K e. ( K ..^ L ) -> ( ( K e. ZZ /\ L e. ZZ /\ K < L ) -> ( ( K ..^ L ) C_ ( M ..^ N ) -> ( M <_ K /\ L <_ N ) ) ) ) )
25 3 24 mpcom 
 |-  ( K e. ( K ..^ L ) -> ( ( K e. ZZ /\ L e. ZZ /\ K < L ) -> ( ( K ..^ L ) C_ ( M ..^ N ) -> ( M <_ K /\ L <_ N ) ) ) )
26 2 25 mpcom 
 |-  ( ( K e. ZZ /\ L e. ZZ /\ K < L ) -> ( ( K ..^ L ) C_ ( M ..^ N ) -> ( M <_ K /\ L <_ N ) ) )