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