---

Step * 2 1 2 1 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. X1 : ℕ
14. X2 : p-adics(p)
⊢ bpa-equiv(p;bpa-add(p;<X1, X2>;0(p));<X1, X2>)
BY
{ (RepUR ``bpa-add bpa-equiv`` 0
   THEN (Subst' imax(X1;0) ~ X1 0 THENA (RWO  "imax_unfold" 0 THEN Auto))
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (RW IntNormC 0 THENA Auto)
   THEN (Subst' X1 - 0 ~ X1 0 THENA Auto)
   THEN (Subst' p^0 ~ 1 0 THENA (RWO "exp-fastexp<" 0 THEN Auto))
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN Reduce 0
   THEN (RWW "exp-fastexp< p-mul-assoc p-mul-int p-distrib.1 p-distrib.2" 0 THENA Auto)
   THEN Reduce 0
   THEN (Subst' p^X1 * 1 ~ p^X1 0 THENA Auto)
   THEN Subst' ((p^X1 * p^X1) * 0) = 0 ∈ ℤ 0
   THEN Auto) }

---

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.  X1  :  \mBbbN{}
14.  X2  :  p-adics(p)
\mvdash{}  bpa-equiv(p;bpa-add(p;<X1,  X2>0(p));<X1,  X2>)


By

---

Latex:
(RepUR  ``bpa-add  bpa-equiv``  0
  THEN  (Subst'  imax(X1;0)  \msim{}  X1  0  THENA  (RWO    "imax\_unfold"  0  THEN  Auto))
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (RW  IntNormC  0  THENA  Auto)
  THEN  (Subst'  X1  -  0  \msim{}  X1  0  THENA  Auto)
  THEN  (Subst'  p\^{}0  \msim{}  1  0  THENA  (RWO  "exp-fastexp<"  0  THEN  Auto))
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  Reduce  0
  THEN  (RWW  "exp-fastexp<  p-mul-assoc  p-mul-int  p-distrib.1  p-distrib.2"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (Subst'  p\^{}X1  *  1  \msim{}  p\^{}X1  0  THENA  Auto)
  THEN  Subst'  ((p\^{}X1  *  p\^{}X1)  *  0)  =  0  0
  THEN  Auto)

---

Home Index