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