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 ≠ b 
⇒ (¬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: P 
⇒ Q
, 
and: P ∧ Q
Definitions unfolded in proof : 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
and: P ∧ Q
, 
cand: A c∧ B
, 
member: t ∈ T
, 
uall: ∀[x:A]. B[x]
, 
uimplies: b 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