---

Step * of Lemma rpoly-nth-deriv_functionality

∀[d,n:ℕ]. ∀[a,b:ℕd + 1 ⟶ ℝ]. ∀[x1,x2:ℝ].
  (rpoly-nth-deriv(n;d;a;x1) = rpoly-nth-deriv(n;d;b;x2)) supposing ((x1 = x2) and (∀i:ℕd + 1. ((a i) = (b i))))
BY
{ (Auto
   THEN Unfold `rpoly-nth-deriv` 0
   THEN AutoSplit
   THEN Unfold `rpolynomial` 0
   THEN (InstLemma `poly-nth-deriv_wf` [⌜n⌝;⌜(d - n) + 1⌝;⌜a⌝]⋅ THENA Auto)
   THEN (InstLemma `poly-nth-deriv_wf` [⌜n⌝;⌜(d - n) + 1⌝;⌜b⌝]⋅ THENA Auto)
   THEN BLemma `rsum_functionality`
   THEN Auto
   THEN D 0
   THEN Auto
   THEN BLemma `rmul_functionality`
   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)
⊢ (poly-nth-deriv(n;a) i) = (poly-nth-deriv(n;b) i)

2
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

---

Latex:

---

Latex:
\mforall{}[d,n:\mBbbN{}].  \mforall{}[a,b:\mBbbN{}d  +  1  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[x1,x2:\mBbbR{}].
    (rpoly-nth-deriv(n;d;a;x1)  =  rpoly-nth-deriv(n;d;b;x2))  supposing 
          ((x1  =  x2)  and 
          (\mforall{}i:\mBbbN{}d  +  1.  ((a  i)  =  (b  i))))


By

---

Latex:
(Auto
  THEN  Unfold  `rpoly-nth-deriv`  0
  THEN  AutoSplit
  THEN  Unfold  `rpolynomial`  0
  THEN  (InstLemma  `poly-nth-deriv\_wf`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}(d  -  n)  +  1\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `poly-nth-deriv\_wf`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}(d  -  n)  +  1\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BLemma  `rsum\_functionality`
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  BLemma  `rmul\_functionality`
  THEN  Auto)

---

Home Index