Step
*
1
1
2
1
1
1
2
of Lemma
Legendre-roots-sq
1. n : ℤ
2. z : i:ℕn - 1 ⟶ {x:ℝ|
(x ∈ (r(-1), r1))
∧ (Legendre(n - 1;x) = r0)
∧ (r0 < (r((-1)^(n - 1 - i)) * Legendre((n - 1) + 1;x)))}
3. ∀i:ℕn - 2. ((z i) < (z (i + 1)))
4. 2 ≤ n
5. ∀a,b:ℝ. rational_fun_zero(λx.ratLegendre(n;x);a;b) ∈ {c:ℝ| (c ∈ (a, b)) ∧ (Legendre(n;c) = r0)} supposing (a < b) ∧\000C ((Legendre(n;a) * Legendre(n;b)) < r0)
6. λi.rational_fun_zero(λx.ratLegendre(n;x);if i=0 then r(-1) else (z (i - 1));if i=n - 1 then r1 else (z i)) ∈ i:ℕn
⟶ {x:ℝ|
(x ∈ (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i)))
∧ (Legendre(n;x) = r0)
∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))}
7. i : ℕn
8. ((λi.rational_fun_zero(λx.ratLegendre(n;x);if i=0 then r(-1) else (z (i - 1));if i=n - 1 then r1 else (z i))) i)
= ((λi.rational_fun_zero(λx.ratLegendre(n;x);if i=0 then r(-1) else (z (i - 1));if i=n - 1 then r1 else (z i))) i)
∈ {x:ℝ|
(x ∈ (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i)))
∧ (Legendre(n;x) = r0)
∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))}
⊢ {x:ℝ|
(x ∈ (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i)))
∧ (Legendre(n;x) = r0)
∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))} ⊆r {x:ℝ|
(x ∈ (r(-1), r1))
∧ (Legendre(n;x) = r0)
∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))}
BY
{ ((D 0 THENA Auto) THEN D -1 THEN MemTypeCD THEN Auto THEN All Reduce) }
1
1. n : ℤ
2. z : i:ℕn - 1 ⟶ {x:ℝ|
((r(-1) < x) ∧ (x < r1))
∧ (Legendre(n - 1;x) = r0)
∧ (r0 < (r((-1)^(n - 1 - i)) * Legendre((n - 1) + 1;x)))}
3. ∀i:ℕn - 2. ((z i) < (z (i + 1)))
4. 2 ≤ n
5. ∀a,b:ℝ. rational_fun_zero(λx.ratLegendre(n;x);a;b) ∈ {c:ℝ| ((a < c) ∧ (c < b)) ∧ (Legendre(n;c) = r0)} supposing (a\000C < b) ∧ ((Legendre(n;a) * Legendre(n;b)) < r0)
6. λi.rational_fun_zero(λx.ratLegendre(n;x);if i=0 then r(-1) else (z (i - 1));if i=n - 1 then r1 else (z i)) ∈ i:ℕn
⟶ {x:ℝ|
((if i=0 then r(-1) else (z (i - 1)) < x) ∧ (x < if i=n - 1 then r1 else (z i)))
∧ (Legendre(n;x) = r0)
∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))}
7. i : ℕn
8. rational_fun_zero(λx.ratLegendre(n;x);if i=0 then r(-1) else (z (i - 1));if i=n - 1 then r1 else (z i))
= rational_fun_zero(λx.ratLegendre(n;x);if i=0 then r(-1) else (z (i - 1));if i=n - 1 then r1 else (z i))
∈ {x:ℝ|
((if i=0 then r(-1) else (z (i - 1)) < x) ∧ (x < if i=n - 1 then r1 else (z i)))
∧ (Legendre(n;x) = r0)
∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))}
9. x : ℝ
10. (if i=0 then r(-1) else (z (i - 1)) < x) ∧ (x < if i=n - 1 then r1 else (z i))
11. Legendre(n;x) = r0
12. r0 < (r((-1)^(n - i)) * Legendre(n + 1;x))
⊢ (r(-1) < x) ∧ (x < r1)
Latex:
Latex:
1. n : \mBbbZ{}
2. z : i:\mBbbN{}n - 1 {}\mrightarrow{} \{x:\mBbbR{}|
(x \mmember{} (r(-1), r1))
\mwedge{} (Legendre(n - 1;x) = r0)
\mwedge{} (r0 < (r((-1)\^{}(n - 1 - i)) * Legendre((n - 1) + 1;x)))\}
3. \mforall{}i:\mBbbN{}n - 2. ((z i) < (z (i + 1)))
4. 2 \mleq{} n
5. \mforall{}a,b:\mBbbR{}.
rational\_fun\_zero(\mlambda{}x.ratLegendre(n;x);a;b) \mmember{} \{c:\mBbbR{}| (c \mmember{} (a, b)) \mwedge{} (Legendre(n;c) = r0)\}
supposing (a < b) \mwedge{} ((Legendre(n;a) * Legendre(n;b)) < r0)
6. \mlambda{}i.rational\_fun\_zero(\mlambda{}x.ratLegendre(n;x);if i=0 then r(-1) else (z (i - 1));if i=n - 1
then r1
else (z i)) \mmember{} i:\mBbbN{}n
{}\mrightarrow{} \{x:\mBbbR{}|
(x \mmember{} (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i)))
\mwedge{} (Legendre(n;x) = r0)
\mwedge{} (r0 < (r((-1)\^{}(n - i)) * Legendre(n + 1;x)))\}
7. i : \mBbbN{}n
8. ((\mlambda{}i.rational\_fun\_zero(\mlambda{}x.ratLegendre(n;x);if i=0 then r(-1) else (z (i - 1));if i=n - 1
then r1
else (z i)))
i)
= ((\mlambda{}i.rational\_fun\_zero(\mlambda{}x.ratLegendre(n;x);if i=0 then r(-1) else (z (i - 1));if i=n - 1
then r1
else (z i)))
i)
\mvdash{} \{x:\mBbbR{}|
(x \mmember{} (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i)))
\mwedge{} (Legendre(n;x) = r0)
\mwedge{} (r0 < (r((-1)\^{}(n - i)) * Legendre(n + 1;x)))\} \msubseteq{}r \{x:\mBbbR{}|
(x \mmember{} (r(-1), r1))
\mwedge{} (Legendre(n;x) = r0)
\mwedge{} (r0 < (r((-1)\^{}(n - i))
* Legendre(n + 1;x)))\}
By
Latex:
((D 0 THENA Auto) THEN D -1 THEN MemTypeCD THEN Auto THEN All Reduce)
Home
Index