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 NKM..^R¬KM..^NKN..^R

Proof

Step Hyp Ref Expression
1 elfzo2 KM..^RKMRK<R
2 simpr KMRK<R¬KM..^NNN
3 eluzelz KMK
4 3 3ad2ant1 KMRK<RK
5 4 ad2antrr KMRK<R¬KM..^NNK
6 eluzelre KMK
7 zre NN
8 ltnle KNK<N¬NK
9 6 7 8 syl2an KMNK<N¬NK
10 id KMNK<NKMNK<N
11 10 3expa KMNK<NKMNK<N
12 elfzo2 KM..^NKMNK<N
13 11 12 sylibr KMNK<NKM..^N
14 13 ex KMNK<NKM..^N
15 9 14 sylbird KMN¬NKKM..^N
16 15 con1d KMN¬KM..^NNK
17 16 ex KMN¬KM..^NNK
18 17 com23 KM¬KM..^NNNK
19 18 3ad2ant1 KMRK<R¬KM..^NNNK
20 19 imp31 KMRK<R¬KM..^NNNK
21 eluz2 KNNKNK
22 2 5 20 21 syl3anbrc KMRK<R¬KM..^NNKN
23 simpll2 KMRK<R¬KM..^NNR
24 simpll3 KMRK<R¬KM..^NNK<R
25 elfzo2 KN..^RKNRK<R
26 22 23 24 25 syl3anbrc KMRK<R¬KM..^NNKN..^R
27 26 ex KMRK<R¬KM..^NNKN..^R
28 1 27 sylanb KM..^R¬KM..^NNKN..^R
29 28 com12 NKM..^R¬KM..^NKN..^R