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 ABNAB<ANA0..^NB

Proof

Step Hyp Ref Expression
1 simpl NAB<ANA
2 1 adantl ABNAB<ANA
3 simpl ABA
4 3 adantr ABNAB<AA
5 eluzelz NAN
6 5 ad2antrr NAB<AABN
7 simprr NAB<AABB
8 6 7 zsubcld NAB<AABNB
9 8 ancoms ABNAB<ANB
10 4 9 zaddcld ABNAB<AA+N-B
11 zre BB
12 zre AA
13 posdif BAB<A0<AB
14 13 biimpd BAB<A0<AB
15 11 12 14 syl2anr ABB<A0<AB
16 15 adantld ABNAB<A0<AB
17 16 imp ABNAB<A0<AB
18 resubcl ABAB
19 12 11 18 syl2an ABAB
20 19 adantr ABNAB<AAB
21 eluzelre NAN
22 21 ad2antrl ABNAB<AN
23 20 22 ltaddposd ABNAB<A0<ABN<N+A-B
24 17 23 mpbid ABNAB<AN<N+A-B
25 zcn AA
26 25 ad2antrr ABNAB<AA
27 eluzelcn NAN
28 27 ad2antrl ABNAB<AN
29 zcn BB
30 29 adantl ABB
31 30 adantr ABNAB<AB
32 addsub12 ANBA+N-B=N+A-B
33 32 breq2d ANBN<A+N-BN<N+A-B
34 26 28 31 33 syl3anc ABNAB<AN<A+N-BN<N+A-B
35 24 34 mpbird ABNAB<AN<A+N-B
36 elfzo2 NA..^A+N-BNAA+N-BN<A+N-B
37 2 10 35 36 syl3anbrc ABNAB<ANA..^A+N-B
38 fzosubel3 NA..^A+N-BNBNA0..^NB
39 37 9 38 syl2anc ABNAB<ANA0..^NB
40 39 ex ABNAB<ANA0..^NB