`∀[x:ℝ]. (((x + -(x)) = r0) ∧ ((-(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]` and: `P ∧ Q` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` and: `P ∧ Q` cand: `A c∧ B` squash: `↓T` prop: `ℙ` true: `True` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q`
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