---

Step * 1 1 1 2 1 1 1 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. i : ℕn
6. x : ℝ
7. x ∈ (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i))
8. Legendre(n;x) = r0
9. x ∈ (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i))
10. Legendre(n;x) = r0
⊢ r0 < (r((-1)^(n - i)) * Legendre(n + 1;x))
BY
{ (InstLemma `Legendre-roots-lemma2` [⌜n⌝;⌜z⌝;⌜i⌝;⌜x⌝]⋅ THEN Auto) }

1
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. i : ℕn
6. x : ℝ
7. x ∈ (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i))
8. Legendre(n;x) = r0
9. x ∈ (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i))
10. Legendre(n;x) = r0
11. i1 : ℕn - 1
⊢ Legendre(n - 1;z i1) = r0

2
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. i : ℕn
6. x : ℝ
7. x ∈ (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i))
8. Legendre(n;x) = r0
9. x ∈ (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i))
10. Legendre(n;x) = r0
11. r0 < (r(-1)^n - i * Legendre(n + 1;x))
⊢ r0 < (r((-1)^(n - i)) * Legendre(n + 1;x))

---

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.  i  :  \mBbbN{}n
6.  x  :  \mBbbR{}
7.  x  \mmember{}  (if  i=0  then  r(-1)  else  (z  (i  -  1)),  if  i=n  -  1  then  r1  else  (z  i))
8.  Legendre(n;x)  =  r0
9.  x  \mmember{}  (if  i=0  then  r(-1)  else  (z  (i  -  1)),  if  i=n  -  1  then  r1  else  (z  i))
10.  Legendre(n;x)  =  r0
\mvdash{}  r0  <  (r((-1)\^{}(n  -  i))  *  Legendre(n  +  1;x))


By

---

Latex:
(InstLemma  `Legendre-roots-lemma2`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index