This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )