Nuprl Lemma : rv-be-five-segment
∀a,b,c,d,A,B,C,D:ℝ^2. (a ≠ b ⇒ a_b_c ⇒ A_B_C ⇒ ab=AB ⇒ bc=BC ⇒ ad=AD ⇒ bd=BD ⇒ cd=CD)
Proof
Definitions occuring in Statement :
rv-be: a_b_c,
real-vec-sep: a ≠ b,
rv-congruent: ab=cd,
real-vec: ℝ^n,
all: ∀x:A. B[x],
implies: P ⇒ Q,
natural_number: $n
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
nat: ℕ,
le: A ≤ B,
and: P ∧ Q,
less_than': less_than'(a;b),
false: False,
not: ¬A,
implies: P ⇒ Q,
prop: ℙ,
all: ∀x:A. B[x],
stable: Stable{P},
uimplies: b supposing a,
or: P ∨ Q,
rv-be: a_b_c,
cand: A c∧ B,
uiff: uiff(P;Q),
iff: P ⇐⇒ Q,
rv-congruent: ab=cd,
guard: {T},
subtype_rel: A ⊆r B,
rev_implies: P ⇐ Q
Lemmas referenced :
rv-five-segment,
false_wf,
le_wf,
rv-congruent_wf,
rv-be_wf,
real-vec-sep_wf,
real-vec_wf,
stable_rv-congruent,
or_wf,
rv-between_wf,
not_wf,
minimal-double-negation-hyp-elim,
minimal-not-not-excluded-middle,
rv-congruent-preserves-sep,
not-real-vec-sep-iff-eq,
rv-congruent_functionality,
req-vec_weakening,
req_inversion,
real-vec-dist_wf,
rv-congruent-implies-eq,
rv-between_functionality,
rv-between-symmetry,
rv-between-sep,
not-real-vec-sep-refl,
req-vec_inversion
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isectElimination,
thin,
dependent_set_memberEquality,
natural_numberEquality,
sqequalRule,
independent_pairFormation,
lambdaFormation,
hypothesis,
hypothesisEquality,
functionEquality,
because_Cache,
independent_isectElimination,
independent_functionElimination,
unionElimination,
voidElimination,
dependent_functionElimination,
productElimination,
applyEquality
Latex:
\mforall{}a,b,c,d,A,B,C,D:\mBbbR{}\^{}2. (a \mneq{} b {}\mRightarrow{} a\_b\_c {}\mRightarrow{} A\_B\_C {}\mRightarrow{} ab=AB {}\mRightarrow{} bc=BC {}\mRightarrow{} ad=AD {}\mRightarrow{} bd=BD {}\mRightarrow{} cd=CD)
Date html generated:
2017_10_03-AM-11_32_25
Last ObjectModification:
2017_08_11-PM-06_45_29
Theory : reals
Home
Index