`∀[x:ℝ]. ((x + -(x)) = r0)`

Proof

Definitions occuring in Statement :  req: `x = y` rminus: `-(x)` radd: `a + 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: `b supposing a` radd: `a + b` implies: `P `` Q` nat_plus: `ℕ+` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` true: `True` prop: `ℙ` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` top: `Top` real: `ℝ` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` int-to-real: `r(n)` rminus: `-(x)` 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: `n - m`
Lemmas referenced :  add-mul-special add-zero zero-mul zero-add mul-commutes mul-associates minus-one-mul add-associates subtract_wf absval_wf all_wf le_wf false_wf l_sum_nil_lemma l_sum_cons_lemma map_nil_lemma map_cons_lemma bdd-diff_weakening accelerate-bdd-diff bdd-diff_functionality 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 rminus_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 hypothesis natural_numberEquality 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 minusEquality multiplyEquality

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

Date html generated: 2016_05_18-AM-06_51_46
Last ObjectModification: 2016_01_17-AM-01_46_34

Theory : reals

Home Index