Nuprl Lemma : rv-line-circle-lemma0
∀n:ℕ. ∀r:ℝ. ∀p,q:ℝ^n. ((||p|| ≤ r) ⇒ (r0 ≤ (p⋅q - p^2 - ||q - p||^2 * (||p||^2 - r^2))))
Proof
Definitions occuring in Statement :
real-vec-norm: ||x||,
dot-product: x⋅y,
real-vec-sub: X - Y,
real-vec: ℝ^n,
rleq: x ≤ y,
rnexp: x^k1,
rsub: x - y,
rmul: a * b,
int-to-real: r(n),
real: ℝ,
nat: ℕ,
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,
prop: ℙ,
uall: ∀[x:A]. B[x],
uiff: uiff(P;Q),
and: P ∧ Q,
rev_uimplies: rev_uimplies(P;Q),
uimplies: b supposing a,
nat: ℕ,
le: A ≤ B,
less_than': less_than'(a;b),
false: False,
not: ¬A,
req_int_terms: t1 ≡ t2,
top: Top,
rge: x ≥ y,
guard: {T}
Lemmas referenced :
rleq_wf,
real-vec-norm_wf,
real-vec_wf,
real_wf,
nat_wf,
radd-preserves-rleq,
rsub_wf,
rnexp_wf,
int-to-real_wf,
rleq_functionality,
radd_wf,
false_wf,
le_wf,
radd-zero,
rnexp-rleq,
real-vec-norm-nonneg,
itermSubtract_wf,
itermAdd_wf,
itermVar_wf,
req-iff-rsub-is-0,
real_polynomial_null,
real_term_value_sub_lemma,
real_term_value_add_lemma,
real_term_value_var_lemma,
real_term_value_const_lemma,
real-vec-sub_wf,
dot-product_wf,
equal_wf,
rmul_wf,
itermMultiply_wf,
real_term_value_mul_lemma,
rmul_preserves_rleq2,
rnexp2-nonneg,
rmul_comm,
rmul-zero-both,
rleq_functionality_wrt_implies,
rleq_weakening_equal
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
because_Cache,
natural_numberEquality,
productElimination,
independent_isectElimination,
dependent_set_memberEquality,
sqequalRule,
independent_pairFormation,
dependent_functionElimination,
independent_functionElimination,
approximateComputation,
lambdaEquality,
int_eqEquality,
equalityTransitivity,
equalitySymmetry,
intEquality,
isect_memberEquality,
voidElimination,
voidEquality
Latex:
\mforall{}n:\mBbbN{}. \mforall{}r:\mBbbR{}. \mforall{}p,q:\mBbbR{}\^{}n. ((||p|| \mleq{} r) {}\mRightarrow{} (r0 \mleq{} (p\mcdot{}q - p\^{}2 - ||q - p||\^{}2 * (||p||\^{}2 - r\^{}2))))
Date html generated:
2018_05_22-PM-02_29_18
Last ObjectModification:
2018_03_23-PM-04_31_29
Theory : reals
Home
Index