---

Step * of Lemma rv-congruent_functionality2

∀n:ℕ. ∀a1,a2,b1,b2,c1,c2,d1,d2:ℝ^n.  ((¬a1 ≠ a2) ⇒ (¬b1 ≠ b2) ⇒ (¬c1 ≠ c2) ⇒ (¬d1 ≠ d2) ⇒ (a1b1=c1d1 ⇐⇒ a2b2=c2d2))
BY
{ (InstLemma `rv-congruent_functionality` []
   THEN RepeatFor 13 ((ParallelLast' THENA (Auto THEN BLemma `not-real-vec-sep-iff-eq` THEN Auto)))
   ) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a1,a2,b1,b2,c1,c2,d1,d2:\mBbbR{}\^{}n.
    ((\mneg{}a1  \mneq{}  a2)  {}\mRightarrow{}  (\mneg{}b1  \mneq{}  b2)  {}\mRightarrow{}  (\mneg{}c1  \mneq{}  c2)  {}\mRightarrow{}  (\mneg{}d1  \mneq{}  d2)  {}\mRightarrow{}  (a1b1=c1d1  \mLeftarrow{}{}\mRightarrow{}  a2b2=c2d2))


By

---

Latex:
(InstLemma  `rv-congruent\_functionality`  []
  THEN  RepeatFor  13  ((ParallelLast'  THENA  (Auto  THEN  BLemma  `not-real-vec-sep-iff-eq`  THEN  Auto)))
  )

---

Home Index