### 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) p^j(p) b ∈ p-adics(p)

Proof

Definitions occuring in Statement :  p-units: p-units(p) p-int: k(p) p-mul: y p-adics: p-adics(p) exp: i^n int_upper: {i...} nat: uimplies: supposing a uall: [x:A]. B[x] and: P ∧ Q natural_number: \$n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T int_upper: {i...} subtype_rel: A ⊆B nat: so_lambda: λ2x.t[x] so_apply: x[s] implies:  Q sq_stable: SqStable(P) squash: T nat_plus: + all: x:A. B[x] and: P ∧ Q le: A ≤ B cand: c∧ B decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q not: ¬A rev_implies:  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: m label: ...\$L... t top: Top exists: x:A. B[x] satisfiable_int_formula: satisfiable_int_formula(fmla) ge: i ≥  guard: {T} prop: int_seg: {i..j-} less_than: a < b p-adics: p-adics(p) p-mul: y p-int: k(p) p-reduce: mod(p^n) nequal: a ≠ b ∈  int_nzero: -o
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