---

Step * 2 1 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. v1 : ℝ
10. v2 : ℝ
11. cantor-interval(a;b;f;n - 1) = <v1, v2> ∈ (ℝ × ℝ)
12. ↑(f (n - 1))
13. v1 ≤ v2
⊢ (2 * v1 + v2) ≤ (r(3) * v2)
BY
{ ((RWO  "int-rmul-req" 0 THENA Auto) THEN (nRMul ⌜r(2)⌝ (-1)⋅ THENA Auto) THEN nRAdd ⌜v2⌝ (-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.  v1  :  \mBbbR{}
10.  v2  :  \mBbbR{}
11.  cantor-interval(a;b;f;n  -  1)  =  <v1,  v2>
12.  \muparrow{}(f  (n  -  1))
13.  v1  \mleq{}  v2
\mvdash{}  (2  *  v1  +  v2)  \mleq{}  (r(3)  *  v2)


By

---

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

---

Home Index