---

Step * of Lemma nonzero-mul-polynom

∀[n:ℕ]. ∀[p,q:polynom(n)].
  (poly-zero(n;mul-polynom(n;p;q)) = ff) supposing (poly-zero(n;q) = ff and poly-zero(n;p) = ff)
BY
{ (CompleteInductionOnNat
   THEN (UnivCD THENA Auto)
   THEN RecUnfold `mul-polynom` 0⋅
   THEN (CaseNat 0 `n' THENL [Reduce 0; (InstHyp [⌜n - 1⌝] 2⋅ THENA Auto)])) }

1
1. n : ℕ
2. ∀n:ℕn
     ∀[p,q:polynom(n)].  (poly-zero(n;mul-polynom(n;p;q)) = ff) supposing (poly-zero(n;q) = ff and poly-zero(n;p) = ff)
3. p : polynom(n)
4. q : polynom(n)
5. poly-zero(n;p) = ff
6. poly-zero(n;q) = ff
7. n = 0 ∈ ℤ
⊢ poly-zero(0;p * q) = ff

2
1. n : ℕ
2. ∀n:ℕn
     ∀[p,q:polynom(n)].  (poly-zero(n;mul-polynom(n;p;q)) = ff) supposing (poly-zero(n;q) = ff and poly-zero(n;p) = ff)
3. p : polynom(n)
4. q : polynom(n)
5. poly-zero(n;p) = ff
6. poly-zero(n;q) = ff
7. ¬(n = 0 ∈ ℤ)
8. ∀[p,q:polynom(n - 1)].
     (poly-zero(n - 1;mul-polynom(n - 1;p;q)) = ff) supposing (poly-zero(n - 1;q) = ff and poly-zero(n - 1;p) = ff)
⊢ poly-zero(n;if n=0
                 then p * q
                 else eager-accum(z,a.add-polynom(n;tt;if null(z)
                      then []
                      else z @ [polyconst(n - 1;0)]
                      fi ;if poly-zero(n - 1;a) then [] else map(λx.mul-polynom(n - 1;a;x);q) fi );polyconst(n;0);p)) 
= ff

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[p,q:polynom(n)].
    (poly-zero(n;mul-polynom(n;p;q))  =  ff)  supposing  (poly-zero(n;q)  =  ff  and  poly-zero(n;p)  =  ff)


By

---

Latex:
(CompleteInductionOnNat
  THEN  (UnivCD  THENA  Auto)
  THEN  RecUnfold  `mul-polynom`  0\mcdot{}
  THEN  (CaseNat  0  `n'  THENL  [Reduce  0;  (InstHyp  [\mkleeneopen{}n  -  1\mkleeneclose{}]  2\mcdot{}  THENA  Auto)]))

---

Home Index