Step * of Lemma rv-be-symmetry

n:ℕ. ∀a,b,c:ℝ^n.  (a_b_c  c_b_a)
BY
(Auto THEN RepeatFor (ParallelLast) THEN Auto THEN Try ((BLemma `real-vec-sep-symmetry` THEN Auto))) }

1
1. : ℕ
2. : ℝ^n
3. : ℝ^n
4. : ℝ^n
5. c ≠ b
6. b ≠ a
7. ¬c-b-a
8. a ≠ b
9. b ≠ c
⊢ ¬a-b-c


Latex:


Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b,c:\mBbbR{}\^{}n.    (a\_b\_c  {}\mRightarrow{}  c\_b\_a)


By


Latex:
(Auto
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Auto
  THEN  Try  ((BLemma  `real-vec-sep-symmetry`  THEN  Auto)))




Home Index