---

Step * 1 of Lemma Legendre-orthogonal


1. n : ℕ
2. ∀n:ℕn
     ∀[k:ℕ]
       r(-1)_∫-r1 x^k * Legendre(n;x) dx = if (k =z n) then (r(2 * (n)!)/r(doublefact((2 * n) + 1))) else r0 fi  
       supposing k ≤ n
3. n = 0 ∈ ℤ
4. k : ℕ
5. k ≤ 0
⊢ r(-1)_∫-r1 r1 * r1 dx = (r(2)/r(doublefact(1)))
BY
{ ((Subst' doublefact(1) ~ 1 0 THENA Computation)
   THEN (Assert (r(2)/r1) = r(2) BY
               Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN (RWO "rmul-int" 0 THENA Auto)
   THEN (RWO "integral-const" 0 THENA Auto)
   THEN nRNorm 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  \mforall{}n:\mBbbN{}n
          \mforall{}[k:\mBbbN{}]
              r(-1)\_\mint{}\msupminus{}r1  x\^{}k  *  Legendre(n;x)  dx
              =  if  (k  =\msubz{}  n)  then  (r(2  *  (n)!)/r(doublefact((2  *  n)  +  1)))  else  r0  fi   
              supposing  k  \mleq{}  n
3.  n  =  0
4.  k  :  \mBbbN{}
5.  k  \mleq{}  0
\mvdash{}  r(-1)\_\mint{}\msupminus{}r1  r1  *  r1  dx  =  (r(2)/r(doublefact(1)))


By

---

Latex:
((Subst'  doublefact(1)  \msim{}  1  0  THENA  Computation)
  THEN  (Assert  (r(2)/r1)  =  r(2)  BY
                          Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (RWO  "rmul-int"  0  THENA  Auto)
  THEN  (RWO  "integral-const"  0  THENA  Auto)
  THEN  nRNorm  0
  THEN  Auto)

---

Home Index