---

Step * of Lemma proj-eq-iff

No Annotations
∀n:ℕ. ∀a,b:ℙ^n.  (a = b ⇐⇒ ↓∃m:{m:ℝ| m ≠ r0} . req-vec(n + 1;a;m*b))
BY
{ Auto }

1
1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. a = b
⊢ ↓∃m:{m:ℝ| m ≠ r0} . req-vec(n + 1;a;m*b)

2
1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. ↓∃m:{m:ℝ| m ≠ r0} . req-vec(n + 1;a;m*b)
⊢ a = b

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\mBbbN{}.  \mforall{}a,b:\mBbbP{}\^{}n.    (a  =  b  \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}\mexists{}m:\{m:\mBbbR{}|  m  \mneq{}  r0\}  .  req-vec(n  +  1;a;m*b))


By

---

Latex:
Auto

---

Home Index