### Nuprl Lemma : real-vec-norm-mul

`∀[n:ℕ]. ∀[x:ℝ^n]. ∀[a:ℝ].  (||a*x|| = (|a| * ||x||))`

Proof

Definitions occuring in Statement :  real-vec-norm: `||x||` real-vec-mul: `a*X` real-vec: `ℝ^n` rabs: `|x|` req: `x = y` rmul: `a * b` real: `ℝ` nat: `ℕ` uall: `∀[x:A]. B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` nat_plus: `ℕ+` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` true: `True` and: `P ∧ Q` prop: `ℙ` implies: `P `` Q` uimplies: `b supposing a` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` nat: `ℕ` le: `A ≤ B` false: `False` not: `¬A` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)` itermConstant: `"const"` req_int_terms: `t1 ≡ t2` top: `Top`
Lemmas referenced :  rnexp-req-iff less_than_wf real-vec-norm_wf real-vec-mul_wf rmul_wf rabs_wf real-vec-norm-nonneg rmul-nonneg-case1 zero-rleq-rabs req_witness real_wf real-vec_wf nat_wf rnexp_wf false_wf le_wf dot-product_wf req_functionality real-vec-norm-squared req_weakening req_wf uiff_transitivity req_transitivity dot-product-linearity2 rmul_functionality rmul-assoc req_inversion rnexp2 square-nonneg real_term_polynomial itermSubtract_wf itermMultiply_wf itermVar_wf int-to-real_wf real_term_value_const_lemma real_term_value_sub_lemma real_term_value_mul_lemma real_term_value_var_lemma req-iff-rsub-is-0 rabs-rmul rabs-of-nonneg
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution dependent_functionElimination thin dependent_set_memberEquality natural_numberEquality sqequalRule independent_pairFormation imageMemberEquality hypothesisEquality baseClosed hypothesis isectElimination independent_functionElimination independent_isectElimination because_Cache productElimination isect_memberEquality lambdaFormation computeAll lambdaEquality int_eqEquality intEquality voidElimination voidEquality

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x:\mBbbR{}\^{}n].  \mforall{}[a:\mBbbR{}].    (||a*x||  =  (|a|  *  ||x||))

Date html generated: 2017_10_03-AM-10_49_56
Last ObjectModification: 2017_07_28-AM-08_20_26

Theory : reals

Home Index