Step
*
1
4
of Lemma
Legendre-differential-equation
1. n : ℕ
2. λx.r0 ∈ (-∞, ∞) ⟶ℝ
3. λx.r1 ∈ (-∞, ∞) ⟶ℝ
4. ¬(n = 0 ∈ ℤ)
5. ¬(n = 1 ∈ ℤ)
6. f1 : (-∞, ∞) ⟶ℝ
7. g1 : (-∞, ∞) ⟶ℝ
8. ∀x,y:ℝ. ((x = y) ⇒ ((f1 x) = (f1 y)))
9. ∀x,y:ℝ. ((x = y) ⇒ ((g1 x) = (g1 y)))
10. d(g1[x])/dx = λx.f1[x] on (-∞, ∞)
11. d(Legendre(n - 2;x))/dx = λx.g1[x] on (-∞, ∞)
12. ∀x:ℝ. (((((r1 - x * x) * (f1 x)) - (r(2) * x) * (g1 x)) + (r((n - 2) * ((n - 2) + 1)) * Legendre(n - 2;x))) = r0)
13. 0 < n - 2
⇒ (∀x:ℝ. (((r1 - x * x) * (g1 x)) = ((r(n - 2) * Legendre(n - 2 - 1;x)) - (r(n - 2) * x) * Legendre(n - 2;x))))
14. f : (-∞, ∞) ⟶ℝ
15. g : (-∞, ∞) ⟶ℝ
16. ∀x,y:ℝ. ((x = y) ⇒ ((f x) = (f y)))
17. ∀x,y:ℝ. ((x = y) ⇒ ((g x) = (g y)))
18. d(g[x])/dx = λx.f[x] on (-∞, ∞)
19. d(Legendre(n - 1;x))/dx = λx.g[x] on (-∞, ∞)
20. ∀x:ℝ. (((((r1 - x * x) * (f x)) - (r(2) * x) * (g x)) + (r((n - 1) * ((n - 1) + 1)) * Legendre(n - 1;x))) = r0)
21. 0 < n - 1
⇒ (∀x:ℝ. (((r1 - x * x) * (g x)) = ((r(n - 1) * Legendre(n - 1 - 1;x)) - (r(n - 1) * x) * Legendre(n - 1;x))))
22. ∀x,y:ℝ.
((x = y)
⇒ (((λx.((2 * n) - 1 * ((x * (f x)) + (g x)) + (g x) - n - 1 * f1 x)/n) x)
= ((λx.((2 * n) - 1 * ((x * (f x)) + (g x)) + (g x) - n - 1 * f1 x)/n) y)))
23. ∀x,y:ℝ.
((x = y)
⇒ (((λx.((2 * n) - 1 * (x * (g x)) + Legendre(n - 1;x) - n - 1 * g1 x)/n) x)
= ((λx.((2 * n) - 1 * (x * (g x)) + Legendre(n - 1;x) - n - 1 * g1 x)/n) y)))
24. d(λx.((2 * n) - 1 * (x * (g x)) + Legendre(n - 1;x) - n
- 1 * g1 x)/n[x])/dx = λx.λx.((2 * n) - 1 * ((x * (f x)) + (g x)) + (g x) - n - 1 * f1 x)/n[x] on (-∞, ∞)
25. d(Legendre(n;x))/dx = λx.λx.((2 * n) - 1 * (x * (g x)) + Legendre(n - 1;x) - n - 1 * g1 x)/n[x] on (-∞, ∞)
26. x : ℝ
⊢ ((((r1 - x * x) * ((2 * n) - 1 * ((x * (f x)) + (g x)) + (g x) - n - 1 * f1 x)/n) - (r(2) * x)
* ((2 * n) - 1 * (x * (g x)) + Legendre(n - 1;x) - n - 1 * g1 x)/n)
+ (r(n * (n + 1)) * Legendre(n;x)))
= r0
BY
{ (RepeatFor 4 (Thin (-2))
THEN (D -2 THENA Auto)
THEN (D -1 With ⌜x⌝ THENA Auto)
THEN MoveToConcl (-1)
THEN (D -2 With ⌜x⌝ THENA Auto)
THEN MoveToConcl (-1)
THEN RepeatFor 4 (Thin (-2))
THEN Thin (-4)
THEN (D -4 With ⌜x⌝ THENA Auto)
THEN MoveToConcl (-1)
THEN RepeatFor 4 (Thin (-4))
THEN (Subst' (n - 1) + 1 ~ n 0 THENA Auto)
THEN (Subst' (n - 2) + 1 ~ n - 1 0 THENA Auto)
THEN (Subst' n - 1 - 1 ~ n - 2 0 THENA Auto)) }
1
1. n : ℕ
2. λx.r0 ∈ (-∞, ∞) ⟶ℝ
3. λx.r1 ∈ (-∞, ∞) ⟶ℝ
4. ¬(n = 0 ∈ ℤ)
5. ¬(n = 1 ∈ ℤ)
6. f1 : (-∞, ∞) ⟶ℝ
7. g1 : (-∞, ∞) ⟶ℝ
8. f : (-∞, ∞) ⟶ℝ
9. g : (-∞, ∞) ⟶ℝ
10. x : ℝ
⊢ (((((r1 - x * x) * (f1 x)) - (r(2) * x) * (g1 x)) + (r((n - 2) * (n - 1)) * Legendre(n - 2;x))) = r0)
⇒ (((((r1 - x * x) * (f x)) - (r(2) * x) * (g x)) + (r((n - 1) * n) * Legendre(n - 1;x))) = r0)
⇒ (((r1 - x * x) * (g x)) = ((r(n - 1) * Legendre(n - 2;x)) - (r(n - 1) * x) * Legendre(n - 1;x)))
⇒ (((((r1 - x * x) * ((2 * n) - 1 * ((x * (f x)) + (g x)) + (g x) - n - 1 * f1 x)/n) - (r(2) * x)
* ((2 * n) - 1 * (x * (g x)) + Legendre(n - 1;x) - n - 1 * g1 x)/n)
+ (r(n * (n + 1)) * Legendre(n;x)))
= r0)
Latex:
Latex:
1. n : \mBbbN{}
2. \mlambda{}x.r0 \mmember{} (-\minfty{}, \minfty{}) {}\mrightarrow{}\mBbbR{}
3. \mlambda{}x.r1 \mmember{} (-\minfty{}, \minfty{}) {}\mrightarrow{}\mBbbR{}
4. \mneg{}(n = 0)
5. \mneg{}(n = 1)
6. f1 : (-\minfty{}, \minfty{}) {}\mrightarrow{}\mBbbR{}
7. g1 : (-\minfty{}, \minfty{}) {}\mrightarrow{}\mBbbR{}
8. \mforall{}x,y:\mBbbR{}. ((x = y) {}\mRightarrow{} ((f1 x) = (f1 y)))
9. \mforall{}x,y:\mBbbR{}. ((x = y) {}\mRightarrow{} ((g1 x) = (g1 y)))
10. d(g1[x])/dx = \mlambda{}x.f1[x] on (-\minfty{}, \minfty{})
11. d(Legendre(n - 2;x))/dx = \mlambda{}x.g1[x] on (-\minfty{}, \minfty{})
12. \mforall{}x:\mBbbR{}
(((((r1 - x * x) * (f1 x)) - (r(2) * x) * (g1 x))
+ (r((n - 2) * ((n - 2) + 1)) * Legendre(n - 2;x)))
= r0)
13. 0 < n - 2
{}\mRightarrow{} (\mforall{}x:\mBbbR{}
(((r1 - x * x) * (g1 x))
= ((r(n - 2) * Legendre(n - 2 - 1;x)) - (r(n - 2) * x) * Legendre(n - 2;x))))
14. f : (-\minfty{}, \minfty{}) {}\mrightarrow{}\mBbbR{}
15. g : (-\minfty{}, \minfty{}) {}\mrightarrow{}\mBbbR{}
16. \mforall{}x,y:\mBbbR{}. ((x = y) {}\mRightarrow{} ((f x) = (f y)))
17. \mforall{}x,y:\mBbbR{}. ((x = y) {}\mRightarrow{} ((g x) = (g y)))
18. d(g[x])/dx = \mlambda{}x.f[x] on (-\minfty{}, \minfty{})
19. d(Legendre(n - 1;x))/dx = \mlambda{}x.g[x] on (-\minfty{}, \minfty{})
20. \mforall{}x:\mBbbR{}
(((((r1 - x * x) * (f x)) - (r(2) * x) * (g x))
+ (r((n - 1) * ((n - 1) + 1)) * Legendre(n - 1;x)))
= r0)
21. 0 < n - 1
{}\mRightarrow{} (\mforall{}x:\mBbbR{}
(((r1 - x * x) * (g x))
= ((r(n - 1) * Legendre(n - 1 - 1;x)) - (r(n - 1) * x) * Legendre(n - 1;x))))
22. \mforall{}x,y:\mBbbR{}.
((x = y)
{}\mRightarrow{} (((\mlambda{}x.((2 * n) - 1 * ((x * (f x)) + (g x)) + (g x) - n - 1 * f1 x)/n) x)
= ((\mlambda{}x.((2 * n) - 1 * ((x * (f x)) + (g x)) + (g x) - n - 1 * f1 x)/n) y)))
23. \mforall{}x,y:\mBbbR{}.
((x = y)
{}\mRightarrow{} (((\mlambda{}x.((2 * n) - 1 * (x * (g x)) + Legendre(n - 1;x) - n - 1 * g1 x)/n) x)
= ((\mlambda{}x.((2 * n) - 1 * (x * (g x)) + Legendre(n - 1;x) - n - 1 * g1 x)/n) y)))
24. d(\mlambda{}x.((2 * n) - 1 * (x * (g x)) + Legendre(n - 1;x) - n
- 1 * g1 x)/n[x])/dx = \mlambda{}x.\mlambda{}x.((2 * n) - 1 * ((x * (f x)) + (g x)) + (g x) - n
- 1 * f1 x)/n[x] on (-\minfty{}, \minfty{})
25. d(Legendre(n;x))/dx = \mlambda{}x.\mlambda{}x.((2 * n) - 1 * (x * (g x)) + Legendre(n - 1;x) - n
- 1 * g1 x)/n[x] on (-\minfty{}, \minfty{})
26. x : \mBbbR{}
\mvdash{} ((((r1 - x * x) * ((2 * n) - 1 * ((x * (f x)) + (g x)) + (g x) - n - 1 * f1 x)/n) - (r(2) * x)
* ((2 * n) - 1 * (x * (g x)) + Legendre(n - 1;x) - n - 1 * g1 x)/n)
+ (r(n * (n + 1)) * Legendre(n;x)))
= r0
By
Latex:
(RepeatFor 4 (Thin (-2))
THEN (D -2 THENA Auto)
THEN (D -1 With \mkleeneopen{}x\mkleeneclose{} THENA Auto)
THEN MoveToConcl (-1)
THEN (D -2 With \mkleeneopen{}x\mkleeneclose{} THENA Auto)
THEN MoveToConcl (-1)
THEN RepeatFor 4 (Thin (-2))
THEN Thin (-4)
THEN (D -4 With \mkleeneopen{}x\mkleeneclose{} THENA Auto)
THEN MoveToConcl (-1)
THEN RepeatFor 4 (Thin (-4))
THEN (Subst' (n - 1) + 1 \msim{} n 0 THENA Auto)
THEN (Subst' (n - 2) + 1 \msim{} n - 1 0 THENA Auto)
THEN (Subst' n - 1 - 1 \msim{} n - 2 0 THENA Auto))
Home
Index