### Nuprl Lemma : absval_cases

`∀x:ℤ. ∀[y:ℕ]. uiff(|x| = y ∈ ℤ;(x = y ∈ ℤ) ∨ (x = (-y) ∈ ℤ))`

Proof

Definitions occuring in Statement :  absval: `|i|` nat: `ℕ` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` or: `P ∨ Q` minus: `-n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` prop: `ℙ` subtype_rel: `A ⊆r B` nat: `ℕ` implies: `P `` Q` decidable: `Dec(P)` or: `P ∨ Q` less_than: `a < b` less_than': `less_than'(a;b)` top: `Top` true: `True` squash: `↓T` not: `¬A` false: `False` guard: `{T}` sq_type: `SQType(T)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  equal-wf-base-T int_subtype_base or_wf nat_wf absval_unfold2 decidable__lt top_wf less_than_wf subtype_base_sq minus-minus equal_wf squash_wf true_wf absval_pos iff_weakening_equal absval_sym
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation independent_pairFormation cut introduction axiomEquality hypothesis thin rename extract_by_obid sqequalHypSubstitution isectElimination intEquality sqequalRule baseApply closedConclusion baseClosed hypothesisEquality applyEquality setElimination because_Cache minusEquality independent_functionElimination dependent_functionElimination natural_numberEquality unionElimination lessCases sqequalAxiom isect_memberEquality voidElimination voidEquality imageMemberEquality imageElimination productElimination inlFormation inrFormation instantiate cumulativity independent_isectElimination equalityTransitivity equalitySymmetry lambdaEquality universeEquality

Latex:
\mforall{}x:\mBbbZ{}.  \mforall{}[y:\mBbbN{}].  uiff(|x|  =  y;(x  =  y)  \mvee{}  (x  =  (-y)))

Date html generated: 2017_04_14-AM-07_17_26
Last ObjectModification: 2017_02_27-PM-02_52_03

Theory : arithmetic

Home Index