Nuprl Lemma : rv-T-iff
∀n:ℕ. ∀a,b,c:ℝ^n. (rv-T(n;a;b;c) ⇐⇒ ¬(a ≠ b ∧ b ≠ c ∧ (¬a-b-c)))
Proof
Definitions occuring in Statement :
rv-T: rv-T(n;a;b;c),
rv-between: a-b-c,
real-vec-sep: a ≠ b,
real-vec: ℝ^n,
nat: ℕ,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
and: P ∧ Q
Definitions unfolded in proof :
rv-T: rv-T(n;a;b;c),
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
not: ¬A,
false: False,
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
rev_implies: P ⇐ Q,
or: P ∨ Q,
uiff: uiff(P;Q),
uimplies: b supposing a,
cand: A c∧ B,
rv-between: a-b-c
Lemmas referenced :
real-vec-sep_wf,
not_wf,
rv-between_wf,
real-vec-be_wf,
real-vec_wf,
nat_wf,
false_wf,
or_wf,
minimal-double-negation-hyp-elim,
minimal-not-not-excluded-middle,
rv-non-strict-between-iff,
not-real-vec-sep-iff-eq,
real-vec-sep_functionality,
req-vec_weakening,
rv-between_functionality,
real-vec-sep-symmetry
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaFormation,
independent_pairFormation,
cut,
thin,
sqequalHypSubstitution,
productElimination,
hypothesis,
independent_functionElimination,
voidElimination,
productEquality,
introduction,
extract_by_obid,
isectElimination,
hypothesisEquality,
functionEquality,
unionElimination,
dependent_functionElimination,
because_Cache,
independent_isectElimination,
addLevel,
impliesFunctionality,
andLevelFunctionality,
impliesLevelFunctionality,
levelHypothesis,
promote_hyp
Latex:
\mforall{}n:\mBbbN{}. \mforall{}a,b,c:\mBbbR{}\^{}n. (rv-T(n;a;b;c) \mLeftarrow{}{}\mRightarrow{} \mneg{}(a \mneq{} b \mwedge{} b \mneq{} c \mwedge{} (\mneg{}a-b-c)))
Date html generated:
2016_10_26-AM-10_45_54
Last ObjectModification:
2016_10_05-PM-00_08_14
Theory : reals
Home
Index