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