---

Step * of Lemma rv-between_functionality2

∀n:ℕ. ∀a1,a2,b1,b2,c1,c2:ℝ^n.  ((¬a1 ≠ a2) ⇒ (¬b1 ≠ b2) ⇒ (¬c1 ≠ c2) ⇒ (a1-b1-c1 ⇐⇒ a2-b2-c2))
BY
{ (InstLemma `rv-between_functionality` []
   THEN RepeatFor 10 ((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:\mBbbR{}\^{}n.    ((\mneg{}a1  \mneq{}  a2)  {}\mRightarrow{}  (\mneg{}b1  \mneq{}  b2)  {}\mRightarrow{}  (\mneg{}c1  \mneq{}  c2)  {}\mRightarrow{}  (a1-b1-c1  \mLeftarrow{}{}\mRightarrow{}  a2-b2-c2))


By

---

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

---

Home Index