Proof of Nuprl Lemma : Legendre-differential-equation

Step * 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))))

⊢ ∃f,g:(-∞, ∞) ⟶ℝ
   ((∀x,y:ℝ.  ((x = y) ⇒ ((f x) = (f y))))
   ∧ (∀x,y:ℝ.  ((x = y) ⇒ ((g x) = (g y))))
   ∧ d(g[x])/dx = λx.f[x] on (-∞, ∞)
   ∧ d(Legendre(n;x))/dx = λx.g[x] on (-∞, ∞)

   ∧ (∀x:ℝ. (((((r1 - x * x) * (f x)) - (r(2) * x) * (g x)) + (r(n * (n + 1)) * Legendre(n;x))) = r0))

   ∧ (0 < n ⇒ (∀x:ℝ. (((r1 - x * x) * (g x)) = ((r(n) * Legendre(n - 1;x)) - (r(n) * x) * Legendre(n;x))))))
BY
{ (InstConcl [⌜λx.((2 * n) - 1 * ((x * (f x)) + (g x)) + (g x) - n - 1 * f1 x)/n⌝;
   ⌜λx.((2 * n) - 1 * (x * (g x)) + Legendre(n - 1;x) - n - 1 * g1 x)/n⌝]⋅
   THEN Auto
   THEN RepUR ``so_apply`` 0
   THEN Auto
   THEN ((Progress(ProveDerivative) THEN Auto) ORELSE Reduce 0)) }

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))))

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 : ℝ
23. y : ℝ
24. 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

2
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))))

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 : ℝ
24. y : ℝ
25. 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

3
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))))

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 (-∞, ∞)

⊢ d(Legendre(n;x))/dx = λx.((2 * n) - 1 * (x * (g x)) + Legendre(n - 1;x) - n - 1 * g1 x)/n on (-∞, ∞)

4
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))))

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))))

         - 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

5
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))))

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))))

         - 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) * ((λx.((2 * n) - 1 * ((x * (f x)) + (g x)) + (g x) - n - 1 * f1 x)/n) x)) - (r(2) * x)

      * ((λx.((2 * n) - 1 * (x * (g x)) + Legendre(n - 1;x) - n - 1 * g1 x)/n) x))
      + (r(n * (n + 1)) * Legendre(n;x)))
      = r0)
27. 0 < n
28. x : ℝ
⊢ ((r1 - x * x) * ((2 * n) - 1 * (x * (g x)) + Legendre(n - 1;x) - n - 1 * g1 x)/n)
= ((r(n) * Legendre(n - 1;x)) - (r(n) * x) * Legendre(n;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)))) \mvdash{} \mexists{}f,g:(-\minfty{}, \minfty{}) {}\mrightarrow{}\mBbbR{} ((\mforall{}x,y:\mBbbR{}. ((x = y) {}\mRightarrow{} ((f x) = (f y)))) \mwedge{} (\mforall{}x,y:\mBbbR{}. ((x = y) {}\mRightarrow{} ((g x) = (g y)))) \mwedge{} d(g[x])/dx = \mlambda{}x.f[x] on (-\minfty{}, \minfty{}) \mwedge{} d(Legendre(n;x))/dx = \mlambda{}x.g[x] on (-\minfty{}, \minfty{}) \mwedge{} (\mforall{}x:\mBbbR{} (((((r1 - x * x) * (f x)) - (r(2) * x) * (g x)) + (r(n * (n + 1)) * Legendre(n;x))) = r0)) \mwedge{} (0 < n {}\mRightarrow{} (\mforall{}x:\mBbbR{} (((r1 - x * x) * (g x)) = ((r(n) * Legendre(n - 1;x)) - (r(n) * x) * Legendre(n;x)))))) By Latex: (InstConcl [\mkleeneopen{}\mlambda{}x.((2 * n) - 1 * ((x * (f x)) + (g x)) + (g x) - n - 1 * f1 x)/n\mkleeneclose{}; \mkleeneopen{}\mlambda{}x.((2 * n) - 1 * (x * (g x)) + Legendre(n - 1;x) - n - 1 * g1 x)/n\mkleeneclose{}]\mcdot{} THEN Auto THEN RepUR ``so\_apply`` 0 THEN Auto THEN ((Progress(ProveDerivative) THEN Auto) ORELSE Reduce 0)) Home Index