---

Step * 1 4 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. 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. N : ℝ
28. r(m) = N ∈ ℝ
29. (((y * v4) - (r(2) * x) * v5) + (((N - r(2)) * (N - r1)) * v1)) = r0
30. (((y * v2) - (r(2) * x) * v3) + (((N - r1) * N) * v)) = r0
31. (y * v3) = (((N - r1) * v1) - ((N - r1) * x) * v)
⊢ (((y * ((((r(2) * N) - r1) * (((x * v2) + v3) + v3)) - (N - r1) * v4)) - (r(2) * x)
* ((((r(2) * N) - r1) * ((x * v3) + v)) - (N - r1) * v5))
+ ((N * (N + r1)) * ((((r(2) * N) - r1) * x * v) - (N - r1) * v1)))
= r0
BY
{ (((Assert (y * v2) = (((r(2) * x) * v3) - ((N - r1) * N) * v) BY Auto) THEN Thin (-3))
   THEN (Assert (y * v4) = (((r(2) * x) * v5) - ((N - r(2)) * (N - r1)) * v1) BY
               Auto)
   THEN Thin (-4)
   THEN (Assert (y * ((((r(2) * N) - r1) * (((x * v2) + v3) + v3)) - (N - r1) * v4))
               = ((((r(2) * N) - r1) * ((x * y * v2) + (r(2) * y * v3))) - (N - r1) * y * v4) BY
               Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN Thin (-1)
   THEN (RWO  "-1 -2 -3" 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. N : ℝ
28. r(m) = N ∈ ℝ
29. (y * v3) = (((N - r1) * v1) - ((N - r1) * x) * v)
30. (y * v2) = (((r(2) * x) * v3) - ((N - r1) * N) * v)
31. (y * v4) = (((r(2) * x) * v5) - ((N - r(2)) * (N - r1)) * v1)
⊢ (((((r(2) * N) - r1)
* ((x * (((r(2) * x) * v3) - ((N - r1) * N) * v)) + (r(2) * (((N - r1) * v1) - ((N - r1) * x) * v)))) - (N - r1)
* (((r(2) * x) * v5) - ((N - r(2)) * (N - r1)) * v1) - (r(2) * x)
* ((((r(2) * N) - r1) * ((x * v3) + v)) - (N - r1) * v5))
+ ((N * (N + r1)) * ((((r(2) * N) - r1) * x * v) - (N - r1) * v1)))
= 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{}
11.  v  :  \mBbbR{}
12.  Legendre(n  -  1;x)  =  v
13.  v1  :  \mBbbR{}
14.  Legendre(n  -  2;x)  =  v1
15.  v2  :  \mBbbR{}
16.  (f  x)  =  v2
17.  v3  :  \mBbbR{}
18.  (g  x)  =  v3
19.  v4  :  \mBbbR{}
20.  (f1  x)  =  v4
21.  v5  :  \mBbbR{}
22.  (g1  x)  =  v5
23.  m  :  \{2...\}
24.  n  =  m
25.  y  :  \mBbbR{}
26.  (r1  -  x  *  x)  =  y
27.  N  :  \mBbbR{}
28.  r(m)  =  N
29.  (((y  *  v4)  -  (r(2)  *  x)  *  v5)  +  (((N  -  r(2))  *  (N  -  r1))  *  v1))  =  r0
30.  (((y  *  v2)  -  (r(2)  *  x)  *  v3)  +  (((N  -  r1)  *  N)  *  v))  =  r0
31.  (y  *  v3)  =  (((N  -  r1)  *  v1)  -  ((N  -  r1)  *  x)  *  v)
\mvdash{}  (((y  *  ((((r(2)  *  N)  -  r1)  *  (((x  *  v2)  +  v3)  +  v3))  -  (N  -  r1)  *  v4))  -  (r(2)  *  x)
*  ((((r(2)  *  N)  -  r1)  *  ((x  *  v3)  +  v))  -  (N  -  r1)  *  v5))
+  ((N  *  (N  +  r1))  *  ((((r(2)  *  N)  -  r1)  *  x  *  v)  -  (N  -  r1)  *  v1)))
=  r0


By

---

Latex:
(((Assert  (y  *  v2)  =  (((r(2)  *  x)  *  v3)  -  ((N  -  r1)  *  N)  *  v)  BY  Auto)  THEN  Thin  (-3))
  THEN  (Assert  (y  *  v4)  =  (((r(2)  *  x)  *  v5)  -  ((N  -  r(2))  *  (N  -  r1))  *  v1)  BY
                          Auto)
  THEN  Thin  (-4)
  THEN  (Assert  (y  *  ((((r(2)  *  N)  -  r1)  *  (((x  *  v2)  +  v3)  +  v3))  -  (N  -  r1)  *  v4))
                          =  ((((r(2)  *  N)  -  r1)  *  ((x  *  y  *  v2)  +  (r(2)  *  y  *  v3)))  -  (N  -  r1)  *  y  *  v4)  BY
                          Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  (RWO    "-1  -2  -3"  0  THENA  Auto))

---

Home Index