Nuprl Lemma : mul-minus-2

x,y:Top.  (x (-y) -(x y))


Proof




Definitions occuring in Statement :  top: Top all: x:A. B[x] multiply: m minus: -n sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] has-value: (a)↓ member: t ∈ T and: P ∧ Q implies:  Q uall: [x:A]. B[x] uimplies: supposing a top: Top sq_type: SQType(T) guard: {T}
Lemmas referenced :  value-type-has-value int-value-type has-value_wf_base is-exception_wf istype-top subtype_base_sq int_subtype_base minus-one-mul mul-swap istype-void minus-one-mul-top int-mul-exception
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  cut sqequalRule thin sqequalSqle divergentSqle callbyvalueMultiply sqequalHypSubstitution hypothesis baseApply closedConclusion baseClosed hypothesisEquality productElimination equalityTransitivity equalitySymmetry Error :inhabitedIsType,  introduction extract_by_obid isectElimination intEquality independent_isectElimination Error :equalityIstype,  dependent_functionElimination independent_functionElimination callbyvalueMinus multiplyExceptionCases axiomSqleEquality minusExceptionCases exceptionSqequal sqleReflexivity because_Cache instantiate cumulativity Error :isect_memberEquality_alt,  voidElimination multiplyEquality minusEquality

Latex:
\mforall{}x,y:Top.    (x  *  (-y)  \msim{}  -(x  *  y))



Date html generated: 2019_06_20-AM-11_22_16
Last ObjectModification: 2019_05_21-PM-10_55_32

Theory : arithmetic


Home Index