Nuprl Lemma : integer-nth-root2

n:{n:ℕ+(n mod 2) 1 ∈ ℤ. ∀x:{...0}.  (∃r:{...0} [((r 1)^n < x ∧ (x ≤ r^n))])


Proof




Definitions occuring in Statement :  exp: i^n modulus: mod n int_lower: {...i} nat_plus: + less_than: a < b le: A ≤ B all: x:A. B[x] sq_exists: x:A [B[x]] and: P ∧ Q set: {x:A| B[x]}  subtract: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T nat: int_lower: {...i} uall: [x:A]. B[x] guard: {T} sq_stable: SqStable(P) implies:  Q squash: T nat_plus: + decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top and: P ∧ Q prop: so_lambda: λ2x.t[x] less_than: a < b less_than': less_than'(a;b) true: True subtype_rel: A ⊆B so_apply: x[s] sq_exists: x:A [B[x]] ge: i ≥  cand: c∧ B sq_type: SQType(T) iff: ⇐⇒ Q rev_implies:  Q eq_int: (i =z j) ifthenelse: if then else fi  bfalse: ff le: A ≤ B
Lemmas referenced :  subtract_wf int_formula_prop_less_lemma intformless_wf exp_wf2 decidable__lt set_subtype_base iff_weakening_equal nat_plus_subtype_nat nat_wf exp-minus true_wf squash_wf int_term_value_add_lemma int_term_value_subtract_lemma int_formula_prop_eq_lemma itermAdd_wf itermSubtract_wf intformeq_wf decidable__equal_int int_subtype_base subtype_base_sq nat_properties int-subtype-int_mod int_mod_wf subtype_rel_set less_than_wf modulus_wf_int_mod equal-wf-T-base nat_plus_wf set_wf int_lower_wf le_wf int_formula_prop_wf int_term_value_var_lemma int_term_value_minus_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermMinus_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_plus_properties sq_stable__equal int_lower_properties integer-nth-root-ext
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin setElimination rename hypothesisEquality dependent_set_memberEquality minusEquality isectElimination natural_numberEquality hypothesis because_Cache equalityTransitivity equalitySymmetry independent_functionElimination introduction sqequalRule imageMemberEquality baseClosed imageElimination unionElimination independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll comment applyEquality dependent_set_memberFormation productElimination instantiate addEquality universeEquality productEquality

Latex:
\mforall{}n:\{n:\mBbbN{}\msupplus{}|  (n  mod  2)  =  1\}  .  \mforall{}x:\{...0\}.    (\mexists{}r:\{...0\}  [((r  -  1)\^{}n  <  x  \mwedge{}  (x  \mleq{}  r\^{}n))])



Date html generated: 2019_06_20-PM-02_33_47
Last ObjectModification: 2019_03_19-AM-10_49_03

Theory : num_thy_1


Home Index