Metamath Proof Explorer


Theorem ply1term

Description: A one-term polynomial. (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Hypothesis ply1term.1 F = z A z N
Assertion ply1term S A S N 0 F Poly S

Proof

Step Hyp Ref Expression
1 ply1term.1 F = z A z N
2 ssel2 S A S A
3 1 ply1termlem A N 0 F = z k = 0 N if k = N A 0 z k
4 2 3 stoic3 S A S N 0 F = z k = 0 N if k = N A 0 z k
5 simp1 S A S N 0 S
6 0cnd S A S N 0 0
7 6 snssd S A S N 0 0
8 5 7 unssd S A S N 0 S 0
9 simp3 S A S N 0 N 0
10 simpl2 S A S N 0 k 0 N A S
11 elun1 A S A S 0
12 10 11 syl S A S N 0 k 0 N A S 0
13 ssun2 0 S 0
14 c0ex 0 V
15 14 snss 0 S 0 0 S 0
16 13 15 mpbir 0 S 0
17 ifcl A S 0 0 S 0 if k = N A 0 S 0
18 12 16 17 sylancl S A S N 0 k 0 N if k = N A 0 S 0
19 8 9 18 elplyd S A S N 0 z k = 0 N if k = N A 0 z k Poly S 0
20 4 19 eqeltrd S A S N 0 F Poly S 0
21 plyun0 Poly S 0 = Poly S
22 20 21 eleqtrdi S A S N 0 F Poly S