Metamath Proof Explorer


Theorem elincfzoext

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 ZM..^NI0Z+IM..^N+I

Proof

Step Hyp Ref Expression
1 elfzole1 ZM..^NMZ
2 elfzoelz ZM..^NZ
3 2 zred ZM..^NZ
4 3 adantr ZM..^NMZZ
5 nn0addge1 ZI0ZZ+I
6 4 5 sylan ZM..^NMZI0ZZ+I
7 elfzoel1 ZM..^NM
8 7 zred ZM..^NM
9 8 adantr ZM..^NI0M
10 3 adantr ZM..^NI0Z
11 nn0re I0I
12 11 adantl ZM..^NI0I
13 10 12 readdcld ZM..^NI0Z+I
14 letr MZZ+IMZZZ+IMZ+I
15 9 10 13 14 syl3anc ZM..^NI0MZZZ+IMZ+I
16 15 exp4b ZM..^NI0MZZZ+IMZ+I
17 16 com23 ZM..^NMZI0ZZ+IMZ+I
18 17 imp31 ZM..^NMZI0ZZ+IMZ+I
19 6 18 mpd ZM..^NMZI0MZ+I
20 19 exp31 ZM..^NMZI0MZ+I
21 1 20 mpd ZM..^NI0MZ+I
22 21 imp ZM..^NI0MZ+I
23 elfzoel2 ZM..^NN
24 23 zred ZM..^NN
25 24 adantr ZM..^NI0N
26 elfzolt2 ZM..^NZ<N
27 26 adantr ZM..^NI0Z<N
28 10 25 12 27 ltadd1dd ZM..^NI0Z+I<N+I
29 2 adantr ZM..^NI0Z
30 nn0z I0I
31 30 adantl ZM..^NI0I
32 29 31 zaddcld ZM..^NI0Z+I
33 7 adantr ZM..^NI0M
34 23 adantr ZM..^NI0N
35 34 31 zaddcld ZM..^NI0N+I
36 elfzo Z+IMN+IZ+IM..^N+IMZ+IZ+I<N+I
37 32 33 35 36 syl3anc ZM..^NI0Z+IM..^N+IMZ+IZ+I<N+I
38 22 28 37 mpbir2and ZM..^NI0Z+IM..^N+I