Nuprl Lemma : radd-rminus-both

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


Proof




Definitions occuring in Statement :  req: y rminus: -(x) radd: b int-to-real: r(n) real: uall: [x:A]. B[x] and: P ∧ Q natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T and: P ∧ Q cand: c∧ B squash: T prop: true: True subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q
Lemmas referenced :  radd_wf req_witness iff_weakening_equal int-to-real_wf rminus_wf radd_comm_eq real_wf true_wf squash_wf req_wf radd-rminus
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_pairFormation applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry natural_numberEquality sqequalRule imageMemberEquality baseClosed universeEquality independent_isectElimination productElimination independent_functionElimination independent_pairEquality because_Cache

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



Date html generated: 2016_05_18-AM-06_51_48
Last ObjectModification: 2016_01_17-AM-01_46_30

Theory : reals


Home Index