Nuprl Lemma : rmul-one

[x:ℝ]. ((x r1) x)


Proof




Definitions occuring in Statement :  req: y rmul: b int-to-real: r(n) real: uall: [x:A]. B[x] natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a implies:  Q subtype_rel: A ⊆B real: int-to-real: r(n) reg-seq-mul: reg-seq-mul(x;y) bdd-diff: bdd-diff(f;g) exists: x:A. B[x] nat: le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A prop: all: x:A. B[x] so_lambda: λ2x.t[x] nat_plus: + nequal: a ≠ b ∈  ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top so_apply: x[s] iff: ⇐⇒ Q rev_implies:  Q subtract: m decidable: Dec(P) or: P ∨ Q sq_type: SQType(T) guard: {T} int_nzero: -o absval: |i|
Lemmas referenced :  zero-mul add-mul-special nat_wf nequal_wf div-cancel int_formula_prop_not_lemma intformnot_wf decidable__equal_int int_subtype_base subtype_base_sq add-commutes mul-associates mul-commutes mul-swap minus-one-mul bdd-diff_weakening rmul-bdd-diff-reg-seq-mul bdd-diff_functionality equal_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_term_value_mul_lemma int_formula_prop_eq_lemma int_formula_prop_and_lemma intformless_wf itermVar_wf itermConstant_wf itermMultiply_wf intformeq_wf intformand_wf satisfiable-full-omega-tt nat_properties nat_plus_properties subtract_wf absval_wf all_wf nat_plus_wf le_wf false_wf reg-seq-mul_wf real_wf req_witness int-to-real_wf rmul_wf req-iff-bdd-diff
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality natural_numberEquality hypothesis productElimination independent_isectElimination independent_functionElimination applyEquality lambdaEquality setElimination rename sqequalRule because_Cache dependent_pairFormation dependent_set_memberEquality independent_pairFormation lambdaFormation divideEquality multiplyEquality int_eqEquality intEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality computeAll instantiate unionElimination equalityTransitivity equalitySymmetry minusEquality

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



Date html generated: 2016_05_18-AM-06_52_09
Last ObjectModification: 2016_01_17-AM-01_47_03

Theory : reals


Home Index