---

Step * 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 ∈ ℤ
⊢ ∀[k:ℕ]. r(-1)_∫-r1 x^k * x dx = if (k =z 1) then (r(2 * (1)!)/r(doublefact(3))) else r0 fi  supposing k ≤ 1
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN (CaseNat 0 `k' THENL [Reduce 0; ((Subst' k ~ 1 0 THENA Auto) THEN Reduce 0)])) }

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 ≤ 1
7. k = 0 ∈ ℤ
⊢ r(-1)_∫-r1 r1 * x dx = r0

2
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 ≤ 1
7. ¬(k = 0 ∈ ℤ)
⊢ r(-1)_∫-r1 x^1 * x dx = (r(2 * (1)!)/r(doublefact(3)))

---

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.  n  =  1
\mvdash{}  \mforall{}[k:\mBbbN{}]
        r(-1)\_\mint{}\msupminus{}r1  x\^{}k  *  x  dx  =  if  (k  =\msubz{}  1)  then  (r(2  *  (1)!)/r(doublefact(3)))  else  r0  fi   
        supposing  k  \mleq{}  1


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (CaseNat  0  `k'  THENL  [Reduce  0;  ((Subst'  k  \msim{}  1  0  THENA  Auto)  THEN  Reduce  0)])
  )

---

Home Index