Nuprl Lemma : radd-zero

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


Proof




Definitions occuring in Statement :  req: y radd: 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 radd: b implies:  Q nat_plus: + less_than: a < b squash: T less_than': less_than'(a;b) true: True prop: subtype_rel: A ⊆B all: x:A. B[x] top: Top real: guard: {T} iff: ⇐⇒ Q rev_implies:  Q int-to-real: r(n) bdd-diff: bdd-diff(f;g) exists: x:A. B[x] nat: le: A ≤ B false: False not: ¬A so_lambda: λ2x.t[x] so_apply: x[s] absval: |i| subtract: m
Lemmas referenced :  add-mul-special zero-add zero-mul mul-associates mul-swap mul-commutes minus-one-mul add-associates bdd-diff_weakening accelerate-bdd-diff bdd-diff_functionality nat_wf subtract_wf absval_wf all_wf le_wf false_wf l_sum_nil_lemma l_sum_cons_lemma map_nil_lemma map_cons_lemma iff_weakening_equal reg-seq-list-add-as-l_sum true_wf squash_wf bdd-diff_wf length_wf regular-int-seq_wf nat_plus_wf length_of_nil_lemma length_of_cons_lemma nil_wf cons_wf reg-seq-list-add_wf less_than_wf accelerate_wf real_wf req_witness int-to-real_wf radd_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 dependent_set_memberEquality sqequalRule independent_pairFormation imageMemberEquality baseClosed because_Cache applyEquality lambdaEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality setEquality functionEquality intEquality setElimination rename imageElimination equalityTransitivity equalitySymmetry universeEquality dependent_pairFormation lambdaFormation addEquality multiplyEquality minusEquality

Latex:
\mforall{}[x:\mBbbR{}].  ((x  +  r0)  =  x)



Date html generated: 2016_05_18-AM-06_51_41
Last ObjectModification: 2016_01_17-AM-01_46_39

Theory : reals


Home Index