Metamath Proof Explorer


Theorem uzsubsubfz

Description: Membership of an integer greater than L decreased by ( L - M ) in an M-based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018)

Ref Expression
Assertion uzsubsubfz
|- ( ( L e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` L ) ) -> ( N - ( L - M ) ) e. ( M ... N ) )

Proof

Step Hyp Ref Expression
1 eluz2
 |-  ( L e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ L e. ZZ /\ M <_ L ) )
2 eluz2
 |-  ( N e. ( ZZ>= ` L ) <-> ( L e. ZZ /\ N e. ZZ /\ L <_ N ) )
3 simpr
 |-  ( ( ( L e. ZZ /\ N e. ZZ ) /\ M e. ZZ ) -> M e. ZZ )
4 simpr
 |-  ( ( L e. ZZ /\ N e. ZZ ) -> N e. ZZ )
5 4 adantr
 |-  ( ( ( L e. ZZ /\ N e. ZZ ) /\ M e. ZZ ) -> N e. ZZ )
6 zsubcl
 |-  ( ( L e. ZZ /\ M e. ZZ ) -> ( L - M ) e. ZZ )
7 6 adantlr
 |-  ( ( ( L e. ZZ /\ N e. ZZ ) /\ M e. ZZ ) -> ( L - M ) e. ZZ )
8 5 7 zsubcld
 |-  ( ( ( L e. ZZ /\ N e. ZZ ) /\ M e. ZZ ) -> ( N - ( L - M ) ) e. ZZ )
9 3 5 8 3jca
 |-  ( ( ( L e. ZZ /\ N e. ZZ ) /\ M e. ZZ ) -> ( M e. ZZ /\ N e. ZZ /\ ( N - ( L - M ) ) e. ZZ ) )
10 9 ex
 |-  ( ( L e. ZZ /\ N e. ZZ ) -> ( M e. ZZ -> ( M e. ZZ /\ N e. ZZ /\ ( N - ( L - M ) ) e. ZZ ) ) )
11 10 3adant3
 |-  ( ( L e. ZZ /\ N e. ZZ /\ L <_ N ) -> ( M e. ZZ -> ( M e. ZZ /\ N e. ZZ /\ ( N - ( L - M ) ) e. ZZ ) ) )
12 11 com12
 |-  ( M e. ZZ -> ( ( L e. ZZ /\ N e. ZZ /\ L <_ N ) -> ( M e. ZZ /\ N e. ZZ /\ ( N - ( L - M ) ) e. ZZ ) ) )
13 12 adantr
 |-  ( ( M e. ZZ /\ M <_ L ) -> ( ( L e. ZZ /\ N e. ZZ /\ L <_ N ) -> ( M e. ZZ /\ N e. ZZ /\ ( N - ( L - M ) ) e. ZZ ) ) )
14 13 imp
 |-  ( ( ( M e. ZZ /\ M <_ L ) /\ ( L e. ZZ /\ N e. ZZ /\ L <_ N ) ) -> ( M e. ZZ /\ N e. ZZ /\ ( N - ( L - M ) ) e. ZZ ) )
15 zre
 |-  ( N e. ZZ -> N e. RR )
16 15 adantl
 |-  ( ( L e. ZZ /\ N e. ZZ ) -> N e. RR )
17 16 adantr
 |-  ( ( ( L e. ZZ /\ N e. ZZ ) /\ ( M e. ZZ /\ M <_ L ) ) -> N e. RR )
18 zre
 |-  ( L e. ZZ -> L e. RR )
19 18 adantr
 |-  ( ( L e. ZZ /\ N e. ZZ ) -> L e. RR )
20 19 adantr
 |-  ( ( ( L e. ZZ /\ N e. ZZ ) /\ ( M e. ZZ /\ M <_ L ) ) -> L e. RR )
21 17 20 subge0d
 |-  ( ( ( L e. ZZ /\ N e. ZZ ) /\ ( M e. ZZ /\ M <_ L ) ) -> ( 0 <_ ( N - L ) <-> L <_ N ) )
