---

Step * 1 1 of Lemma qexp-convex2


1. a : ℚ@i
2. b : ℚ@i
3. 0 ≤ a@i
4. 0 ≤ b@i
5. n : ℕ+@i
6. a ≤ b
⊢ |b - a| ↑ n ≤ |b ↑ n - a ↑ n|
BY
{ (SwapVars `a' `b'
   THEN ((RWO "qabs-of-nonneg" 0
          THENA (Auto
                 THEN Try ((QAdd ⌜b⌝ 0⋅ THEN Complete (Auto)))
                 THEN (QAdd ⌜b ↑ n⌝ 0⋅ THEN Auto)⋅
                 THEN BLemma `qexp_preserves_qle`
                 THEN Auto)
          )
         THEN BLemma `qexp-convex`
         THEN Auto)⋅
   ) }

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}@i
2.  b  :  \mBbbQ{}@i
3.  0  \mleq{}  a@i
4.  0  \mleq{}  b@i
5.  n  :  \mBbbN{}\msupplus{}@i
6.  a  \mleq{}  b
\mvdash{}  |b  -  a|  \muparrow{}  n  \mleq{}  |b  \muparrow{}  n  -  a  \muparrow{}  n|


By

---

Latex:
(SwapVars  `a'  `b'
  THEN  ((RWO  "qabs-of-nonneg"  0
                THENA  (Auto
                              THEN  Try  ((QAdd  \mkleeneopen{}b\mkleeneclose{}  0\mcdot{}  THEN  Complete  (Auto)))
                              THEN  (QAdd  \mkleeneopen{}b  \muparrow{}  n\mkleeneclose{}  0\mcdot{}  THEN  Auto)\mcdot{}
                              THEN  BLemma  `qexp\_preserves\_qle`
                              THEN  Auto)
                )
              THEN  BLemma  `qexp-convex`
              THEN  Auto)\mcdot{}
  )

---

Home Index