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 ( ( 𝐿 ∈ ( ℤ𝑀 ) ∧ 𝑁 ∈ ( ℤ𝐿 ) ) → ( 𝑁 − ( 𝐿𝑀 ) ) ∈ ( 𝑀 ... 𝑁 ) )

Proof

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