---

Step * of Lemma qexp-convex2

∀a,b:ℚ.  (((0 ≤ a) ∧ (0 ≤ b)) ⇒ (∀n:ℕ+. (|a - b| ↑ n ≤ |a ↑ n - b ↑ n|)))
BY
{ (Auto THEN (InstLemma `qle_connex` [⌜a⌝;⌜b⌝]⋅ THENA Auto) THEN D -1) }

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

2
1. a : ℚ@i
2. b : ℚ@i
3. 0 ≤ a@i
4. 0 ≤ b@i
5. n : ℕ+@i
6. b ≤ a
⊢ |a - b| ↑ n ≤ |a ↑ n - b ↑ n|

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (InstLemma  `qle\_connex`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1)

---

Home Index