Metamath Proof Explorer


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