Nuprl Lemma : rv-pos-angle-implies

n:ℕ. ∀a,b,c:ℝ^n.
  (rv-pos-angle(n;a;b;c)
   (rv-pos-angle(n;c;b;a)
     ∧ rv-pos-angle(n;c;a;b)
     ∧ a ≠ c
     ∧ a-b-c)
     ∧ (∀z:ℝ^n. (z ≠  rv-pos-angle(n;a;b;z))  rv-pos-angle(n;z;b;c)))))


Proof




Definitions occuring in Statement :  rv-between: a-b-c real-vec-sep: a ≠ b rv-pos-angle: rv-pos-angle(n;a;b;c) real-vec: ^n nat: all: x:A. B[x] not: ¬A implies:  Q and: P ∧ Q
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q and: P ∧ Q cand: c∧ B member: t ∈ T uall: [x:A]. B[x] uimplies: supposing a prop:
Lemmas referenced :  rv-pos-angle-symmetry rv-pos-angle-permute rv-pos-angle-implies-separated rv-pos-angle-not-between rv-pos-angle-shift not_wf rv-pos-angle_wf real-vec-sep_wf real-vec_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination hypothesis independent_pairFormation because_Cache isectElimination independent_isectElimination

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b,c:\mBbbR{}\^{}n.
    (rv-pos-angle(n;a;b;c)
    {}\mRightarrow{}  (rv-pos-angle(n;c;b;a)
          \mwedge{}  rv-pos-angle(n;c;a;b)
          \mwedge{}  a  \mneq{}  c
          \mwedge{}  (\mneg{}a-b-c)
          \mwedge{}  (\mforall{}z:\mBbbR{}\^{}n.  (z  \mneq{}  b  {}\mRightarrow{}  (\mneg{}rv-pos-angle(n;a;b;z))  {}\mRightarrow{}  rv-pos-angle(n;z;b;c)))))



Date html generated: 2017_10_03-AM-11_07_17
Last ObjectModification: 2017_03_02-PM-05_32_36

Theory : reals


Home Index