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 
|- ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> ( Z + I ) e. ( M ..^ ( N + I ) ) )

Proof

Step Hyp Ref Expression
1 elfzole1 
 |-  ( Z e. ( M ..^ N ) -> M <_ Z )
2 elfzoelz 
 |-  ( Z e. ( M ..^ N ) -> Z e. ZZ )
3 2 zred 
 |-  ( Z e. ( M ..^ N ) -> Z e. RR )
4 3 adantr 
 |-  ( ( Z e. ( M ..^ N ) /\ M <_ Z ) -> Z e. RR )
5 nn0addge1 
 |-  ( ( Z e. RR /\ I e. NN0 ) -> Z <_ ( Z + I ) )
6 4 5 sylan 
 |-  ( ( ( Z e. ( M ..^ N ) /\ M <_ Z ) /\ I e. NN0 ) -> Z <_ ( Z + I ) )
7 elfzoel1 
 |-  ( Z e. ( M ..^ N ) -> M e. ZZ )
8 7 zred 
 |-  ( Z e. ( M ..^ N ) -> M e. RR )
9 8 adantr 
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> M e. RR )
10 3 adantr 
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> Z e. RR )
11 nn0re 
 |-  ( I e. NN0 -> I e. RR )
12 11 adantl 
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> I e. RR )
13 10 12 readdcld 
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> ( Z + I ) e. RR )
14 letr 
 |-  ( ( M e. RR /\ Z e. RR /\ ( Z + I ) e. RR ) -> ( ( M <_ Z /\ Z <_ ( Z + I ) ) -> M <_ ( Z + I ) ) )
15 9 10 13 14 syl3anc 
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> ( ( M <_ Z /\ Z <_ ( Z + I ) ) -> M <_ ( Z + I ) ) )
16 15 exp4b 
 |-  ( Z e. ( M ..^ N ) -> ( I e. NN0 -> ( M <_ Z -> ( Z <_ ( Z + I ) -> M <_ ( Z + I ) ) ) ) )
17 16 com23 
 |-  ( Z e. ( M ..^ N ) -> ( M <_ Z -> ( I e. NN0 -> ( Z <_ ( Z + I ) -> M <_ ( Z + I ) ) ) ) )
18 17 imp31 
 |-  ( ( ( Z e. ( M ..^ N ) /\ M <_ Z ) /\ I e. NN0 ) -> ( Z <_ ( Z + I ) -> M <_ ( Z + I ) ) )
19 6 18 mpd 
 |-  ( ( ( Z e. ( M ..^ N ) /\ M <_ Z ) /\ I e. NN0 ) -> M <_ ( Z + I ) )
20 19 exp31 
 |-  ( Z e. ( M ..^ N ) -> ( M <_ Z -> ( I e. NN0 -> M <_ ( Z + I ) ) ) )
21 1 20 mpd 
 |-  ( Z e. ( M ..^ N ) -> ( I e. NN0 -> M <_ ( Z + I ) ) )
22 21 imp 
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> M <_ ( Z + I ) )
23 elfzoel2 
 |-  ( Z e. ( M ..^ N ) -> N e. ZZ )
24 23 zred 
 |-  ( Z e. ( M ..^ N ) -> N e. RR )
25 24 adantr 
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> N e. RR )
26 elfzolt2 
 |-  ( Z e. ( M ..^ N ) -> Z < N )
27 26 adantr 
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> Z < N )
28 10 25 12 27 ltadd1dd 
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> ( Z + I ) < ( N + I ) )
29 2 adantr 
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> Z e. ZZ )
30 nn0z 
 |-  ( I e. NN0 -> I e. ZZ )
31 30 adantl 
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> I e. ZZ )
32 29 31 zaddcld 
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> ( Z + I ) e. ZZ )
33 7 adantr 
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> M e. ZZ )
34 23 adantr 
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> N e. ZZ )
35 34 31 zaddcld 
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> ( N + I ) e. ZZ )
36 elfzo 
 |-  ( ( ( Z + I ) e. ZZ /\ M e. ZZ /\ ( N + I ) e. ZZ ) -> ( ( Z + I ) e. ( M ..^ ( N + I ) ) <-> ( M <_ ( Z + I ) /\ ( Z + I ) < ( N + I ) ) ) )
37 32 33 35 36 syl3anc 
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> ( ( Z + I ) e. ( M ..^ ( N + I ) ) <-> ( M <_ ( Z + I ) /\ ( Z + I ) < ( N + I ) ) ) )
38 22 28 37 mpbir2and 
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> ( Z + I ) e. ( M ..^ ( N + I ) ) )