---

Step * 1 of Lemma qexp-convex3

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

---

Latex:

---

Latex:
.....subterm.....  T:t
1: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  -  b|  \muparrow{}  n  =  |-(a)  -  -(b)|  \muparrow{}  n


By

---

Latex:
(EqCD
  THEN  Auto
  THEN  (RW  (AddrC  [2]  (LemmaC  `qabs-difference-symmetry`))  0  THENA  Auto)
  THEN  EqCD
  THEN  Auto
  THEN  QNorm  0)

---

Home Index