Nuprl Lemma : le-add-cancel-alt

[c,t:ℤ].  uiff(t ≤ (c t);0 ≤ c)


Proof




Definitions occuring in Statement :  uiff: uiff(P;Q) uall: [x:A]. B[x] le: A ≤ B add: m natural_number: $n int:
Definitions unfolded in proof :  uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a member: t ∈ T le: A ≤ B not: ¬A implies:  Q false: False prop: uall: [x:A]. B[x] all: x:A. B[x] subtype_rel: A ⊆B top: Top sq_type: SQType(T) guard: {T}
Lemmas referenced :  zero-add add-zero zero-mul add-mul-special minus-one-mul add-associates add-is-int-iff int_subtype_base subtype_base_sq add-inverse add_functionality_wrt_le le_reflexive less_than'_wf le_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality lambdaEquality dependent_functionElimination hypothesisEquality because_Cache axiomEquality equalityTransitivity hypothesis equalitySymmetry lemma_by_obid isectElimination addEquality voidElimination natural_numberEquality intEquality isect_memberEquality minusEquality independent_isectElimination instantiate baseApply closedConclusion baseClosed applyEquality voidEquality independent_functionElimination

Latex:
\mforall{}[c,t:\mBbbZ{}].    uiff(t  \mleq{}  (c  +  t);0  \mleq{}  c)



Date html generated: 2016_05_13-PM-03_31_13
Last ObjectModification: 2016_01_14-PM-06_41_16

Theory : arithmetic


Home Index