---

Step * 3 1 2 1 1 2 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. ¬(n = 1 ∈ ℤ)
5. k : ℕ
6. ∀k:ℕ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
7. ¬(k = 0 ∈ ℤ)
8. k ≤ n
9. g : (-∞, ∞) ⟶ℝ
10. ∀x,y:ℝ.  ((x = y) ⇒ ((g x) = (g y)))
11. d(Legendre(n;x))/dx = λx.g[x] on (-∞, ∞)
12. ∀x:ℝ. ((x * Legendre(n;x)) = (Legendre(n - 1;x) + ((x^2 - r1/r(n)) * (g x))))
13. ∀x:ℝ. ((x^k * Legendre(n;x)) = ((x^k - 1 * Legendre(n - 1;x)) + ((x^k + 1 - x^k - 1/r(n)) * (g x))))
⊢ 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 
BY
{ (Assert r(-1)_∫-r1 x^k * Legendre(n;x) dx
         = r(-1)_∫-r1 (x^k - 1 * Legendre(n - 1;x)) + ((x^k + 1 - x^k - 1/r(n)) * (g x)) dx BY
         (BLemma `integral_functionality`
          THEN Auto
          THEN (BLemma `radd_functionality` THEN Auto)
          THEN BLemma `rmul_functionality`
          THEN Auto)) }

1
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. ¬(n = 1 ∈ ℤ)
5. k : ℕ
6. ∀k:ℕ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
7. ¬(k = 0 ∈ ℤ)
8. k ≤ n
9. g : (-∞, ∞) ⟶ℝ
10. ∀x,y:ℝ.  ((x = y) ⇒ ((g x) = (g y)))
11. d(Legendre(n;x))/dx = λx.g[x] on (-∞, ∞)
12. ∀x:ℝ. ((x * Legendre(n;x)) = (Legendre(n - 1;x) + ((x^2 - r1/r(n)) * (g x))))
13. ∀x:ℝ. ((x^k * Legendre(n;x)) = ((x^k - 1 * Legendre(n - 1;x)) + ((x^k + 1 - x^k - 1/r(n)) * (g x))))
14. r(-1)_∫-r1 x^k * Legendre(n;x) dx = r(-1)_∫-r1 (x^k - 1 * Legendre(n - 1;x)) + ((x^k + 1 - x^k - 1/r(n)) * (g x)) dx
⊢ 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 

---

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.  \mneg{}(n  =  0)
4.  \mneg{}(n  =  1)
5.  k  :  \mBbbN{}
6.  \mforall{}k:\mBbbN{}k
          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
7.  \mneg{}(k  =  0)
8.  k  \mleq{}  n
9.  g  :  (-\minfty{},  \minfty{})  {}\mrightarrow{}\mBbbR{}
10.  \mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  ((g  x)  =  (g  y)))
11.  d(Legendre(n;x))/dx  =  \mlambda{}x.g[x]  on  (-\minfty{},  \minfty{})
12.  \mforall{}x:\mBbbR{}.  ((x  *  Legendre(n;x))  =  (Legendre(n  -  1;x)  +  ((x\^{}2  -  r1/r(n))  *  (g  x))))
13.  \mforall{}x:\mBbbR{}
            ((x\^{}k  *  Legendre(n;x))  =  ((x\^{}k  -  1  *  Legendre(n  -  1;x))  +  ((x\^{}k  +  1  -  x\^{}k  -  1/r(n))  *  (g  x))))
\mvdash{}  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 


By

---

Latex:
(Assert  r(-1)\_\mint{}\msupminus{}r1  x\^{}k  *  Legendre(n;x)  dx
              =  r(-1)\_\mint{}\msupminus{}r1  (x\^{}k  -  1  *  Legendre(n  -  1;x))  +  ((x\^{}k  +  1  -  x\^{}k  -  1/r(n))  *  (g  x))  dx  BY
              (BLemma  `integral\_functionality`
                THEN  Auto
                THEN  (BLemma  `radd\_functionality`  THEN  Auto)
                THEN  BLemma  `rmul\_functionality`
                THEN  Auto))

---

Home Index