`∀p:{p:{2...}| prime(p)} . ∀a:{a:p-adics(p)| ¬((a 1) = 0 ∈ ℤ)} . ∀n:ℕ+.  (∃c:ℕp^n [((c * (a n)) ≡ 1 mod p^n)])`

Proof

Definitions occuring in Statement :  p-adics: `p-adics(p)` eqmod: `a ≡ b mod m` prime: `prime(a)` exp: `i^n` int_upper: `{i...}` int_seg: `{i..j-}` nat_plus: `ℕ+` all: `∀x:A. B[x]` sq_exists: `∃x:A [B[x]]` not: `¬A` set: `{x:A| B[x]} ` apply: `f a` multiply: `n * m` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  member: `t ∈ T` subtract: `n - m` spreadn: spread7 genrec-ap: genrec-ap p-reduce: `i mod(p^n)` modulus: `a mod n` p-adic-inv-lemma1 gcd-reduce-coprime gcd-reduce-ext uall: `∀[x:A]. B[x]` so_lambda: `so_lambda(x,y,z,w.t[x; y; z; w])` so_apply: `x[s1;s2;s3;s4]` so_lambda: `λ2x y.t[x; y]` top: `Top` so_apply: `x[s1;s2]` uimplies: `b supposing a`
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry isectElimination baseClosed isect_memberEquality_alt voidElimination independent_isectElimination

Latex:
\mforall{}p:\{p:\{2...\}|  prime(p)\}  .  \mforall{}a:\{a:p-adics(p)|  \mneg{}((a  1)  =  0)\}  .  \mforall{}n:\mBbbN{}\msupplus{}.
(\mexists{}c:\mBbbN{}p\^{}n  [((c  *  (a  n))  \mequiv{}  1  mod  p\^{}n)])

Date html generated: 2019_10_15-AM-10_34_47
Last ObjectModification: 2019_06_20-PM-06_50_52

Theory : rings_1

Home Index