---

Step * 2 2 of Lemma cantor-interval-rleq


1. a : ℝ
2. b : ℝ
3. a ≤ b
4. n : ℤ
5. n ≠ 0
6. 0 < n
7. ∀[f:ℕn - 1 ⟶ 𝔹]. ((fst(cantor-interval(a;b;f;n - 1))) ≤ (snd(cantor-interval(a;b;f;n - 1))))
8. f : ℕn ⟶ 𝔹
9. ¬↑(f (n - 1))
10. v1 : ℝ
11. v2 : ℝ
12. cantor-interval(a;b;f;n - 1) = <v1, v2> ∈ (ℝ × ℝ)
13. v1 ≤ v2
⊢ (r(3) * v1) ≤ (2 * v2 + v1)
BY
{ ((RWO  "int-rmul-req" 0 THENA Auto) THEN (nRMul ⌜r(2)⌝ (-1)⋅ THENA Auto) THEN nRAdd ⌜v1⌝ (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  a  \mleq{}  b
4.  n  :  \mBbbZ{}
5.  n  \mneq{}  0
6.  0  <  n
7.  \mforall{}[f:\mBbbN{}n  -  1  {}\mrightarrow{}  \mBbbB{}].  ((fst(cantor-interval(a;b;f;n  -  1)))  \mleq{}  (snd(cantor-interval(a;b;f;n  -  1))))
8.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbB{}
9.  \mneg{}\muparrow{}(f  (n  -  1))
10.  v1  :  \mBbbR{}
11.  v2  :  \mBbbR{}
12.  cantor-interval(a;b;f;n  -  1)  =  <v1,  v2>
13.  v1  \mleq{}  v2
\mvdash{}  (r(3)  *  v1)  \mleq{}  (2  *  v2  +  v1)


By

---

Latex:
((RWO    "int-rmul-req"  0  THENA  Auto)
  THEN  (nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  nRAdd  \mkleeneopen{}v1\mkleeneclose{}  (-1)\mcdot{}
  THEN  Auto)

---

Home Index