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

[n:ℕ]. ∀[x:ℝ^n].  (||x||^2 x ⋅ x)

Proof

Definitions occuring in Statement :  real-vec-norm: ||x|| dot-product: x ⋅ y real-vec: ^n rnexp: x^k1 req: y nat: uall: [x:A]. B[x] natural_number: \$n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T real-vec: ^n nat: le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A implies:  Q prop: real-vec-norm: ||x|| uimplies: supposing a uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  req_witness rnexp_wf false_wf le_wf real-vec-norm_wf dot-product_wf real-vec_wf nat_wf rmul_wf rsqrt_squared dot-product-nonneg rleq_wf int-to-real_wf req_functionality rnexp2 req_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution lemma_by_obid isectElimination thin dependent_set_memberEquality natural_numberEquality sqequalRule independent_pairFormation lambdaFormation hypothesis hypothesisEquality independent_functionElimination isect_memberEquality because_Cache independent_isectElimination productElimination

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

Date html generated: 2016_05_18-AM-09_48_48
Last ObjectModification: 2015_12_27-PM-11_11_25

Theory : reals

Home Index