Metamath Proof Explorer


Theorem fz0fzelfz0

Description: If a member of a finite set of sequential integers with a lower bound being a member of a finite set of sequential nonnegative integers with the same upper bound, this member is also a member of the finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 21-Apr-2018)

Ref Expression
Assertion fz0fzelfz0
|- ( ( N e. ( 0 ... R ) /\ M e. ( N ... R ) ) -> M e. ( 0 ... R ) )

Proof

Step Hyp Ref Expression
1 elfz2nn0
 |-  ( N e. ( 0 ... R ) <-> ( N e. NN0 /\ R e. NN0 /\ N <_ R ) )
2 elfz2
 |-  ( M e. ( N ... R ) <-> ( ( N e. ZZ /\ R e. ZZ /\ M e. ZZ ) /\ ( N <_ M /\ M <_ R ) ) )
3 simplr
 |-  ( ( ( N e. NN0 /\ M e. ZZ ) /\ N <_ M ) -> M e. ZZ )
4 0red
 |-  ( ( N e. NN0 /\ M e. ZZ ) -> 0 e. RR )
5 nn0re
 |-  ( N e. NN0 -> N e. RR )
6 5 adantr
 |-  ( ( N e. NN0 /\ M e. ZZ ) -> N e. RR )
7 zre
 |-  ( M e. ZZ -> M e. RR )
8 7 adantl
 |-  ( ( N e. NN0 /\ M e. ZZ ) -> M e. RR )
9 4 6 8 3jca
 |-  ( ( N e. NN0 /\ M e. ZZ ) -> ( 0 e. RR /\ N e. RR /\ M e. RR ) )
10 9 adantr
 |-  ( ( ( N e. NN0 /\ M e. ZZ ) /\ N <_ M ) -> ( 0 e. RR /\ N e. RR /\ M e. RR ) )
11 nn0ge0
 |-  ( N e. NN0 -> 0 <_ N )
12 11 adantr
 |-  ( ( N e. NN0 /\ M e. ZZ ) -> 0 <_ N )
13 12 anim1i
 |-  ( ( ( N e. NN0 /\ M e. ZZ ) /\ N <_ M ) -> ( 0 <_ N /\ N <_ M ) )
14 letr
 |-  ( ( 0 e. RR /\ N e. RR /\ M e. RR ) -> ( ( 0 <_ N /\ N <_ M ) -> 0 <_ M ) )
15 10 13 14 sylc
 |-  ( ( ( N e. NN0 /\ M e. ZZ ) /\ N <_ M ) -> 0 <_ M )
16 elnn0z
 |-  ( M e. NN0 <-> ( M e. ZZ /\ 0 <_ M ) )
17 3 15 16 sylanbrc
 |-  ( ( ( N e. NN0 /\ M e. ZZ ) /\ N <_ M ) -> M e. NN0 )
18 17 exp31
 |-  ( N e. NN0 -> ( M e. ZZ -> ( N <_ M -> M e. NN0 ) ) )
19 18 com23
 |-  ( N e. NN0 -> ( N <_ M -> ( M e. ZZ -> M e. NN0 ) ) )
20 19 3ad2ant1
 |-  ( ( N e. NN0 /\ R e. NN0 /\ N <_ R ) -> ( N <_ M -> ( M e. ZZ -> M e. NN0 ) ) )
21 20 com13
 |-  ( M e. ZZ -> ( N <_ M -> ( ( N e. NN0 /\ R e. NN0 /\ N <_ R ) -> M e. NN0 ) ) )
22 21 adantrd
 |-  ( M e. ZZ -> ( ( N <_ M /\ M <_ R ) -> ( ( N e. NN0 /\ R e. NN0 /\ N <_ R ) -> M e. NN0 ) ) )
23 22 3ad2ant3
 |-  ( ( N e. ZZ /\ R e. ZZ /\ M e. ZZ ) -> ( ( N <_ M /\ M <_ R ) -> ( ( N e. NN0 /\ R e. NN0 /\ N <_ R ) -> M e. NN0 ) ) )
24 23 imp
 |-  ( ( ( N e. ZZ /\ R e. ZZ /\ M e. ZZ ) /\ ( N <_ M /\ M <_ R ) ) -> ( ( N e. NN0 /\ R e. NN0 /\ N <_ R ) -> M e. NN0 ) )
25 24 imp
 |-  ( ( ( ( N e. ZZ /\ R e. ZZ /\ M e. ZZ ) /\ ( N <_ M /\ M <_ R ) ) /\ ( N e. NN0 /\ R e. NN0 /\ N <_ R ) ) -> M e. NN0 )
26 simpr2
 |-  ( ( ( ( N e. ZZ /\ R e. ZZ /\ M e. ZZ ) /\ ( N <_ M /\ M <_ R ) ) /\ ( N e. NN0 /\ R e. NN0 /\ N <_ R ) ) -> R e. NN0 )
27 simplrr
 |-  ( ( ( ( N e. ZZ /\ R e. ZZ /\ M e. ZZ ) /\ ( N <_ M /\ M <_ R ) ) /\ ( N e. NN0 /\ R e. NN0 /\ N <_ R ) ) -> M <_ R )
28 25 26 27 3jca
 |-  ( ( ( ( N e. ZZ /\ R e. ZZ /\ M e. ZZ ) /\ ( N <_ M /\ M <_ R ) ) /\ ( N e. NN0 /\ R e. NN0 /\ N <_ R ) ) -> ( M e. NN0 /\ R e. NN0 /\ M <_ R ) )
29 28 ex
 |-  ( ( ( N e. ZZ /\ R e. ZZ /\ M e. ZZ ) /\ ( N <_ M /\ M <_ R ) ) -> ( ( N e. NN0 /\ R e. NN0 /\ N <_ R ) -> ( M e. NN0 /\ R e. NN0 /\ M <_ R ) ) )
30 2 29 sylbi
 |-  ( M e. ( N ... R ) -> ( ( N e. NN0 /\ R e. NN0 /\ N <_ R ) -> ( M e. NN0 /\ R e. NN0 /\ M <_ R ) ) )
31 30 com12
 |-  ( ( N e. NN0 /\ R e. NN0 /\ N <_ R ) -> ( M e. ( N ... R ) -> ( M e. NN0 /\ R e. NN0 /\ M <_ R ) ) )
32 1 31 sylbi
 |-  ( N e. ( 0 ... R ) -> ( M e. ( N ... R ) -> ( M e. NN0 /\ R e. NN0 /\ M <_ R ) ) )
33 32 imp
 |-  ( ( N e. ( 0 ... R ) /\ M e. ( N ... R ) ) -> ( M e. NN0 /\ R e. NN0 /\ M <_ R ) )
34 elfz2nn0
 |-  ( M e. ( 0 ... R ) <-> ( M e. NN0 /\ R e. NN0 /\ M <_ R ) )
35 33 34 sylibr
 |-  ( ( N e. ( 0 ... R ) /\ M e. ( N ... R ) ) -> M e. ( 0 ... R ) )