Nuprl Lemma : prime-factors-unique

ps:{m:ℕprime(m)}  List. ∀qs:{qs:{m:ℕprime(m)}  List| Π(ps)  = Π(qs)  ∈ ℤ.  permutation(ℤ;ps;qs)

This theorem is one of freek's list of 100 theorems


Definitions occuring in Statement :  mul-list: Π(ns)  prime: prime(a) permutation: permutation(T;L1;L2) list: List nat: all: x:A. B[x] set: {x:A| B[x]}  int: equal: t ∈ T
Definitions unfolded in proof :  mul-list: Π(ns)  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T nat: prop: so_lambda: λ2x.t[x] implies:  Q subtype_rel: A ⊆B uimplies: supposing a so_apply: x[s] top: Top exists: x:A. B[x] divides: a false: False and: P ∧ Q prime: prime(a) assoced: b not: ¬A label: ...$L... t guard: {T} permutation: permutation(T;L1;L2) cand: c∧ B sq_type: SQType(T) so_apply: x[s1;s2] assoc: Assoc(T;op) infix_ap: y ge: i ≥  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) comm: Comm(T;op) iff: ⇐⇒ Q rev_implies:  Q int_nzero: -o nequal: a ≠ b ∈ 
Lemmas referenced :  list_induction nat_wf prime_wf list_wf equal-wf-base list_subtype_base set_subtype_base istype-nat le_wf istype-int int_subtype_base permutation_wf subtype_rel_list reduce_nil_lemma reduce_cons_lemma set_wf nil_wf reduce_wf equal-wf-base-T permutation-nil one_divs_any positive-prime-divides-product l_member-permutation cons_wf permutation_inversion inject_wf int_seg_wf length_wf permute_list_wf subtype_base_sq reduce-permutation nat_properties decidable__equal_int full-omega-unsat intformnot_wf intformeq_wf itermMultiply_wf itermVar_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_mul_lemma int_term_value_var_lemma int_formula_prop_wf permutation_functionality_wrt_permutation cons_functionality_wrt_permutation permutation_weakening mul_cancel_in_eq nequal_wf mul-list_wf equal_wf
Rules used in proof :  cut sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation_alt thin introduction extract_by_obid sqequalHypSubstitution isectElimination setEquality hypothesis setElimination rename because_Cache lambdaEquality_alt functionEquality hypothesisEquality intEquality baseApply closedConclusion baseClosed applyEquality independent_isectElimination natural_numberEquality setIsType universeIsType independent_functionElimination dependent_functionElimination Error :memTop,  functionIsType equalityIstype sqequalBase equalitySymmetry voidEquality voidElimination isect_memberEquality multiplyEquality lambdaEquality lambdaFormation dependent_pairFormation productElimination independent_pairFormation inhabitedIsType dependent_pairFormation_alt equalityTransitivity promote_hyp productIsType instantiate cumulativity isect_memberFormation_alt unionElimination approximateComputation int_eqEquality isect_memberEquality_alt axiomEquality isectIsTypeImplies dependent_set_memberEquality_alt levelHypothesis addLevel

\mforall{}ps:\{m:\mBbbN{}|  prime(m)\}    List.  \mforall{}qs:\{qs:\{m:\mBbbN{}|  prime(m)\}    List|  \mPi{}(ps)    =  \mPi{}(qs)  \}  .    permutation(\mBbbZ{};ps;qs)

Date html generated: 2020_05_20-AM-08_08_03
Last ObjectModification: 2020_01_04-PM-11_11_31

Theory : general

Home Index