---

Step * 1 4 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. 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)
BY
{ ((Subst' Legendre(n;x) ~ ((2 * n) - 1 * x * Legendre(n - 1;x) - n - 1 * Legendre(n - 2;x))/n 0
    THENA (RW (AddrC [1] UnfoldTopAbC) 0 THEN Auto)
    )
   THEN GenConclTerms Auto [⌜Legendre(n - 1;x)⌝;⌜Legendre(n - 2;x)⌝;⌜f x⌝;⌜g x⌝;⌜f1 x⌝; ⌜g1 x⌝]⋅
   THEN (GenConcl ⌜n = m ∈ {2...}⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(r1 - x * x) = y ∈ ℝ⌝⋅ THENA Auto)
   THEN RepeatFor 3 ((D 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 : ℝ
11. v : ℝ
12. Legendre(n - 1;x) = v ∈ ℝ
13. v1 : ℝ
14. Legendre(n - 2;x) = v1 ∈ ℝ
15. v2 : ℝ
16. (f x) = v2 ∈ ℝ
17. v3 : ℝ
18. (g x) = v3 ∈ ℝ
19. v4 : ℝ
20. (f1 x) = v4 ∈ ℝ
21. v5 : ℝ
22. (g1 x) = v5 ∈ ℝ
23. m : {2...}
24. n = m ∈ {2...}
25. y : ℝ
26. (r1 - x * x) = y ∈ ℝ
27. (((y * v4) - (r(2) * x) * v5) + (r((m - 2) * (m - 1)) * v1)) = r0
28. (((y * v2) - (r(2) * x) * v3) + (r((m - 1) * m) * v)) = r0
29. (y * v3) = ((r(m - 1) * v1) - (r(m - 1) * x) * v)
⊢ (((y * ((2 * m) - 1 * ((x * v2) + v3) + v3 - m - 1 * v4)/m) - (r(2) * x)
* ((2 * m) - 1 * (x * v3) + v - m - 1 * v5)/m)
+ (r(m * (m + 1)) * ((2 * m) - 1 * x * v - m - 1 * v1)/m))
= 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.  f  :  (-\minfty{},  \minfty{})  {}\mrightarrow{}\mBbbR{}
9.  g  :  (-\minfty{},  \minfty{})  {}\mrightarrow{}\mBbbR{}
10.  x  :  \mBbbR{}
\mvdash{}  (((((r1  -  x  *  x)  *  (f1  x))  -  (r(2)  *  x)  *  (g1  x))  +  (r((n  -  2)  *  (n  -  1))  *  Legendre(n  -  2;x)))
    =  r0)
{}\mRightarrow{}  (((((r1  -  x  *  x)  *  (f  x))  -  (r(2)  *  x)  *  (g  x))  +  (r((n  -  1)  *  n)  *  Legendre(n  -  1;x)))  =  r0)
{}\mRightarrow{}  (((r1  -  x  *  x)  *  (g  x))  =  ((r(n  -  1)  *  Legendre(n  -  2;x))  -  (r(n  -  1)  *  x)  *  Legendre(n  -  1;x)))
{}\mRightarrow{}  (((((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:
((Subst'  Legendre(n;x)  \msim{}  ((2  *  n)  -  1  *  x  *  Legendre(n  -  1;x)  -  n  -  1  *  Legendre(n  -  2;x))/n  0
    THENA  (RW  (AddrC  [1]  UnfoldTopAbC)  0  THEN  Auto)
    )
  THEN  GenConclTerms  Auto  [\mkleeneopen{}Legendre(n  -  1;x)\mkleeneclose{};\mkleeneopen{}Legendre(n  -  2;x)\mkleeneclose{};\mkleeneopen{}f  x\mkleeneclose{};\mkleeneopen{}g  x\mkleeneclose{};\mkleeneopen{}f1  x\mkleeneclose{};  \mkleeneopen{}g1  x\mkleeneclose{}]\mcdot{}
  THEN  (GenConcl  \mkleeneopen{}n  =  m\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(r1  -  x  *  x)  =  y\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  3  ((D  0  THENA  Auto)))

---

Home Index