Nuprl Lemma : ip-between-iff2
∀rv:InnerProductSpace. ∀a,b,c:Point.
  (a_b_c 
⇐⇒ (a ≡ c 
⇒ b ≡ c) ∧ (a # c 
⇒ (∃t:ℝ. ((t ∈ [r0, r1]) ∧ b ≡ t*a + r1 - t*c))))
Proof
Definitions occuring in Statement : 
ip-between: a_b_c
, 
inner-product-space: InnerProductSpace
, 
rv-mul: a*x
, 
rv-add: x + y
, 
rccint: [l, u]
, 
i-member: r ∈ I
, 
rsub: x - y
, 
int-to-real: r(n)
, 
real: ℝ
, 
ss-eq: x ≡ y
, 
ss-sep: x # y
, 
ss-point: Point
, 
all: ∀x:A. B[x]
, 
exists: ∃x:A. B[x]
, 
iff: P 
⇐⇒ Q
, 
implies: P 
⇒ Q
, 
and: P ∧ Q
, 
natural_number: $n
Definitions unfolded in proof : 
all: ∀x:A. B[x]
, 
iff: P 
⇐⇒ Q
, 
and: P ∧ Q
, 
implies: P 
⇒ Q
, 
member: t ∈ T
, 
prop: ℙ
, 
uall: ∀[x:A]. B[x]
, 
subtype_rel: A ⊆r B
, 
guard: {T}
, 
uimplies: b supposing a
, 
rev_implies: P 
⇐ Q
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s]
, 
exists: ∃x:A. B[x]
, 
or: P ∨ Q
, 
not: ¬A
, 
false: False
, 
cand: A c∧ B
, 
top: Top
, 
rev_uimplies: rev_uimplies(P;Q)
, 
subtract: n - m
, 
uiff: uiff(P;Q)
, 
less_than': less_than'(a;b)
, 
le: A ≤ B
, 
rccint: [l, u]
, 
i-member: r ∈ I
, 
ss-eq: x ≡ y
, 
rneq: x ≠ y
, 
stable: Stable{P}
, 
rdiv: (x/y)
, 
req_int_terms: t1 ≡ t2
, 
itermConstant: "const"
, 
ip-between: a_b_c
, 
label: ...$L... t
, 
ml-term-to-poly: ml-term-to-poly(t)
, 
nil: []
, 
it: ⋅
, 
has-value: (a)↓
, 
rv-sub: x - y
, 
rv-minus: -x
, 
nat: ℕ
, 
rsub: x - y
, 
true: True
, 
squash: ↓T
Lemmas referenced : 
ss-eq_wf, 
real-vector-space_subtype1, 
inner-product-space_subtype, 
subtype_rel_transitivity, 
inner-product-space_wf, 
real-vector-space_wf, 
separation-space_wf, 
ss-sep_wf, 
ip-between_wf, 
exists_wf, 
real_wf, 
i-member_wf, 
rccint_wf, 
int-to-real_wf, 
rv-add_wf, 
rv-mul_wf, 
rsub_wf, 
ss-point_wf, 
ss-eq_weakening, 
ip-between_functionality, 
ip-between-same, 
minimal-not-not-excluded-middle, 
minimal-double-negation-hyp-elim, 
not_wf, 
or_wf, 
false_wf, 
ss-sep-symmetry, 
ip-between-iff, 
rleq_weakening_rless, 
member_rccint_lemma, 
member_rooint_lemma, 
rv-mul1, 
rsub-int, 
rv-add-0, 
rv-mul0, 
uiff_transitivity, 
ss-eq_inversion, 
req_weakening, 
rv-mul_functionality, 
rv-add_functionality, 
ss-eq_functionality, 
rv-0_wf, 
rleq-int, 
rleq_weakening_equal, 
rv-0-add, 
rless_wf, 
rv-norm_wf, 
rdiv_wf, 
rv-sep-iff, 
rv-sub_wf, 
rv-norm-positive, 
stable__not, 
stable__rleq, 
rv-ip_wf, 
rmul_wf, 
req_wf, 
rleq_wf, 
stable__and, 
rv-sub_functionality, 
rv-norm_functionality, 
req_functionality, 
rabs_wf, 
ip-dist-between-2, 
rabs-of-nonneg, 
rmul_functionality, 
rmul-rinv3, 
req_transitivity, 
req-iff-rsub-is-0, 
real_term_value_var_lemma, 
real_term_value_mul_lemma, 
real_term_value_sub_lemma, 
real_term_value_const_lemma, 
itermVar_wf, 
itermMultiply_wf, 
itermSubtract_wf, 
real_term_polynomial, 
req-implies-req, 
rinv_wf2, 
rmul_preserves_req, 
rsub_functionality, 
i-member_functionality, 
stable__ip-between, 
ip-between-trivial2, 
radd_wf, 
rminus_wf, 
rv-minus_wf, 
real_polynomial_null, 
itermConstant_wf, 
itermMinus_wf, 
evalall-sqequal, 
real_term_value_minus_lemma, 
itermAdd_wf, 
real_term_value_add_lemma, 
rv-mul-linear, 
rv-add-assoc, 
rv-mul-mul, 
rv-mul-1-add, 
radd_functionality, 
rv-add-comm, 
rv-mul-1-add-alt, 
rv-ip_functionality, 
equal_wf, 
rv-norm-mul, 
rnexp2, 
rv-norm-squared, 
req_inversion, 
rv-ip-mul2, 
rv-ip-mul, 
le_wf, 
rnexp_wf, 
radd-zero-both, 
radd-rminus-both, 
radd-ac, 
radd_comm, 
rleq_functionality, 
radd-preserves-rleq, 
iff_weakening_equal, 
rabs-rminus, 
true_wf, 
squash_wf, 
rmul-ac, 
rminus_functionality, 
rmul_comm, 
rmul-assoc, 
rmul_over_rminus
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
lambdaFormation, 
independent_pairFormation, 
cut, 
introduction, 
extract_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
hypothesisEquality, 
applyEquality, 
hypothesis, 
instantiate, 
independent_isectElimination, 
sqequalRule, 
because_Cache, 
productElimination, 
productEquality, 
functionEquality, 
lambdaEquality, 
natural_numberEquality, 
dependent_functionElimination, 
independent_functionElimination, 
unionElimination, 
voidElimination, 
promote_hyp, 
dependent_pairFormation, 
voidEquality, 
isect_memberEquality, 
impliesLevelFunctionality, 
existsLevelFunctionality, 
andLevelFunctionality, 
existsFunctionality, 
impliesFunctionality, 
addLevel, 
inrFormation, 
setEquality, 
rename, 
setElimination, 
intEquality, 
int_eqEquality, 
computeAll, 
minusEquality, 
baseClosed, 
sqleReflexivity, 
mlComputation, 
equalitySymmetry, 
equalityTransitivity, 
dependent_set_memberEquality, 
universeEquality, 
imageMemberEquality, 
imageElimination
Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}a,b,c:Point.
    (a\_b\_c  \mLeftarrow{}{}\mRightarrow{}  (a  \mequiv{}  c  {}\mRightarrow{}  b  \mequiv{}  c)  \mwedge{}  (a  \#  c  {}\mRightarrow{}  (\mexists{}t:\mBbbR{}.  ((t  \mmember{}  [r0,  r1])  \mwedge{}  b  \mequiv{}  t*a  +  r1  -  t*c))))
Date html generated:
2017_10_05-AM-00_02_08
Last ObjectModification:
2017_07_28-AM-08_54_50
Theory : inner!product!spaces
Home
Index