---

Step * 2 of Lemma qexp-convex3

.....subterm..... T:t
2:n
1. a : ℚ
2. b : ℚ
3. a ≤ 0
4. b ≤ 0
5. n : ℕ+
6. |-(a) - -(b)| ↑ n ≤ |-(a) ↑ n - -(b) ↑ n|
⊢ |a ↑ n - b ↑ n| = |-(a) ↑ n - -(b) ↑ n| ∈ ℚ
BY
{ (RWO "qexp-qminus" 0
   THEN Auto
   THEN AutoSplit
   THEN (RW (AddrC [3] (LemmaC `qabs-qminus`)) 0 THENA Auto)
   THEN EqCD
   THEN Auto
   THEN QNorm 0) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
3.  a  \mleq{}  0
4.  b  \mleq{}  0
5.  n  :  \mBbbN{}\msupplus{}
6.  |-(a)  -  -(b)|  \muparrow{}  n  \mleq{}  |-(a)  \muparrow{}  n  -  -(b)  \muparrow{}  n|
\mvdash{}  |a  \muparrow{}  n  -  b  \muparrow{}  n|  =  |-(a)  \muparrow{}  n  -  -(b)  \muparrow{}  n|


By

---

Latex:
(RWO  "qexp-qminus"  0
  THEN  Auto
  THEN  AutoSplit
  THEN  (RW  (AddrC  [3]  (LemmaC  `qabs-qminus`))  0  THENA  Auto)
  THEN  EqCD
  THEN  Auto
  THEN  QNorm  0)

---

Home Index