---

Step * 2 1 1 1 1 of Lemma p-mul-int-cancelation-2


1. p : {p:{2...}| prime(p)} 
2. k : ℕ
3. CoPrime(k,p)
4. p-inv(p;k(p)) ∈ p-adics(p)
5. k(p) * p-inv(p;k(p)) = 1(p) ∈ p-adics(p)
6. ℤ(p) ∈ RngSig
7. ∀[x,y,z:p-adics(p)].  (x + y + z = x + y + z ∈ p-adics(p))
8. ∀[x:p-adics(p)]. ((x + 0(p) = x ∈ p-adics(p)) ∧ (0(p) + x = x ∈ p-adics(p)))
9. ∀[x:p-adics(p)]. ((x + -(x) = 0(p) ∈ p-adics(p)) ∧ (-(x) + x = 0(p) ∈ p-adics(p)))
10. ∀[x,y,z:p-adics(p)].  (x * y * z = x * y * z ∈ p-adics(p))
11. ∀[x:p-adics(p)]. ((x * 1(p) = x ∈ p-adics(p)) ∧ (1(p) * x = x ∈ p-adics(p)))
12. ∀[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)))
13. ∀[x,y:p-adics(p)].  (x * y = y * x ∈ p-adics(p))
14. c : p-adics(p)
⊢ p-inv(p;k(p)) * k(p) * c = c ∈ p-adics(p)
BY
{ ((RWO "10" 0 THENA Auto) THEN (RW (AddrC [2;2] (HypC 13)) 0 THENA Auto)) }

1
1. p : {p:{2...}| prime(p)} 
2. k : ℕ
3. CoPrime(k,p)
4. p-inv(p;k(p)) ∈ p-adics(p)
5. k(p) * p-inv(p;k(p)) = 1(p) ∈ p-adics(p)
6. ℤ(p) ∈ RngSig
7. ∀[x,y,z:p-adics(p)].  (x + y + z = x + y + z ∈ p-adics(p))
8. ∀[x:p-adics(p)]. ((x + 0(p) = x ∈ p-adics(p)) ∧ (0(p) + x = x ∈ p-adics(p)))
9. ∀[x:p-adics(p)]. ((x + -(x) = 0(p) ∈ p-adics(p)) ∧ (-(x) + x = 0(p) ∈ p-adics(p)))
10. ∀[x,y,z:p-adics(p)].  (x * y * z = x * y * z ∈ p-adics(p))
11. ∀[x:p-adics(p)]. ((x * 1(p) = x ∈ p-adics(p)) ∧ (1(p) * x = x ∈ p-adics(p)))
12. ∀[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)))
13. ∀[x,y:p-adics(p)].  (x * y = y * x ∈ p-adics(p))
14. c : p-adics(p)
⊢ k(p) * p-inv(p;k(p)) * c = c ∈ p-adics(p)

---

Latex:

---

Latex:

1.  p  :  \{p:\{2...\}|  prime(p)\} 
2.  k  :  \mBbbN{}
3.  CoPrime(k,p)
4.  p-inv(p;k(p))  \mmember{}  p-adics(p)
5.  k(p)  *  p-inv(p;k(p))  =  1(p)
6.  \mBbbZ{}(p)  \mmember{}  RngSig
7.  \mforall{}[x,y,z:p-adics(p)].    (x  +  y  +  z  =  x  +  y  +  z)
8.  \mforall{}[x:p-adics(p)].  ((x  +  0(p)  =  x)  \mwedge{}  (0(p)  +  x  =  x))
9.  \mforall{}[x:p-adics(p)].  ((x  +  -(x)  =  0(p))  \mwedge{}  (-(x)  +  x  =  0(p)))
10.  \mforall{}[x,y,z:p-adics(p)].    (x  *  y  *  z  =  x  *  y  *  z)
11.  \mforall{}[x:p-adics(p)].  ((x  *  1(p)  =  x)  \mwedge{}  (1(p)  *  x  =  x))
12.  \mforall{}[a,x,y:p-adics(p)].    ((a  *  x  +  y  =  a  *  x  +  a  *  y)  \mwedge{}  (x  +  y  *  a  =  x  *  a  +  y  *  a))
13.  \mforall{}[x,y:p-adics(p)].    (x  *  y  =  y  *  x)
14.  c  :  p-adics(p)
\mvdash{}  p-inv(p;k(p))  *  k(p)  *  c  =  c


By

---

Latex:
((RWO  "10"  0  THENA  Auto)  THEN  (RW  (AddrC  [2;2]  (HypC  13))  0  THENA  Auto))

---

Home Index