Step |
Hyp |
Ref |
Expression |
1 |
|
id |
|- ( z e. CC -> z e. CC ) |
2 |
|
simp3 |
|- ( ( S C_ CC /\ 1 e. S /\ N e. NN0 ) -> N e. NN0 ) |
3 |
|
expcl |
|- ( ( z e. CC /\ N e. NN0 ) -> ( z ^ N ) e. CC ) |
4 |
1 2 3
|
syl2anr |
|- ( ( ( S C_ CC /\ 1 e. S /\ N e. NN0 ) /\ z e. CC ) -> ( z ^ N ) e. CC ) |
5 |
4
|
mulid2d |
|- ( ( ( S C_ CC /\ 1 e. S /\ N e. NN0 ) /\ z e. CC ) -> ( 1 x. ( z ^ N ) ) = ( z ^ N ) ) |
6 |
5
|
mpteq2dva |
|- ( ( S C_ CC /\ 1 e. S /\ N e. NN0 ) -> ( z e. CC |-> ( 1 x. ( z ^ N ) ) ) = ( z e. CC |-> ( z ^ N ) ) ) |
7 |
|
eqid |
|- ( z e. CC |-> ( 1 x. ( z ^ N ) ) ) = ( z e. CC |-> ( 1 x. ( z ^ N ) ) ) |
8 |
7
|
ply1term |
|- ( ( S C_ CC /\ 1 e. S /\ N e. NN0 ) -> ( z e. CC |-> ( 1 x. ( z ^ N ) ) ) e. ( Poly ` S ) ) |
9 |
6 8
|
eqeltrrd |
|- ( ( S C_ CC /\ 1 e. S /\ N e. NN0 ) -> ( z e. CC |-> ( z ^ N ) ) e. ( Poly ` S ) ) |