Metamath Proof Explorer

Theorem zpnn0elfzo1

Description: Membership of an integer increased by a nonnegative integer in a half- open integer range. (Contributed by Alexander van der Vekens, 22-Sep-2018)

Ref Expression
Assertion zpnn0elfzo1 
|- ( ( Z e. ZZ /\ N e. NN0 ) -> ( Z + N ) e. ( Z ..^ ( Z + ( N + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 zpnn0elfzo 
 |-  ( ( Z e. ZZ /\ N e. NN0 ) -> ( Z + N ) e. ( Z ..^ ( ( Z + N ) + 1 ) ) )
2 zcn 
 |-  ( Z e. ZZ -> Z e. CC )
3 2 adantr 
 |-  ( ( Z e. ZZ /\ N e. NN0 ) -> Z e. CC )
4 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
5 4 adantl 
 |-  ( ( Z e. ZZ /\ N e. NN0 ) -> N e. CC )
6 1cnd 
 |-  ( ( Z e. ZZ /\ N e. NN0 ) -> 1 e. CC )
7 3 5 6 addassd 
 |-  ( ( Z e. ZZ /\ N e. NN0 ) -> ( ( Z + N ) + 1 ) = ( Z + ( N + 1 ) ) )
8 7 oveq2d 
 |-  ( ( Z e. ZZ /\ N e. NN0 ) -> ( Z ..^ ( ( Z + N ) + 1 ) ) = ( Z ..^ ( Z + ( N + 1 ) ) ) )
9 1 8 eleqtrd 
 |-  ( ( Z e. ZZ /\ N e. NN0 ) -> ( Z + N ) e. ( Z ..^ ( Z + ( N + 1 ) ) ) )