Nuprl Lemma : rmul-one-both

[x:ℝ]. (((x r1) x) ∧ ((r1 x) x))


Proof




Definitions occuring in Statement :  req: y rmul: 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: c∧ B implies:  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