Nuprl Lemma : i-member-convex
∀I:Interval. ∀a,b:ℝ. ((a ∈ I) ⇒ (b ∈ I) ⇒ (∀t:ℝ. ((r0 ≤ t) ⇒ (t ≤ r1) ⇒ ((t * a) + ((r1 - t) * b) ∈ I))))
Proof
Definitions occuring in Statement :
i-member: r ∈ I,
interval: Interval,
rleq: x ≤ y,
rsub: x - y,
rmul: a * b,
radd: a + b,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x],
prop: ℙ
Lemmas referenced :
i-member-between,
rmin_wf,
rmax_wf,
rmin-i-member,
rmax-i-member,
radd_wf,
rmul_wf,
rsub_wf,
int-to-real_wf,
rmin-lb-convex,
rmax-ub-convex,
rleq_wf,
real_wf,
i-member_wf,
interval_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
isectElimination,
hypothesis,
independent_functionElimination,
natural_numberEquality
Latex:
\mforall{}I:Interval. \mforall{}a,b:\mBbbR{}.
((a \mmember{} I) {}\mRightarrow{} (b \mmember{} I) {}\mRightarrow{} (\mforall{}t:\mBbbR{}. ((r0 \mleq{} t) {}\mRightarrow{} (t \mleq{} r1) {}\mRightarrow{} ((t * a) + ((r1 - t) * b) \mmember{} I))))
Date html generated:
2018_05_22-PM-02_05_36
Last ObjectModification:
2017_10_20-PM-04_50_38
Theory : reals
Home
Index