---

Step * of Lemma Legendre-differential-equation

∀n:ℕ
  ∃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
{ (CompleteInductionOnNat
   THEN (Assert λx.r0 ∈ (-∞, ∞) ⟶ℝ BY
               Auto)
   THEN (Assert λx.r1 ∈ (-∞, ∞) ⟶ℝ BY
               Auto)
   THEN (CaseNat 0 `n'
         THENL [(InstConcl [⌜λx.r0⌝;⌜λx.r0⌝]⋅ THEN Auto THEN RepUR ``so_apply`` 0 THEN Reduce 0 THEN Auto)
               ; (CaseNat 1 `n'
                  THENL [(InstConcl [⌜λx.r0⌝;⌜λx.r1⌝]⋅ THEN Auto THEN RepUR ``so_apply`` 0 THEN Reduce 0 THEN Auto)
                        ; ((InstHyp [⌜n - 2⌝] 2⋅ THENA Auto) THEN (D 2 With ⌜n - 1⌝  THENA Auto) THEN ExRepD)]
               )]
   )) }

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

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}
    \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:
(CompleteInductionOnNat
  THEN  (Assert  \mlambda{}x.r0  \mmember{}  (-\minfty{},  \minfty{})  {}\mrightarrow{}\mBbbR{}  BY
                          Auto)
  THEN  (Assert  \mlambda{}x.r1  \mmember{}  (-\minfty{},  \minfty{})  {}\mrightarrow{}\mBbbR{}  BY
                          Auto)
  THEN  (CaseNat  0  `n'
              THENL  [(InstConcl  [\mkleeneopen{}\mlambda{}x.r0\mkleeneclose{};\mkleeneopen{}\mlambda{}x.r0\mkleeneclose{}]\mcdot{}
                              THEN  Auto
                              THEN  RepUR  ``so\_apply``  0
                              THEN  Reduce  0
                              THEN  Auto)
                          ;  (CaseNat  1  `n'
                                THENL  [(InstConcl  [\mkleeneopen{}\mlambda{}x.r0\mkleeneclose{};\mkleeneopen{}\mlambda{}x.r1\mkleeneclose{}]\mcdot{}
                                                THEN  Auto
                                                THEN  RepUR  ``so\_apply``  0
                                                THEN  Reduce  0
                                                THEN  Auto)
                                            ;  ((InstHyp  [\mkleeneopen{}n  -  2\mkleeneclose{}]  2\mcdot{}  THENA  Auto)
                                                  THEN  (D  2  With  \mkleeneopen{}n  -  1\mkleeneclose{}    THENA  Auto)
                                                  THEN  ExRepD)]
                          )]
  ))

---

Home Index