Metamath Proof Explorer


Theorem elfz0fzfz0

Description: A member of a finite set of sequential nonnegative integers is a member of a finite set of sequential nonnegative integers with a member of a finite set of sequential nonnegative integers starting at the upper bound of the first interval. (Contributed by Alexander van der Vekens, 27-May-2018)

Ref Expression
Assertion elfz0fzfz0
|- ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> M e. ( 0 ... N ) )

Proof

Step Hyp Ref Expression
1 elfz2nn0
 |-  ( M e. ( 0 ... L ) <-> ( M e. NN0 /\ L e. NN0 /\ M <_ L ) )
2 elfz2
 |-  ( N e. ( L ... X ) <-> ( ( L e. ZZ /\ X e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ X ) ) )
3 nn0re
 |-  ( M e. NN0 -> M e. RR )
4 nn0re
 |-  ( L e. NN0 -> L e. RR )
5 zre
 |-  ( N e. ZZ -> N e. RR )
6 3 4 5 3anim123i
 |-  ( ( M e. NN0 /\ L e. NN0 /\ N e. ZZ ) -> ( M e. RR /\ L e. RR /\ N e. RR ) )
7 6 3expa
 |-  ( ( ( M e. NN0 /\ L e. NN0 ) /\ N e. ZZ ) -> ( M e. RR /\ L e. RR /\ N e. RR ) )
8 letr
 |-  ( ( M e. RR /\ L e. RR /\ N e. RR ) -> ( ( M <_ L /\ L <_ N ) -> M <_ N ) )
9 7 8 syl
 |-  ( ( ( M e. NN0 /\ L e. NN0 ) /\ N e. ZZ ) -> ( ( M <_ L /\ L <_ N ) -> M <_ N ) )
10 simplll
 |-  ( ( ( ( M e. NN0 /\ L e. NN0 ) /\ N e. ZZ ) /\ M <_ N ) -> M e. NN0 )
11 simpr
 |-  ( ( ( M e. NN0 /\ L e. NN0 ) /\ N e. ZZ ) -> N e. ZZ )
12 11 adantr
 |-  ( ( ( ( M e. NN0 /\ L e. NN0 ) /\ N e. ZZ ) /\ M <_ N ) -> N e. ZZ )
13 elnn0z
 |-  ( M e. NN0 <-> ( M e. ZZ /\ 0 <_ M ) )
14 0red
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> 0 e. RR )
15 zre
 |-  ( M e. ZZ -> M e. RR )
16 15 adantr
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> M e. RR )
17 5 adantl
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> N e. RR )
18 letr
 |-  ( ( 0 e. RR /\ M e. RR /\ N e. RR ) -> ( ( 0 <_ M /\ M <_ N ) -> 0 <_ N ) )
19 14 16 17 18 syl3anc
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( 0 <_ M /\ M <_ N ) -> 0 <_ N ) )
20 19 exp4b
 |-  ( M e. ZZ -> ( N e. ZZ -> ( 0 <_ M -> ( M <_ N -> 0 <_ N ) ) ) )
21 20 com23
 |-  ( M e. ZZ -> ( 0 <_ M -> ( N e. ZZ -> ( M <_ N -> 0 <_ N ) ) ) )
22 21 imp
 |-  ( ( M e. ZZ /\ 0 <_ M ) -> ( N e. ZZ -> ( M <_ N -> 0 <_ N ) ) )
23 13 22 sylbi
 |-  ( M e. NN0 -> ( N e. ZZ -> ( M <_ N -> 0 <_ N ) ) )
24 23 adantr
 |-  ( ( M e. NN0 /\ L e. NN0 ) -> ( N e. ZZ -> ( M <_ N -> 0 <_ N ) ) )
25 24 imp
 |-  ( ( ( M e. NN0 /\ L e. NN0 ) /\ N e. ZZ ) -> ( M <_ N -> 0 <_ N ) )
26 25 imp
 |-  ( ( ( ( M e. NN0 /\ L e. NN0 ) /\ N e. ZZ ) /\ M <_ N ) -> 0 <_ N )
27 elnn0z
 |-  ( N e. NN0 <-> ( N e. ZZ /\ 0 <_ N ) )
28 12 26 27 sylanbrc
 |-  ( ( ( ( M e. NN0 /\ L e. NN0 ) /\ N e. ZZ ) /\ M <_ N ) -> N e. NN0 )
29 simpr
 |-  ( ( ( ( M e. NN0 /\ L e. NN0 ) /\ N e. ZZ ) /\ M <_ N ) -> M <_ N )
30 10 28 29 3jca
 |-  ( ( ( ( M e. NN0 /\ L e. NN0 ) /\ N e. ZZ ) /\ M <_ N ) -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) )
31 30 ex
 |-  ( ( ( M e. NN0 /\ L e. NN0 ) /\ N e. ZZ ) -> ( M <_ N -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) ) )
32 9 31 syld
 |-  ( ( ( M e. NN0 /\ L e. NN0 ) /\ N e. ZZ ) -> ( ( M <_ L /\ L <_ N ) -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) ) )
33 32 exp4b
 |-  ( ( M e. NN0 /\ L e. NN0 ) -> ( N e. ZZ -> ( M <_ L -> ( L <_ N -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) ) ) ) )
34 33 com23
 |-  ( ( M e. NN0 /\ L e. NN0 ) -> ( M <_ L -> ( N e. ZZ -> ( L <_ N -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) ) ) ) )
35 34 3impia
 |-  ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( N e. ZZ -> ( L <_ N -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) ) ) )
36 35 com13
 |-  ( L <_ N -> ( N e. ZZ -> ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) ) ) )
37 36 adantr
 |-  ( ( L <_ N /\ N <_ X ) -> ( N e. ZZ -> ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) ) ) )
38 37 com12
 |-  ( N e. ZZ -> ( ( L <_ N /\ N <_ X ) -> ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) ) ) )
39 38 3ad2ant3
 |-  ( ( L e. ZZ /\ X e. ZZ /\ N e. ZZ ) -> ( ( L <_ N /\ N <_ X ) -> ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) ) ) )
40 39 imp
 |-  ( ( ( L e. ZZ /\ X e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ X ) ) -> ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) ) )
41 2 40 sylbi
 |-  ( N e. ( L ... X ) -> ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) ) )
42 41 com12
 |-  ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( N e. ( L ... X ) -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) ) )
43 1 42 sylbi
 |-  ( M e. ( 0 ... L ) -> ( N e. ( L ... X ) -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) ) )
44 43 imp
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) )
45 elfz2nn0
 |-  ( M e. ( 0 ... N ) <-> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) )
46 44 45 sylibr
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> M e. ( 0 ... N ) )