Nuprl Lemma : triangular-num_wf

[n:ℕ]. (t(n) ∈ ℕ)


Proof




Definitions occuring in Statement :  triangular-num: t(n) nat: uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T triangular-num: t(n) nat: ge: i ≥  all: x:A. B[x] decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False implies:  Q not: ¬A top: Top and: P ∧ Q prop: nat_plus: + less_than: a < b squash: T less_than': less_than'(a;b) true: True
Lemmas referenced :  nat_wf less_than_wf le_wf int_formula_prop_wf int_term_value_var_lemma int_term_value_add_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermAdd_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_properties mul_bounds_1a divide_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin dependent_set_memberEquality multiplyEquality setElimination rename hypothesisEquality addEquality natural_numberEquality hypothesis dependent_functionElimination unionElimination independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll imageMemberEquality baseClosed axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[n:\mBbbN{}].  (t(n)  \mmember{}  \mBbbN{})



Date html generated: 2016_05_15-PM-05_19_16
Last ObjectModification: 2016_01_16-AM-11_39_18

Theory : general


Home Index