---

Step * 1 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)
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)!
BY
{ (Assert ⌜(a (i + n)) = (b (i + n))⌝⋅ THEN 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)!)
16. (a (i + n)) = (b (i + n))
⊢ (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)
15.  \mforall{}[a:\mBbbN{}n  +  (d  -  n)  +  1  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[i:\mBbbN{}(d  -  n)  +  1].
            ((poly-nth-deriv(n;a)  i)  =  (r((i  +  n)!)  *  (a  (i  +  n)))/(i)!)
\mvdash{}  (r((i  +  n)!)  *  (a  (i  +  n)))/(i)!  =  (r((i  +  n)!)  *  (b  (i  +  n)))/(i)!


By

---

Latex:
(Assert  \mkleeneopen{}(a  (i  +  n))  =  (b  (i  +  n))\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index