Description: Membership of an increased integer in a correspondingly extended half-open range of integers. (Contributed by AV, 30-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | elincfzoext | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzole1 | |
|
2 | elfzoelz | |
|
3 | 2 | zred | |
4 | 3 | adantr | |
5 | nn0addge1 | |
|
6 | 4 5 | sylan | |
7 | elfzoel1 | |
|
8 | 7 | zred | |
9 | 8 | adantr | |
10 | 3 | adantr | |
11 | nn0re | |
|
12 | 11 | adantl | |
13 | 10 12 | readdcld | |
14 | letr | |
|
15 | 9 10 13 14 | syl3anc | |
16 | 15 | exp4b | |
17 | 16 | com23 | |
18 | 17 | imp31 | |
19 | 6 18 | mpd | |
20 | 19 | exp31 | |
21 | 1 20 | mpd | |
22 | 21 | imp | |
23 | elfzoel2 | |
|
24 | 23 | zred | |
25 | 24 | adantr | |
26 | elfzolt2 | |
|
27 | 26 | adantr | |
28 | 10 25 12 27 | ltadd1dd | |
29 | 2 | adantr | |
30 | nn0z | |
|
31 | 30 | adantl | |
32 | 29 31 | zaddcld | |
33 | 7 | adantr | |
34 | 23 | adantr | |
35 | 34 31 | zaddcld | |
36 | elfzo | |
|
37 | 32 33 35 36 | syl3anc | |
38 | 22 28 37 | mpbir2and | |