---

Step * of Lemma Legendre-orthogonality

∀[n,m:ℕ].  (r(-1)_∫-r1 Legendre(n;x) * Legendre(m;x) dx = if (n =z m) then (r(2)/r((2 * n) + 1)) else r0 fi )
BY
{ (Auto THEN AutoSplit) }

1
1. n : ℕ
2. m : ℕ
3. n = m ∈ ℤ
⊢ r(-1)_∫-r1 Legendre(n;x) * Legendre(m;x) dx = (r(2)/r((2 * n) + 1))

2
1. n : ℕ
2. m : ℕ
3. n ≠ m
⊢ r(-1)_∫-r1 Legendre(n;x) * Legendre(m;x) dx = r0

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbN{}].
    (r(-1)\_\mint{}\msupminus{}r1  Legendre(n;x)  *  Legendre(m;x)  dx  =  if  (n  =\msubz{}  m)  then  (r(2)/r((2  *  n)  +  1))  else  r0  fi  )


By

---

Latex:
(Auto  THEN  AutoSplit)

---

Home Index