22 21 exbiri
 |-  ( ( L e. ZZ /\ N e. ZZ ) -> ( ( M e. ZZ /\ M <_ L ) -> ( L <_ N -> 0 <_ ( N - L ) ) ) )
23 22 com23
 |-  ( ( L e. ZZ /\ N e. ZZ ) -> ( L <_ N -> ( ( M e. ZZ /\ M <_ L ) -> 0 <_ ( N - L ) ) ) )
24 23 3impia
 |-  ( ( L e. ZZ /\ N e. ZZ /\ L <_ N ) -> ( ( M e. ZZ /\ M <_ L ) -> 0 <_ ( N - L ) ) )
25 24 impcom
 |-  ( ( ( M e. ZZ /\ M <_ L ) /\ ( L e. ZZ /\ N e. ZZ /\ L <_ N ) ) -> 0 <_ ( N - L ) )
26 zre
 |-  ( M e. ZZ -> M e. RR )
27 26 adantr
 |-  ( ( M e. ZZ /\ M <_ L ) -> M e. RR )
28 27 adantr
 |-  ( ( ( M e. ZZ /\ M <_ L ) /\ ( L e. ZZ /\ N e. ZZ /\ L <_ N ) ) -> M e. RR )
29 resubcl
 |-  ( ( N e. RR /\ L e. RR ) -> ( N - L ) e. RR )
30 15 18 29 syl2anr
 |-  ( ( L e. ZZ /\ N e. ZZ ) -> ( N - L ) e. RR )
31 30 3adant3
 |-  ( ( L e. ZZ /\ N e. ZZ /\ L <_ N ) -> ( N - L ) e. RR )
32 31 adantl
 |-  ( ( ( M e. ZZ /\ M <_ L ) /\ ( L e. ZZ /\ N e. ZZ /\ L <_ N ) ) -> ( N - L ) e. RR )
33 28 32 addge02d
 |-  ( ( ( M e. ZZ /\ M <_ L ) /\ ( L e. ZZ /\ N e. ZZ /\ L <_ N ) ) -> ( 0 <_ ( N - L ) <-> M <_ ( ( N - L ) + M ) ) )
34 25 33 mpbid
 |-  ( ( ( M e. ZZ /\ M <_ L ) /\ ( L e. ZZ /\ N e. ZZ /\ L <_ N ) ) -> M <_ ( ( N - L ) + M ) )
35 zcn
 |-  ( N e. ZZ -> N e. CC )
36 35 3ad2ant2
 |-  ( ( L e. ZZ /\ N e. ZZ /\ L <_ N ) -> N e. CC )
37 36 adantl
 |-  ( ( ( M e. ZZ /\ M <_ L ) /\ ( L e. ZZ /\ N e. ZZ /\ L <_ N ) ) -> N e. CC )
38 zcn
 |-  ( L e. ZZ -> L e. CC )
39 38 3ad2ant1
 |-  ( ( L e. ZZ /\ N e. ZZ /\ L <_ N ) -> L e. CC )
40 39 adantl
 |-  ( ( ( M e. ZZ /\ M <_ L ) /\ ( L e. ZZ /\ N e. ZZ /\ L <_ N ) ) -> L e. CC )
41 zcn
 |-  ( M e. ZZ -> M e. CC )
42 41 adantr
 |-  ( ( M e. ZZ /\ M <_ L ) -> M e. CC )
43 42 adantr
 |-  ( ( ( M e. ZZ /\ M <_ L ) /\ ( L e. ZZ /\ N e. ZZ /\ L <_ N ) ) -> M e. CC )
44 37 40 43 subsubd
 |-  ( ( ( M e. ZZ /\ M <_ L ) /\ ( L e. ZZ /\ N e. ZZ /\ L <_ N ) ) -> ( N - ( L - M ) ) = ( ( N - L ) + M ) )
45 34 44 breqtrrd
 |-  ( ( ( M e. ZZ /\ M <_ L ) /\ ( L e. ZZ /\ N e. ZZ /\ L <_ N ) ) -> M <_ ( N - ( L - M ) ) )
46 18 3ad2ant1
 |-  ( ( L e. ZZ /\ N e. ZZ /\ L <_ N ) -> L e. RR )
