---

Step * 2 5 1 1 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. IsMonoid(padic(p);λu,v. pa-mul(p;u;v);1(p))
13. a : padic(p)
14. x : padic(p)
15. y : padic(p)
16. X1 : ℕ
17. X2 : p-adics(p)
18. Y1 : ℕ
19. Y2 : p-adics(p)
20. Z1 : ℕ
21. Z2 : p-adics(p)
22. M : ℤ
23. imax(X1;Y1) = M ∈ ℤ
24. X1 ≤ M
25. Y1 ≤ M
26. v : ℤ
27. (M - X1) = v ∈ ℤ
28. v1 : ℤ
29. (M - Y1) = v1 ∈ ℤ
30. v2 : ℤ
31. (Z1 + M) = v2 ∈ ℤ
⊢ p^v2(p) * Z2 * p^v(p) * X2 + p^v2(p) * Z2 * p^v1(p) * Y2
= p^(v2 + v)(p) * Z2 * X2 + p^(v2 + v1)(p) * Z2 * Y2
∈ p-adics(p)
BY
{ ((EqCDA THEN (RWW "exp_add p-mul-int< p-mul-assoc" 0 THENA Auto))
   THEN EqCDA
   THEN (RWW "p-mul-assoc<" 0 THENA Auto)
   THEN EqCDA
   THEN BackThruSomeHyp) }

---

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.  IsMonoid(padic(p);\mlambda{}u,v.  pa-mul(p;u;v);1(p))
13.  a  :  padic(p)
14.  x  :  padic(p)
15.  y  :  padic(p)
16.  X1  :  \mBbbN{}
17.  X2  :  p-adics(p)
18.  Y1  :  \mBbbN{}
19.  Y2  :  p-adics(p)
20.  Z1  :  \mBbbN{}
21.  Z2  :  p-adics(p)
22.  M  :  \mBbbZ{}
23.  imax(X1;Y1)  =  M
24.  X1  \mleq{}  M
25.  Y1  \mleq{}  M
26.  v  :  \mBbbZ{}
27.  (M  -  X1)  =  v
28.  v1  :  \mBbbZ{}
29.  (M  -  Y1)  =  v1
30.  v2  :  \mBbbZ{}
31.  (Z1  +  M)  =  v2
\mvdash{}  p\^{}v2(p)  *  Z2  *  p\^{}v(p)  *  X2  +  p\^{}v2(p)  *  Z2  *  p\^{}v1(p)  *  Y2
=  p\^{}(v2  +  v)(p)  *  Z2  *  X2  +  p\^{}(v2  +  v1)(p)  *  Z2  *  Y2


By

---

Latex:
((EqCDA  THEN  (RWW  "exp\_add  p-mul-int<  p-mul-assoc"  0  THENA  Auto))
  THEN  EqCDA
  THEN  (RWW  "p-mul-assoc<"  0  THENA  Auto)
  THEN  EqCDA
  THEN  BackThruSomeHyp)

---

Home Index