### Nuprl Lemma : rabs-rinv

`∀y:ℝ. (y ≠ r0 `` (|rinv(y)| = rinv(|y|)))`

Proof

Definitions occuring in Statement :  rneq: `x ≠ y` rabs: `|x|` rinv: `rinv(x)` req: `x = y` int-to-real: `r(n)` real: `ℝ` all: `∀x:A. B[x]` implies: `P `` Q` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` rneq: `x ≠ y` or: `P ∨ Q` prop: `ℙ` uall: `∀[x:A]. B[x]` uimplies: `b supposing a` itermConstant: `"const"` req_int_terms: `t1 ≡ t2` false: `False` not: `¬A` top: `Top` uiff: `uiff(P;Q)` and: `P ∧ Q` guard: `{T}` rev_uimplies: `rev_uimplies(P;Q)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` le: `A ≤ B` less_than': `less_than'(a;b)`
Lemmas referenced :  rabs-neq-zero rneq_wf int-to-real_wf real_wf rless-implies-rless rminus_wf real_term_polynomial itermSubtract_wf itermConstant_wf itermVar_wf itermMinus_wf real_term_value_const_lemma real_term_value_sub_lemma real_term_value_var_lemma real_term_value_minus_lemma req-iff-rsub-is-0 rsub_wf rless_wf rabs-of-nonpos rleq_weakening_rless rabs_wf rinv_wf2 req_functionality req_weakening rinv_functionality2 rmul_reverses_rleq_iff rmul_wf rleq-int false_wf rleq_functionality itermMultiply_wf real_term_value_mul_lemma req_transitivity rmul-rinv rmul_preserves_req rabs-of-nonneg rmul_preserves_rleq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination hypothesis addLevel unionElimination levelHypothesis isectElimination natural_numberEquality inrFormation because_Cache independent_isectElimination sqequalRule computeAll lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality productElimination independent_pairFormation

Latex:
\mforall{}y:\mBbbR{}.  (y  \mneq{}  r0  {}\mRightarrow{}  (|rinv(y)|  =  rinv(|y|)))

Date html generated: 2017_10_03-AM-08_37_35
Last ObjectModification: 2017_07_28-AM-07_30_14

Theory : reals

Home Index