47 subge0
 |-  ( ( L e. RR /\ M e. RR ) -> ( 0 <_ ( L - M ) <-> M <_ L ) )
48 46 26 47 syl2anr
 |-  ( ( M e. ZZ /\ ( L e. ZZ /\ N e. ZZ /\ L <_ N ) ) -> ( 0 <_ ( L - M ) <-> M <_ L ) )
49 48 exbiri
 |-  ( M e. ZZ -> ( ( L e. ZZ /\ N e. ZZ /\ L <_ N ) -> ( M <_ L -> 0 <_ ( L - M ) ) ) )
50 49 com23
 |-  ( M e. ZZ -> ( M <_ L -> ( ( L e. ZZ /\ N e. ZZ /\ L <_ N ) -> 0 <_ ( L - M ) ) ) )
51 50 imp31
 |-  ( ( ( M e. ZZ /\ M <_ L ) /\ ( L e. ZZ /\ N e. ZZ /\ L <_ N ) ) -> 0 <_ ( L - M ) )
52 15 3ad2ant2
 |-  ( ( L e. ZZ /\ N e. ZZ /\ L <_ N ) -> N e. RR )
53 52 adantl
 |-  ( ( ( M e. ZZ /\ M <_ L ) /\ ( L e. ZZ /\ N e. ZZ /\ L <_ N ) ) -> N e. RR )
54 resubcl
 |-  ( ( L e. RR /\ M e. RR ) -> ( L - M ) e. RR )
55 46 27 54 syl2anr
 |-  ( ( ( M e. ZZ /\ M <_ L ) /\ ( L e. ZZ /\ N e. ZZ /\ L <_ N ) ) -> ( L - M ) e. RR )
56 53 55 subge02d
 |-  ( ( ( M e. ZZ /\ M <_ L ) /\ ( L e. ZZ /\ N e. ZZ /\ L <_ N ) ) -> ( 0 <_ ( L - M ) <-> ( N - ( L - M ) ) <_ N ) )
57 51 56 mpbid
 |-  ( ( ( M e. ZZ /\ M <_ L ) /\ ( L e. ZZ /\ N e. ZZ /\ L <_ N ) ) -> ( N - ( L - M ) ) <_ N )
58 45 57 jca
 |-  ( ( ( M e. ZZ /\ M <_ L ) /\ ( L e. ZZ /\ N e. ZZ /\ L <_ N ) ) -> ( M <_ ( N - ( L - M ) ) /\ ( N - ( L - M ) ) <_ N ) )
59 elfz2
 |-  ( ( N - ( L - M ) ) e. ( M ... N ) <-> ( ( M e. ZZ /\ N e. ZZ /\ ( N - ( L - M ) ) e. ZZ ) /\ ( M <_ ( N - ( L - M ) ) /\ ( N - ( L - M ) ) <_ N ) ) )
60 14 58 59 sylanbrc
 |-  ( ( ( M e. ZZ /\ M <_ L ) /\ ( L e. ZZ /\ N e. ZZ /\ L <_ N ) ) -> ( N - ( L - M ) ) e. ( M ... N ) )
61 60 ex
 |-  ( ( M e. ZZ /\ M <_ L ) -> ( ( L e. ZZ /\ N e. ZZ /\ L <_ N ) -> ( N - ( L - M ) ) e. ( M ... N ) ) )
62 61 3adant2
 |-  ( ( M e. ZZ /\ L e. ZZ /\ M <_ L ) -> ( ( L e. ZZ /\ N e. ZZ /\ L <_ N ) -> ( N - ( L - M ) ) e. ( M ... N ) ) )
63 2 62 syl5bi
 |-  ( ( M e. ZZ /\ L e. ZZ /\ M <_ L ) -> ( N e. ( ZZ>= ` L ) -> ( N - ( L - M ) ) e. ( M ... N ) ) )
64 1 63 sylbi
 |-  ( L e. ( ZZ>= ` M ) -> ( N e. ( ZZ>= ` L ) -> ( N - ( L - M ) ) e. ( M ... N ) ) )
65 64 imp
 |-  ( ( L e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` L ) ) -> ( N - ( L - M ) ) e. ( M ... N ) )