---

Step * of Lemma qexp-convex3

∀a,b:ℚ.  ((((0 ≤ a) ∧ (0 ≤ b)) ∨ ((a ≤ 0) ∧ (b ≤ 0))) ⇒ (∀n:ℕ+. (|a - b| ↑ n ≤ |a ↑ n - b ↑ n|)))
BY
{ xxx(Auto
      THEN D -2
      THEN Auto
      THEN Try (Complete ((BLemma `qexp-convex2` THEN Auto)))
      THEN (Assert |-(a) - -(b)| ↑ n ≤ |-(a) ↑ n - -(b) ↑ n| BY
                  ((BLemma `qexp-convex2` THEN Auto)⋅ THEN QMul ⌜-1⌝ 0⋅ THEN Auto))
      THEN NthHypEq (-1)
      THEN EqCD
      THEN Auto)xxx }

1
.....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 ∈ ℚ

2
.....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| ∈ ℚ

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbQ{}.    ((((0  \mleq{}  a)  \mwedge{}  (0  \mleq{}  b))  \mvee{}  ((a  \mleq{}  0)  \mwedge{}  (b  \mleq{}  0)))  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}\msupplus{}.  (|a  -  b|  \muparrow{}  n  \mleq{}  |a  \muparrow{}  n  -  b  \muparrow{}  n|)))


By

---

Latex:
xxx(Auto
        THEN  D  -2
        THEN  Auto
        THEN  Try  (Complete  ((BLemma  `qexp-convex2`  THEN  Auto)))
        THEN  (Assert  |-(a)  -  -(b)|  \muparrow{}  n  \mleq{}  |-(a)  \muparrow{}  n  -  -(b)  \muparrow{}  n|  BY
                                ((BLemma  `qexp-convex2`  THEN  Auto)\mcdot{}  THEN  QMul  \mkleeneopen{}-1\mkleeneclose{}  0\mcdot{}  THEN  Auto))
        THEN  NthHypEq  (-1)
        THEN  EqCD
        THEN  Auto)xxx

---

Home Index