---

Step * of Lemma reg-seq-adjust-property

∀[n:ℕ+]. ∀[x:ℝ].  ∀m:ℕ+. (m ≤ (n * |reg-seq-adjust(n;x) m|)) supposing 5 ≤ |x n|
BY
{ TACTIC:(Intros
          THEN RepUR ``reg-seq-adjust`` 0
          THEN Unhide
          THEN Auto
          THEN AutoSplit
          THEN Try ((BLemma `rnonzero-lemma1` THEN Auto))
          THEN RWO "absval_pos" 0
          THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[x:\mBbbR{}].    \mforall{}m:\mBbbN{}\msupplus{}.  (m  \mleq{}  (n  *  |reg-seq-adjust(n;x)  m|))  supposing  5  \mleq{}  |x  n|


By

---

Latex:
TACTIC:(Intros
                THEN  RepUR  ``reg-seq-adjust``  0
                THEN  Unhide
                THEN  Auto
                THEN  AutoSplit
                THEN  Try  ((BLemma  `rnonzero-lemma1`  THEN  Auto))
                THEN  RWO  "absval\_pos"  0
                THEN  Auto)

---

Home Index