Nuprl Lemma : qexpfact

Nuprl Lemma : qexpfact_wf

∀[n:ℕ]. ∀[x:{q:ℚ| 0 ≤ q} ]. ∀[p:ℚ]. ∀[b:{b:ℤ| b = (n)! ∈ ℤ} ].  (qexpfact(n;x;p;b) ∈ {n...})

Proof

Definitions occuring in Statement : qexpfact: qexpfact(n;x;p;b), qle: r ≤ s, rationals: ℚ, fact: (n)!, int_upper: {i...}, nat: ℕ, uall: ∀[x:A]. B[x], member: t ∈ T, set: {x:A| B[x]} , natural_number: $n, int: ℤ, equal: s = t ∈ T
Definitions unfolded in proof : uall: ∀[x:A]. B[x], member: t ∈ T, uimplies: b supposing a, sq_type: SQType(T), all: ∀x:A. B[x], implies: P ⇒ Q, guard: {T}, subtype_rel: A ⊆r B, decidable: Dec(P), or: P ∨ Q, nat: ℕ, so_lambda: λ₂x.t[x], so_apply: x[s], prop: ℙ, has-value: (a)↓, true: True, squash: ↓T, assert: ↑b, bnot: ¬_bb, bfalse: ff, top: Top, not: ¬A, false: False, exists: ∃x:A. B[x], satisfiable_int_formula: satisfiable_int_formula(fmla), ge: i ≥ j , int_upper: {i...}, ifthenelse: if b then t else f fi , iff: P ⇐⇒ Q, nat_plus: ℕ⁺, and: P ∧ Q, uiff: uiff(P;Q), btrue: tt, it: ⋅, unit: Unit, bool: 𝔹, qexpfact: qexpfact(n;x;p;b), less_than': less_than'(a;b), subtract: n - m, rev_implies: P ⇐ Q, le: A ≤ B, rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced : subtype_base_sq, int_subtype_base, decidable__equal_rationals, istype-int, set_subtype_base, le_wf, rationals_wf, qle_wf, int-subtype-rationals, istype-nat, nat_plus_wf, int_term_value_constant_lemma, int_term_value_add_lemma, itermConstant_wf, itermAdd_wf, qmul_wf, value-type-has-value, true_wf, squash_wf, not_wf, assert-bnot, bool_subtype_base, bool_cases_sqequal, equal_wf, eqff_to_assert, int_formula_prop_wf, int_term_value_var_lemma, int_formula_prop_le_lemma, int_formula_prop_not_lemma, itermVar_wf, intformle_wf, intformnot_wf, satisfiable-full-omega-tt, decidable__le, nat_properties, iff_weakening_equal, less_than_wf, subtype_rel_set, assert-q_less-eq, eqtt_to_assert, bool_wf, fact_wf, q_less_wf, qless_wf, le-add-cancel, add-zero, add-associates, add_functionality_wrt_le, add-commutes, minus-one-mul-top, zero-add, minus-one-mul, minus-add, condition-implies-le, not-lt-2, false_wf, decidable__lt, mul_bounds_1b, qless-int, equal-wf-T-base, qmul_zero_qrng, qle_complement_qorder, qle_antisymmetry, q-archimedean, fact-greater-exp, qexp_wf, exp_wf2, qmul-mul, qexp-exp, qexp_preserves_qle, qle_weakening_lt_qorder, qmul_preserves_qle2, qle-int, full-omega-unsat, intformand_wf, int_formula_prop_and_lemma, istype-void, qle_witness, qmul_comm_qrng, subtype_rel_self, qexp-nonneg, qle_transitivity_qorder, qless_transitivity_1_qorder, qless_transitivity_2_qorder, fact-non-decreasing, int_term_value_subtract_lemma, itermSubtract_wf, subtract_wf, nat_wf, ge_wf, int_formula_prop_less_lemma, intformless_wf, qmul_one_qrng, qexp-zero, add-subtract-cancel, int_formula_prop_eq_lemma, intformeq_wf, fact_unroll_1, add-swap, qmul_assoc_qrng, exp_unroll_q, qmul_com, int_upper_properties, int_upper_subtype_int_upper
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, isect_memberFormation_alt, introduction, cut, setElimination, thin, rename, instantiate, extract_by_obid, sqequalHypSubstitution, isectElimination, cumulativity, intEquality, independent_isectElimination, hypothesis, dependent_functionElimination, hypothesisEquality, equalityTransitivity, equalitySymmetry, independent_functionElimination, natural_numberEquality, applyEquality, because_Cache, sqequalRule, unionElimination, axiomEquality, setIsType, equalityIstype, baseApply, closedConclusion, baseClosed, lambdaEquality_alt, inhabitedIsType, sqequalBase, isect_memberEquality_alt, isectIsTypeImplies, universeIsType, addEquality, multiplyEquality, callbyvalueReduce, imageMemberEquality, universeEquality, imageElimination, promote_hyp, computeAll, voidEquality, voidElimination, isect_memberEquality, int_eqEquality, dependent_pairFormation, dependent_set_memberEquality, lambdaEquality, productElimination, equalityElimination, lambdaFormation, applyLambdaEquality, hyp_replacement, minusEquality, independent_pairFormation, lambdaFormation_alt, dependent_pairFormation_alt, approximateComputation, intWeakElimination, levelHypothesis, addLevel

Latex:
\mforall{}[n:\mBbbN{}]. \mforall{}[x:\{q:\mBbbQ{}| 0 \mleq{} q\} ]. \mforall{}[p:\mBbbQ{}]. \mforall{}[b:\{b:\mBbbZ{}| b = (n)!\} ]. (qexpfact(n;x;p;b) \mmember{} \{n...\}) Date html generated: 2020_05_20-AM-09_26_27 Last ObjectModification: 2019_11_27-PM-01_38_46 Theory : rationals Home Index