# 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 ${⊢}\left({L}\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {L}}\right)\to {N}-\left({L}-{M}\right)\in \left({M}\dots {N}\right)$

### Proof

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