---

Step * 2 of Lemma poly-zero-implies


1. n : ℕ
2. p : polyform(n - 1) List
3. ↑null(p)
4. u : ℤ
5. v : ℤ List
6. (||v|| + 1) = n ∈ ℤ
7. ¬(n = 0 ∈ ℤ)
8. ¬(n = 0 ∈ ℤ)
9. 0 ≤ ||v||
⊢ Σ(v@p[i] * u^||p|| - 1 - i | i < ||p||) = 0 ∈ ℤ
BY
{ (DVar `p' THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  p  :  polyform(n  -  1)  List
3.  \muparrow{}null(p)
4.  u  :  \mBbbZ{}
5.  v  :  \mBbbZ{}  List
6.  (||v||  +  1)  =  n
7.  \mneg{}(n  =  0)
8.  \mneg{}(n  =  0)
9.  0  \mleq{}  ||v||
\mvdash{}  \mSigma{}(v@p[i]  *  u\^{}||p||  -  1  -  i  |  i  <  ||p||)  =  0


By

---

Latex:
(DVar  `p'  THEN  All  Reduce  THEN  Auto)

---

Home Index