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 
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( N e. ( ZZ>= ` A ) /\ B < A ) -> ( N - A ) e. ( 0 ..^ ( N - B ) ) ) )

Proof

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