---

Step * of Lemma realvec-ibs-property

∀k:ℕ. ∀p:ℝ^k.
  ((r0 < ||p|| ⇐⇒ ∃n:ℕ. ((realvec-ibs(k;p) n) = 1 ∈ ℤ))
  ∧ (∀n:ℕ. (((realvec-ibs(k;p) n) = 0 ∈ ℤ) ⇒ (||p|| ≤ (r(4)/r(n + 1))))))
BY
{ ((Intros
    THEN (Assert r0 ≤ ||p|| BY
                Auto)
    THEN (Assert |r0 - ||p||| = ||p|| BY
                (nRNorm 0 THEN RWO "rabs-rminus" 0 THEN InstLemma `rabs-of-nonneg` [⌜||p||⌝]⋅ THEN Auto)))
   THEN Unfold `realvec-ibs` 0
   THEN (InstLemma `rless_ibs_property` [⌜r0⌝;⌜||p||⌝]⋅ THENA Auto)
   THEN RepeatFor 3 (ParallelLast)
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}p:\mBbbR{}\^{}k.
    ((r0  <  ||p||  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  ((realvec-ibs(k;p)  n)  =  1))
    \mwedge{}  (\mforall{}n:\mBbbN{}.  (((realvec-ibs(k;p)  n)  =  0)  {}\mRightarrow{}  (||p||  \mleq{}  (r(4)/r(n  +  1))))))


By

---

Latex:
((Intros
    THEN  (Assert  r0  \mleq{}  ||p||  BY
                            Auto)
    THEN  (Assert  |r0  -  ||p|||  =  ||p||  BY
                            (nRNorm  0
                              THEN  RWO  "rabs-rminus"  0
                              THEN  InstLemma  `rabs-of-nonneg`  [\mkleeneopen{}||p||\mkleeneclose{}]\mcdot{}
                              THEN  Auto)))
  THEN  Unfold  `realvec-ibs`  0
  THEN  (InstLemma  `rless\_ibs\_property`  [\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}||p||\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  3  (ParallelLast)
  THEN  D  -1
  THEN  Auto)

---

Home Index