Step
*
1
4
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. (((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
BY
{ Assert ⌜(((y * ((2 * m) - 1 * ((x * v2) + v3) + v3 - m - 1 * v4)) - (r(2) * x)
* ((2 * m) - 1 * (x * v3) + v - m - 1 * v5))
+ (r(m * (m + 1)) * ((2 * m) - 1 * x * v - m - 1 * v1)))
= r0⌝⋅ }
1
.....assertion.....
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)) - (r(2) * x) * ((2 * m) - 1 * (x * v3) + v - m - 1 * v5))
+ (r(m * (m + 1)) * ((2 * m) - 1 * x * v - m - 1 * v1)))
= r0
2
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)
30. (((y * ((2 * m) - 1 * ((x * v2) + v3) + v3 - m - 1 * v4)) - (r(2) * x) * ((2 * m) - 1 * (x * v3) + v - m - 1 * v5))
+ (r(m * (m + 1)) * ((2 * m) - 1 * x * v - m - 1 * v1)))
= r0
⊢ (((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{}
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. (((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)
\mvdash{} (((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
By
Latex:
Assert \mkleeneopen{}(((y * ((2 * m) - 1 * ((x * v2) + v3) + v3 - m - 1 * v4)) - (r(2) * x)
* ((2 * m) - 1 * (x * v3) + v - m - 1 * v5))
+ (r(m * (m + 1)) * ((2 * m) - 1 * x * v - m - 1 * v1)))
= r0\mkleeneclose{}\mcdot{}
Home
Index