Nuprl Lemma : iroot-property

[n:ℕ+]. ∀[x:ℕ].  ((iroot(n;x)^n ≤ x) ∧ x < (iroot(n;x) 1)^n)


Proof




Definitions occuring in Statement :  iroot: iroot(n;x) exp: i^n nat_plus: + nat: less_than: a < b uall: [x:A]. B[x] le: A ≤ B and: P ∧ Q add: m natural_number: $n
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 le: A ≤ B not: ¬A false: False uimplies: supposing a sq_stable: SqStable(P) squash: T
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 equal_wf member-less_than less_than'_wf nat_plus_subtype_nat iroot_wf squash_wf sq_stable__and sq_stable__le sq_stable__less_than
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 productElimination independent_pairEquality axiomEquality independent_isectElimination isect_memberEquality voidElimination imageMemberEquality baseClosed imageElimination

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[x:\mBbbN{}].    ((iroot(n;x)\^{}n  \mleq{}  x)  \mwedge{}  x  <  (iroot(n;x)  +  1)\^{}n)



Date html generated: 2019_06_20-PM-02_34_03
Last ObjectModification: 2019_03_19-AM-10_49_16

Theory : num_thy_1


Home Index