Metamath Proof Explorer

Theorem elfzoext

Description: Membership of an integer in an extended open range of integers. (Contributed by AV, 30-Apr-2020)

Ref Expression
Assertion elfzoext 
|- ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> Z e. ( M ..^ ( N + I ) ) )

Proof

Step Hyp Ref Expression
1 elfzoel2 
 |-  ( Z e. ( M ..^ N ) -> N e. ZZ )
2 zcn 
 |-  ( N e. ZZ -> N e. CC )
3 nn0cn 
 |-  ( I e. NN0 -> I e. CC )
4 addcom 
 |-  ( ( N e. CC /\ I e. CC ) -> ( N + I ) = ( I + N ) )
5 2 3 4 syl2an 
 |-  ( ( N e. ZZ /\ I e. NN0 ) -> ( N + I ) = ( I + N ) )
6 nn0pzuz 
 |-  ( ( I e. NN0 /\ N e. ZZ ) -> ( I + N ) e. ( ZZ>= ` N ) )
7 6 ancoms 
 |-  ( ( N e. ZZ /\ I e. NN0 ) -> ( I + N ) e. ( ZZ>= ` N ) )
8 5 7 eqeltrd 
 |-  ( ( N e. ZZ /\ I e. NN0 ) -> ( N + I ) e. ( ZZ>= ` N ) )
9 fzoss2 
 |-  ( ( N + I ) e. ( ZZ>= ` N ) -> ( M ..^ N ) C_ ( M ..^ ( N + I ) ) )
10 8 9 syl 
 |-  ( ( N e. ZZ /\ I e. NN0 ) -> ( M ..^ N ) C_ ( M ..^ ( N + I ) ) )
11 10 sselda 
 |-  ( ( ( N e. ZZ /\ I e. NN0 ) /\ Z e. ( M ..^ N ) ) -> Z e. ( M ..^ ( N + I ) ) )
12 11 expcom 
 |-  ( Z e. ( M ..^ N ) -> ( ( N e. ZZ /\ I e. NN0 ) -> Z e. ( M ..^ ( N + I ) ) ) )
13 1 12 mpand 
 |-  ( Z e. ( M ..^ N ) -> ( I e. NN0 -> Z e. ( M ..^ ( N + I ) ) ) )
14 13 imp 
 |-  ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> Z e. ( M ..^ ( N + I ) ) )