### 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

Proof

Definitions occuring in Statement :  mul-list: `Π(ns) ` prime: `prime(a)` permutation: `permutation(T;L1;L2)` list: `T List` nat: `ℕ` all: `∀x:A. B[x]` set: `{x:A| B[x]} ` int: `ℤ` equal: `s = 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: `P `` Q` subtype_rel: `A ⊆r B` uimplies: `b supposing a` so_apply: `x[s]` top: `Top` exists: `∃x:A. B[x]` divides: `b | a` false: `False` and: `P ∧ Q` prime: `prime(a)` assoced: `a ~ b` not: `¬A` label: `...\$L... t` guard: `{T}` permutation: `permutation(T;L1;L2)` cand: `A c∧ B` sq_type: `SQType(T)` so_apply: `x[s1;s2]` assoc: `Assoc(T;op)` infix_ap: `x f y` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` comm: `Comm(T;op)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` int_nzero: `ℤ-o` nequal: `a ≠ b ∈ T `
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

Latex:
\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