Nuprl Lemma : iroot-zero

[n:ℕ+]. (iroot(n;0) 0)


Proof




Definitions occuring in Statement :  iroot: iroot(n;x) nat_plus: + uall: [x:A]. B[x] natural_number: $n sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a nat: so_lambda: λ2x.t[x] so_apply: x[s] iroot: iroot(n;x) integer-nth-root-ext has-value: (a)↓ nat_plus: + subtype_rel: A ⊆B less_than: a < b squash: T less_than': less_than'(a;b) true: True and: P ∧ Q prop: genrec-ap: genrec-ap all: x:A. B[x] decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top false: False le: A ≤ B not: ¬A implies:  Q sq_type: SQType(T) guard: {T}
Lemmas referenced :  integer-nth-root-ext le_wf false_wf int_formula_prop_wf int_term_value_constant_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma itermConstant_wf intformeq_wf intformnot_wf satisfiable-full-omega-tt decidable__equal_int nat_plus_properties nat_plus_subtype_nat exp_wf_nat_plus int-value-type less_than_wf set-value-type nat_plus_wf value-type-has-value int_subtype_base set_subtype_base subtype_base_sq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin instantiate lemma_by_obid sqequalHypSubstitution isectElimination because_Cache independent_isectElimination sqequalRule hypothesis callbyvalueReduce intEquality lambdaEquality natural_numberEquality hypothesisEquality applyEquality dependent_set_memberEquality independent_pairFormation imageMemberEquality baseClosed setElimination rename dependent_functionElimination unionElimination dependent_pairFormation isect_memberEquality voidElimination voidEquality computeAll equalityTransitivity equalitySymmetry lambdaFormation independent_functionElimination axiomSqEquality

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  (iroot(n;0)  \msim{}  0)



Date html generated: 2019_06_20-PM-02_34_45
Last ObjectModification: 2019_03_19-AM-10_49_32

Theory : num_thy_1


Home Index