---

Step * of Lemma 0-dim-complex-polyhedron

∀k:ℕ. ∀K:0-dim-complex. ∀x:|K|.  ∃i:ℕ||K||. req-vec(k;x;λj.rat2real(fst((K[i] j))))
BY
{ (Auto
   THEN (Assert ¬¬(∃i:ℕ||K||. req-vec(k;x;λj.rat2real(fst((K[i] j))))) BY
               ((Assert ¬¬(∃i:ℕ||K||. in-rat-cube(k;x;K[i])) BY
                       (D -1 THEN Auto))
                THEN (DVar `K' THENW Auto)
                THEN RepeatFor 3 (ParallelLast)
                THEN (D 0 THENA Auto)
                THEN (D -2 With ⌜i@0⌝  THENA Auto)
                THEN Reduce 0
                THEN Auto
                THEN (D 5 With ⌜i⌝  THENA Auto)
                THEN (RWO  "rat-cube-dimension-zero" (-1) THENA Auto)
                THEN (D -1 With ⌜i@0⌝  THENA Auto)
                THEN RepeatFor 3 (MoveToConcl (-1))
                THEN (GenConclTerm ⌜K[i] i@0⌝⋅ THENA Auto)
                THEN D -2
                THEN Reduce 0
                THEN Auto
                THEN RationalElim⌜v1⌝⋅
                THEN EAuto 1))
   ) }

1
1. k : ℕ
2. K : 0-dim-complex
3. x : |K|
4. ¬¬(∃i:ℕ||K||. req-vec(k;x;λj.rat2real(fst((K[i] j)))))
⊢ ∃i:ℕ||K||. req-vec(k;x;λj.rat2real(fst((K[i] j))))

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}K:0-dim-complex.  \mforall{}x:|K|.    \mexists{}i:\mBbbN{}||K||.  req-vec(k;x;\mlambda{}j.rat2real(fst((K[i]  j))))


By

---

Latex:
(Auto
  THEN  (Assert  \mneg{}\mneg{}(\mexists{}i:\mBbbN{}||K||.  req-vec(k;x;\mlambda{}j.rat2real(fst((K[i]  j)))))  BY
                          ((Assert  \mneg{}\mneg{}(\mexists{}i:\mBbbN{}||K||.  in-rat-cube(k;x;K[i]))  BY
                                          (D  -1  THEN  Auto))
                            THEN  (DVar  `K'  THENW  Auto)
                            THEN  RepeatFor  3  (ParallelLast)
                            THEN  (D  0  THENA  Auto)
                            THEN  (D  -2  With  \mkleeneopen{}i@0\mkleeneclose{}    THENA  Auto)
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  (D  5  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
                            THEN  (RWO    "rat-cube-dimension-zero"  (-1)  THENA  Auto)
                            THEN  (D  -1  With  \mkleeneopen{}i@0\mkleeneclose{}    THENA  Auto)
                            THEN  RepeatFor  3  (MoveToConcl  (-1))
                            THEN  (GenConclTerm  \mkleeneopen{}K[i]  i@0\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  D  -2
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  RationalElim\mkleeneopen{}v1\mkleeneclose{}\mcdot{}
                            THEN  EAuto  1))
  )

---

Home Index