Nuprl Lemma : iroot_wf

[n:ℕ+]. ∀[x:ℕ].  (iroot(n;x) ∈ ℕ)


Proof




Definitions occuring in Statement :  iroot: iroot(n;x) nat_plus: + nat: uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T iroot: iroot(n;x) subtype_rel: A ⊆B all: x:A. B[x] so_lambda: λ2x.t[x] prop: and: P ∧ Q nat: so_apply: x[s] sq_exists: x:A [B[x]] implies:  Q
Lemmas referenced :  integer-nth-root-ext subtype_rel_self nat_plus_wf all_wf nat_wf sq_exists_wf le_wf exp_wf2 less_than_wf nat_plus_subtype_nat equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut applyEquality thin instantiate extract_by_obid hypothesis sqequalRule sqequalHypSubstitution isectElimination functionEquality lambdaEquality productEquality hypothesisEquality because_Cache setElimination rename addEquality natural_numberEquality lambdaFormation equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination axiomEquality isect_memberEquality

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



Date html generated: 2019_06_20-PM-02_33_58
Last ObjectModification: 2019_03_19-AM-10_49_11

Theory : num_thy_1


Home Index