---

Step * of Lemma rat-point-in-half-cube

No Annotations
∀[k:ℕ]. ∀[x:ℕk ⟶ ℚ]. ∀[c,d:ℚCube(k)].
  (rat-point-in-cube(k;x;c)) supposing (rat-point-in-cube(k;x;d) and (↑is-half-cube(k;d;c)))
BY
{ ((Auto THEN RepeatFor 2 (ParallelLast))
   THEN (RWO "assert-is-half-cube" 5 THENA Auto)
   THEN (D 5 With ⌜i⌝  THENA Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN GenConclTerms Auto [⌜c i⌝;⌜d i⌝;⌜x i⌝]⋅
   THEN All Thin
   THEN D 2
   THEN D 1
   THEN RepUR ``is-half-interval`` 0
   THEN RW assert_pushdownC 0
   THEN Auto
   THEN SplitOrHyps
   THEN Auto) }

1
1. v5 : ℚ
2. v6 : ℚ
3. v3 : ℚ
4. v4 : ℚ
5. v2 : ℚ
6. v3 ≤ v2
7. v2 ≤ v4
8. v3 = qavg(v5;v6) ∈ ℚ
9. v4 = v6 ∈ ℚ
⊢ v5 ≤ v2

2
1. v5 : ℚ
2. v6 : ℚ
3. v3 : ℚ
4. v4 : ℚ
5. v2 : ℚ
6. v3 ≤ v2
7. v2 ≤ v4
8. v3 = v5 ∈ ℚ
9. v4 = qavg(v5;v6) ∈ ℚ
10. v5 ≤ v2
⊢ v2 ≤ v6

---

Latex:

---

Latex:
No  Annotations
\mforall{}[k:\mBbbN{}].  \mforall{}[x:\mBbbN{}k  {}\mrightarrow{}  \mBbbQ{}].  \mforall{}[c,d:\mBbbQ{}Cube(k)].
    (rat-point-in-cube(k;x;c))  supposing  (rat-point-in-cube(k;x;d)  and  (\muparrow{}is-half-cube(k;d;c)))


By

---

Latex:
((Auto  THEN  RepeatFor  2  (ParallelLast))
  THEN  (RWO  "assert-is-half-cube"  5  THENA  Auto)
  THEN  (D  5  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}c  i\mkleeneclose{};\mkleeneopen{}d  i\mkleeneclose{};\mkleeneopen{}x  i\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  D  2
  THEN  D  1
  THEN  RepUR  ``is-half-interval``  0
  THEN  RW  assert\_pushdownC  0
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto)

---

Home Index