### Nuprl Lemma : rmul-nonneg-rabs

`∀[x,y:ℝ].  (x * |y|) = |x * y| supposing r0 ≤ x`

Proof

Definitions occuring in Statement :  rleq: `x ≤ y` rabs: `|x|` req: `x = y` rmul: `a * b` int-to-real: `r(n)` real: `ℝ` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` implies: `P `` Q` prop: `ℙ` uiff: `uiff(P;Q)` and: `P ∧ Q` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  req_witness rmul_wf rabs_wf rleq_wf int-to-real_wf real_wf req_weakening req_functionality rabs-rmul rmul_functionality rabs-of-nonneg
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_functionElimination universeIsType natural_numberEquality sqequalRule isect_memberEquality_alt because_Cache isectIsTypeImplies inhabitedIsType independent_isectElimination productElimination

Latex:
\mforall{}[x,y:\mBbbR{}].    (x  *  |y|)  =  |x  *  y|  supposing  r0  \mleq{}  x

Date html generated: 2019_10_29-AM-09_39_09
Last ObjectModification: 2019_02_13-PM-02_32_11

Theory : reals

Home Index