---

Step * of Lemma Legendre-deriv-equation1

∀n:ℕ+
  ∃g:(-∞, ∞) ⟶ℝ
   ((∀x,y:ℝ.  ((x = y) ⇒ ((g x) = (g y))))
   ∧ d(Legendre(n;x))/dx = λx.g[x] on (-∞, ∞)
   ∧ (∀x:ℝ. ((x * Legendre(n;x)) = (Legendre(n - 1;x) + ((x^2 - r1/r(n)) * (g x))))))
BY
{ (InstLemma `Legendre-differential-equation` []
   THEN ParallelLast'
   THEN ExRepD
   THEN D 0 With ⌜g⌝ 
   THEN Auto
   THEN (InstHyp [⌜x⌝] (-4)⋅ THENA Auto)
   THEN (nRMul ⌜r(n)⌝ 0⋅ THENA Auto)
   THEN RWO "rnexp2" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}
    \mexists{}g:(-\minfty{},  \minfty{})  {}\mrightarrow{}\mBbbR{}
      ((\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  ((g  x)  =  (g  y))))
      \mwedge{}  d(Legendre(n;x))/dx  =  \mlambda{}x.g[x]  on  (-\minfty{},  \minfty{})
      \mwedge{}  (\mforall{}x:\mBbbR{}.  ((x  *  Legendre(n;x))  =  (Legendre(n  -  1;x)  +  ((x\^{}2  -  r1/r(n))  *  (g  x))))))


By

---

Latex:
(InstLemma  `Legendre-differential-equation`  []
  THEN  ParallelLast'
  THEN  ExRepD
  THEN  D  0  With  \mkleeneopen{}g\mkleeneclose{} 
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  (nRMul  \mkleeneopen{}r(n)\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  RWO  "rnexp2"  0
  THEN  Auto)

---

Home Index