---

Step * 1 of Lemma rpoly-nth-deriv_functionality


1. d : ℕ
2. n : ℕ
3. ¬d < n
4. a : ℕd + 1 ⟶ ℝ
5. b : ℕd + 1 ⟶ ℝ
6. x1 : ℝ
7. x2 : ℝ
8. ∀i:ℕd + 1. ((a i) = (b i))
9. x1 = x2
10. poly-nth-deriv(n;a) ∈ ℕ(d - n) + 1 ⟶ ℝ
11. poly-nth-deriv(n;b) ∈ ℕ(d - n) + 1 ⟶ ℝ
12. i : ℤ
13. 0 ≤ i
14. i ≤ (d - n)
⊢ (poly-nth-deriv(n;a) i) = (poly-nth-deriv(n;b) i)
BY
{ ((InstLemma `poly-nth-deriv-req` [⌜n⌝;⌜(d - n) + 1⌝]⋅ THENA Auto) THEN (RWO "-1" 0 THENA Auto)) }

1
1. d : ℕ
2. n : ℕ
3. ¬d < n
4. a : ℕd + 1 ⟶ ℝ
5. b : ℕd + 1 ⟶ ℝ
6. x1 : ℝ
7. x2 : ℝ
8. ∀i:ℕd + 1. ((a i) = (b i))
9. x1 = x2
10. poly-nth-deriv(n;a) ∈ ℕ(d - n) + 1 ⟶ ℝ
11. poly-nth-deriv(n;b) ∈ ℕ(d - n) + 1 ⟶ ℝ
12. i : ℤ
13. 0 ≤ i
14. i ≤ (d - n)
15. ∀[a:ℕn + (d - n) + 1 ⟶ ℝ]. ∀[i:ℕ(d - n) + 1].  ((poly-nth-deriv(n;a) i) = (r((i + n)!) * (a (i + n)))/(i)!)
⊢ (r((i + n)!) * (a (i + n)))/(i)! = (r((i + n)!) * (b (i + n)))/(i)!

---

Latex:

---

Latex:

1.  d  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  \mneg{}d  <  n
4.  a  :  \mBbbN{}d  +  1  {}\mrightarrow{}  \mBbbR{}
5.  b  :  \mBbbN{}d  +  1  {}\mrightarrow{}  \mBbbR{}
6.  x1  :  \mBbbR{}
7.  x2  :  \mBbbR{}
8.  \mforall{}i:\mBbbN{}d  +  1.  ((a  i)  =  (b  i))
9.  x1  =  x2
10.  poly-nth-deriv(n;a)  \mmember{}  \mBbbN{}(d  -  n)  +  1  {}\mrightarrow{}  \mBbbR{}
11.  poly-nth-deriv(n;b)  \mmember{}  \mBbbN{}(d  -  n)  +  1  {}\mrightarrow{}  \mBbbR{}
12.  i  :  \mBbbZ{}
13.  0  \mleq{}  i
14.  i  \mleq{}  (d  -  n)
\mvdash{}  (poly-nth-deriv(n;a)  i)  =  (poly-nth-deriv(n;b)  i)


By

---

Latex:
((InstLemma  `poly-nth-deriv-req`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}(d  -  n)  +  1\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index