### Nuprl Lemma : rinv_functionality2

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

Proof

Definitions occuring in Statement :  rneq: `x ≠ y` rinv: `rinv(x)` req: `x = y` int-to-real: `r(n)` real: `ℝ` uall: `∀[x:A]. B[x]` implies: `P `` Q` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` prop: `ℙ` uimplies: `b supposing a` uiff: `uiff(P;Q)` and: `P ∧ Q` rev_uimplies: `rev_uimplies(P;Q)` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  req_wf rneq_wf int-to-real_wf req_witness rinv_wf2 real_wf req_weakening req_functionality rinv_functionality req_inversion rneq_functionality rnonzero_functionality rnonzero-iff
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis natural_numberEquality sqequalRule lambdaEquality dependent_functionElimination independent_functionElimination isect_memberEquality because_Cache independent_isectElimination productElimination

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

Date html generated: 2016_05_18-AM-07_11_01
Last ObjectModification: 2015_12_28-AM-00_39_35

Theory : reals

Home Index