### Nuprl Lemma : p-digits_wf

`∀[p:ℕ+]. ∀[a:p-adics(p)].  (p-digits(p;a) ∈ ℕ+ ⟶ ℕp)`

Proof

Definitions occuring in Statement :  p-digits: `p-digits(p;a)` p-adics: `p-adics(p)` int_seg: `{i..j-}` nat_plus: `ℕ+` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` p-digits: `p-digits(p;a)` nat_plus: `ℕ+`
Lemmas referenced :  p-digit_wf nat_plus_wf p-adics_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lambdaEquality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry setElimination rename isect_memberEquality because_Cache

Latex:
\mforall{}[p:\mBbbN{}\msupplus{}].  \mforall{}[a:p-adics(p)].    (p-digits(p;a)  \mmember{}  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbN{}p)

Date html generated: 2018_05_21-PM-03_21_33
Last ObjectModification: 2018_05_19-AM-08_18_35

Theory : rings_1

Home Index