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	biimtrid	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) → ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∈ ( 𝑀 ... 𝑁 ) ) )
64	1 63	sylbi	⊢ ( 𝐿 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) → ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∈ ( 𝑀 ... 𝑁 ) ) )
65	64	imp	⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) ) → ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∈ ( 𝑀 ... 𝑁 ) )