---

Step * of Lemma Legendre-roots-sq

∀n:ℕ
  (∃z:i:ℕn ⟶ {x:ℝ| (x ∈ (r(-1), r1)) ∧ (Legendre(n;x) = r0) ∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))} 
  [(∀i:ℕn - 1. ((z i) < (z (i + 1))))])
BY
{ (InductionOnNat
   THENL [(D 0 With ⌜λi.r0⌝  THEN Auto)
         ; (ExRepD
            THEN (CaseNat 1 `n'
                  THENL [(D 0 With ⌜λi.r0⌝ 
                          THEN Reduce 0
                          THEN Auto
                          THEN MemTypeCD
                          THEN Auto
                          THEN (Subst' i ~ 0 0 THENA Auto)
                          THEN Reduce 0
                          THEN (D 0 With ⌜5⌝  THENA Auto)
                          THEN Computation
                          THEN Auto)
                        ; ((Assert 2 ≤ n BY
                                  Auto)
                           THEN Thin (-2)
                           THEN Thin 2
                           THEN (Subst' n - 1 - 1 ~ n - 2 -2 THENA 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
⊢ ∃z:i:ℕn ⟶ {x:ℝ| (x ∈ (r(-1), r1)) ∧ (Legendre(n;x) = r0) ∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))} 
[(∀i:ℕn - 1. ((z i) < (z (i + 1))))]

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}
    (\mexists{}z:i:\mBbbN{}n  {}\mrightarrow{}  \{x:\mBbbR{}| 
                              (x  \mmember{}  (r(-1),  r1))
                              \mwedge{}  (Legendre(n;x)  =  r0)
                              \mwedge{}  (r0  <  (r((-1)\^{}(n  -  i))  *  Legendre(n  +  1;x)))\}    [(\mforall{}i:\mBbbN{}n  -  1.  ((z  i)  <  (z  (i  +  1))))]\000C)


By

---

Latex:
(InductionOnNat
  THENL  [(D  0  With  \mkleeneopen{}\mlambda{}i.r0\mkleeneclose{}    THEN  Auto)
              ;  (ExRepD
                    THEN  (CaseNat  1  `n'
                                THENL  [(D  0  With  \mkleeneopen{}\mlambda{}i.r0\mkleeneclose{} 
                                                THEN  Reduce  0
                                                THEN  Auto
                                                THEN  MemTypeCD
                                                THEN  Auto
                                                THEN  (Subst'  i  \msim{}  0  0  THENA  Auto)
                                                THEN  Reduce  0
                                                THEN  (D  0  With  \mkleeneopen{}5\mkleeneclose{}    THENA  Auto)
                                                THEN  Computation
                                                THEN  Auto)
                                            ;  ((Assert  2  \mleq{}  n  BY
                                                                Auto)
                                                  THEN  Thin  (-2)
                                                  THEN  Thin  2
                                                  THEN  (Subst'  n  -  1  -  1  \msim{}  n  -  2  -2  THENA  Auto))]
                              )
                    )]
)

---

Home Index