# Metamath Proof Explorer

## 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 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left(\left({N}\in {ℤ}_{\ge {A}}\wedge {B}<{A}\right)\to {N}-{A}\in \left(0..^{N}-{B}\right)\right)$

### Proof

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