---

Step * 2 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)
⊢ x1^i = x2^i
BY
{ (RWO "-6" 0 THEN Auto) }

---

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{}  x1\^{}i  =  x2\^{}i


By

---

Latex:
(RWO  "-6"  0  THEN  Auto)

---

Home Index