Nuprl Lemma : vec-midpoint_wf

[n:ℕ]. ∀[a,b:ℝ^n].  (vec-midpoint(a;b) ∈ ℝ^n)

Proof

Definitions occuring in Statement :  vec-midpoint: vec-midpoint(a;b) real-vec: ^n nat: uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T vec-midpoint: vec-midpoint(a;b) uimplies: supposing a rneq: x ≠ y guard: {T} or: P ∨ Q all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q less_than: a < b squash: T less_than': less_than'(a;b) true: True prop:
Lemmas referenced :  real-vec-mul_wf real-vec-add_wf rdiv_wf int-to-real_wf rless-int rless_wf real-vec_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality because_Cache hypothesis natural_numberEquality independent_isectElimination inrFormation dependent_functionElimination productElimination independent_functionElimination independent_pairFormation imageMemberEquality baseClosed axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[a,b:\mBbbR{}\^{}n].    (vec-midpoint(a;b)  \mmember{}  \mBbbR{}\^{}n)

Date html generated: 2016_10_28-AM-07_42_32
Last ObjectModification: 2016_09_28-PM-04_08_57

Theory : reals!model!euclidean!geometry

Home Index