---

Step * of Lemma qexp-difference-bound

∀[a,b:ℚ].  ∀n:ℕ+. (|a ↑ n - b ↑ n| ≤ (|a - b| * n * qmax(|a|;|b|) ↑ n - 1))
BY
{ xxx(xxxAutoxxx
      THEN (RWW "qexp-difference-factor qabs-qmul" 0 THENA Auto)
      THEN (BLemma `qmul_preserves_qle2` THENA Auto)
      THEN Try ((BLemma `qabs-nonneg` THEN Auto)))xxx }

1
1. a : ℚ
2. b : ℚ
3. n : ℕ+
⊢ |Σ0 ≤ i < n. a ↑ i * b ↑ n - i + 1| ≤ (n * qmax(|a|;|b|) ↑ n - 1)

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbQ{}].    \mforall{}n:\mBbbN{}\msupplus{}.  (|a  \muparrow{}  n  -  b  \muparrow{}  n|  \mleq{}  (|a  -  b|  *  n  *  qmax(|a|;|b|)  \muparrow{}  n  -  1))


By

---

Latex:
xxx(xxxAutoxxx
        THEN  (RWW  "qexp-difference-factor  qabs-qmul"  0  THENA  Auto)
        THEN  (BLemma  `qmul\_preserves\_qle2`  THENA  Auto)
        THEN  Try  ((BLemma  `qabs-nonneg`  THEN  Auto)))xxx

---

Home Index