---

Step * 2 of Lemma cantor-interval-rless

.....upcase..... 
1. a : ℝ
2. b : ℝ
3. a < b
4. n : ℤ
5. [%2] : 0 < n
6. ∀f:ℕn - 1 ⟶ 𝔹. ((fst(cantor-interval(a;b;f;n - 1))) < (snd(cantor-interval(a;b;f;n - 1))))
⊢ ∀f:ℕn ⟶ 𝔹. ((fst(cantor-interval(a;b;f;n))) < (snd(cantor-interval(a;b;f;n))))
BY
{ (ParallelLast
   THEN Unfold `cantor-interval` 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN AutoSplit
   THEN Fold `cantor-interval` 0
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜cantor-interval(a;b;f;n - 1)⌝⋅ THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN AutoSplit
   THEN Auto
   THEN (RWO "int-rdiv-req" 0 THENA Auto)
   THEN (nRMul ⌜r(3)⌝ 0⋅ THENA Auto)) }

1
1. a : ℝ
2. b : ℝ
3. a < b
4. n : ℤ
5. n ≠ 0
6. [%2] : 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)

2
1. a : ℝ
2. b : ℝ
3. a < b
4. n : ℤ
5. n ≠ 0
6. [%2] : 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)

---

Latex:

---

Latex:
.....upcase..... 
1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  a  <  b
4.  n  :  \mBbbZ{}
5.  [\%2]  :  0  <  n
6.  \mforall{}f:\mBbbN{}n  -  1  {}\mrightarrow{}  \mBbbB{}.  ((fst(cantor-interval(a;b;f;n  -  1)))  <  (snd(cantor-interval(a;b;f;n  -  1))))
\mvdash{}  \mforall{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.  ((fst(cantor-interval(a;b;f;n)))  <  (snd(cantor-interval(a;b;f;n))))


By

---

Latex:
(ParallelLast
  THEN  Unfold  `cantor-interval`  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  Fold  `cantor-interval`  0
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}cantor-interval(a;b;f;n  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  Auto
  THEN  (RWO  "int-rdiv-req"  0  THENA  Auto)
  THEN  (nRMul  \mkleeneopen{}r(3)\mkleeneclose{}  0\mcdot{}  THENA  Auto))

---

Home Index