### Nuprl Lemma : rmul-one-both

`∀[x:ℝ]. (((x * r1) = x) ∧ ((r1 * x) = x))`

Proof

Definitions occuring in Statement :  req: `x = y` rmul: `a * b` int-to-real: `r(n)` real: `ℝ` uall: `∀[x:A]. B[x]` and: `P ∧ Q` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` and: `P ∧ Q` cand: `A c∧ B` implies: `P `` Q`
Lemmas referenced :  rmul-one rmul-identity1 req_witness rmul_wf int-to-real_wf real_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_pairFormation because_Cache sqequalRule productElimination independent_pairEquality natural_numberEquality independent_functionElimination

Latex:
\mforall{}[x:\mBbbR{}].  (((x  *  r1)  =  x)  \mwedge{}  ((r1  *  x)  =  x))

Date html generated: 2016_05_18-AM-06_52_14
Last ObjectModification: 2015_12_28-AM-00_30_20

Theory : reals

Home Index