---

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


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))
BY
{ (MoveToConcl (-1)
   THEN (Assert r1 ≤ r(doublefact((2 * n) - 1)) BY
               Auto)
   THEN (Assert r1 ≤ r(doublefact((2 * n) + 1)) BY
               Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN GenConclTerms Auto [⌜r(doublefact((2 * n) + 1))⌝;⌜r(doublefact((2 * n) - 1))⌝]⋅
   THEN Auto) }

1
1. n : ℕ
2. ¬(n = 0 ∈ ℤ)
3. v : ℝ
4. r(doublefact((2 * n) + 1)) = v ∈ ℝ
5. v1 : ℝ
6. r(doublefact((2 * n) - 1)) = v1 ∈ ℝ
7. r1 ≤ v1
8. r1 ≤ v
9. v = (v1 * r((2 * n) + 1))
⊢ ((r(2 * (n)!)/v) * (v1/r((n)!))) = (r(2)/r((2 * n) + 1))

---

Latex:

---

Latex:

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


By

---

Latex:
(MoveToConcl  (-1)
  THEN  (Assert  r1  \mleq{}  r(doublefact((2  *  n)  -  1))  BY
                          Auto)
  THEN  (Assert  r1  \mleq{}  r(doublefact((2  *  n)  +  1))  BY
                          Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}r(doublefact((2  *  n)  +  1))\mkleeneclose{};\mkleeneopen{}r(doublefact((2  *  n)  -  1))\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index