### Nuprl Lemma : abs-val_wf

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

Proof

Definitions occuring in Statement :  abs-val: |x| nat: uall: [x:A]. B[x] member: t ∈ T int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T abs-val: |x| all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt subtype_rel: A ⊆B uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a ifthenelse: if then else fi  nat: prop: bfalse: ff guard: {T} top: Top subtract: m le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A nat_plus: + less_than: a < b squash: T true: True decidable: Dec(P) or: P ∨ Q
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality natural_numberEquality hypothesis lambdaFormation unionElimination equalityElimination sqequalRule baseApply closedConclusion baseClosed applyEquality independent_functionElimination because_Cache productElimination independent_isectElimination dependent_set_memberEquality minusEquality dependent_functionElimination equalityTransitivity equalitySymmetry axiomEquality intEquality multiplyEquality lambdaEquality isect_memberEquality voidElimination voidEquality addEquality independent_pairFormation imageMemberEquality

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

Date html generated: 2019_06_20-PM-00_25_54
Last ObjectModification: 2018_08_07-PM-04_55_34

Theory : int_1

Home Index