---

Step * 3 1 2 1 1 1 of Lemma Legendre-orthogonal

.....aux..... 
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 : ℝ
14. (x * Legendre(n;x)) = (Legendre(n - 1;x) + ((x^2 - r1/r(n)) * (g x)))
⊢ (x^k * Legendre(n;x)) = ((x^k - 1 * Legendre(n - 1;x)) + ((x^k + 1 - x^k - 1/r(n)) * (g x)))
BY
{ ((InstLemma `rnexp_step` [⌜x⌝;⌜k⌝]⋅ THENA Auto) THEN (RWO  "-1" 0 THENA 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 : ℝ
14. (x * Legendre(n;x)) = (Legendre(n - 1;x) + ((x^2 - r1/r(n)) * (g x)))
15. x^k = (x^k - 1 * x)
⊢ ((x^k - 1 * x) * Legendre(n;x)) = ((x^k - 1 * Legendre(n - 1;x)) + ((x^k + 1 - x^k - 1/r(n)) * (g x)))

---

Latex:

---

Latex:
.....aux..... 
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.  x  :  \mBbbR{}
14.  (x  *  Legendre(n;x))  =  (Legendre(n  -  1;x)  +  ((x\^{}2  -  r1/r(n))  *  (g  x)))
\mvdash{}  (x\^{}k  *  Legendre(n;x))  =  ((x\^{}k  -  1  *  Legendre(n  -  1;x))  +  ((x\^{}k  +  1  -  x\^{}k  -  1/r(n))  *  (g  x)))


By

---

Latex:
((InstLemma  `rnexp\_step`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  (RWO    "-1"  0  THENA  Auto))

---

Home Index