---

Step * of Lemma Legendre-annihilates-rpolynomial

∀[n:ℕ]. ∀[f:[r(-1), r1] ⟶ℝ].
  r(-1)_∫-r1 f[x] * Legendre(n;x) dx = r0 
  supposing ∃k:ℕn. ∃a:ℕk + 1 ⟶ ℝ. ∀x:{x:ℝ| x ∈ [r(-1), r1]} . ((f x) = (Σi≤k. a_i * x^i))
BY
{ (Unfold `so_apply` 0
   THEN Intros
   THEN Assert ⌜λx.((f x) * Legendre(n;x)) ∈ {f:[rmin(r(-1);r1), rmax(r(-1);r1)] ⟶ℝ| 
                                              ifun(f;[rmin(r(-1);r1), rmax(r(-1);r1)])} ⌝⋅) }

1
.....assertion..... 
1. [n] : ℕ
2. [f] : [r(-1), r1] ⟶ℝ
3. [%] : ∃k:ℕn. ∃a:ℕk + 1 ⟶ ℝ. ∀x:{x:ℝ| x ∈ [r(-1), r1]} . ((f x) = (Σi≤k. a_i * x^i))
⊢ λx.((f x) * Legendre(n;x)) ∈ {f:[rmin(r(-1);r1), rmax(r(-1);r1)] ⟶ℝ| ifun(f;[rmin(r(-1);r1), rmax(r(-1);r1)])} 

2
1. [n] : ℕ
2. [f] : [r(-1), r1] ⟶ℝ
3. [%] : ∃k:ℕn. ∃a:ℕk + 1 ⟶ ℝ. ∀x:{x:ℝ| x ∈ [r(-1), r1]} . ((f x) = (Σi≤k. a_i * x^i))
4. λx.((f x) * Legendre(n;x)) ∈ {f:[rmin(r(-1);r1), rmax(r(-1);r1)] ⟶ℝ| ifun(f;[rmin(r(-1);r1), rmax(r(-1);r1)])} 
⊢ r(-1)_∫-r1 (f x) * Legendre(n;x) dx = r0

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:[r(-1),  r1]  {}\mrightarrow{}\mBbbR{}].
    r(-1)\_\mint{}\msupminus{}r1  f[x]  *  Legendre(n;x)  dx  =  r0 
    supposing  \mexists{}k:\mBbbN{}n.  \mexists{}a:\mBbbN{}k  +  1  {}\mrightarrow{}  \mBbbR{}.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [r(-1),  r1]\}  .  ((f  x)  =  (\mSigma{}i\mleq{}k.  a\_i  *  x\^{}i))


By

---

Latex:
(Unfold  `so\_apply`  0
  THEN  Intros
  THEN  Assert  \mkleeneopen{}\mlambda{}x.((f  x)  *  Legendre(n;x))  \mmember{}  \{f:[rmin(r(-1);r1),  rmax(r(-1);r1)]  {}\mrightarrow{}\mBbbR{}| 
                                                                                        ifun(f;[rmin(r(-1);r1),  rmax(r(-1);r1)])\}  \mkleeneclose{}\mcdot{})

---

Home Index