### Nuprl Lemma : p-unit-part-unique

`∀[p:{2...}]. ∀[k,j:ℕ]. ∀[a,b:p-units(p)].`
`  (a = b ∈ p-units(p)) ∧ (k = j ∈ ℤ) supposing p^k(p) * a = p^j(p) * b ∈ p-adics(p)`

Proof

Definitions occuring in Statement :  p-units: `p-units(p)` p-int: `k(p)` p-mul: `x * y` p-adics: `p-adics(p)` exp: `i^n` int_upper: `{i...}` nat: `ℕ` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` and: `P ∧ Q` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` int_upper: `{i...}` subtype_rel: `A ⊆r B` nat: `ℕ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` implies: `P `` Q` sq_stable: `SqStable(P)` squash: `↓T` nat_plus: `ℕ+` all: `∀x:A. B[x]` and: `P ∧ Q` le: `A ≤ B` cand: `A c∧ B` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` not: `¬A` rev_implies: `P `` Q` false: `False` uiff: `uiff(P;Q)` less_than': `less_than'(a;b)` true: `True` p-units: `p-units(p)` sq_type: `SQType(T)` subtract: `n - m` label: `...\$L... t` top: `Top` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` ge: `i ≥ j ` guard: `{T}` prop: `ℙ` int_seg: `{i..j-}` less_than: `a < b` p-adics: `p-adics(p)` p-mul: `x * y` p-int: `k(p)` p-reduce: `i mod(p^n)` nequal: `a ≠ b ∈ T ` int_nzero: `ℤ-o`
Lemmas referenced :  sq_stable__and equal_wf p-units_wf equal-wf-base set_subtype_base le_wf istype-int int_subtype_base sq_stable__equal p-adics_wf p-mul_wf subtype_rel_sets_simple less_than_wf decidable__lt istype-false not-lt-2 add_functionality_wrt_le add-commutes zero-add le-add-cancel istype-le p-int_wf exp_wf2 istype-nat istype-int_upper nat_wf iff_weakening_equal subtype_rel_self add-zero zero-mul add-mul-special add-associates add-swap minus-minus minus-add minus-one-mul-top minus-one-mul condition-implies-le less-iff-le exp-positive int_term_value_mul_lemma int_formula_prop_eq_lemma itermMultiply_wf intformeq_wf multiply-is-int-iff decidable__equal_int int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_subtract_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformless_wf itermVar_wf itermSubtract_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf full-omega-unsat decidable__le int_upper_properties nat_properties subtract_wf exp_add false_wf exp_wf_nat_plus true_wf squash_wf nat_plus_wf subtype_base_sq p-mul-int p-mul-assoc p-mul-int-cancelation-1 int_seg_wf exp1 rem-exact exp_step rem_bounds_1 nat_plus_properties nequal_wf subtype_rel_sets upper_subtype_nat nat_plus_subtype_nat exp_wf4 modulus-is-rem p-reduce-0 istype-universe istype-less_than itermAdd_wf int_term_value_add_lemma p-adic-property eqmod_wf equal-wf-T-base not_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename because_Cache hypothesis hypothesisEquality isect_memberEquality_alt intEquality applyEquality sqequalRule lambdaEquality_alt natural_numberEquality independent_isectElimination equalityIstype inhabitedIsType independent_functionElimination lambdaFormation_alt dependent_functionElimination axiomEquality functionIsTypeImplies imageMemberEquality baseClosed imageElimination universeIsType independent_pairFormation productElimination unionElimination voidElimination Error :memTop,  minusEquality addEquality closedConclusion baseApply promote_hyp pointwiseFunctionality voidEquality isect_memberEquality int_eqEquality dependent_pairFormation approximateComputation lambdaFormation dependent_set_memberEquality universeEquality equalitySymmetry equalityTransitivity lambdaEquality cumulativity instantiate setEquality dependent_pairFormation_alt dependent_set_memberEquality_alt functionEquality multiplyEquality functionIsType

Latex:
\mforall{}[p:\{2...\}].  \mforall{}[k,j:\mBbbN{}].  \mforall{}[a,b:p-units(p)].    (a  =  b)  \mwedge{}  (k  =  j)  supposing  p\^{}k(p)  *  a  =  p\^{}j(p)  *  b

Date html generated: 2020_05_19-PM-10_08_30
Last ObjectModification: 2020_01_08-PM-06_00_00

Theory : rings_1

Home Index