### Nuprl Lemma : int2nat2int

`∀[i:ℤ]. (nat2int(int2nat(i)) = i ∈ ℤ)`

Proof

Definitions occuring in Statement :  nat2int: `nat2int(m)` int2nat: `int2nat(i)` uall: `∀[x:A]. B[x]` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` int2nat: `int2nat(i)` nat2int: `nat2int(m)` member: `t ∈ T` has-value: `(a)↓` uimplies: `b supposing a` all: `∀x:A. B[x]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` less_than: `a < b` and: `P ∧ Q` less_than': `less_than'(a;b)` true: `True` squash: `↓T` top: `Top` bfalse: `ff` int_nzero: `ℤ-o` nequal: `a ≠ b ∈ T ` not: `¬A` sq_type: `SQType(T)` guard: `{T}` false: `False` prop: `ℙ` uiff: `uiff(P;Q)` exists: `∃x:A. B[x]` or: `P ∨ Q` bnot: `¬bb` ifthenelse: `if b then t else f fi ` assert: `↑b` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` subtype_rel: `A ⊆r B` nat_plus: `ℕ+` nat: `ℕ` ge: `i ≥ j ` remainder: `n rem m`
Lemmas referenced :  eq_int_wf remainder_wfa value-type-has-value int-value-type lt_int_wf istype-top istype-void subtract_wf subtype_base_sq int_subtype_base nequal_wf eqtt_to_assert assert_of_eq_int assert_of_lt_int eqff_to_assert bool_cases_sqequal bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf less_than_wf istype-less_than divide-exact neg_assert_of_eq_int istype-int decidable__equal_int full-omega-unsat intformnot_wf intformeq_wf itermConstant_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_constant_lemma int_formula_prop_wf equal_wf add_functionality_wrt_eq mul_com iff_weakening_equal squash_wf true_wf istype-universe int_nzero_wf add_com subtype_rel_self decidable__lt int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_minus_lemma int_term_value_subtract_lemma int_formula_prop_and_lemma intformless_wf itermVar_wf itermMinus_wf itermSubtract_wf intformand_wf istype-le int_formula_prop_le_lemma intformle_wf decidable__le rem_invariant int_term_value_add_lemma itermAdd_wf nat_properties false_wf multiply-is-int-iff add-is-int-iff int_term_value_mul_lemma itermMultiply_wf rem_bounds_1 div_rem_sum mul-commutes zero-add
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin sqequalRule callbyvalueReduce intEquality independent_isectElimination hypothesis hypothesisEquality closedConclusion natural_numberEquality because_Cache Error :inhabitedIsType,  Error :lambdaFormation_alt,  unionElimination equalityElimination lessCases independent_pairFormation baseClosed equalityTransitivity equalitySymmetry imageMemberEquality axiomSqEquality Error :isect_memberEquality_alt,  Error :isectIsTypeImplies,  promote_hyp voidElimination addEquality multiplyEquality minusEquality Error :equalityIstype,  dependent_functionElimination independent_functionElimination Error :dependent_set_memberEquality_alt,  instantiate cumulativity sqequalBase Error :universeIsType,  productElimination int_eqReduceTrueSq imageElimination Error :dependent_pairFormation_alt,  int_eqReduceFalseSq approximateComputation Error :lambdaEquality_alt,  applyEquality universeEquality int_eqEquality rename setElimination applyLambdaEquality baseApply pointwiseFunctionality

Latex:
\mforall{}[i:\mBbbZ{}].  (nat2int(int2nat(i))  =  i)

Date html generated: 2019_06_20-PM-02_52_15
Last ObjectModification: 2019_03_06-AM-10_52_13

Theory : continuity

Home Index