---

Step * of Lemma rat-cube-third-half

∀k:ℕ. ∀p:ℝ^k. ∀c:ℚCube(k).  (rat-cube-third(k;p;c) ⇒ (∀h:ℚCube(k). ((↑is-half-cube(k;h;c)) ⇒ rat-cube-third(k;p;h))))
BY
{ ((Auto THEN ParallelOp -3 THEN Intro THEN (FLemma `in-rat-half-cube` [-2;-1] THENA Auto) THEN ThinTrivial)
   THEN (RWO "assert-is-half-cube" (-4) THENA Auto)
   THEN (ParallelLast THEN MoveToConcl  (-1))
   THEN RepeatFor 3 (((D -3 With ⌜i⌝  THENA Auto) THEN MoveToConcl  (-1)))
   THEN GenConclTerms Auto [⌜c i⌝;⌜h i⌝;⌜p i⌝]⋅
   THEN All Thin
   THEN RenameVar `r' (-1)
   THEN D 1
   THEN D -2
   THEN RepUR ``rat-interval-third is-half-interval`` 0
   THEN RW assert_pushdownC 0
   THEN Auto
   THEN ((Assert rat2real(v2) ≤ rat2real(v3) BY Auto) THEN (RWO "rleq-rat2real" (-1) THENA Auto))
   THEN ((Assert rat2real(v4) ≤ rat2real(v5) BY Auto) THEN (RWO "rleq-rat2real" (-1) THENA Auto))
   THEN (Assert ((rat2real(v2) + (r(2) * rat2real(v3))/r(3)) ≤ rat2real(qavg(v2;v3))) ⇒ (v2 = v3 ∈ ℚ) BY
               (ThinVar `r'
                THEN Auto
                THEN (nRMul ⌜r(2)⌝ (-1)⋅ THENA Auto)
                THEN (RWO "rat2real-qavg-2" (-1) THENA Auto)
                THEN (nRMul ⌜r(3)⌝ (-1)⋅ THENA Auto)
                THEN (nRAdd ⌜-((r(2) * rat2real(v2)) + (r(3) * rat2real(v3)))⌝ (-1)⋅ THENA Auto)
                THEN RWO "rleq-rat2real" (-1)
                THEN Auto))) }

1
1. v2 : ℚ
2. v3 : ℚ
3. v4 : ℚ
4. v5 : ℚ
5. r : ℝ
6. ((v4 = v2 ∈ ℚ) ∧ (v5 = qavg(v2;v3) ∈ ℚ)) ∨ ((v4 = qavg(v2;v3) ∈ ℚ) ∧ (v5 = v3 ∈ ℚ))
7. rat2real(v4) ≤ r
8. r ≤ rat2real(v5)
9. rat2real(v2) ≤ r
10. r ≤ rat2real(v3)
11. (r = ((r(2) * rat2real(v2)) + rat2real(v3)/r(3))) ∨ (r = (rat2real(v2) + (r(2) * rat2real(v3))/r(3)))
12. v2 ≤ v3
13. v4 ≤ v5
14. ((rat2real(v2) + (r(2) * rat2real(v3))/r(3)) ≤ rat2real(qavg(v2;v3))) ⇒ (v2 = v3 ∈ ℚ)
⊢ (r = ((r(2) * rat2real(v4)) + rat2real(v5)/r(3))) ∨ (r = (rat2real(v4) + (r(2) * rat2real(v5))/r(3)))

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}p:\mBbbR{}\^{}k.  \mforall{}c:\mBbbQ{}Cube(k).
    (rat-cube-third(k;p;c)  {}\mRightarrow{}  (\mforall{}h:\mBbbQ{}Cube(k).  ((\muparrow{}is-half-cube(k;h;c))  {}\mRightarrow{}  rat-cube-third(k;p;h))))


By

---

Latex:
((Auto
    THEN  ParallelOp  -3
    THEN  Intro
    THEN  (FLemma  `in-rat-half-cube`  [-2;-1]  THENA  Auto)
    THEN  ThinTrivial)
  THEN  (RWO  "assert-is-half-cube"  (-4)  THENA  Auto)
  THEN  (ParallelLast  THEN  MoveToConcl    (-1))
  THEN  RepeatFor  3  (((D  -3  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)  THEN  MoveToConcl    (-1)))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}c  i\mkleeneclose{};\mkleeneopen{}h  i\mkleeneclose{};\mkleeneopen{}p  i\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  RenameVar  `r'  (-1)
  THEN  D  1
  THEN  D  -2
  THEN  RepUR  ``rat-interval-third  is-half-interval``  0
  THEN  RW  assert\_pushdownC  0
  THEN  Auto
  THEN  ((Assert  rat2real(v2)  \mleq{}  rat2real(v3)  BY  Auto)  THEN  (RWO  "rleq-rat2real"  (-1)  THENA  Auto))
  THEN  ((Assert  rat2real(v4)  \mleq{}  rat2real(v5)  BY  Auto)  THEN  (RWO  "rleq-rat2real"  (-1)  THENA  Auto))
  THEN  (Assert  ((rat2real(v2)  +  (r(2)  *  rat2real(v3))/r(3))  \mleq{}  rat2real(qavg(v2;v3)))  {}\mRightarrow{}  (v2  =  v3)  BY
                          (ThinVar  `r'
                            THEN  Auto
                            THEN  (nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
                            THEN  (RWO  "rat2real-qavg-2"  (-1)  THENA  Auto)
                            THEN  (nRMul  \mkleeneopen{}r(3)\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
                            THEN  (nRAdd  \mkleeneopen{}-((r(2)  *  rat2real(v2))  +  (r(3)  *  rat2real(v3)))\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
                            THEN  RWO  "rleq-rat2real"  (-1)
                            THEN  Auto)))

---

Home Index