---

Step * 1 1 2 1 1 1 1 2 of Lemma 0-dim-complex-polyhedron


1. k : ℤ
2. [%1] : 0 < k
3. ∀u,a:ℕk - 1 ⟶ ℚ.  ((¬(u = a ∈ (ℕk - 1 ⟶ ℚ))) ⇒ (∃i:ℕk - 1. (¬((u i) = (a i) ∈ ℚ))))
4. u : ℕk ⟶ ℚ
5. a : ℕk ⟶ ℚ
6. ¬(u = a ∈ (ℕk ⟶ ℚ))
⊢ ∃i:ℕk. (¬((u i) = (a i) ∈ ℚ))
BY
{ (Decide ⌜(u (k - 1)) = (a (k - 1)) ∈ ℚ⌝⋅ THEN Auto) }

1
1. k : ℤ
2. [%1] : 0 < k
3. ∀u,a:ℕk - 1 ⟶ ℚ.  ((¬(u = a ∈ (ℕk - 1 ⟶ ℚ))) ⇒ (∃i:ℕk - 1. (¬((u i) = (a i) ∈ ℚ))))
4. u : ℕk ⟶ ℚ
5. a : ℕk ⟶ ℚ
6. ¬(u = a ∈ (ℕk ⟶ ℚ))
7. (u (k - 1)) = (a (k - 1)) ∈ ℚ
⊢ ∃i:ℕk. (¬((u i) = (a i) ∈ ℚ))

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  [\%1]  :  0  <  k
3.  \mforall{}u,a:\mBbbN{}k  -  1  {}\mrightarrow{}  \mBbbQ{}.    ((\mneg{}(u  =  a))  {}\mRightarrow{}  (\mexists{}i:\mBbbN{}k  -  1.  (\mneg{}((u  i)  =  (a  i)))))
4.  u  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbQ{}
5.  a  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbQ{}
6.  \mneg{}(u  =  a)
\mvdash{}  \mexists{}i:\mBbbN{}k.  (\mneg{}((u  i)  =  (a  i)))


By

---

Latex:
(Decide  \mkleeneopen{}(u  (k  -  1))  =  (a  (k  -  1))\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index