Nuprl Lemma : absval_wf

[x:ℤ]. (|x| ∈ ℕ)


Proof




Definitions occuring in Statement :  absval: |i| nat: uall: [x:A]. B[x] member: t ∈ T int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T less_than: a < b and: P ∧ Q less_than': less_than'(a;b) true: True squash: T top: Top not: ¬A implies:  Q false: False prop: nat: all: x:A. B[x] guard: {T} uimplies: supposing a uiff: uiff(P;Q) gt: i > j le: A ≤ B subtype_rel: A ⊆B
Lemmas referenced :  absval_unfold2 less_than_wf le_weakening2 le_wf not-gt-2 add_functionality_wrt_le le_reflexive minus-one-mul minus-one-mul-top zero-add add-mul-special zero-mul
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis natural_numberEquality lessCases independent_pairFormation baseClosed equalityTransitivity equalitySymmetry imageMemberEquality because_Cache axiomSqEquality isect_memberEquality voidElimination voidEquality lambdaFormation imageElimination productElimination independent_functionElimination dependent_set_memberEquality dependent_functionElimination independent_isectElimination axiomEquality intEquality minusEquality multiplyEquality applyEquality lambdaEquality

Latex:
\mforall{}[x:\mBbbZ{}].  (|x|  \mmember{}  \mBbbN{})



Date html generated: 2019_06_20-AM-11_24_24
Last ObjectModification: 2018_08_20-PM-09_28_16

Theory : arithmetic


Home Index