### Nuprl Lemma : rmul-rinv1

`∀[x:ℝ]. (rnonzero(x) `` ((x * rinv(x)) = r1))`

Proof

Definitions occuring in Statement :  rinv: `rinv(x)` rnonzero: `rnonzero(x)` req: `x = y` rmul: `a * b` 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` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` prop: `ℙ` real: `ℝ` subtype_rel: `A ⊆r B` rinv: `rinv(x)` rnonzero: `rnonzero(x)` int_upper: `{i...}` so_lambda: `λ2x.t[x]` so_apply: `x[s]` squash: `↓T` has-value: `(a)↓` nat_plus: `ℕ+` le: `A ≤ B` all: `∀x:A. B[x]` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` not: `¬A` rev_implies: `P `` Q` false: `False` less_than': `less_than'(a;b)` true: `True` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` nat: `ℕ` rev_uimplies: `rev_uimplies(P;Q)` sq_type: `SQType(T)` guard: `{T}` int_seg: `{i..j-}` lelt: `i ≤ j < k` less_than: `a < b` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` bnot: `¬bb` assert: `↑b` bdd-diff: `bdd-diff(f;g)` ge: `i ≥ j ` int-to-real: `r(n)` reg-seq-inv: `reg-seq-inv(x)` reg-seq-mul: `reg-seq-mul(x;y)` nequal: `a ≠ b ∈ T ` absval: `|i|` int_nzero: `ℤ-o` subtract: `n - m` sq_stable: `SqStable(P)` reg-seq-adjust: `reg-seq-adjust(n;x)`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_functionElimination hypothesis natural_numberEquality productElimination independent_isectElimination setElimination rename sqequalRule lambdaEquality dependent_functionElimination because_Cache applyEquality instantiate cumulativity intEquality imageElimination callbyvalueReduce dependent_set_memberEquality unionElimination independent_pairFormation voidElimination dependent_pairFormation setEquality approximateComputation int_eqEquality isect_memberEquality voidEquality imageMemberEquality baseClosed equalityTransitivity equalitySymmetry promote_hyp applyLambdaEquality equalityElimination hypothesis_subsumption productEquality multiplyEquality pointwiseFunctionality baseApply closedConclusion functionEquality universeEquality addEquality minusEquality divideEquality remainderEquality hyp_replacement lessCases axiomSqEquality

Latex:
\mforall{}[x:\mBbbR{}].  (rnonzero(x)  {}\mRightarrow{}  ((x  *  rinv(x))  =  r1))

Date html generated: 2019_10_16-PM-03_07_40
Last ObjectModification: 2018_08_27-PM-00_08_07

Theory : reals

Home Index