Nuprl Lemma : rsub-int

[n:ℤ]. ∀m:ℤ((r(n) r(m)) r(n m))


Proof




Definitions occuring in Statement :  rsub: y req: y int-to-real: r(n) uall: [x:A]. B[x] all: x:A. B[x] subtract: m int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] rsub: y implies:  Q true: True uimplies: supposing a squash: T prop: subtype_rel: A ⊆B top: Top subtract: m uiff: uiff(P;Q) and: P ∧ Q rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  req_witness rsub_wf int-to-real_wf subtract_wf req_wf radd_wf rminus_wf req_weakening squash_wf true_wf minus-one-mul add-commutes minus-one-mul-top uiff_transitivity3 real_wf rminus-int req_functionality radd-int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation intEquality sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality extract_by_obid isectElimination hypothesis independent_functionElimination because_Cache minusEquality addEquality natural_numberEquality independent_isectElimination applyEquality imageElimination equalityTransitivity equalitySymmetry isect_memberEquality voidElimination voidEquality imageMemberEquality baseClosed productElimination

Latex:
\mforall{}[n:\mBbbZ{}].  \mforall{}m:\mBbbZ{}.  ((r(n)  -  r(m))  =  r(n  -  m))



Date html generated: 2017_10_02-PM-07_17_31
Last ObjectModification: 2017_07_28-AM-07_21_10

Theory : reals


Home Index