Nuprl Lemma : super-fact-int-prod-exp

[k:ℕ]. ((k)!! = Π((k i)^(i 1) i < k) ∈ ℤ)


Proof




Definitions occuring in Statement :  super-fact: (n)!! exp: i^n int-prod: Π(f[x] x < k) nat: uall: [x:A]. B[x] subtract: m add: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nat: implies:  Q false: False ge: i ≥  uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] not: ¬A all: x:A. B[x] top: Top and: P ∧ Q prop: super-fact: (n)!! primrec: primrec(n;b;c) int-prod: Π(f[x] x < k) le: A ≤ B less_than': less_than'(a;b) so_lambda: λ2x.t[x] guard: {T} int_seg: {i..j-} lelt: i ≤ j < k so_apply: x[s] decidable: Dec(P) or: P ∨ Q nat_plus: + sq_type: SQType(T) squash: T subtype_rel: A ⊆B true: True iff: ⇐⇒ Q rev_implies:  Q uiff: uiff(P;Q) subtract: m bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff bnot: ¬bb assert: b nequal: a ≠ b ∈  exp: i^n
Lemmas referenced :  nat_properties satisfiable-full-omega-tt intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf less_than_wf int-prod_wf false_wf le_wf exp_wf2 int_seg_properties subtract_wf int_seg_wf decidable__le intformnot_wf itermSubtract_wf int_formula_prop_not_lemma int_term_value_subtract_lemma super-fact-unroll subtype_base_sq int_subtype_base nat_wf equal_wf squash_wf true_wf itermAdd_wf int_term_value_add_lemma int-prod-factor int_seg_subtype_nat iff_weakening_equal exp_step decidable__lt not-lt-2 condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-commutes add_functionality_wrt_le add-associates add-zero le-add-cancel add-subtract-cancel fact0_redex_lemma int_prod0_lemma int-prod-split lelt_wf fact_unroll eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int intformeq_wf int_formula_prop_eq_lemma eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot neg_assert_of_eq_int primrec1_lemma decidable__equal_int itermMultiply_wf int_term_value_mul_lemma add-swap one-mul
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename intWeakElimination lambdaFormation natural_numberEquality independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation computeAll independent_functionElimination axiomEquality dependent_set_memberEquality because_Cache productElimination unionElimination instantiate cumulativity equalityTransitivity equalitySymmetry applyEquality imageElimination universeEquality addEquality imageMemberEquality baseClosed minusEquality multiplyEquality equalityElimination promote_hyp functionEquality

Latex:
\mforall{}[k:\mBbbN{}].  ((k)!!  =  \mPi{}((k  -  i)\^{}(i  +  1)  |  i  <  k))



Date html generated: 2018_05_21-PM-01_04_52
Last ObjectModification: 2018_01_28-PM-02_13_18

Theory : num_thy_1


Home Index