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

Proof

Definitions occuring in Statement :  req: `x = y` 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 because_Cache sqequalRule imageMemberEquality baseClosed universeEquality independent_isectElimination productElimination independent_functionElimination independent_pairEquality

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

Date html generated: 2016_05_18-AM-06_51_43
Last ObjectModification: 2016_01_17-AM-01_46_28

Theory : reals

Home Index