---

Step * 2 1 of Lemma p-unit-iff


1. p : {p:{2...}| prime(p)} 
2. a : p-adics(p)
3. b : p-adics(p)
4. a * b = 1(p) ∈ p-adics(p)
⊢ ¬((a 1) = 0 ∈ ℤ)
BY
{ ((Assert (a * b 1) = (1(p) 1) ∈ ℤ BY
          Auto)
   THEN RepUR ``p-mul p-int p-reduce`` -1
   THEN (Subst' p^1 ~ p -1 THENA Auto)) }

1
1. p : {p:{2...}| prime(p)} 
2. a : p-adics(p)
3. b : p-adics(p)
4. a * b = 1(p) ∈ p-adics(p)
5. (((a 1) * (b 1)) mod p) = (1 mod p) ∈ ℤ
⊢ ¬((a 1) = 0 ∈ ℤ)

---

Latex:

---

Latex:

1.  p  :  \{p:\{2...\}|  prime(p)\} 
2.  a  :  p-adics(p)
3.  b  :  p-adics(p)
4.  a  *  b  =  1(p)
\mvdash{}  \mneg{}((a  1)  =  0)


By

---

Latex:
((Assert  (a  *  b  1)  =  (1(p)  1)  BY
                Auto)
  THEN  RepUR  ``p-mul  p-int  p-reduce``  -1
  THEN  (Subst'  p\^{}1  \msim{}  p  -1  THENA  Auto))

---

Home Index