---

Step * of Lemma Legendre-orthogonal-rpolynomial

∀[n,k:ℕ]. ∀[a:ℕk + 1 ⟶ ℝ].
  r(-1)_∫-r1 (Σi≤k. a_i * x^i) * Legendre(n;x) dx
  = if (k =z n) then (r(2 * (n)!)/r(doublefact((2 * n) + 1))) * (a n) else r0 fi  
  supposing k ≤ n
BY
{ (Auto
   THEN Try (((BLemma `rmul_functionality` THEN Auto)
              THEN BLemma `rpolynomial_functionality`
              THEN Auto
              THEN D 0
              THEN Reduce 0
              THEN Auto))
   ) }

1
1. n : ℕ
2. k : ℕ
3. a : ℕk + 1 ⟶ ℝ
4. k ≤ n
⊢ r(-1)_∫-r1 (Σi≤k. a_i * x^i) * Legendre(n;x) dx
= if (k =z n) then (r(2 * (n)!)/r(doublefact((2 * n) + 1))) * (a n) else r0 fi 

---

Latex:

---

Latex:
\mforall{}[n,k:\mBbbN{}].  \mforall{}[a:\mBbbN{}k  +  1  {}\mrightarrow{}  \mBbbR{}].
    r(-1)\_\mint{}\msupminus{}r1  (\mSigma{}i\mleq{}k.  a\_i  *  x\^{}i)  *  Legendre(n;x)  dx
    =  if  (k  =\msubz{}  n)  then  (r(2  *  (n)!)/r(doublefact((2  *  n)  +  1)))  *  (a  n)  else  r0  fi   
    supposing  k  \mleq{}  n


By

---

Latex:
(Auto
  THEN  Try  (((BLemma  `rmul\_functionality`  THEN  Auto)
                        THEN  BLemma  `rpolynomial\_functionality`
                        THEN  Auto
                        THEN  D  0
                        THEN  Reduce  0
                        THEN  Auto))
  )

---

Home Index