---

Step * 1 1 1 1 2 1 1 1 1 1 1 of Lemma exp-convex


1. c : ℕ
2. v : ℕ
3. v1 : ℕ
4. m : ℕ
5. c < v
6. c^m < v1
7. (v * v1) ≤ (c * c^m)
⊢ False
BY
{ xxxMul ⌜v⌝ (-2)⋅xxx }

1
1. c : ℕ
2. v : ℕ
3. v1 : ℕ
4. m : ℕ
5. c < v
6. c^m < v1
7. (v * v1) ≤ (c * c^m)
8. v * c^m < v * v1
⊢ False

---

Latex:

---

Latex:

1.  c  :  \mBbbN{}
2.  v  :  \mBbbN{}
3.  v1  :  \mBbbN{}
4.  m  :  \mBbbN{}
5.  c  <  v
6.  c\^{}m  <  v1
7.  (v  *  v1)  \mleq{}  (c  *  c\^{}m)
\mvdash{}  False


By

---

Latex:
xxxMul  \mkleeneopen{}v\mkleeneclose{}  (-2)\mcdot{}xxx

---

Home Index