### Nuprl Lemma : reducible-nat

`∀n:ℤ. reducible(n) `` (∃n1:ℕ. (n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))) supposing 2 ≤ n`

Proof

Definitions occuring in Statement :  reducible: `reducible(a)` divides: `b | a` nat: `ℕ` less_than: `a < b` uimplies: `b supposing a` le: `A ≤ B` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` le: `A ≤ B` and: `P ∧ Q` not: `¬A` implies: `P `` Q` false: `False` uall: `∀[x:A]. B[x]` prop: `ℙ` reducible: `reducible(a)` exists: `∃x:A. B[x]` int_nzero: `ℤ-o` decidable: `Dec(P)` or: `P ∨ Q` nat: `ℕ` nequal: `a ≠ b ∈ T ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` cand: `A c∧ B` iff: `P `⇐⇒` Q` gt: `i > j` rev_implies: `P `` Q` divides: `b | a` guard: `{T}`
Lemmas referenced :  int_formula_prop_or_lemma intformor_wf decidable__or int_term_value_minus_lemma itermMinus_wf mul_preserves_le equal_wf assoced_elim decidable__equal_int int_formula_prop_eq_lemma int_term_value_mul_lemma int_formula_prop_less_lemma intformeq_wf itermMultiply_wf intformless_wf decidable__lt pos_mul_arg_bounds divides_wf less_than_wf and_wf int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt int_nzero_properties decidable__le le_wf reducible_wf less_than'_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut introduction sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality lambdaEquality dependent_functionElimination hypothesisEquality voidElimination lemma_by_obid isectElimination natural_numberEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry rename intEquality setElimination unionElimination dependent_pairFormation dependent_set_memberEquality independent_isectElimination int_eqEquality isect_memberEquality voidEquality independent_pairFormation computeAll independent_functionElimination because_Cache inlFormation minusEquality multiplyEquality inrFormation

Latex:
\mforall{}n:\mBbbZ{}.  reducible(n)  {}\mRightarrow{}  (\mexists{}n1:\mBbbN{}.  (n1  <  n  \mwedge{}  (2  \mleq{}  n1)  \mwedge{}  (n1  |  n)))  supposing  2  \mleq{}  n

Date html generated: 2016_05_15-PM-04_02_33
Last ObjectModification: 2016_01_16-AM-11_02_34

Theory : general

Home Index