Nuprl Lemma : fact-positive

[m:ℕ]. (1 ≤ (m)!)


Proof




Definitions occuring in Statement :  fact: (n)! nat: uall: [x:A]. B[x] le: A ≤ B natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nat: ge: i ≥  all: x:A. B[x] prop: subtype_rel: A ⊆B decidable: Dec(P) or: P ∨ Q nat_plus: + guard: {T} 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 le: A ≤ B
Lemmas referenced :  nat_wf less_than'_wf int_formula_prop_wf int_formula_prop_le_lemma int_formula_prop_not_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_and_lemma intformle_wf intformnot_wf itermVar_wf itermConstant_wf intformless_wf intformand_wf satisfiable-full-omega-tt less_than_wf nat_plus_properties le_wf fact_wf decidable__le nat_properties
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename dependent_functionElimination natural_numberEquality dependent_set_memberEquality applyEquality because_Cache sqequalRule unionElimination equalityTransitivity equalitySymmetry lambdaEquality setEquality intEquality independent_isectElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll productElimination independent_pairEquality axiomEquality

Latex:
\mforall{}[m:\mBbbN{}].  (1  \mleq{}  (m)!)



Date html generated: 2018_05_21-PM-01_01_32
Last ObjectModification: 2018_01_28-PM-02_12_16

Theory : num_thy_1


Home Index