---

Step * 1 of Lemma p-inv_wf

.....assertion..... 
1. p : {p:{2...}| prime(p)} 
2. a : {a:p-adics(p)| ¬((a 1) = 0 ∈ ℤ)} 
⊢ p-inv(p;a) = (λn.(TERMOF{p-adic-inv-lemma:o, \\v:l} p a n)) ∈ (n:ℕ+ ⟶ (∃c:ℕp^n [((c * (a n)) ≡ 1 mod p^n)]))
BY
{ ((FunExt THENA Auto)
   THEN RepUR ``p-inv`` 0
   THEN RepeatFor 2 ((CallByValueReduce 0⋅ THENA Auto))
   THEN Symmetry
   THEN (ShowSqEq
         THENL [(RW (AddrC [2] (TagC (mk_tag_term 1))) 0 THEN Reduce 0⋅ THEN Subst' sign(a n) ~ 1 0 THEN Auto); Auto]
   )
   THEN D -2
   THEN GenConclTerm ⌜a n⌝⋅
   THEN Auto
   THEN Unfold `sign` 0
   THEN AutoSplit) }

---

Latex:

---

Latex:
.....assertion..... 
1.  p  :  \{p:\{2...\}|  prime(p)\} 
2.  a  :  \{a:p-adics(p)|  \mneg{}((a  1)  =  0)\} 
\mvdash{}  p-inv(p;a)  =  (\mlambda{}n.(TERMOF\{p-adic-inv-lemma:o,  \mbackslash{}\mbackslash{}v:l\}  p  a  n))


By

---

Latex:
((FunExt  THENA  Auto)
  THEN  RepUR  ``p-inv``  0
  THEN  RepeatFor  2  ((CallByValueReduce  0\mcdot{}  THENA  Auto))
  THEN  Symmetry
  THEN  (ShowSqEq
              THENL  [(RW  (AddrC  [2]  (TagC  (mk\_tag\_term  1)))  0
                              THEN  Reduce
                              0\mcdot{}
                              THEN  Subst'  sign(a  n)  \msim{}  1  0
                              THEN  Auto)
                          ;  Auto]
  )
  THEN  D  -2
  THEN  GenConclTerm  \mkleeneopen{}a  n\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Unfold  `sign`  0
  THEN  AutoSplit)

---

Home Index