Nuprl Lemma : r2-compass-compass
∀a,b:ℝ^2. ∀c:{c:ℝ^2| a ≠ c} . ∀d:{d:ℝ^2|
↓∃p,q:ℝ^2
((ab=ap ∧ (¬¬(∃w:ℝ^2. (c_w_d ∧ cw=cp)))) ∧ cd=cq ∧ (¬¬(∃w:ℝ^2. (a_w_b ∧ aw=aq))))} .
∃u:{u:ℝ^2| ab=au ∧ cd=cu}
(∃v:{ℝ^2| ((ab=av ∧ cd=cv)
∧ ((↓∃p,q:ℝ^2. ((ab=ap ∧ (↓∃w:ℝ^2. (c_w_d ∧ cw=cp ∧ w ≠ d))) ∧ cd=cq ∧ (↓∃w:ℝ^2. (a_w_b ∧ aw=aq ∧ w ≠ b))))
⇒ (r2-left(u;a;c) ∧ r2-left(v;c;a))))})
Proof
Definitions occuring in Statement :
r2-left: r2-left(p;q;r),
rv-be: a_b_c,
real-vec-sep: a ≠ b,
rv-congruent: ab=cd,
real-vec: ℝ^n,
all: ∀x:A. B[x],
sq_exists: ∃x:{A| B[x]},
exists: ∃x:A. B[x],
not: ¬A,
squash: ↓T,
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
implies: P ⇒ Q,
sq_stable: SqStable(P),
squash: ↓T,
prop: ℙ,
uall: ∀[x:A]. B[x],
nat: ℕ,
le: A ≤ B,
and: P ∧ Q,
less_than': less_than'(a;b),
false: False,
not: ¬A,
so_lambda: λ2x.t[x],
so_apply: x[s],
exists: ∃x:A. B[x],
rv-congruent: ab=cd,
cand: A c∧ B,
subtype_rel: A ⊆r B,
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q),
uimplies: b supposing a,
stable: Stable{P},
or: P ∨ Q,
sq_exists: ∃x:{A| B[x]},
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
rless: x < y,
real-vec-sep: a ≠ b
Lemmas referenced :
rv-compass-compass-lemma,
sq_stable__real-vec-sep,
set_wf,
real-vec_wf,
false_wf,
le_wf,
squash_wf,
exists_wf,
rv-congruent_wf,
not_wf,
rv-be_wf,
real-vec-sep_wf,
req_wf,
real-vec-dist_wf,
rleq_wf,
real_wf,
int-to-real_wf,
stable__rleq,
or_wf,
rv-be-dist,
radd_wf,
radd-preserves-rleq,
rminus_wf,
rleq_functionality,
radd-rminus-both,
radd-rminus-assoc,
real-vec-dist-nonneg,
minimal-double-negation-hyp-elim,
minimal-not-not-excluded-middle,
req_weakening,
req_transitivity,
radd_functionality,
r2-left_wf,
sq_exists_wf,
rless_wf,
sq_stable__rless,
radd-preserves-rless,
rless_functionality
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
setElimination,
rename,
hypothesis,
independent_functionElimination,
because_Cache,
sqequalRule,
imageMemberEquality,
baseClosed,
imageElimination,
isectElimination,
dependent_set_memberEquality,
natural_numberEquality,
independent_pairFormation,
lambdaEquality,
productEquality,
productElimination,
dependent_pairFormation,
applyEquality,
setEquality,
functionEquality,
independent_isectElimination,
voidElimination,
unionElimination
Latex:
\mforall{}a,b:\mBbbR{}\^{}2. \mforall{}c:\{c:\mBbbR{}\^{}2| a \mneq{} c\} . \mforall{}d:\{d:\mBbbR{}\^{}2|
\mdownarrow{}\mexists{}p,q:\mBbbR{}\^{}2
((ab=ap \mwedge{} (\mneg{}\mneg{}(\mexists{}w:\mBbbR{}\^{}2. (c\_w\_d \mwedge{} cw=cp))))
\mwedge{} cd=cq
\mwedge{} (\mneg{}\mneg{}(\mexists{}w:\mBbbR{}\^{}2. (a\_w\_b \mwedge{} aw=aq))))\} .
\mexists{}u:\{u:\mBbbR{}\^{}2| ab=au \mwedge{} cd=cu\}
(\mexists{}v:\{\mBbbR{}\^{}2| ((ab=av \mwedge{} cd=cv)
\mwedge{} ((\mdownarrow{}\mexists{}p,q:\mBbbR{}\^{}2
((ab=ap \mwedge{} (\mdownarrow{}\mexists{}w:\mBbbR{}\^{}2. (c\_w\_d \mwedge{} cw=cp \mwedge{} w \mneq{} d)))
\mwedge{} cd=cq
\mwedge{} (\mdownarrow{}\mexists{}w:\mBbbR{}\^{}2. (a\_w\_b \mwedge{} aw=aq \mwedge{} w \mneq{} b))))
{}\mRightarrow{} (r2-left(u;a;c) \mwedge{} r2-left(v;c;a))))\})
Date html generated:
2017_10_03-AM-11_53_24
Last ObjectModification:
2017_08_13-PM-01_06_59
Theory : reals
Home
Index