---

Step * 1 1 1 1 1 1 1 of Lemma proj-eq-iff


1. n : ℕ
2. a : ℝ^n + 1
3. k1 : ℕn + 1
4. a k1 ≠ r0
5. b : ℝ^n + 1
6. k : ℕn + 1
7. b k ≠ r0
8. ∀i,j:ℕn + 1.  (((a i) * (b j)) = ((b i) * (a j)))
9. ∀j:ℕn + 1. (((a k1) * (b j)) = ((b k1) * (a j)))
10. ((a k1) * (b k)) = ((b k1) * (a k))
⊢ (a k/b k) ≠ r0
BY
{ ((Assert (a k1) * (b k) ≠ r0 BY
          (BLemma `rmul-nonzero` THEN Auto))
   THEN (RWO "-2" (-1) THENA Auto)
   THEN (RWO "rmul-nonzero" (-1) THENA Auto)) }

1
1. n : ℕ
2. a : ℝ^n + 1
3. k1 : ℕn + 1
4. a k1 ≠ r0
5. b : ℝ^n + 1
6. k : ℕn + 1
7. b k ≠ r0
8. ∀i,j:ℕn + 1.  (((a i) * (b j)) = ((b i) * (a j)))
9. ∀j:ℕn + 1. (((a k1) * (b j)) = ((b k1) * (a j)))
10. ((a k1) * (b k)) = ((b k1) * (a k))
11. b k1 ≠ r0 ∧ a k ≠ r0
⊢ (a k/b k) ≠ r0

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbR{}\^{}n  +  1
3.  k1  :  \mBbbN{}n  +  1
4.  a  k1  \mneq{}  r0
5.  b  :  \mBbbR{}\^{}n  +  1
6.  k  :  \mBbbN{}n  +  1
7.  b  k  \mneq{}  r0
8.  \mforall{}i,j:\mBbbN{}n  +  1.    (((a  i)  *  (b  j))  =  ((b  i)  *  (a  j)))
9.  \mforall{}j:\mBbbN{}n  +  1.  (((a  k1)  *  (b  j))  =  ((b  k1)  *  (a  j)))
10.  ((a  k1)  *  (b  k))  =  ((b  k1)  *  (a  k))
\mvdash{}  (a  k/b  k)  \mneq{}  r0


By

---

Latex:
((Assert  (a  k1)  *  (b  k)  \mneq{}  r0  BY
                (BLemma  `rmul-nonzero`  THEN  Auto))
  THEN  (RWO  "-2"  (-1)  THENA  Auto)
  THEN  (RWO  "rmul-nonzero"  (-1)  THENA  Auto))

---

Home Index