Database
BASIC REAL AND COMPLEX FUNCTIONS
Polynomials
Elementary properties of complex polynomials
plypow
Next ⟩
plyconst
Metamath Proof Explorer
Ascii
Unicode
Theorem
plypow
Description:
A power is a polynomial.
(Contributed by
Mario Carneiro
, 17-Jul-2014)
Ref
Expression
Assertion
plypow
⊢
S
⊆
ℂ
∧
1
∈
S
∧
N
∈
ℕ
0
→
z
∈
ℂ
⟼
z
N
∈
Poly
⁡
S
Proof
Step
Hyp
Ref
Expression
1
id
⊢
z
∈
ℂ
→
z
∈
ℂ
2
simp3
⊢
S
⊆
ℂ
∧
1
∈
S
∧
N
∈
ℕ
0
→
N
∈
ℕ
0
3
expcl
⊢
z
∈
ℂ
∧
N
∈
ℕ
0
→
z
N
∈
ℂ
4
1
2
3
syl2anr
⊢
S
⊆
ℂ
∧
1
∈
S
∧
N
∈
ℕ
0
∧
z
∈
ℂ
→
z
N
∈
ℂ
5
4
mulid2d
⊢
S
⊆
ℂ
∧
1
∈
S
∧
N
∈
ℕ
0
∧
z
∈
ℂ
→
1
⁢
z
N
=
z
N
6
5
mpteq2dva
⊢
S
⊆
ℂ
∧
1
∈
S
∧
N
∈
ℕ
0
→
z
∈
ℂ
⟼
1
⁢
z
N
=
z
∈
ℂ
⟼
z
N
7
eqid
⊢
z
∈
ℂ
⟼
1
⁢
z
N
=
z
∈
ℂ
⟼
1
⁢
z
N
8
7
ply1term
⊢
S
⊆
ℂ
∧
1
∈
S
∧
N
∈
ℕ
0
→
z
∈
ℂ
⟼
1
⁢
z
N
∈
Poly
⁡
S
9
6
8
eqeltrrd
⊢
S
⊆
ℂ
∧
1
∈
S
∧
N
∈
ℕ
0
→
z
∈
ℂ
⟼
z
N
∈
Poly
⁡
S