Nuprl Lemma : r2-upper-dimension

  (p ≠ q ∧ q ≠ r ∧ r ≠ p ∧ p-q-r) ∧ q-r-p) ∧ r-p-q))) supposing (ra=rb and qa=qb and pa=pb and a ≠ b)


Definitions occuring in Statement :  rv-between: a-b-c real-vec-sep: a ≠ b rv-congruent: ab=cd real-vec: ^n uimplies: supposing a uall: [x:A]. B[x] not: ¬A and: P ∧ Q natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a not: ¬A implies:  Q false: False all: x:A. B[x] so_lambda: λ2x.t[x] and: P ∧ Q prop: so_apply: x[s] nat: le: A ≤ B less_than': less_than'(a;b) real-vec-dist: d(x;y) subtype_rel: A ⊆B rless: x < y sq_exists: x:{A| B[x]} real-vec-sep: a ≠ b iff: ⇐⇒ Q rev_implies:  Q exists: x:A. B[x] cand: c∧ B or: P ∨ Q less_than: a < b squash: T true: True rneq: x ≠ y guard: {T} rsub: y
Lemmas referenced :  r2-equidistant-implies' vec-midpoint_wf r2-perp_wf real-vec-sub_wf set_wf real-vec_wf req_wf dot-product_wf int-to-real_wf real-vec-norm_wf equal_wf real-vec-sep_wf false_wf le_wf not_wf rv-between_wf rv-congruent_wf real-vec-dist_wf rless_functionality req_weakening real-vec-dist-symmetry exists_wf real_wf req-vec_wf real-vec-add_wf real-vec-mul_wf real-vec-sep_functionality req-vec_weakening rv-between_functionality rv-between-translation rv-between-vec-mul or_wf rless_wf rless-int rmul_wf rabs_wf rsub_wf radd_wf rminus_wf rabs-positive-iff radd-preserves-rless real-vec-dist-translation2 real-vec-dist-vec-mul rmul_functionality rmul-one-both rabs_functionality radd_comm req_transitivity radd_functionality rminus-as-rmul radd-assoc req_inversion rmul-identity1 rmul-distrib2 radd-int rmul-zero-both radd-zero-both radd-ac radd-rminus-both
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin extract_by_obid sqequalHypSubstitution dependent_functionElimination hypothesisEquality independent_functionElimination hypothesis because_Cache isectElimination sqequalRule lambdaEquality productEquality natural_numberEquality equalityTransitivity equalitySymmetry voidElimination dependent_set_memberEquality independent_pairFormation isect_memberEquality applyEquality independent_isectElimination productElimination setElimination rename promote_hyp addLevel impliesFunctionality andLevelFunctionality impliesLevelFunctionality levelHypothesis imageMemberEquality baseClosed unionElimination minusEquality addEquality inlFormation inrFormation

    (\mneg{}(p  \mneq{}  q  \mwedge{}  q  \mneq{}  r  \mwedge{}  r  \mneq{}  p  \mwedge{}  (\mneg{}p-q-r)  \mwedge{}  (\mneg{}q-r-p)  \mwedge{}  (\mneg{}r-p-q)))  supposing 
          (ra=rb  and 
          qa=qb  and 
          pa=pb  and 
          a  \mneq{}  b)

Date html generated: 2017_10_03-PM-00_47_13
Last ObjectModification: 2017_07_28-AM-08_47_17

Theory : reals!model!euclidean!geometry

Home Index