---

Step * 1 1 1 1 1 of Lemma Legendre-orthogonality


1. n : ℕ
⊢ ((r(2 * (n)!)/r(doublefact((2 * n) + 1))) * (r(doublefact((2 * n) - 1))/r((n)!))) = (r(2)/r((2 * n) + 1))
BY
{ CaseNat 0 `n' }

1
1. n : ℕ
2. n = 0 ∈ ℤ
⊢ ((r(2 * (0)!)/r(doublefact((2 * 0) + 1))) * (r(doublefact((2 * 0) - 1))/r((0)!))) = (r(2)/r((2 * 0) + 1))

2
1. n : ℕ
2. ¬(n = 0 ∈ ℤ)
⊢ ((r(2 * (n)!)/r(doublefact((2 * n) + 1))) * (r(doublefact((2 * n) - 1))/r((n)!))) = (r(2)/r((2 * n) + 1))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
\mvdash{}  ((r(2  *  (n)!)/r(doublefact((2  *  n)  +  1)))  *  (r(doublefact((2  *  n)  -  1))/r((n)!)))
=  (r(2)/r((2  *  n)  +  1))


By

---

Latex:
CaseNat  0  `n'

---

Home Index