Metamath Proof Explorer

Theorem elfzonelfzo

Description: If an element of a half-open integer range is not contained in the lower subrange, it must be in the upper subrange. (Contributed by Alexander van der Vekens, 30-Mar-2018)

Ref Expression
Assertion elfzonelfzo 
|- ( N e. ZZ -> ( ( K e. ( M ..^ R ) /\ -. K e. ( M ..^ N ) ) -> K e. ( N ..^ R ) ) )

Proof

Step Hyp Ref Expression
1 elfzo2 
 |-  ( K e. ( M ..^ R ) <-> ( K e. ( ZZ>= ` M ) /\ R e. ZZ /\ K < R ) )
2 simpr 
 |-  ( ( ( ( K e. ( ZZ>= ` M ) /\ R e. ZZ /\ K < R ) /\ -. K e. ( M ..^ N ) ) /\ N e. ZZ ) -> N e. ZZ )
3 eluzelz 
 |-  ( K e. ( ZZ>= ` M ) -> K e. ZZ )
4 3 3ad2ant1 
 |-  ( ( K e. ( ZZ>= ` M ) /\ R e. ZZ /\ K < R ) -> K e. ZZ )
5 4 ad2antrr 
 |-  ( ( ( ( K e. ( ZZ>= ` M ) /\ R e. ZZ /\ K < R ) /\ -. K e. ( M ..^ N ) ) /\ N e. ZZ ) -> K e. ZZ )
6 eluzelre 
 |-  ( K e. ( ZZ>= ` M ) -> K e. RR )
7 zre 
 |-  ( N e. ZZ -> N e. RR )
8 ltnle 
 |-  ( ( K e. RR /\ N e. RR ) -> ( K < N <-> -. N <_ K ) )
9 6 7 8 syl2an 
 |-  ( ( K e. ( ZZ>= ` M ) /\ N e. ZZ ) -> ( K < N <-> -. N <_ K ) )
10 id 
 |-  ( ( K e. ( ZZ>= ` M ) /\ N e. ZZ /\ K < N ) -> ( K e. ( ZZ>= ` M ) /\ N e. ZZ /\ K < N ) )
11 10 3expa 
 |-  ( ( ( K e. ( ZZ>= ` M ) /\ N e. ZZ ) /\ K < N ) -> ( K e. ( ZZ>= ` M ) /\ N e. ZZ /\ K < N ) )
12 elfzo2 
 |-  ( K e. ( M ..^ N ) <-> ( K e. ( ZZ>= ` M ) /\ N e. ZZ /\ K < N ) )
13 11 12 sylibr 
 |-  ( ( ( K e. ( ZZ>= ` M ) /\ N e. ZZ ) /\ K < N ) -> K e. ( M ..^ N ) )
14 13 ex 
 |-  ( ( K e. ( ZZ>= ` M ) /\ N e. ZZ ) -> ( K < N -> K e. ( M ..^ N ) ) )
15 9 14 sylbird 
 |-  ( ( K e. ( ZZ>= ` M ) /\ N e. ZZ ) -> ( -. N <_ K -> K e. ( M ..^ N ) ) )
16 15 con1d 
 |-  ( ( K e. ( ZZ>= ` M ) /\ N e. ZZ ) -> ( -. K e. ( M ..^ N ) -> N <_ K ) )
17 16 ex 
 |-  ( K e. ( ZZ>= ` M ) -> ( N e. ZZ -> ( -. K e. ( M ..^ N ) -> N <_ K ) ) )
18 17 com23 
 |-  ( K e. ( ZZ>= ` M ) -> ( -. K e. ( M ..^ N ) -> ( N e. ZZ -> N <_ K ) ) )
19 18 3ad2ant1 
 |-  ( ( K e. ( ZZ>= ` M ) /\ R e. ZZ /\ K < R ) -> ( -. K e. ( M ..^ N ) -> ( N e. ZZ -> N <_ K ) ) )
20 19 imp31 
 |-  ( ( ( ( K e. ( ZZ>= ` M ) /\ R e. ZZ /\ K < R ) /\ -. K e. ( M ..^ N ) ) /\ N e. ZZ ) -> N <_ K )
21 eluz2 
 |-  ( K e. ( ZZ>= ` N ) <-> ( N e. ZZ /\ K e. ZZ /\ N <_ K ) )
22 2 5 20 21 syl3anbrc 
 |-  ( ( ( ( K e. ( ZZ>= ` M ) /\ R e. ZZ /\ K < R ) /\ -. K e. ( M ..^ N ) ) /\ N e. ZZ ) -> K e. ( ZZ>= ` N ) )
23 simpll2 
 |-  ( ( ( ( K e. ( ZZ>= ` M ) /\ R e. ZZ /\ K < R ) /\ -. K e. ( M ..^ N ) ) /\ N e. ZZ ) -> R e. ZZ )
24 simpll3 
 |-  ( ( ( ( K e. ( ZZ>= ` M ) /\ R e. ZZ /\ K < R ) /\ -. K e. ( M ..^ N ) ) /\ N e. ZZ ) -> K < R )
25 elfzo2 
 |-  ( K e. ( N ..^ R ) <-> ( K e. ( ZZ>= ` N ) /\ R e. ZZ /\ K < R ) )
26 22 23 24 25 syl3anbrc 
 |-  ( ( ( ( K e. ( ZZ>= ` M ) /\ R e. ZZ /\ K < R ) /\ -. K e. ( M ..^ N ) ) /\ N e. ZZ ) -> K e. ( N ..^ R ) )
27 26 ex 
 |-  ( ( ( K e. ( ZZ>= ` M ) /\ R e. ZZ /\ K < R ) /\ -. K e. ( M ..^ N ) ) -> ( N e. ZZ -> K e. ( N ..^ R ) ) )
28 1 27 sylanb 
 |-  ( ( K e. ( M ..^ R ) /\ -. K e. ( M ..^ N ) ) -> ( N e. ZZ -> K e. ( N ..^ R ) ) )
29 28 com12 
 |-  ( N e. ZZ -> ( ( K e. ( M ..^ R ) /\ -. K e. ( M ..^ N ) ) -> K e. ( N ..^ R ) ) )