Nuprl Lemma : r2-left-cases

a,b:ℝ^2. ∀c:{c:ℝ^2| |a r(-1)*b⋅r(-1)*b| < (||a r(-1)*b|| ||c r(-1)*b||)} .
  (r2-left(a;b;c) ∨ r2-left(a;c;b))


Proof




Definitions occuring in Statement :  r2-left: r2-left(p;q;r) real-vec-norm: ||x|| dot-product: x⋅y real-vec-mul: a*X real-vec-add: Y real-vec: ^n rless: x < y rabs: |x| rmul: b int-to-real: r(n) all: x:A. B[x] or: P ∨ Q set: {x:A| B[x]}  minus: -n natural_number: $n
Definitions unfolded in proof :  rneq: x ≠ y eq_int: (i =z j) sq_exists: x:A [B[x]] rless: x < y nequal: a ≠ b ∈  sq_stable: SqStable(P) req_int_terms: t1 ≡ t2 real-vec-add: Y real-vec-mul: a*X real-vec-sub: Y req-vec: req-vec(n;x;y) assert: b bnot: ¬bb sq_type: SQType(T) bfalse: ff lelt: i ≤ j < k uiff: uiff(P;Q) ifthenelse: if then else fi  btrue: tt it: unit: Unit bool: 𝔹 int_seg: {i..j-} real-vec: ^n rminus: -(x) guard: {T} top: Top satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] int-to-real: r(n) decidable: Dec(P) true: True squash: T less_than: a < b nat_plus: + real: subtype_rel: A ⊆B rev_implies:  Q iff: ⇐⇒ Q uimplies: supposing a or: P ∨ Q so_apply: x[s] so_lambda: λ2x.t[x] implies:  Q not: ¬A false: False less_than': less_than'(a;b) and: P ∧ Q le: A ≤ B nat: uall: [x:A]. B[x] prop: member: t ∈ T r2-left: r2-left(p;q;r) all: x:A. B[x]
Lemmas referenced :  rabs-positive-iff real_term_value_minus_lemma rless-implies-rless nat_plus_properties rnexp2 real-vec-norm-squared rnexp-rmul r2-dot-product rnexp_functionality req_transitivity rnexp-rless rabs-of-nonneg rabs-rnexp req_inversion rnexp0 rnexp2-nonneg rnexp_wf zero-rleq-rabs square-rless-implies real-vec-norm_functionality rmul_functionality dot-product_functionality sq_stable__rless real_term_value_const_lemma real_term_value_mul_lemma real_term_value_var_lemma real_term_value_add_lemma real_term_value_sub_lemma real_polynomial_null req-iff-rsub-is-0 itermSubtract_wf rsub_wf radd_wf r2-det-is-dot-product rabs_functionality neg_assert_of_eq_int assert-bnot bool_subtype_base subtype_base_sq bool_cases_sqequal eqff_to_assert lelt_wf int_seg_wf subtype_rel_self assert_of_eq_int eqtt_to_assert bool_wf eq_int_wf real-vec-sub_wf int_term_value_minus_lemma itermMinus_wf int_formula_prop_wf int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_term_value_mul_lemma int_term_value_add_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformeq_wf itermVar_wf itermConstant_wf itermMultiply_wf itermAdd_wf intformless_wf intformnot_wf intformand_wf full-omega-unsat rless-iff2 decidable__lt int-value-type set-value-type equal_wf less_than_wf real_wf req_weakening rless_functionality or_wf rminus_wf r2-det_wf r2-det-antisymmetry real-vec-norm_wf rmul_wf int-to-real_wf real-vec-mul_wf real-vec-add_wf dot-product_wf rabs_wf rless_wf le_wf false_wf real-vec_wf set_wf
Rules used in proof :  imageElimination cumulativity instantiate promote_hyp functionEquality equalityElimination inrFormation voidEquality voidElimination isect_memberEquality int_eqEquality approximateComputation multiplyEquality addEquality dependent_pairFormation inlFormation unionElimination equalitySymmetry equalityTransitivity cutEval baseClosed imageMemberEquality applyEquality intEquality independent_functionElimination productElimination independent_isectElimination dependent_functionElimination orFunctionality addLevel rename setElimination minusEquality because_Cache lambdaEquality hypothesisEquality hypothesis independent_pairFormation sqequalRule natural_numberEquality dependent_set_memberEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}a,b:\mBbbR{}\^{}2.  \mforall{}c:\{c:\mBbbR{}\^{}2|  |a  +  r(-1)*b\mcdot{}c  +  r(-1)*b|  <  (||a  +  r(-1)*b||  *  ||c  +  r(-1)*b||)\}  .
    (r2-left(a;b;c)  \mvee{}  r2-left(a;c;b))



Date html generated: 2018_05_22-PM-02_38_24
Last ObjectModification: 2018_05_21-AM-00_50_59

Theory : reals


Home Index