Nuprl Lemma : absval_nat_plus

`∀[x:ℤ]. |x| ∈ ℕ+ supposing ¬(x = 0 ∈ ℤ)`

Proof

Definitions occuring in Statement :  absval: `|i|` nat_plus: `ℕ+` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` member: `t ∈ T` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` nat_plus: `ℕ+` subtype_rel: `A ⊆r B` nat: `ℕ` prop: `ℙ` uiff: `uiff(P;Q)` and: `P ∧ Q` rev_uimplies: `rev_uimplies(P;Q)` nequal: `a ≠ b ∈ T `
Lemmas referenced :  absval_wf nat_wf less_than_wf not_wf equal_wf absval-positive
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut dependent_set_memberEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality lambdaEquality setElimination rename sqequalRule natural_numberEquality axiomEquality equalityTransitivity equalitySymmetry intEquality isect_memberEquality because_Cache productElimination independent_isectElimination

Latex:
\mforall{}[x:\mBbbZ{}].  |x|  \mmember{}  \mBbbN{}\msupplus{}  supposing  \mneg{}(x  =  0)

Date html generated: 2016_05_14-AM-07_20_37
Last ObjectModification: 2015_12_26-PM-01_32_12

Theory : int_2

Home Index