Nuprl Lemma : rcp-mul2

[a,b:ℝ^3]. ∀[c:ℝ].  req-vec(3;(a c*b);c*(a b))


Proof




Definitions occuring in Statement :  rcp: (a b) real-vec-mul: a*X req-vec: req-vec(n;x;y) real-vec: ^n real: uall: [x:A]. B[x] natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T req-vec: req-vec(n;x;y) all: x:A. B[x] rcp: (a b) real-vec-mul: a*X int_seg: {i..j-} decidable: Dec(P) or: P ∨ Q uimplies: supposing a sq_type: SQType(T) implies:  Q guard: {T} select: L[n] cons: [a b] and: P ∧ Q le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A prop: subtract: m lelt: i ≤ j < k satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top nat: subtype_rel: A ⊆B real-vec: ^n less_than: a < b squash: T true: True uiff: uiff(P;Q) req_int_terms: t1 ≡ t2
Lemmas referenced :  decidable__equal_int subtype_base_sq int_subtype_base int_seg_properties int_seg_subtype false_wf int_seg_cases full-omega-unsat intformand_wf intformless_wf itermVar_wf itermConstant_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf int_seg_wf req_witness rcp_wf real-vec-mul_wf le_wf real_wf real-vec_wf rsub_wf rmul_wf lelt_wf itermSubtract_wf itermMultiply_wf req-iff-rsub-is-0 real_polynomial_null int-to-real_wf real_term_value_sub_lemma real_term_value_mul_lemma real_term_value_var_lemma real_term_value_const_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalRule extract_by_obid sqequalHypSubstitution dependent_functionElimination thin setElimination rename hypothesisEquality hypothesis natural_numberEquality unionElimination instantiate isectElimination cumulativity intEquality independent_isectElimination because_Cache independent_functionElimination equalityTransitivity equalitySymmetry hypothesis_subsumption addEquality independent_pairFormation productElimination approximateComputation dependent_pairFormation lambdaEquality int_eqEquality isect_memberEquality voidElimination voidEquality applyEquality dependent_set_memberEquality imageMemberEquality baseClosed

Latex:
\mforall{}[a,b:\mBbbR{}\^{}3].  \mforall{}[c:\mBbbR{}].    req-vec(3;(a  x  c*b);c*(a  x  b))



Date html generated: 2018_05_22-PM-02_42_15
Last ObjectModification: 2018_05_09-PM-01_16_43

Theory : reals


Home Index