Nuprl Lemma : general-iroot-property

[n:ℕ+]. ∀[x:ℤ].
  (((0 ≤ x)  ((general-iroot(n;x)^n ≤ x) ∧ x < (general-iroot(n;x) 1)^n))
  ∧ ((x < 0 ∧ ((n mod 2) 1 ∈ ℤ))  ((x ≤ general-iroot(n;x)^n) ∧ (general-iroot(n;x) 1)^n < x))
  ∧ ((x < 0 ∧ ((n mod 2) 0 ∈ ℤ))  (general-iroot(n;x) 0 ∈ ℤ)))


Proof




Definitions occuring in Statement :  general-iroot: general-iroot(n;x) exp: i^n modulus: mod n nat_plus: + less_than: a < b uall: [x:A]. B[x] le: A ≤ B implies:  Q and: P ∧ Q subtract: m add: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T and: P ∧ Q implies:  Q general-iroot: general-iroot(n;x) prop: subtype_rel: A ⊆B nat_plus: + so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a has-value: (a)↓ all: x:A. B[x] bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) less_than: a < b less_than': less_than'(a;b) top: Top true: True squash: T not: ¬A false: False satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] bfalse: ff or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb ifthenelse: if then else fi  assert: b nequal: a ≠ b ∈  le: A ≤ B cand: c∧ B nat: int_lower: {...i} sq_exists: x:A [B[x]] decidable: Dec(P) sq_stable: SqStable(P)
Lemmas referenced :  le_wf less_than_wf equal-wf-T-base modulus_wf_int_mod subtype_rel_set int_mod_wf int-subtype-int_mod value-type-has-value nat_plus_wf set-value-type int-value-type lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int top_wf eq_int_wf assert_of_eq_int nat_plus_properties satisfiable-full-omega-tt intformand_wf intformeq_wf itermVar_wf itermConstant_wf int_formula_prop_and_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int member-less_than less_than'_wf exp_wf2 nat_plus_subtype_nat general-iroot_wf subtract_wf intformless_wf intformle_wf int_formula_prop_less_lemma int_formula_prop_le_lemma iroot-property int_subtype_base integer-nth-root2 all_wf int_lower_wf sq_exists_wf decidable__le intformnot_wf int_formula_prop_not_lemma squash_wf sq_stable__and sq_stable__le sq_stable__less_than
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation lambdaFormation extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality hypothesisEquality hypothesis productEquality because_Cache applyEquality sqequalRule intEquality lambdaEquality independent_isectElimination baseClosed callbyvalueReduce productElimination unionElimination equalityElimination equalityTransitivity equalitySymmetry lessCases axiomSqEquality isect_memberEquality voidElimination voidEquality imageMemberEquality imageElimination independent_functionElimination dependent_set_memberEquality int_eqReduceTrueSq setElimination rename dependent_pairFormation int_eqEquality dependent_functionElimination computeAll promote_hyp instantiate cumulativity int_eqReduceFalseSq independent_pairEquality axiomEquality addEquality setEquality

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[x:\mBbbZ{}].
    (((0  \mleq{}  x)  {}\mRightarrow{}  ((general-iroot(n;x)\^{}n  \mleq{}  x)  \mwedge{}  x  <  (general-iroot(n;x)  +  1)\^{}n))
    \mwedge{}  ((x  <  0  \mwedge{}  ((n  mod  2)  =  1))  {}\mRightarrow{}  ((x  \mleq{}  general-iroot(n;x)\^{}n)  \mwedge{}  (general-iroot(n;x)  -  1)\^{}n  <  x))
    \mwedge{}  ((x  <  0  \mwedge{}  ((n  mod  2)  =  0))  {}\mRightarrow{}  (general-iroot(n;x)  =  0)))



Date html generated: 2019_06_20-PM-02_35_08
Last ObjectModification: 2019_03_19-AM-10_49_49

Theory : num_thy_1


Home Index