Step |
Hyp |
Ref |
Expression |
1 |
|
elfzoextl |
|- ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> Z e. ( M ..^ ( I + N ) ) ) |
2 |
|
elfzoel2 |
|- ( Z e. ( M ..^ N ) -> N e. ZZ ) |
3 |
2
|
zcnd |
|- ( Z e. ( M ..^ N ) -> N e. CC ) |
4 |
3
|
adantr |
|- ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> N e. CC ) |
5 |
|
nn0cn |
|- ( I e. NN0 -> I e. CC ) |
6 |
5
|
adantl |
|- ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> I e. CC ) |
7 |
4 6
|
addcomd |
|- ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> ( N + I ) = ( I + N ) ) |
8 |
7
|
oveq2d |
|- ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> ( M ..^ ( N + I ) ) = ( M ..^ ( I + N ) ) ) |
9 |
1 8
|
eleqtrrd |
|- ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> Z e. ( M ..^ ( N + I ) ) ) |