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 \in ℤ_{\geq M} \land N \in ℤ_{\geq L}) \to N - (L - M) \in (M \dots N)$

Proof

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

Metamath Proof Explorer

Theorem uzsubsubfz

Proof