---

Step * 1 5 1 2 1 1 1 1 1 1 1 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)
      ⇒ (((2 * n) - 1 * ((x * (f x)) + (g x)) + (g x) - n - 1 * f1 x)/n
         = ((2 * n) - 1 * ((y * (f y)) + (g y)) + (g y) - n - 1 * f1 y)/n))
23. ∀x,y:ℝ.
      ((x = y)
      ⇒ (((2 * n) - 1 * (x * (g x)) + Legendre(n - 1;x) - n - 1 * g1 x)/n
         = ((2 * n) - 1 * (y * (g y)) + Legendre(n - 1;y) - n - 1 * g1 y)/n))
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)
27. 0 < n
28. x : ℝ
29. ¬(n = 2 ∈ ℤ)
30. y : ℝ
31. (r1 - x * x) = y ∈ ℝ
32. (y * (g1 x)) = ((r(n - 2) * Legendre(n - 3;x)) - (r(n - 2) * x) * Legendre(n - 2;x))
33. (y * (g x)) = ((r(n - 1) * Legendre(n - 2;x)) - (r(n - 1) * x) * Legendre(n - 1;x))
34. N : ℝ
35. r(n) = N ∈ ℝ
⊢ ((((r(2) * N) - r1)
* ((x * (((N - r1) * Legendre(n - 2;x)) - ((N - r1) * x) * Legendre(n - 1;x))) + (y * Legendre(n - 1;x)))) - (N - r1)
* (((N - r(2)) * Legendre(n - 3;x)) - ((N - r(2)) * x) * Legendre(n - 2;x)))
= (((N * N) * Legendre(n - 1;x)) - (N * x)
  * ((((r(2) * N) - r1) * x * Legendre(n - 1;x)) - (N - r1) * Legendre(n - 2;x)))
BY
{ (Assert Legendre(n - 1;x) ~ ((2 * n) - 3 * x * Legendre(n - 2;x) - n - 2 * Legendre(n - 3;x))/n - 1 BY
         (RW (AddrC [1] UnfoldTopAbC) 0 THEN Auto)) }

1
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)
      ⇒ (((2 * n) - 1 * ((x * (f x)) + (g x)) + (g x) - n - 1 * f1 x)/n
         = ((2 * n) - 1 * ((y * (f y)) + (g y)) + (g y) - n - 1 * f1 y)/n))
23. ∀x,y:ℝ.
      ((x = y)
      ⇒ (((2 * n) - 1 * (x * (g x)) + Legendre(n - 1;x) - n - 1 * g1 x)/n
         = ((2 * n) - 1 * (y * (g y)) + Legendre(n - 1;y) - n - 1 * g1 y)/n))
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)
27. 0 < n
28. x : ℝ
29. ¬(n = 2 ∈ ℤ)
30. y : ℝ
31. (r1 - x * x) = y ∈ ℝ
32. (y * (g1 x)) = ((r(n - 2) * Legendre(n - 3;x)) - (r(n - 2) * x) * Legendre(n - 2;x))
33. (y * (g x)) = ((r(n - 1) * Legendre(n - 2;x)) - (r(n - 1) * x) * Legendre(n - 1;x))
34. N : ℝ
35. r(n) = N ∈ ℝ
36. Legendre(n - 1;x) ~ ((2 * n) - 3 * x * Legendre(n - 2;x) - n - 2 * Legendre(n - 3;x))/n - 1
⊢ ((((r(2) * N) - r1)
* ((x * (((N - r1) * Legendre(n - 2;x)) - ((N - r1) * x) * Legendre(n - 1;x))) + (y * Legendre(n - 1;x)))) - (N - r1)
* (((N - r(2)) * Legendre(n - 3;x)) - ((N - r(2)) * x) * Legendre(n - 2;x)))
= (((N * N) * Legendre(n - 1;x)) - (N * x)
  * ((((r(2) * N) - r1) * x * Legendre(n - 1;x)) - (N - r1) * Legendre(n - 2;x)))

---

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{}  (((2  *  n)  -  1  *  ((x  *  (f  x))  +  (g  x))  +  (g  x)  -  n  -  1  *  f1  x)/n
                  =  ((2  *  n)  -  1  *  ((y  *  (f  y))  +  (g  y))  +  (g  y)  -  n  -  1  *  f1  y)/n))
23.  \mforall{}x,y:\mBbbR{}.
            ((x  =  y)
            {}\mRightarrow{}  (((2  *  n)  -  1  *  (x  *  (g  x))  +  Legendre(n  -  1;x)  -  n  -  1  *  g1  x)/n
                  =  ((2  *  n)  -  1  *  (y  *  (g  y))  +  Legendre(n  -  1;y)  -  n  -  1  *  g1  y)/n))
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.  \mforall{}x:\mBbbR{}
            (((((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)
27.  0  <  n
28.  x  :  \mBbbR{}
29.  \mneg{}(n  =  2)
30.  y  :  \mBbbR{}
31.  (r1  -  x  *  x)  =  y
32.  (y  *  (g1  x))  =  ((r(n  -  2)  *  Legendre(n  -  3;x))  -  (r(n  -  2)  *  x)  *  Legendre(n  -  2;x))
33.  (y  *  (g  x))  =  ((r(n  -  1)  *  Legendre(n  -  2;x))  -  (r(n  -  1)  *  x)  *  Legendre(n  -  1;x))
34.  N  :  \mBbbR{}
35.  r(n)  =  N
\mvdash{}  ((((r(2)  *  N)  -  r1)
*  ((x  *  (((N  -  r1)  *  Legendre(n  -  2;x))  -  ((N  -  r1)  *  x)  *  Legendre(n  -  1;x)))
    +  (y  *  Legendre(n  -  1;x))))  -  (N  -  r1)
*  (((N  -  r(2))  *  Legendre(n  -  3;x))  -  ((N  -  r(2))  *  x)  *  Legendre(n  -  2;x)))
=  (((N  *  N)  *  Legendre(n  -  1;x))  -  (N  *  x)
    *  ((((r(2)  *  N)  -  r1)  *  x  *  Legendre(n  -  1;x))  -  (N  -  r1)  *  Legendre(n  -  2;x)))


By

---

Latex:
(Assert  Legendre(n  -  1;x)  \msim{}  ((2  *  n)  -  3  *  x  *  Legendre(n  -  2;x)  -  n  -  2  *  Legendre(n  -  3;x))/n 
              -  1  BY
              (RW  (AddrC  [1]  UnfoldTopAbC)  0  THEN  Auto))

---

Home Index