eluzgtdifelfzo

Description: Membership of the difference of integers in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 17-Sep-2018)

		Ref	Expression
	Assertion	eluzgtdifelfzo	$⊢ (A \in ℤ \land B \in ℤ) \to ((N \in ℤ_{\geq A} \land B < A) \to N - A \in (0 ..^N - B))$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (N \in ℤ_{\geq A} \land B < A) \to N \in ℤ_{\geq A}$
2	1	adantl	$⊢ ((A \in ℤ \land B \in ℤ) \land (N \in ℤ_{\geq A} \land B < A)) \to N \in ℤ_{\geq A}$
3		simpl	$⊢ (A \in ℤ \land B \in ℤ) \to A \in ℤ$
4	3	adantr	$⊢ ((A \in ℤ \land B \in ℤ) \land (N \in ℤ_{\geq A} \land B < A)) \to A \in ℤ$
5		eluzelz	$⊢ N \in ℤ_{\geq A} \to N \in ℤ$
6	5	ad2antrr	$⊢ ((N \in ℤ_{\geq A} \land B < A) \land (A \in ℤ \land B \in ℤ)) \to N \in ℤ$
7		simprr	$⊢ ((N \in ℤ_{\geq A} \land B < A) \land (A \in ℤ \land B \in ℤ)) \to B \in ℤ$
8	6 7	zsubcld	$⊢ ((N \in ℤ_{\geq A} \land B < A) \land (A \in ℤ \land B \in ℤ)) \to N - B \in ℤ$
9	8	ancoms	$⊢ ((A \in ℤ \land B \in ℤ) \land (N \in ℤ_{\geq A} \land B < A)) \to N - B \in ℤ$
10	4 9	zaddcld	$⊢ ((A \in ℤ \land B \in ℤ) \land (N \in ℤ_{\geq A} \land B < A)) \to A + N - B \in ℤ$
11		zre	$⊢ B \in ℤ \to B \in ℝ$
12		zre	$⊢ A \in ℤ \to A \in ℝ$
13		posdif	$⊢ (B \in ℝ \land A \in ℝ) \to (B < A \leftrightarrow 0 < A - B)$
14	13	biimpd	$⊢ (B \in ℝ \land A \in ℝ) \to (B < A \to 0 < A - B)$
15	11 12 14	syl2anr	$⊢ (A \in ℤ \land B \in ℤ) \to (B < A \to 0 < A - B)$
16	15	adantld	$⊢ (A \in ℤ \land B \in ℤ) \to ((N \in ℤ_{\geq A} \land B < A) \to 0 < A - B)$
17	16	imp	$⊢ ((A \in ℤ \land B \in ℤ) \land (N \in ℤ_{\geq A} \land B < A)) \to 0 < A - B$
18		resubcl	$⊢ (A \in ℝ \land B \in ℝ) \to A - B \in ℝ$
19	12 11 18	syl2an	$⊢ (A \in ℤ \land B \in ℤ) \to A - B \in ℝ$
20	19	adantr	$⊢ ((A \in ℤ \land B \in ℤ) \land (N \in ℤ_{\geq A} \land B < A)) \to A - B \in ℝ$
21		eluzelre	$⊢ N \in ℤ_{\geq A} \to N \in ℝ$
22	21	ad2antrl	$⊢ ((A \in ℤ \land B \in ℤ) \land (N \in ℤ_{\geq A} \land B < A)) \to N \in ℝ$
23	20 22	ltaddposd	$⊢ ((A \in ℤ \land B \in ℤ) \land (N \in ℤ_{\geq A} \land B < A)) \to (0 < A - B \leftrightarrow N < N + A - B)$
24	17 23	mpbid	$⊢ ((A \in ℤ \land B \in ℤ) \land (N \in ℤ_{\geq A} \land B < A)) \to N < N + A - B$
25		zcn	$⊢ A \in ℤ \to A \in ℂ$
26	25	ad2antrr	$⊢ ((A \in ℤ \land B \in ℤ) \land (N \in ℤ_{\geq A} \land B < A)) \to A \in ℂ$
27		eluzelcn	$⊢ N \in ℤ_{\geq A} \to N \in ℂ$
28	27	ad2antrl	$⊢ ((A \in ℤ \land B \in ℤ) \land (N \in ℤ_{\geq A} \land B < A)) \to N \in ℂ$
29		zcn	$⊢ B \in ℤ \to B \in ℂ$
30	29	adantl	$⊢ (A \in ℤ \land B \in ℤ) \to B \in ℂ$
31	30	adantr	$⊢ ((A \in ℤ \land B \in ℤ) \land (N \in ℤ_{\geq A} \land B < A)) \to B \in ℂ$
32		addsub12	$⊢ (A \in ℂ \land N \in ℂ \land B \in ℂ) \to A + N - B = N + A - B$
33	32	breq2d	$⊢ (A \in ℂ \land N \in ℂ \land B \in ℂ) \to (N < A + N - B \leftrightarrow N < N + A - B)$
34	26 28 31 33	syl3anc	$⊢ ((A \in ℤ \land B \in ℤ) \land (N \in ℤ_{\geq A} \land B < A)) \to (N < A + N - B \leftrightarrow N < N + A - B)$
35	24 34	mpbird	$⊢ ((A \in ℤ \land B \in ℤ) \land (N \in ℤ_{\geq A} \land B < A)) \to N < A + N - B$
36		elfzo2	$⊢ N \in (A ..^A + N - B) \leftrightarrow (N \in ℤ_{\geq A} \land A + N - B \in ℤ \land N < A + N - B)$
37	2 10 35 36	syl3anbrc	$⊢ ((A \in ℤ \land B \in ℤ) \land (N \in ℤ_{\geq A} \land B < A)) \to N \in (A ..^A + N - B)$
38		fzosubel3	$⊢ (N \in (A ..^A + N - B) \land N - B \in ℤ) \to N - A \in (0 ..^N - B)$
39	37 9 38	syl2anc	$⊢ ((A \in ℤ \land B \in ℤ) \land (N \in ℤ_{\geq A} \land B < A)) \to N - A \in (0 ..^N - B)$
40	39	ex	$⊢ (A \in ℤ \land B \in ℤ) \to ((N \in ℤ_{\geq A} \land B < A) \to N - A \in (0 ..^N - B))$

Metamath Proof Explorer

Theorem eluzgtdifelfzo

Proof