Step
*
3
1
2
1
1
2
1
1
1
1
1
1
1
4
1
1
1
1
1
2
1
2
1
1
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 ∈ ℤ)
5. k : ℕ
6. ∀k:ℕ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
7. ¬(k = 0 ∈ ℤ)
8. k ≤ n
9. g : (-∞, ∞) ⟶ℝ
10. ∀x,y:ℝ. ((x = y) ⇒ ((g x) = (g y)))
11. d(Legendre(n;x))/dx = λx.g[x] on (-∞, ∞)
12. ∀x:ℝ. ((x * Legendre(n;x)) = (Legendre(n - 1;x) + ((x^2 - r1/r(n)) * (g x))))
13. ∀x:ℝ. ((x^k * Legendre(n;x)) = ((x^k - 1 * Legendre(n - 1;x)) + ((x^k + 1 - x^k - 1/r(n)) * (g x))))
14. r(-1)_∫-r1 x^k * Legendre(n;x) dx
= (if (k =z n) then (r(2 * (n - 1)!)/r(doublefact((2 * n) - 1))) else r0 fi
+ (r0 - r(-1)_∫-r1 ((r(k + 1) * x^k) - r(k - 1) * x^k - 2/r(n)) * Legendre(n;x) dx))
15. r(-1)_∫-r1 ((r(k + 1) * t^k) - r(k - 1) * t^k - 2/r(n)) * Legendre(n;t) dt ∈ ℝ
16. ¬(k = 1 ∈ ℤ)
17. (k =z 1) ~ ff
18. r(-1)_∫-r1 ((r(k + 1) * x^k) - r(k - 1) * x^k - 2/r(n)) * Legendre(n;x) dx
= (((r(k + 1)/r(n)) * r(-1)_∫-r1 x^k * Legendre(n;x) dx) - (r(k - 1)/r(n)) * r(-1)_∫-r1 x^k - 2 * Legendre(n;x) dx)
⊢ 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
BY
{ (RWO "-1" (-5) THENA Auto) }
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:ℕ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
7. ¬(k = 0 ∈ ℤ)
8. k ≤ n
9. g : (-∞, ∞) ⟶ℝ
10. ∀x,y:ℝ. ((x = y) ⇒ ((g x) = (g y)))
11. d(Legendre(n;x))/dx = λx.g[x] on (-∞, ∞)
12. ∀x:ℝ. ((x * Legendre(n;x)) = (Legendre(n - 1;x) + ((x^2 - r1/r(n)) * (g x))))
13. ∀x:ℝ. ((x^k * Legendre(n;x)) = ((x^k - 1 * Legendre(n - 1;x)) + ((x^k + 1 - x^k - 1/r(n)) * (g x))))
14. r(-1)_∫-r1 x^k * Legendre(n;x) dx
= (if (k =z n) then (r(2 * (n - 1)!)/r(doublefact((2 * n) - 1))) else r0 fi
+ (r0 - ((r(k + 1)/r(n)) * r(-1)_∫-r1 x^k * Legendre(n;x) dx) - (r(k - 1)/r(n))
* r(-1)_∫-r1 x^k - 2 * Legendre(n;x) dx))
15. r(-1)_∫-r1 ((r(k + 1) * t^k) - r(k - 1) * t^k - 2/r(n)) * Legendre(n;t) dt ∈ ℝ
16. ¬(k = 1 ∈ ℤ)
17. (k =z 1) ~ ff
18. r(-1)_∫-r1 ((r(k + 1) * x^k) - r(k - 1) * x^k - 2/r(n)) * Legendre(n;x) dx
= (((r(k + 1)/r(n)) * r(-1)_∫-r1 x^k * Legendre(n;x) dx) - (r(k - 1)/r(n)) * r(-1)_∫-r1 x^k - 2 * Legendre(n;x) dx)
⊢ 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
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. \mneg{}(n = 1)
5. k : \mBbbN{}
6. \mforall{}k:\mBbbN{}k
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
7. \mneg{}(k = 0)
8. k \mleq{} n
9. g : (-\minfty{}, \minfty{}) {}\mrightarrow{}\mBbbR{}
10. \mforall{}x,y:\mBbbR{}. ((x = y) {}\mRightarrow{} ((g x) = (g y)))
11. d(Legendre(n;x))/dx = \mlambda{}x.g[x] on (-\minfty{}, \minfty{})
12. \mforall{}x:\mBbbR{}. ((x * Legendre(n;x)) = (Legendre(n - 1;x) + ((x\^{}2 - r1/r(n)) * (g x))))
13. \mforall{}x:\mBbbR{}
((x\^{}k * Legendre(n;x)) = ((x\^{}k - 1 * Legendre(n - 1;x)) + ((x\^{}k + 1 - x\^{}k - 1/r(n)) * (g x))))
14. r(-1)\_\mint{}\msupminus{}r1 x\^{}k * Legendre(n;x) dx
= (if (k =\msubz{} n) then (r(2 * (n - 1)!)/r(doublefact((2 * n) - 1))) else r0 fi
+ (r0 - r(-1)\_\mint{}\msupminus{}r1 ((r(k + 1) * x\^{}k) - r(k - 1) * x\^{}k - 2/r(n)) * Legendre(n;x) dx))
15. r(-1)\_\mint{}\msupminus{}r1 ((r(k + 1) * t\^{}k) - r(k - 1) * t\^{}k - 2/r(n)) * Legendre(n;t) dt \mmember{} \mBbbR{}
16. \mneg{}(k = 1)
17. (k =\msubz{} 1) \msim{} ff
18. r(-1)\_\mint{}\msupminus{}r1 ((r(k + 1) * x\^{}k) - r(k - 1) * x\^{}k - 2/r(n)) * Legendre(n;x) dx
= (((r(k + 1)/r(n)) * r(-1)\_\mint{}\msupminus{}r1 x\^{}k * Legendre(n;x) dx) - (r(k - 1)/r(n))
* r(-1)\_\mint{}\msupminus{}r1 x\^{}k - 2 * Legendre(n;x) dx)
\mvdash{} 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
By
Latex:
(RWO "-1" (-5) THENA Auto)
Home
Index