---

Step * 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
⊢ |a - b| ↑ n ≤ |a ↑ n - b ↑ n|
BY
{ (RWO "qabs-difference-symmetry" 0 THEN Auto) }

1
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|

---

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{}  |a  -  b|  \muparrow{}  n  \mleq{}  |a  \muparrow{}  n  -  b  \muparrow{}  n|


By

---

Latex:
(RWO  "qabs-difference-symmetry"  0  THEN  Auto)

---

Home Index