Theorem 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	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) → ( 𝑁 − 𝐴 ) ∈ ( 0 ..^ ( 𝑁 − 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) )
2	1	adantl	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) )
3		simpl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℤ )
4	3	adantr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 𝐴 ∈ ℤ )
5		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝑁 ∈ ℤ )
6	5	ad2antrr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
7		simprr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → 𝐵 ∈ ℤ )
8	6 7	zsubcld	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( 𝑁 − 𝐵 ) ∈ ℤ )
9	8	ancoms	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → ( 𝑁 − 𝐵 ) ∈ ℤ )
10	4 9	zaddcld	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → ( 𝐴 + ( 𝑁 − 𝐵 ) ) ∈ ℤ )
11		zre	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ )
12		zre	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
13		posdif	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 < 𝐴 ↔ 0 < ( 𝐴 − 𝐵 ) ) )
14	13	biimpd	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 < 𝐴 → 0 < ( 𝐴 − 𝐵 ) ) )
15	11 12 14	syl2anr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 < 𝐴 → 0 < ( 𝐴 − 𝐵 ) ) )
16	15	adantld	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) → 0 < ( 𝐴 − 𝐵 ) ) )
17	16	imp	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 0 < ( 𝐴 − 𝐵 ) )
18		resubcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 − 𝐵 ) ∈ ℝ )
19	12 11 18	syl2an	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∈ ℝ )
20	19	adantr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → ( 𝐴 − 𝐵 ) ∈ ℝ )
21		eluzelre	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝑁 ∈ ℝ )
22	21	ad2antrl	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 𝑁 ∈ ℝ )
23	20 22	ltaddposd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → ( 0 < ( 𝐴 − 𝐵 ) ↔ 𝑁 < ( 𝑁 + ( 𝐴 − 𝐵 ) ) ) )
24	17 23	mpbid	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 𝑁 < ( 𝑁 + ( 𝐴 − 𝐵 ) ) )
25		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
26	25	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 𝐴 ∈ ℂ )
27		eluzelcn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝑁 ∈ ℂ )
28	27	ad2antrl	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 𝑁 ∈ ℂ )
29		zcn	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
30	29	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℂ )
31	30	adantr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 𝐵 ∈ ℂ )
32		addsub12	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + ( 𝑁 − 𝐵 ) ) = ( 𝑁 + ( 𝐴 − 𝐵 ) ) )
33	32	breq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑁 < ( 𝐴 + ( 𝑁 − 𝐵 ) ) ↔ 𝑁 < ( 𝑁 + ( 𝐴 − 𝐵 ) ) ) )
34	26 28 31 33	syl3anc	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → ( 𝑁 < ( 𝐴 + ( 𝑁 − 𝐵 ) ) ↔ 𝑁 < ( 𝑁 + ( 𝐴 − 𝐵 ) ) ) )
35	24 34	mpbird	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 𝑁 < ( 𝐴 + ( 𝑁 − 𝐵 ) ) )
36		elfzo2	⊢ ( 𝑁 ∈ ( 𝐴 ..^ ( 𝐴 + ( 𝑁 − 𝐵 ) ) ) ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ ( 𝐴 + ( 𝑁 − 𝐵 ) ) ∈ ℤ ∧ 𝑁 < ( 𝐴 + ( 𝑁 − 𝐵 ) ) ) )
37	2 10 35 36	syl3anbrc	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 𝑁 ∈ ( 𝐴 ..^ ( 𝐴 + ( 𝑁 − 𝐵 ) ) ) )
38		fzosubel3	⊢ ( ( 𝑁 ∈ ( 𝐴 ..^ ( 𝐴 + ( 𝑁 − 𝐵 ) ) ) ∧ ( 𝑁 − 𝐵 ) ∈ ℤ ) → ( 𝑁 − 𝐴 ) ∈ ( 0 ..^ ( 𝑁 − 𝐵 ) ) )
39	37 9 38	syl2anc	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → ( 𝑁 − 𝐴 ) ∈ ( 0 ..^ ( 𝑁 − 𝐵 ) ) )
40	39	ex	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) → ( 𝑁 − 𝐴 ) ∈ ( 0 ..^ ( 𝑁 − 𝐵 ) ) ) )