Nuprl Lemma : assert-is

Nuprl Lemma : assert-is_power

∀n:ℕ⁺. ∀x:ℤ. (↑is_power(n;x) ⇐⇒ ∃r:ℤ. (x = r^n ∈ ℤ))

Proof

Definitions occuring in Statement : is_power: is_power(n;z), exp: i^n, nat_plus: ℕ⁺, assert: ↑b, all: ∀x:A. B[x], exists: ∃x:A. B[x], iff: P ⇐⇒ Q, int: ℤ, equal: s = t ∈ T
Definitions unfolded in proof : all: ∀x:A. B[x], member: t ∈ T, nat_plus: ℕ⁺, or: P ∨ Q, is_power: is_power(n;z), uall: ∀[x:A]. B[x], uimplies: b supposing a, sq_type: SQType(T), implies: P ⇒ Q, guard: {T}, eq_int: (i =_z j), bfalse: ff, band: p ∧_b q, ifthenelse: if b then t else f fi , bool: 𝔹, unit: Unit, it: ⋅, btrue: tt, uiff: uiff(P;Q), and: P ∧ Q, less_than: a < b, less_than': less_than'(a;b), top: Top, true: True, squash: ↓T, not: ¬A, false: False, assert: ↑b, iff: P ⇐⇒ Q, exists: ∃x:A. B[x], decidable: Dec(P), satisfiable_int_formula: satisfiable_int_formula(fmla), prop: ℙ, rev_implies: P ⇐ Q, subtype_rel: A ⊆r B, bnot: ¬_bb, nat: ℕ, so_lambda: λ₂x.t[x], so_apply: x[s], ge: i ≥ j , int_nzero: ℤ^-^o, nequal: a ≠ b ∈ T
Lemmas referenced : mod2-cases, subtype_base_sq, int_subtype_base, lt_int_wf, eqtt_to_assert, assert_of_lt_int, istype-top, istype-void, mod2-is-zero, nat_plus_properties, decidable__le, full-omega-unsat, intformand_wf, intformnot_wf, intformle_wf, itermConstant_wf, itermVar_wf, intformeq_wf, itermMultiply_wf, intformless_wf, istype-int, int_formula_prop_and_lemma, int_formula_prop_not_lemma, int_formula_prop_le_lemma, int_term_value_constant_lemma, int_term_value_var_lemma, int_formula_prop_eq_lemma, int_term_value_mul_lemma, int_formula_prop_less_lemma, int_formula_prop_wf, eqff_to_assert, bool_cases_sqequal, bool_wf, bool_subtype_base, assert-bnot, iff_weakening_uiff, assert_wf, less_than_wf, istype-less_than, istype-nat, set_subtype_base, le_wf, assert-is-power, istype-le, mod2-is-one, itermAdd_wf, int_term_value_add_lemma, itermMinus_wf, int_term_value_minus_lemma, nat_plus_wf, equal_wf, squash_wf, true_wf, istype-universe, exp_mul, subtype_rel_self, iff_weakening_equal, decidable__equal_int, exp_wf2, exp2, exp-non-neg, square_non_neg, absval_wf, absval_squared, exp-minus, nat_properties, nat_wf, mod_bounds_1, nequal_wf, mod2-2n-plus-1, exp_wf_nat_plus, decidable__lt, eq_int_wf, assert_of_eq_int, neg_assert_of_eq_int, exp-positive
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, Error :lambdaFormation_alt, cut, introduction, extract_by_obid, sqequalHypSubstitution, dependent_functionElimination, thin, setElimination, rename, hypothesisEquality, hypothesis, unionElimination, instantiate, isectElimination, cumulativity, intEquality, independent_isectElimination, equalityTransitivity, equalitySymmetry, independent_functionElimination, sqequalRule, natural_numberEquality, Error :inhabitedIsType, equalityElimination, productElimination, lessCases, Error :isect_memberFormation_alt, axiomSqEquality, Error :isect_memberEquality_alt, Error :isectIsTypeImplies, independent_pairFormation, voidElimination, imageMemberEquality, baseClosed, imageElimination, because_Cache, promote_hyp, approximateComputation, Error :dependent_pairFormation_alt, Error :lambdaEquality_alt, int_eqEquality, Error :universeIsType, Error :productIsType, Error :equalityIstype, applyEquality, baseApply, closedConclusion, sqequalBase, Error :dependent_set_memberEquality_alt, minusEquality, universeEquality, multiplyEquality, addEquality, applyLambdaEquality

Latex:
\mforall{}n:\mBbbN{}\msupplus{}. \mforall{}x:\mBbbZ{}. (\muparrow{}is\_power(n;x) \mLeftarrow{}{}\mRightarrow{} \mexists{}r:\mBbbZ{}. (x = r\^{}n)) Date html generated: 2019_06_20-PM-02_34_39 Last ObjectModification: 2019_03_19-PM-00_16_28 Theory : num_thy_1 Home Index