Nuprl Lemma : rinv-of-rmul

[x,y:ℝ].  (rinv(x y) (rinv(x) rinv(y))) supposing (y ≠ r0 and x ≠ r0)


Definitions occuring in Statement :  rneq: x ≠ y rinv: rinv(x) req: y rmul: b int-to-real: r(n) real: uimplies: supposing a uall: [x:A]. B[x] natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] implies:  Q guard: {T} prop: uiff: uiff(P;Q) and: P ∧ Q rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  rmul-neq-zero req_inversion rmul_wf rinv_wf2 req_witness rneq_wf int-to-real_wf real_wf rmul-inverse-is-rinv req_functionality rmul-ac req_weakening req_wf uiff_transitivity rmul_functionality req_transitivity rmul_assoc rmul-rinv rmul-one rmul-rinv2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination hypothesis isectElimination independent_isectElimination natural_numberEquality sqequalRule isect_memberEquality because_Cache equalityTransitivity equalitySymmetry productElimination

\mforall{}[x,y:\mBbbR{}].    (rinv(x  *  y)  =  (rinv(x)  *  rinv(y)))  supposing  (y  \mneq{}  r0  and  x  \mneq{}  r0)

Date html generated: 2016_05_18-AM-07_12_12
Last ObjectModification: 2015_12_28-AM-00_40_25

Theory : reals

Home Index