---

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


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))
BY
{ (Assert r(doublefact((2 * n) + 1)) = (r(doublefact((2 * n) - 1)) * r((2 * n) + 1)) BY
         ((RWO "rmul-int" 0 THENA Auto)
          THEN (RWO "req-int" 0 THENA Auto)
          THEN RW (AddrC [2] UnfoldTopAbC) 0
          THEN Auto)) }

1
1. n : ℕ
2. ¬(n = 0 ∈ ℤ)
3. r(doublefact((2 * n) + 1)) = (r(doublefact((2 * n) - 1)) * r((2 * n) + 1))
⊢ ((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{}
2.  \mneg{}(n  =  0)
\mvdash{}  ((r(2  *  (n)!)/r(doublefact((2  *  n)  +  1)))  *  (r(doublefact((2  *  n)  -  1))/r((n)!)))
=  (r(2)/r((2  *  n)  +  1))


By

---

Latex:
(Assert  r(doublefact((2  *  n)  +  1))  =  (r(doublefact((2  *  n)  -  1))  *  r((2  *  n)  +  1))  BY
              ((RWO  "rmul-int"  0  THENA  Auto)
                THEN  (RWO  "req-int"  0  THENA  Auto)
                THEN  RW  (AddrC  [2]  UnfoldTopAbC)  0
                THEN  Auto))

---

Home Index