---

Step * 2 2 2 of Lemma padic-ring_wf


1. p : {2...}
2. ℤ(p) ∈ RngSig
3. ∀[x,y,z:p-adics(p)].  (x + y + z = x + y + z ∈ p-adics(p))
4. ∀[x:p-adics(p)]. ((x + 0(p) = x ∈ p-adics(p)) ∧ (0(p) + x = x ∈ p-adics(p)))
5. ∀[x:p-adics(p)]. ((x + -(x) = 0(p) ∈ p-adics(p)) ∧ (-(x) + x = 0(p) ∈ p-adics(p)))
6. ∀[x,y,z:p-adics(p)].  (x * y * z = x * y * z ∈ p-adics(p))
7. ∀[x:p-adics(p)]. ((x * 1(p) = x ∈ p-adics(p)) ∧ (1(p) * x = x ∈ p-adics(p)))
8. ∀[a,x,y:p-adics(p)].  ((a * x + y = a * x + a * y ∈ p-adics(p)) ∧ (x + y * a = x * a + y * a ∈ p-adics(p)))
9. ∀[x,y:p-adics(p)].  (x * y = y * x ∈ p-adics(p))
10. ∀a,b:basic-padic(p).  bpa-equiv(p;bpa-mul(p;a;b);pa-mul(p;a;b))
11. ∀a,b:basic-padic(p).  bpa-equiv(p;bpa-add(p;a;b);pa-add(p;a;b))
12. x : padic(p)
13. pa-add(p;x;pa-minus(p;x)) = 0(p) ∈ padic(p)
⊢ pa-add(p;pa-minus(p;x);x) = 0(p) ∈ padic(p)
BY
{ ((Assert ⌜pa-add(p;bpa-minus(p;x);x) = 0(p) ∈ padic(p)⌝⋅
   THENM (NthHypEqTrans (-1) THEN BLemma `pa-add_functionality` THEN Auto THEN RelRST THEN Auto)
   )
   THEN (Assert ⌜pa-add(p;bpa-minus(p;x);x) = bpa-norm(p;0(p)) ∈ padic(p)⌝⋅ THENM (NthHypEqTrans (-1) THEN Auto))
   THEN Unfold `pa-add` 0
   THEN (RWO "bpa-equiv-iff-norm2" 0 THENA Auto)
   THEN (GenConcl ⌜x = X ∈ basic-padic(p)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN RepUR ``bpa-equiv bpa-add pa-minus pa-int mkpadic`` 0) }

1
1. p : {2...}
2. ℤ(p) ∈ RngSig
3. ∀[x,y,z:p-adics(p)].  (x + y + z = x + y + z ∈ p-adics(p))
4. ∀[x:p-adics(p)]. ((x + 0(p) = x ∈ p-adics(p)) ∧ (0(p) + x = x ∈ p-adics(p)))
5. ∀[x:p-adics(p)]. ((x + -(x) = 0(p) ∈ p-adics(p)) ∧ (-(x) + x = 0(p) ∈ p-adics(p)))
6. ∀[x,y,z:p-adics(p)].  (x * y * z = x * y * z ∈ p-adics(p))
7. ∀[x:p-adics(p)]. ((x * 1(p) = x ∈ p-adics(p)) ∧ (1(p) * x = x ∈ p-adics(p)))
8. ∀[a,x,y:p-adics(p)].  ((a * x + y = a * x + a * y ∈ p-adics(p)) ∧ (x + y * a = x * a + y * a ∈ p-adics(p)))
9. ∀[x,y:p-adics(p)].  (x * y = y * x ∈ p-adics(p))
10. ∀a,b:basic-padic(p).  bpa-equiv(p;bpa-mul(p;a;b);pa-mul(p;a;b))
11. ∀a,b:basic-padic(p).  bpa-equiv(p;bpa-add(p;a;b);pa-add(p;a;b))
12. x : padic(p)
13. pa-add(p;x;pa-minus(p;x)) = 0(p) ∈ padic(p)
14. X1 : ℕ
15. X2 : p-adics(p)
⊢ let n,a = eval k = imax(X1;X1) in
            eval c = p^k - X1 in
            eval d = p^k - X1 in
              <k, c(p) * -(X2) + d(p) * X2> 
  in 1(p) * a = p^n(p) * 0(p) ∈ p-adics(p)

---

Latex:

---

Latex:

1.  p  :  \{2...\}
2.  \mBbbZ{}(p)  \mmember{}  RngSig
3.  \mforall{}[x,y,z:p-adics(p)].    (x  +  y  +  z  =  x  +  y  +  z)
4.  \mforall{}[x:p-adics(p)].  ((x  +  0(p)  =  x)  \mwedge{}  (0(p)  +  x  =  x))
5.  \mforall{}[x:p-adics(p)].  ((x  +  -(x)  =  0(p))  \mwedge{}  (-(x)  +  x  =  0(p)))
6.  \mforall{}[x,y,z:p-adics(p)].    (x  *  y  *  z  =  x  *  y  *  z)
7.  \mforall{}[x:p-adics(p)].  ((x  *  1(p)  =  x)  \mwedge{}  (1(p)  *  x  =  x))
8.  \mforall{}[a,x,y:p-adics(p)].    ((a  *  x  +  y  =  a  *  x  +  a  *  y)  \mwedge{}  (x  +  y  *  a  =  x  *  a  +  y  *  a))
9.  \mforall{}[x,y:p-adics(p)].    (x  *  y  =  y  *  x)
10.  \mforall{}a,b:basic-padic(p).    bpa-equiv(p;bpa-mul(p;a;b);pa-mul(p;a;b))
11.  \mforall{}a,b:basic-padic(p).    bpa-equiv(p;bpa-add(p;a;b);pa-add(p;a;b))
12.  x  :  padic(p)
13.  pa-add(p;x;pa-minus(p;x))  =  0(p)
\mvdash{}  pa-add(p;pa-minus(p;x);x)  =  0(p)


By

---

Latex:
((Assert  \mkleeneopen{}pa-add(p;bpa-minus(p;x);x)  =  0(p)\mkleeneclose{}\mcdot{}
  THENM  (NthHypEqTrans  (-1)  THEN  BLemma  `pa-add\_functionality`  THEN  Auto  THEN  RelRST  THEN  Auto)
  )
  THEN  (Assert  \mkleeneopen{}pa-add(p;bpa-minus(p;x);x)  =  bpa-norm(p;0(p))\mkleeneclose{}\mcdot{}  THENM  (NthHypEqTrans  (-1)  THEN  Auto))
  THEN  Unfold  `pa-add`  0
  THEN  (RWO  "bpa-equiv-iff-norm2"  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}x  =  X\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  RepUR  ``bpa-equiv  bpa-add  pa-minus  pa-int  mkpadic``  0)

---

Home Index