---

Step * 1 of Lemma qexp-convex


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))
BY
{ ((InstLemma `qexp_preserves_qle` [⌜b⌝;⌜a⌝;⌜n⌝]⋅ THENA Auto)
   THEN (QMul ⌜b⌝ (-1)⋅ THENA Auto)
   THEN RWO "-1<" 0
   THEN Auto
   THEN QAdd ⌜-(b ↑ n * b)⌝ 0⋅
   THEN Auto
   THEN (InstLemma `qmul_preserves_qle2` [⌜b⌝;⌜a⌝;⌜b ↑ n⌝]⋅ THEN Auto)⋅)⋅ }

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}@i
2.  b  :  \mBbbQ{}@i
3.  0  \mleq{}  b@i
4.  b  \mleq{}  a@i
5.  n  :  \mBbbZ{}@i
6.  0  <  n
\mvdash{}  (2  *  b  \muparrow{}  n  *  b)  \mleq{}  ((b  \muparrow{}  n  *  a)  +  (a  \muparrow{}  n  *  b))


By

---

Latex:
((InstLemma  `qexp\_preserves\_qle`  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (QMul  \mkleeneopen{}b\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  RWO  "-1<"  0
  THEN  Auto
  THEN  QAdd  \mkleeneopen{}-(b  \muparrow{}  n  *  b)\mkleeneclose{}  0\mcdot{}
  THEN  Auto
  THEN  (InstLemma  `qmul\_preserves\_qle2`  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b  \muparrow{}  n\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{})\mcdot{}

---

Home Index