---

Step * of Lemma power-sum_functionality_wrt_eqmod

∀m:ℤ. ∀n:ℕ. ∀x,y:ℤ. ∀a,b:ℕn ⟶ ℤ.
  ((x ≡ y mod m) ⇒ (∀i:ℕn. (a[i] ≡ b[i] mod m)) ⇒ (Σi<n.a[i]*x^i ≡ Σi<n.b[i]*y^i mod m))
BY
{ (Auto
   THEN Unfold `power-sum` 0
   THEN (RWO "sum-as-primrec" 0 THENA Auto)
   THEN Repeat (MoveToConcl (-1))
   THEN (PrimrecInductionOn `n' THENA Auto)
   THEN Try ((RelRST THENA Auto))
   THEN Try (CompleteAuto ⋅)
   THEN (BLemma `add_functionality_wrt_eqmod` THENA Auto)
   THEN Try ((BackThruSomeHyp THEN Auto)⋅)
   THEN ((RWO "-1 -2" 0 THENM RelRST) THENA Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}m:\mBbbZ{}.  \mforall{}n:\mBbbN{}.  \mforall{}x,y:\mBbbZ{}.  \mforall{}a,b:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}.
    ((x  \mequiv{}  y  mod  m)  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n.  (a[i]  \mequiv{}  b[i]  mod  m))  {}\mRightarrow{}  (\mSigma{}i<n.a[i]*x\^{}i  \mequiv{}  \mSigma{}i<n.b[i]*y\^{}i  mod  m))


By

---

Latex:
(Auto
  THEN  Unfold  `power-sum`  0
  THEN  (RWO  "sum-as-primrec"  0  THENA  Auto)
  THEN  Repeat  (MoveToConcl  (-1))
  THEN  (PrimrecInductionOn  `n'  THENA  Auto)
  THEN  Try  ((RelRST  THENA  Auto))
  THEN  Try  (CompleteAuto  \mcdot{})
  THEN  (BLemma  `add\_functionality\_wrt\_eqmod`  THENA  Auto)
  THEN  Try  ((BackThruSomeHyp  THEN  Auto)\mcdot{})
  THEN  ((RWO  "-1  -2"  0  THENM  RelRST)  THENA  Auto)\mcdot{})

---

Home Index