---

Step * of Lemma qexp-convex

∀a,b:ℚ.  ((0 ≤ b) ⇒ (b ≤ a) ⇒ (∀n:ℕ+. (a - b ↑ n ≤ (a ↑ n - b ↑ n))))
BY
{ (InductionOnNat
   THEN Auto
   THEN RWO "exp_unroll_q" 0⋅
   THEN (Reduce 0 THEN Auto)
   THEN Try (((RWO "exp_zero_q" 0⋅ THEN Auto) THEN QNorm 0 THEN Auto))
   THEN (Subst' (n + 1) - 1 ~ n 0 THENA Auto)
   THEN (RWO "-1" 0 THENA (Auto THEN Try ((BLemma `qexp-nonneg` THEN Auto)) THEN QAdd ⌜b⌝ 0⋅ THEN Auto))
   THEN (Thin (-1)
         THEN QNorm 0
         THEN QAdd ⌜(b ↑ n * b) - a ↑ n * a⌝ 0⋅
         THEN Auto
         THEN QAdd ⌜(b ↑ n * a) + (a ↑ n * b)⌝ 0⋅
         THEN Auto)⋅) }

1
1. a : ℚ@i
2. b : ℚ@i
3. 0 ≤ b@i
4. b ≤ a@i
5. n : ℤ@i
6. 0 < n
⊢ (2 * b ↑ n * b) ≤ ((b ↑ n * a) + (a ↑ n * b))

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbQ{}.    ((0  \mleq{}  b)  {}\mRightarrow{}  (b  \mleq{}  a)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}\msupplus{}.  (a  -  b  \muparrow{}  n  \mleq{}  (a  \muparrow{}  n  -  b  \muparrow{}  n))))


By

---

Latex:
(InductionOnNat
  THEN  Auto
  THEN  RWO  "exp\_unroll\_q"  0\mcdot{}
  THEN  (Reduce  0  THEN  Auto)
  THEN  Try  (((RWO  "exp\_zero\_q"  0\mcdot{}  THEN  Auto)  THEN  QNorm  0  THEN  Auto))
  THEN  (Subst'  (n  +  1)  -  1  \msim{}  n  0  THENA  Auto)
  THEN  (RWO  "-1"  0
              THENA  (Auto  THEN  Try  ((BLemma  `qexp-nonneg`  THEN  Auto))  THEN  QAdd  \mkleeneopen{}b\mkleeneclose{}  0\mcdot{}  THEN  Auto)
              )
  THEN  (Thin  (-1)
              THEN  QNorm  0
              THEN  QAdd  \mkleeneopen{}(b  \muparrow{}  n  *  b)  -  a  \muparrow{}  n  *  a\mkleeneclose{}  0\mcdot{}
              THEN  Auto
              THEN  QAdd  \mkleeneopen{}(b  \muparrow{}  n  *  a)  +  (a  \muparrow{}  n  *  b)\mkleeneclose{}  0\mcdot{}
              THEN  Auto)\mcdot{})

---

Home Index