---

Step * 2 of Lemma qexp-convex2


1. a : ℚ@i
2. b : ℚ@i
3. 0 ≤ a@i
4. 0 ≤ b@i
5. n : ℕ+@i
6. b ≤ a
⊢ |a - b| ↑ n ≤ |a ↑ n - b ↑ n|
BY
{ ((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.  b  \mleq{}  a
\mvdash{}  |a  -  b|  \muparrow{}  n  \mleq{}  |a  \muparrow{}  n  -  b  \muparrow{}  n|


By

---

Latex:
((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