# Metamath Proof Explorer

## Theorem plypow

Description: A power is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Assertion plypow ${⊢}\left({S}\subseteq ℂ\wedge 1\in {S}\wedge {N}\in {ℕ}_{0}\right)\to \left({z}\in ℂ⟼{{z}}^{{N}}\right)\in \mathrm{Poly}\left({S}\right)$

### Proof

Step Hyp Ref Expression
1 id ${⊢}{z}\in ℂ\to {z}\in ℂ$
2 simp3 ${⊢}\left({S}\subseteq ℂ\wedge 1\in {S}\wedge {N}\in {ℕ}_{0}\right)\to {N}\in {ℕ}_{0}$
3 expcl ${⊢}\left({z}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to {{z}}^{{N}}\in ℂ$
4 1 2 3 syl2anr ${⊢}\left(\left({S}\subseteq ℂ\wedge 1\in {S}\wedge {N}\in {ℕ}_{0}\right)\wedge {z}\in ℂ\right)\to {{z}}^{{N}}\in ℂ$
5 4 mulid2d ${⊢}\left(\left({S}\subseteq ℂ\wedge 1\in {S}\wedge {N}\in {ℕ}_{0}\right)\wedge {z}\in ℂ\right)\to 1{{z}}^{{N}}={{z}}^{{N}}$
6 5 mpteq2dva ${⊢}\left({S}\subseteq ℂ\wedge 1\in {S}\wedge {N}\in {ℕ}_{0}\right)\to \left({z}\in ℂ⟼1{{z}}^{{N}}\right)=\left({z}\in ℂ⟼{{z}}^{{N}}\right)$
7 eqid ${⊢}\left({z}\in ℂ⟼1{{z}}^{{N}}\right)=\left({z}\in ℂ⟼1{{z}}^{{N}}\right)$
8 7 ply1term ${⊢}\left({S}\subseteq ℂ\wedge 1\in {S}\wedge {N}\in {ℕ}_{0}\right)\to \left({z}\in ℂ⟼1{{z}}^{{N}}\right)\in \mathrm{Poly}\left({S}\right)$
9 6 8 eqeltrrd ${⊢}\left({S}\subseteq ℂ\wedge 1\in {S}\wedge {N}\in {ℕ}_{0}\right)\to \left({z}\in ℂ⟼{{z}}^{{N}}\right)\in \mathrm{Poly}\left({S}\right)$