### Nuprl Lemma : pa-inv_wf

`∀p:{p:{2...}| prime(p)} . ∀x:{x:padic(p)| pa-sep(p;x;0(p))} .`
`  (pa-inv(p;x) ∈ {y:padic(p)| pa-mul(p;x;y) = 1(p) ∈ padic(p)} )`

Proof

Definitions occuring in Statement :  pa-inv: `pa-inv(p;x)` pa-sep: `pa-sep(p;x;y)` pa-mul: `pa-mul(p;x;y)` pa-int: `k(p)` padic: `padic(p)` prime: `prime(a)` int_upper: `{i...}` all: `∀x:A. B[x]` member: `t ∈ T` set: `{x:A| B[x]} ` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` padic: `padic(p)` pa-int: `k(p)` pa-sep: `pa-sep(p;x;y)` nat: `ℕ` decidable: `Dec(P)` or: `P ∨ Q` uall: `∀[x:A]. B[x]` uimplies: `b supposing a` sq_type: `SQType(T)` implies: `P `` Q` guard: `{T}` int_upper: `{i...}` subtype_rel: `A ⊆r B` prop: `ℙ` not: `¬A` false: `False` eq_int: `(i =z j)` ifthenelse: `if b then t else f fi ` btrue: `tt` p-sep: `p-sep(x;y)` exists: `∃x:A. B[x]` p-int: `k(p)` p-reduce: `i mod(p^n)` nat_plus: `ℕ+` le: `A ≤ B` and: `P ∧ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` uiff: `uiff(P;Q)` less_than': `less_than'(a;b)` true: `True` int_seg: `{i..j-}` lelt: `i ≤ j < k` pa-inv: `pa-inv(p;x)` p-adics: `p-adics(p)` subtract: `n - m` sq_stable: `SqStable(P)` squash: `↓T` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` so_lambda: `λ2x.t[x]` so_apply: `x[s]` has-value: `(a)↓` bnot: `¬bb` ge: `i ≥ j ` less_than: `a < b` p-units: `p-units(p)` basic-padic: `basic-padic(p)` bool: `𝔹` unit: `Unit` it: `⋅` bfalse: `ff` assert: `↑b` pa-mul: `pa-mul(p;x;y)` bpa-mul: `bpa-mul(p;x;y)` bpa-equiv: `bpa-equiv(p;x;y)`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt setElimination thin rename cut sqequalHypSubstitution productElimination introduction extract_by_obid dependent_functionElimination hypothesisEquality hypothesis natural_numberEquality unionElimination instantiate isectElimination cumulativity intEquality independent_isectElimination because_Cache independent_functionElimination setIsType universeIsType applyEquality sqequalRule equalityTransitivity equalitySymmetry voidElimination dependent_set_memberEquality_alt independent_pairFormation productIsType lambdaEquality_alt addEquality minusEquality dependent_pairFormation_alt imageMemberEquality baseClosed imageElimination approximateComputation int_eqEquality isect_memberEquality_alt equalityIsType4 applyLambdaEquality inhabitedIsType equalityIsType1 isectIsType callbyvalueReduce universeEquality equalityIsType3 lambdaFormation lambdaEquality dependent_set_memberEquality baseApply closedConclusion independent_pairEquality dependent_pairEquality_alt equalityElimination equalityIsType2 promote_hyp functionIsType

Latex:
\mforall{}p:\{p:\{2...\}|  prime(p)\}  .  \mforall{}x:\{x:padic(p)|  pa-sep(p;x;0(p))\}  .
(pa-inv(p;x)  \mmember{}  \{y:padic(p)|  pa-mul(p;x;y)  =  1(p)\}  )

Date html generated: 2019_10_15-AM-10_36_44
Last ObjectModification: 2018_10_08-PM-05_26_06

Theory : rings_1

Home Index