### Nuprl Lemma : rinv-of-rinv

`∀[x:ℝ]. rinv(rinv(x)) = x supposing x ≠ r0`

Proof

Definitions occuring in Statement :  rneq: `x ≠ y` rinv: `rinv(x)` req: `x = y` 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` all: `∀x:A. B[x]` implies: `P `` Q` guard: `{T}` prop: `ℙ`
Lemmas referenced :  rinv-neq-zero rmul-inverse-is-rinv rinv_wf2 rmul-rinv2 req_inversion req_witness rneq_wf int-to-real_wf real_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin because_Cache independent_functionElimination hypothesis isectElimination hypothesisEquality independent_isectElimination natural_numberEquality sqequalRule isect_memberEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[x:\mBbbR{}].  rinv(rinv(x))  =  x  supposing  x  \mneq{}  r0

Date html generated: 2016_05_18-AM-07_12_17
Last ObjectModification: 2015_12_28-AM-00_40_19

Theory : reals

Home Index