### Nuprl Lemma : p-unit-iff

`∀p:{p:{2...}| prime(p)} . ∀a:p-adics(p).  (¬((a 1) = 0 ∈ ℤ) `⇐⇒` ∃b:p-adics(p). (a * b = 1(p) ∈ p-adics(p)))`

Proof

Definitions occuring in Statement :  p-int: `k(p)` p-mul: `x * y` p-adics: `p-adics(p)` prime: `prime(a)` int_upper: `{i...}` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` not: `¬A` set: `{x:A| B[x]} ` apply: `f a` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` p-adics: `p-adics(p)` nat_plus: `ℕ+` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` true: `True` subtype_rel: `A ⊆r B` int_seg: `{i..j-}` nat: `ℕ` le: `A ≤ B` false: `False` not: `¬A` int_upper: `{i...}` rev_implies: `P `` Q` so_lambda: `λ2x.t[x]` decidable: `Dec(P)` or: `P ∨ Q` uiff: `uiff(P;Q)` uimplies: `b supposing a` so_apply: `x[s]` exists: `∃x:A. B[x]` p-units: `p-units(p)` guard: `{T}` sq_stable: `SqStable(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` subtract: `n - m` p-int: `k(p)` p-mul: `x * y` p-reduce: `i mod(p^n)` sq_type: `SQType(T)` lelt: `i ≤ j < k`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin intEquality applyEquality setElimination rename hypothesisEquality hypothesis dependent_set_memberEquality natural_numberEquality sqequalRule imageMemberEquality baseClosed lambdaEquality independent_functionElimination voidElimination because_Cache productElimination dependent_functionElimination unionElimination independent_isectElimination dependent_pairFormation addEquality imageElimination approximateComputation int_eqEquality isect_memberEquality voidEquality functionExtensionality addLevel levelHypothesis equalitySymmetry equalityTransitivity applyLambdaEquality minusEquality universeEquality instantiate cumulativity promote_hyp

Latex:
\mforall{}p:\{p:\{2...\}|  prime(p)\}  .  \mforall{}a:p-adics(p).    (\mneg{}((a  1)  =  0)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}b:p-adics(p).  (a  *  b  =  1(p)))

Date html generated: 2018_05_21-PM-03_23_24
Last ObjectModification: 2018_05_19-AM-08_21_50

Theory : rings_1

Home Index