Nuprl Lemma : prime-factors2

n:{2...}. (∃factors:{m:{2...}| prime(m)}  List [(n = Π(factors)  ∈ ℤ)])


Proof




Definitions occuring in Statement :  mul-list: Π(ns)  prime: prime(a) list: List int_upper: {i...} all: x:A. B[x] sq_exists: x:A [B[x]] set: {x:A| B[x]}  natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T uall: [x:A]. B[x] int_upper: {i...} sq_exists: x:A [B[x]] int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q le: A ≤ B prop: subtype_rel: A ⊆B so_lambda: λ2x.t[x] less_than: a < b squash: T so_apply: x[s] uimplies: supposing a so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] decidable: Dec(P) or: P ∨ Q int_nzero: -o nequal: a ≠ b ∈  not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top iff: ⇐⇒ Q sq_type: SQType(T) guard: {T} less_than': less_than'(a;b) nat_plus: + nat: true: True rev_implies:  Q uiff: uiff(P;Q) atomic: atomic(a) cand: c∧ B mul-list: Π(ns) 
Lemmas referenced :  int_seg_wf list_wf int_upper_wf prime_wf istype-int set_subtype_base lelt_wf int_subtype_base list_subtype_base le_wf istype-int_upper natrec_wf_intseg sq_exists_wf equal-wf-base subtype_rel_function subtype_rel_self decidable__proper_divisor divide_wfa int_upper_properties full-omega-unsat intformand_wf intformeq_wf itermVar_wf itermConstant_wf intformle_wf int_formula_prop_and_lemma istype-void int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf nequal_wf set-value-type equal_wf int-value-type istype-le istype-less_than divides_iff_div_exact subtype_base_sq div_bounds_1 upper_subtype_nat istype-false decidable__lt intformnot_wf intformless_wf int_formula_prop_not_lemma int_formula_prop_less_lemma decidable__equal_int itermMultiply_wf int_term_value_mul_lemma decidable__le mul_preserves_le merge-int_wf squash_wf true_wf istype-universe mul-list-merge subtype_rel_list iff_weakening_equal mul-list_wf multiply-is-int-iff false_wf cons_wf nil_wf atomic_imp_prime assoced_wf reducible_wf assoced_nelim reducible-nat less_than_wf divides_wf reduce_cons_lemma reduce_nil_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut thin sqequalRule functionIsType universeIsType introduction extract_by_obid sqequalHypSubstitution isectElimination natural_numberEquality setElimination rename hypothesisEquality hypothesis setIsType setEquality productElimination equalityIstype applyEquality intEquality lambdaEquality_alt imageElimination independent_isectElimination baseApply closedConclusion baseClosed inhabitedIsType sqequalBase equalitySymmetry because_Cache functionExtensionality dependent_functionElimination unionElimination dependent_set_memberEquality_alt approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt voidElimination independent_pairFormation cutEval equalityTransitivity productIsType instantiate cumulativity promote_hyp dependent_set_memberFormation_alt equalityIsType4 universeEquality imageMemberEquality multiplyEquality divideEquality pointwiseFunctionality

Latex:
\mforall{}n:\{2...\}.  (\mexists{}factors:\{m:\{2...\}|  prime(m)\}    List  [(n  =  \mPi{}(factors)  )])



Date html generated: 2020_05_20-AM-08_14_23
Last ObjectModification: 2019_11_27-PM-01_46_06

Theory : general


Home Index