---

Step * of Lemma not-rat-cube-third

∀[k:ℕ]. ∀[p:ℝ^k]. ∀[c:ℚCube(k)].
  (¬rat-cube-third(k;p;c) ⇐⇒ in-rat-cube(k;p;c) ∧ (¬¬(∃i:ℕk. (¬rat-interval-third(p i;c i)))))
BY
{ Auto }

1
1. k : ℕ
2. p : ℝ^k
3. c : ℚCube(k)
4. ¬rat-cube-third(k;p;c)
⊢ in-rat-cube(k;p;c)

2
1. k : ℕ
2. p : ℝ^k
3. c : ℚCube(k)
4. ¬rat-cube-third(k;p;c)
⊢ ¬¬(∃i:ℕk. (¬rat-interval-third(p i;c i)))

3
1. k : ℕ
2. p : ℝ^k
3. c : ℚCube(k)
4. in-rat-cube(k;p;c)
5. ¬¬(∃i:ℕk. (¬rat-interval-third(p i;c i)))
⊢ ¬rat-cube-third(k;p;c)

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[p:\mBbbR{}\^{}k].  \mforall{}[c:\mBbbQ{}Cube(k)].
    (\mneg{}rat-cube-third(k;p;c)  \mLeftarrow{}{}\mRightarrow{}  in-rat-cube(k;p;c)  \mwedge{}  (\mneg{}\mneg{}(\mexists{}i:\mBbbN{}k.  (\mneg{}rat-interval-third(p  i;c  i)))))


By

---

Latex:
Auto

---

Home Index